2.5. Bijective on stalks and ind-Zariski
Lemma2.5.1
Group: Weakly étale ring maps, weak dimension, and the comparison between weakly étale and ind-étale, following Section 2 of Bhatt–Scholze and the Stacks Project. (45)
- Lemma 2.1
- Lemma 2.2
- Lemma 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.6
- Lemma 2.7
- Definition 2.1.1
- Definition 2.1.2
- Lemma 2.1.3
- Lemma 2.1.4
- Lemma 2.1.5
- Lemma 2.1.6
- Lemma 2.1.7
- Lemma 2.1.8
- Lemma 2.1.9
- Lemma 2.1.10
- Lemma 2.1.11
- Lemma 2.1.12
- Definition 2.2.1
- Lemma 2.2.2
- Corollary 2.2.3
- Lemma 2.2.4
- Lemma 2.2.5
- Lemma 2.2.6
- Lemma 2.2.7
- Lemma 2.2.8
- Lemma 2.2.9
- Lemma 2.3.1
- Theorem 2.3.2
- Lemma 2.4.1
- Lemma 2.4.2
- Lemma 2.4.3
- Lemma 2.4.4
- Lemma 2.4.5
- Lemma 2.4.6
- Lemma 2.4.7
- Lemma 2.4.8
- Lemma 2.4.9
- Lemma 2.4.10
- Lemma 2.4.11
- Theorem 2.4.12
- Theorem 2.4.13
- Proposition 2.5.2
- Theorem 2.6.1
Associated Lean declarations
-
RingHom.BijectiveOnStalks.indZariski_of_isWLocal[sorry in proof]
Let A \to B be a w-local ring map of w-local rings that identifies local
rings. Then A \to B is ind-Zariski.
(Stacks Project, Tag 097F)
Lean code for Lemma2.5.1●1 theorem, incomplete
Associated Lean declarations
-
RingHom.BijectiveOnStalks.indZariski_of_isWLocal[sorry in proof]
Associated Lean declarations
-
RingHom.BijectiveOnStalks.indZariski_of_isWLocal[sorry in proof]
-
theoremdefined in Proetale/Algebra/IndBijectiveOnStalks.leancontains sorry
theorem RingHom.BijectiveOnStalks.indZariski_of_isWLocal.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} [IsWLocalRing R] [IsWLocalRing S] (hf : f.IsWLocal) (hf' : f.BijectiveOnStalks) : f.IndZariski
theorem RingHom.BijectiveOnStalks.indZariski_of_isWLocal.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} [IsWLocalRing R] [IsWLocalRing S] (hf : f.IsWLocal) (hf' : f.BijectiveOnStalks) : f.IndZariski
A w-local ring map between w-local spaces that is bijective on stalks is ind-Zariski.
Proposition2.5.2
Group: Weakly étale ring maps, weak dimension, and the comparison between weakly étale and ind-étale, following Section 2 of Bhatt–Scholze and the Stacks Project. (45)
- Lemma 2.1
- Lemma 2.2
- Lemma 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.6
- Lemma 2.7
- Definition 2.1.1
- Definition 2.1.2
- Lemma 2.1.3
- Lemma 2.1.4
- Lemma 2.1.5
- Lemma 2.1.6
- Lemma 2.1.7
- Lemma 2.1.8
- Lemma 2.1.9
- Lemma 2.1.10
- Lemma 2.1.11
- Lemma 2.1.12
- Definition 2.2.1
- Lemma 2.2.2
- Corollary 2.2.3
- Lemma 2.2.4
- Lemma 2.2.5
- Lemma 2.2.6
- Lemma 2.2.7
- Lemma 2.2.8
- Lemma 2.2.9
- Lemma 2.3.1
- Theorem 2.3.2
- Lemma 2.4.1
- Lemma 2.4.2
- Lemma 2.4.3
- Lemma 2.4.4
- Lemma 2.4.5
- Lemma 2.4.6
- Lemma 2.4.7
- Lemma 2.4.8
- Lemma 2.4.9
- Lemma 2.4.10
- Lemma 2.4.11
- Theorem 2.4.12
- Theorem 2.4.13
- Lemma 2.5.1
- Theorem 2.6.1
Associated Lean declarations
-
Algebra.BijectiveOnStalks.exists_indZariski[sorry in proof] -
RingHom.BijectiveOnStalks.exists_indZariski[complete]
Let A \to B be a ring map that is bijective on stalks. Then there exists a
faithfully flat, ind-Zariski map B \to B' such that A \to B' is
ind-Zariski.
(Stacks Project, Tag 097G)
Lean code for Proposition2.5.2●2 theorems, 1 incomplete
Associated Lean declarations
-
Algebra.BijectiveOnStalks.exists_indZariski[sorry in proof]
-
RingHom.BijectiveOnStalks.exists_indZariski[complete]
Associated Lean declarations
-
Algebra.BijectiveOnStalks.exists_indZariski[sorry in proof] -
RingHom.BijectiveOnStalks.exists_indZariski[complete]
-
theoremdefined in Proetale/Algebra/IndBijectiveOnStalks.leancontains sorry
theorem Algebra.BijectiveOnStalks.exists_indZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.BijectiveOnStalks R S] : ∃ T x x_1 x_2, ∃ (_ : IsScalarTower R S T), Algebra.IndZariski S T ∧ Module.FaithfullyFlat S T ∧ Algebra.IndZariski R T
theorem Algebra.BijectiveOnStalks.exists_indZariski.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.BijectiveOnStalks R S] : ∃ T x x_1 x_2, ∃ (_ : IsScalarTower R S T), Algebra.IndZariski S T ∧ Module.FaithfullyFlat S T ∧ Algebra.IndZariski R T
-
theoremdefined in Proetale/Algebra/IndBijectiveOnStalks.leancomplete
theorem RingHom.BijectiveOnStalks.exists_indZariski.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.BijectiveOnStalks) : ∃ T x g, g.IndZariski ∧ g.FaithfullyFlat ∧ (g.comp f).IndZariski
theorem RingHom.BijectiveOnStalks.exists_indZariski.{u} {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.BijectiveOnStalks) : ∃ T x g, g.IndZariski ∧ g.FaithfullyFlat ∧ (g.comp f).IndZariski
If `R → S` is bijective on stalks, ind-Zariski locally it is ind-Zariski.
Proof for Proposition 2.5.2
Proof uses 3
By Lemma 1.1.32, the induced map
A_w \to B_w is again bijective on stalks and hence ind-Zariski by
Lemma 2.5.1. Since B \to B_w
is ind-Zariski and faithfully flat and the composition A \to B \to B_w is
ind-Zariski, the claim follows.