2. More on local structure
This chapter serves for the second half of the commutative algebra preparation of the remaining part of the paper. The key result is Theorem 2.6.1, expressing that every weakly étale map can be covered by ind-étale maps. The proof goes via the local input Theorem 2.4.13.
Lemma2.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.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
- Proposition 2.5.2
- Theorem 2.6.1
Associated Lean declarations
-
HenselianLocalRing.exists_pi_of_finite[sorry in proof]
Let R be a Henselian local ring and S a finite R-algebra. Then S is
a finite product of Henselian local rings, each finite over R.
(Stacks Project, Tag 04GH, (1))
Lean code for Lemma2.1●1 theorem, incomplete
Associated Lean declarations
-
HenselianLocalRing.exists_pi_of_finite[sorry in proof]
Associated Lean declarations
-
HenselianLocalRing.exists_pi_of_finite[sorry in proof]
-
theoremdefined in Proetale/Algebra/IntegralLocal.leancontains sorry
theorem HenselianLocalRing.exists_pi_of_finite.{u} (R : Type u) [CommRing R] [HenselianLocalRing R] (S : Type u) [CommRing S] [Algebra R S] [Module.Finite R S] : ∃ ι x B x, ∃ (_ : ∀ (i : ι), IsLocalRing (B i)) (_ : ∀ (i : ι), HenselianLocalRing (B i)), ∃ x_3, ∃ (_ : ∀ (i : ι), Module.Finite R (B i)), Nonempty (S ≃ₐ[R] (i : ι) → B i)
theorem HenselianLocalRing.exists_pi_of_finite.{u} (R : Type u) [CommRing R] [HenselianLocalRing R] (S : Type u) [CommRing S] [Algebra R S] [Module.Finite R S] : ∃ ι x B x, ∃ (_ : ∀ (i : ι), IsLocalRing (B i)) (_ : ∀ (i : ι), HenselianLocalRing (B i)), ∃ x_3, ∃ (_ : ∀ (i : ι), Module.Finite R (B i)), Nonempty (S ≃ₐ[R] (i : ι) → B i)
A finite algebra over a Henselian local ring is, as a ring, a finite product of Henselian local rings, each finite over the base. [Stacks 04GH (1)](https://stacks.math.columbia.edu/tag/04GH). This is destined to go directly to Mathlib, so it should not be worked on here.
Lemma2.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.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
- Proposition 2.5.2
- Theorem 2.6.1
Associated Lean declarations
A filtered colimit of local rings along local homomorphisms is local.
Lean code for Lemma2.2●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/FilteredLocalColimit.leancomplete
theorem CommRingCat.FilteredColimits.isLocalRing_of_isColimit.{u} {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) {c : CategoryTheory.Limits.Cocone F} [h_obj : ∀ (j : J), IsLocalRing ↑(F.obj j)] [h_hom : ∀ (j j' : J) (f : j ⟶ j'), IsLocalHom (CommRingCat.Hom.hom (F.map f))] (hc : CategoryTheory.Limits.IsColimit c) : IsLocalRing ↑c.pt
theorem CommRingCat.FilteredColimits.isLocalRing_of_isColimit.{u} {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J CommRingCat) {c : CategoryTheory.Limits.Cocone F} [h_obj : ∀ (j : J), IsLocalRing ↑(F.obj j)] [h_hom : ∀ (j j' : J) (f : j ⟶ j'), IsLocalHom (CommRingCat.Hom.hom (F.map f))] (hc : CategoryTheory.Limits.IsColimit c) : IsLocalRing ↑c.pt
Proof for Lemma 2.2
uses 0
Let R = \colim_i R_i with R_i local rings and R_i \to R_j a local ring
map. Suppose x, y \in R_i are non-units. Since R_i is local, their sum is
not a unit. If the image of x + y in \colim_i R_i is a unit, there exists
a j such that the image of x + y is a unit in R_j. But this does not
happen because R_i \to R_j is a local ring map.
Lemma2.3
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.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
- Proposition 2.5.2
- Theorem 2.6.1
Lean status
- No associated Lean code or declarations.
A filtered colimit of (strictly) Henselian local rings along local homomorphisms is (strictly) Henselian. (Stacks Project, Tag 04GI)
Lemma2.4
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.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
- Proposition 2.5.2
- Theorem 2.6.1
Associated Lean declarations
-
IsLocalRing.of_henselianLocalRing_of_isIntegral_of_isDomain[sorry in proof]
Let R be a Henselian local ring and S be an integral R-algebra and an
integral domain. Then S is a local ring.
Lean code for Lemma2.4●1 theorem, incomplete
Associated Lean declarations
-
IsLocalRing.of_henselianLocalRing_of_isIntegral_of_isDomain[sorry in proof]
Associated Lean declarations
-
IsLocalRing.of_henselianLocalRing_of_isIntegral_of_isDomain[sorry in proof]
-
theoremdefined in Proetale/Algebra/IntegralLocal.leancontains sorry
theorem IsLocalRing.of_henselianLocalRing_of_isIntegral_of_isDomain.{u} {R S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing R] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] : IsLocalRing S
theorem IsLocalRing.of_henselianLocalRing_of_isIntegral_of_isDomain.{u} {R S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing R] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] : IsLocalRing S
An integral algebra over a Henselian local ring that is an integral domain is local.
Lemma2.5
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.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
- Proposition 2.5.2
- Theorem 2.6.1
Associated Lean declarations
Let R \to S be an integral ring map of local rings. Then R \to S is a
local ring homomorphism.
Lean code for Lemma2.5●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/RingTheory/Ideal/GoingUp.leancomplete
theorem RingHom.IsIntegral.isLocalHom_of_isLocalRing.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] {f : R →+* S} (hf : f.IsIntegral) : IsLocalHom f
theorem RingHom.IsIntegral.isLocalHom_of_isLocalRing.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] {f : R →+* S} (hf : f.IsIntegral) : IsLocalHom f
An integral ring homomorphism between local rings is a local ring homomorphism. Note that, unlike `RingHom.IsIntegral.isLocalHom`, this does not require injectivity of `f`.
Proof for Lemma 2.5
uses 0
This follows from going-up.
Lemma2.6
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.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
- Proposition 2.5.2
- Theorem 2.6.1
Associated Lean declarations
Let R \to S be a local ring homomorphism of local rings. If R \to S is
integral, the extension of residue fields \kappa(S) / \kappa(R) is
algebraic.
Lean code for Lemma2.6●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/IntegralLocal.leancomplete
theorem Algebra.IsAlgebraic.residueField_of_isIntegral.{u} {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [Algebra.IsIntegral R S] : Algebra.IsAlgebraic (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
theorem Algebra.IsAlgebraic.residueField_of_isIntegral.{u} {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [Algebra.IsIntegral R S] : Algebra.IsAlgebraic (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
The residue field extension induced by a local integral homomorphism of local rings is algebraic.
Proof for Lemma 2.6
uses 0
It suffices to show that \kappa(S) is integral over R. Since S is
integral over R and \kappa(S) is integral over S (the map
S \to \kappa(S) is surjective), the composition R \to S \to \kappa(S) is
integral.
Lemma2.7
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
- 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
- Proposition 2.5.2
- Theorem 2.6.1
Associated Lean declarations
Let R \to S and R \to T be local ring maps of local rings. Suppose
R \to S is integral and \kappa(S) / \kappa(R) or
\kappa(T) / \kappa(R) is purely inseparable, then T \otimes_{R} S is a
local ring.
(Stacks Project, Tag 092Y)
Lean code for Lemma2.7●1 theorem, incomplete
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Algebra/IntegralLocal.leancontains sorry
theorem Algebra.isLocalRing_tensorProduct_of_isPurelyInseparable_residueField.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] (T : Type u) [CommRing T] [Algebra R T] [IsLocalRing T] [IsLocalHom (algebraMap R T)] [Algebra.IsIntegral R S] (h : IsPurelyInseparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) ∨ IsPurelyInseparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField T)) : IsLocalRing (TensorProduct R S T)
theorem Algebra.isLocalRing_tensorProduct_of_isPurelyInseparable_residueField.{u} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] (T : Type u) [CommRing T] [Algebra R T] [IsLocalRing T] [IsLocalHom (algebraMap R T)] [Algebra.IsIntegral R S] (h : IsPurelyInseparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) ∨ IsPurelyInseparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField T)) : IsLocalRing (TensorProduct R S T)
Let `R → S` and `R → T` be local ring homomorphisms of local rings, with `R → S` integral. If `κ(S)/κ(R)` or `κ(T)/κ(R)` is purely inseparable, the tensor product `S ⊗[R] T` is a local ring. [Stacks 092Y](https://stacks.math.columbia.edu/tag/092Y).
Proof for Lemma 2.7
uses 0
Integral is stable under base change, so T \to S' = T \otimes_{R} S is
integral. Hence by going-up any maximal ideal of S' lies over
\mathfrak{m}_T. We have
S' / \mathfrak{m}_T S' = \kappa(T) \otimes_{R} S = \kappa(T) \otimes_{\kappa(R)} S / \mathfrak{m}_R S.
Again by going-up and since S is local, \spec{S / \mathfrak{m}_R S} is a
single point. Thus
\spec{S' / \mathfrak{m}_T S'} \cong \spec{\kappa(T) \otimes_{\kappa(R)} \kappa(S)}.
The latter is a single point, because purely inseparable extensions induce
universal homeomorphisms.