10.154 Filtered colimits of… to 10.168 Colimits and maps of…

Section10.154 Filtered colimits of étale ring maps#

Section 10.154 of the Stacks Project, Tag 0BSG. 7 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BSH, a lemma

Tag 0BSH in the Stacks Project.

filteredColimitEtale_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimit/Basic.lean, line 635.

Stacks 0BSH. Let A and R' be commutative R-algebras, equivalently ring maps R → A and R → R'. If A is a filtered colimit of étale R-algebras, then R' ⊗[R] A, regarded as an R'-algebra via the canonical map R' → R' ⊗[R] A, is a filtered colimit of étale R'-algebras. Here TensorProduct R R' A is R' ⊗[R] A with its canonical R'-algebra structure.

theorem filteredColimitEtale_baseChange
    {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
    {R' : Type u} [CommRing R'] [Algebra R R']
    (hA : IsFilteredColimitOfEtale R A) :
    IsFilteredColimitOfEtale R' (TensorProduct R R' A)

CommAlgCat.ind_etale_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimit/Basic.lean, line 1323. The attribute's comment: “"Λ is a filtered colimit of étale R-algebras" is (CommAlgCat.etale R).ind.{u} (CommAlgCat.of R Λ), as in Lemma 04GN, and the source's S ⊗_R R' is an abstract Algebra.IsPushout R S R' S' rather than a model of the tensor product. Tagged jointly with filteredColimitEtale_baseChange, which is this lemma for the predicate IsFilteredColimitOfEtale and the model TensorProduct R R' A. See the module docstring.”.

An ind-étale algebra stays ind-étale after cobase change. Let R → S and R → R' be ring maps and let S' be a pushout of S and R' over R, that is, S' = S ⊗[R] R'. If R' is a filtered colimit of étale R-algebras, then S' is a filtered colimit of étale S-algebras.

theorem ind_etale_of_isPushout (R S R' S' : Type u) [CommRing R] [CommRing S]
    [CommRing R'] [CommRing S'] [Algebra R S] [Algebra R R'] [Algebra R S'] [Algebra S S']
    [Algebra R' S'] [IsScalarTower R S S'] [IsScalarTower R R' S']
    [Algebra.IsPushout R S R' S']
    (h : (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R R')) :
    (CommAlgCat.etale.{u} S).ind.{u} (CommAlgCat.of S S')

Tag 0BSJ, a lemma

Tag 0BSJ in the Stacks Project.

isFilteredColimitOfEtaleUnder_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimit/Basic.lean, line 407.

Stacks 0BSJ. Let R be a commutative ring, let J be a small filtered category and let G : J ⥤ Under (CommRingCat.of R) be a diagram of R-algebras with colimit cocone cA and apex isomorphic to A. If every G.obj j is a filtered colimit of étale R-algebras, then so is A.

theorem isFilteredColimitOfEtaleUnder_of_isColimit (R : Type) [CommRing R]
    (A : Under (CommRingCat.of R))
    (J : Type) [SmallCategory J] [IsFiltered J]
    (G : J ⥤ Under (CommRingCat.of R))
    (cA : Limits.Cocone G) (hcA : Limits.IsColimit cA) (hA : cA.pt ≅ A)
    (hEach : ∀ j, IsFilteredColimitOfEtaleUnder R (G.obj j)) :
    IsFilteredColimitOfEtaleUnder R A

Tag 0GIM, a lemma

Tag 0GIM in the Stacks Project.

isFilteredColimitOfEtale_colim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimit/Colimit.lean, line 980.

Stacks Tag 0GIM, Lemma 10.154.4.

Let I be a directed set (a nonempty directed preorder). Let 𝓡, 𝓐 : I ⥤ CommRingCat be two functors (the systems i ↦ R_i and i ↦ A_i) and α : 𝓡 ⟶ 𝓐 a natural transformation (the structure maps R_i → A_i, whose naturality squares are the required commutative squares with the transition maps).

Take colimits R = colimit 𝓡 and A = colimit 𝓐; the induced structure map R → A is colimMap α. If each A_i = 𝓐.obj i is a filtered colimit of étale R_i-algebras (via the structure map (α.app i).hom), then A is a filtered colimit of étale R-algebras (via the induced structure map (colimMap α).hom).

theorem isFilteredColimitOfEtale_colim
    (I : Type u) [Preorder I] [IsDirected I (· ≤ ·)] [Nonempty I]
    (𝓡 𝓐 : I ⥤ CommRingCat.{u}) (α : 𝓡 ⟶ 𝓐)
    (hetale : ∀ i, IsFilteredColimitOfEtaleHom (α.app i).hom) :
    IsFilteredColimitOfEtaleHom (colimMap α).hom

Tag 08HS, a lemma

Tag 08HS in the Stacks Project.

CommRingCat.ind_etale_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimit/Basic.lean, line 754. The attribute's comment: “"Λ is a filtered colimit of étale R-algebras" is ObjectProperty.ind.{u} (fun C : Under R ↦ C.hom.hom.Etale) Λ, as in Lemma 07C3; the source's R-algebra map A → B is a map g together with the composite f ≫ g as the R-algebra structure of B, so the triangle commutes by construction. See the module docstring.”.

A filtered colimit of étale algebras over a filtered colimit of étale algebras. Let R → A → B be ring maps. If A and B are filtered colimits of étale R-algebras, then B is a filtered colimit of étale A-algebras.

theorem ind_etale_of_comp {R A B : CommRingCat.{u}} (f : R ⟶ A) (g : A ⟶ B)
    (hf : ObjectProperty.ind.{u} (fun C : Under R ↦ C.hom.hom.Etale) (Under.mk f))
    (hfg : ObjectProperty.ind.{u} (fun C : Under R ↦ C.hom.hom.Etale) (Under.mk (f ≫ g))) :
    ObjectProperty.ind.{u} (fun C : Under A ↦ C.hom.hom.Etale) (Under.mk g)

CommAlgCat.ind_etale_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimit/Basic.lean, line 1348. The attribute's comment: “"Λ is a filtered colimit of étale R-algebras" is (CommAlgCat.etale R).ind.{u} (CommAlgCat.of R Λ), as in Lemma 04GN, and the source's A → B → C is an IsScalarTower A B C. Tagged jointly with CommRingCat.ind_etale_of_comp, which is this lemma for ring maps and the ObjectProperty.ind spelling on Under R. See the module docstring.”.

A filtered colimit of étale algebras over a filtered colimit of étale algebras. Let A → B → C be ring maps. If B and C are filtered colimits of étale A-algebras, then C is a filtered colimit of étale B-algebras.

theorem ind_etale_of_comp {A B C : Type u} [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
    (hB : (CommAlgCat.etale.{u} A).ind.{u} (CommAlgCat.of A B))
    (hC : (CommAlgCat.etale.{u} A).ind.{u} (CommAlgCat.of A C)) :
    (CommAlgCat.etale.{u} B).ind.{u} (CommAlgCat.of B C)

Tag 08HR, a lemma

Tag 08HR in the Stacks Project.

Stacks.Henselian.EtaleLifting.algHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/EtaleLifting/IndEtale.lean, line 665. The attribute's comment: “the map itself; algHom_spec is its two defining properties and algHom_unique its uniqueness”.

The lift of a residue datum along an ind-étale algebra into a henselian local ring (Stacks Tag 08HR, Lemma 10.154.6). Let R → S be a ring map with S henselian local, let A be ind-étale over R, let q be a prime of A lying over p = R ∩ 𝔪 S, and let τ : κ(q) → κ(S) be a κ(p)-algebra map. This is the R-algebra map A → S with q = f⁻¹(𝔪 S) inducing τ on residue fields; algHom_spec is those two properties and algHom_unique says it is the only such map.

noncomputable def algHom
    {R : Type u} {A : Type v} {S : Type w}
    [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S]
    [HenselianLocalRing S]
    (hA : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} A)))
    (p : Ideal R) [p.IsPrime]
    (hp : p = (maximalIdeal S).comap (algebraMap R S))
    (q : Ideal A) [q.IsPrime]
    (hpq : p = q.comap (algebraMap R A))
    (τ : q.ResidueField →+* ResidueField S)
    (hτ : τ.comp (residueFieldMapFib p q hpq) = residueFieldMapBase p hp) :
    A →ₐ[R] S

Stacks.Henselian.EtaleLifting.algHom_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/EtaleLifting/IndEtale.lean, line 682. The attribute's comment: “the two defining properties of algHom”.

algHom pulls the maximal ideal of S back to q and induces τ on residue fields.

theorem algHom_spec
    {R : Type u} {A : Type v} {S : Type w}
    [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S]
    [HenselianLocalRing S]
    (hA : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} A)))
    (p : Ideal R) [p.IsPrime]
    (hp : p = (maximalIdeal S).comap (algebraMap R S))
    (q : Ideal A) [q.IsPrime]
    (hpq : p = q.comap (algebraMap R A))
    (τ : q.ResidueField →+* ResidueField S)
    (hτ : τ.comp (residueFieldMapFib p q hpq) = residueFieldMapBase p hp) :
    q = (maximalIdeal S).comap (algHom hA p hp q hpq τ hτ : A →+* S) ∧
      InducesResidueMap q (algHom hA p hp q hpq τ hτ : A →+* S) τ

Stacks.Henselian.EtaleLifting.algHom_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/EtaleLifting/IndEtale.lean, line 733. The attribute's comment: “uniqueness of algHom”.

algHom is the only R-algebra map A → S pulling 𝔪 S back to q and inducing τ on residue fields.

theorem algHom_unique
    {R : Type u} {A : Type v} {S : Type w}
    [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S]
    [HenselianLocalRing S]
    (hA : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} A)))
    (p : Ideal R) [p.IsPrime]
    (hp : p = (maximalIdeal S).comap (algebraMap R S))
    (q : Ideal A) [q.IsPrime]
    (hpq : p = q.comap (algebraMap R A))
    (τ : q.ResidueField →+* ResidueField S)
    (hτ : τ.comp (residueFieldMapFib p q hpq) = residueFieldMapBase p hp)
    (f : A →ₐ[R] S)
    (hf : q = (maximalIdeal S).comap (f : A →+* S) ∧
      InducesResidueMap q (f : A →+* S) τ) :
    f = algHom hA p hp q hpq τ hτ

Tag 08HT, a lemma

Tag 08HT in the Stacks Project.

HenselianLocalRing.existsUnique_algEquiv_of_ind_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimit/Basic.lean, line 1087. The attribute's comment: “"S is a filtered colimit of étale R-algebras" is (CommAlgCat.etale R).ind (CommAlgCat.of R S), as in Lemma 04GN; the source's commutative square is the two R-algebra maps to K; and "the arrows identify K with the residue field" is their surjectivity, K being a field. Uniqueness is stated among all R-algebra maps S → S', which is stronger than the source's uniqueness among isomorphisms. See the module docstring.”.

Uniqueness of the henselization (Stacks 08HT). Let R be a ring, let S and S' be henselian local R-algebras that are filtered colimits of étale R-algebras, and let p : S →ₐ[R] K and p' : S' →ₐ[R] K be surjections onto a field K, so that K is the residue field of both. Then there is an R-algebra isomorphism e : S ≃ₐ[R] S' such that an R-algebra map f : S → S' satisfies p' ∘ f = p if and only if f = e; in particular e is the unique R-algebra isomorphism S → S' compatible with the maps to K.

theorem HenselianLocalRing.existsUnique_algEquiv_of_ind_etale
    {R : Type u} [CommRing R] {S S' : Type u} [CommRing S] [CommRing S'] [Algebra R S]
    [Algebra R S'] [HenselianLocalRing S] [HenselianLocalRing S']
    (hS : (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R S))
    (hS' : (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R S'))
    {K : Type v} [Field K] [Algebra R K] (p : S →ₐ[R] K) (p' : S' →ₐ[R] K)
    (hp : Function.Surjective p) (hp' : Function.Surjective p') :
    ∃ e : S ≃ₐ[R] S', ∀ f : S →ₐ[R] S', p'.comp f = p ↔ f = (e : S →ₐ[R] S')

Tag 04GI, a lemma

Tag 04GI in the Stacks Project.

part2_henselian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Colimit.lean, line 442. The attribute's comment: “henselian”. References: EGA IV (18.6.14).

Part 2 (Henselian case). If each R_i is henselian, then the colimit R is henselian.

Argument (Stacks 04GI, the essential new content). We verify the HenselianLocalRing.is_henselian clause for R (locality is part1_isLocalRing). Let g : R[X] be monic, a₀ : R with g.eval a₀ ∈ m_R and IsUnit (g.derivative.eval a₀); we must find a : R with g.IsRoot a and a - a₀ ∈ m_R.

1. Descend the data to a finite stage. Since R[X] is the filtered colimit of the G i[X], Ring.DirectLimit.Polynomial.exists_of gives an index and a polynomial mapping to g; arranging it to be monic of the same degree (possible after enlarging the index: the leading coefficient of any preimage maps to 1 = leadingCoeff g, so colimit_isUnit_descend/of.zero_exact makes it 1 at a later stage, or one truncates to the correct degree and sets the top coefficient to 1). Also descend a₀ = φ_k b₀ (Ring.DirectLimit.exists_of). Push polynomial and point to a common index k, obtaining a monic p : G k[X] with p.map (φ_k) = g and b₀ : G k with φ_k b₀ = a₀.

2. The hypotheses descend. Evaluation commutes with map: φ_k (p.eval b₀) = g.eval a₀ and φ\_k (p.derivative.eval b₀) = g.derivative.eval a₀ (Polynomial.eval\_map, Polynomial.derivative\_map).

3. g.derivative.eval a₀ is a unit, so φ_k (p.derivative.eval b₀) is a unit; by colimit_isUnit_descend it becomes a unit p'.eval ... at some l ≥ k; push p, b₀ forward to l (so WLOG k = l) to get IsUnit (p.derivative.eval b₀) in G k.

4. g.eval a₀ ∈ m_R means φ_k (p.eval b₀) is a nonunit of R; if p.eval b₀ were a unit of G k, its image φ_k (p.eval b₀) would be a unit of R — contradiction. So p.eval b₀ ∈ m_k.

5. Apply henselianness of G k. hhens k gives c : G k with p.IsRoot c (p.eval c = 0) and c - b₀ ∈ m_k.

6. Push the root forward. Set a := φ_k c. Then g.eval a = (p.map φ_k).eval (φ_k c) = φ_k (p.eval c) = φ_k 0 = 0 (Polynomial.eval_map + eval₂ is a ring hom), so g.IsRoot a. And a - a₀ = φ_k c - φ_k b₀ = φ_k (c - b₀), which lies in m_R because c - b₀ ∈ m_k and φ_k is local (part1_mem_maximalIdeal ⟸, or IsLocalRing.map_nonunit).

theorem part2_henselian (hhens : ∀ i, HenselianLocalRing (G i)) :
    HenselianLocalRing (colimitRing G f)

part3_strictlyHenselian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Colimit.lean, line 542. The attribute's comment: “strictly henselian”. References: EGA IV (18.8.18), “i)”.

Part 3 (Strictly henselian case). If each R_i is strictly henselian (henselian with separably closed residue field), then the colimit R is strictly henselian: it is henselian and its residue field is separably closed.

Argument. The henselian conjunct is exactly part2_henselian G f hlocal hhens. For separable-closedness of κ_R: by part1_residueField_colimit, κ_R ≃+* colim_i κ_i, and IsSepClosed transports across a ring isomorphism (IsSepClosed is preserved by RingEquiv, e.g. via RingEquiv.isSepClosed / pulling separable polynomials back and forth). So it suffices that K := colim_i κ_i is separably closed. Use IsSepClosed.of_exists_root: let q : K[X] be monic, irreducible and separable; we find a root. Ring.DirectLimit.Polynomial.exists_of descends q to q_i : κ_i[X] with q_i.map (of i) = q at some stage i; q separable forces (after enlarging i) q_i separable and of positive degree. Since κ_i is separably closed (hsep i), IsSepClosed.exists_root gives a root r ∈ κ_i of q_i; its image of i r ∈ K is a root of q (Polynomial.eval_map/eval₂ hom + of_f). Hence K is separably closed, and so is κ_R.

theorem part3_strictlyHenselian
    (hhens : ∀ i, HenselianLocalRing (G i))
    (hsep : ∀ i, IsSepClosed (ResidueField (G i))) :
    letI := part1_isLocalRing G f hlocal
    HenselianLocalRing (colimitRing G f) ∧
      IsSepClosed (ResidueField (colimitRing G f))

Sources

• Section 10.154, Tag 0BSG
• AxiomMath/Stacks at 5ed82d14

LeanfilteredColimitEtale_baseChange · CommAlgCat.ind_etale_of_isPushout · isFilteredColimitOfEtaleUnder_of_isColimit · isFilteredColimitOfEtale_colim · CommRingCat.ind_etale_of_comp · CommAlgCat.ind_etale_of_comp · Stacks.Henselian.EtaleLifting.algHom · Stacks.Henselian.EtaleLifting.algHom_spec

Section10.155 Henselization and strict henselization#

Section 10.155 of the Stacks Project, Tag 0BSK. 13 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04GN, a lemma

Tag 04GN in the Stacks Project.

IsLocalRing.exists_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/Existence.lean, line 709. The attribute's comment: “The lemma's preamble, a local ring map R → Rh, is the Algebra R Rh, IsLocalRing Rh and IsLocalHom (algebraMap R Rh) binders; the four conjuncts are its items (1)–(4). Rh being a filtered colimit of étale R-algebras is (CommAlgCat.etale R).ind, i.e. Rh is ind-étale over R; 𝔪 Rh is Ideal.map; and κ = Rh/𝔪 Rh is bijectivity of the canonical IsLocalRing.ResidueField.map. See the module docstring.”. References: EGA IV (18.6.6), “(i), part of (iii)”; SGA 4 VIII (4.1), “henselization”; SGA 4 VIII (4.1), “henselization”.

Existence of the henselization of a local ring (Stacks 04GN). For a local ring (R, 𝔪, κ) there is a local ring map R → Rh such that (1) Rh is henselian, (2) Rh is a filtered colimit of étale R-algebras, (3) 𝔪 Rh is the maximal ideal of Rh, and (4) the residue field of Rh is κ.

public theorem IsLocalRing.exists_henselization (R : Type u) [CommRing R] [IsLocalRing R] :
    ∃ (Rh : Type u) (_ : CommRing Rh) (_ : Algebra R Rh) (_ : IsLocalRing Rh)
      (_ : IsLocalHom (algebraMap R Rh)),
      HenselianLocalRing Rh ∧
      (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R Rh) ∧
      (maximalIdeal R).map (algebraMap R Rh) = maximalIdeal Rh ∧
      Function.Bijective (ResidueField.map (algebraMap R Rh))

Tag 04GP, a lemma

Tag 04GP in the Stacks Project.

IsLocalRing.exists_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/Existence.lean, line 898. The attribute's comment: “The diagram's middle column is a hypothesis: Rh is any local ind-étale R-algebra with residue field κ, which by Lemmas 04GN and 04GS is the henselization; the conclusion produces Rsh with the algebra structure over Rh and item (1). Strictly henselian is HenselianLocalRing plus IsSepClosed on the residue field, Rsh a filtered colimit of étale R-algebras is (CommAlgCat.etale R).ind, 𝔪 Rsh is Ideal.map, and κ^sep = Rsh/𝔪 Rsh is an isomorphism κ^sep ≃+* ResidueField Rsh compatible with the maps out of R. See the module docstring.”. References: EGA IV (18.8.8), “(i), part of (iii)”.

Existence of the strict henselization of a local ring. Let (R, 𝔪, κ) be a local ring, let κ ⊆ κ^sep be a separable algebraic closure, and let Rh be a local R-algebra with R → Rh local which is a filtered colimit of étale R-algebras with residue field κ (the henselization of R). Then there is a commutative diagram R → Rh → Rsh over κ → κ → κ^sep such that (1) Rh → Rsh is a local ring map, (2) Rsh is strictly henselian, (3) Rsh is a filtered colimit of étale R-algebras, (4) 𝔪 Rsh is the maximal ideal of Rsh, and (5) the residue field of Rsh is κ^sep.

public theorem IsLocalRing.exists_strictHenselization (R : Type u) [CommRing R] [IsLocalRing R]
    (Rh : Type u) [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh] [IsLocalHom (algebraMap R Rh)]
    (hRh : (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R Rh))
    (hRhres : Function.Surjective (ResidueField.map (algebraMap R Rh)))
    (κsep : Type u) [Field κsep] [Algebra (ResidueField R) κsep]
    [IsSepClosure (ResidueField R) κsep] :
    ∃ (Rsh : Type u) (_ : CommRing Rsh) (_ : IsLocalRing Rsh) (_ : Algebra R Rsh)
      (_ : Algebra Rh Rsh) (_ : IsScalarTower R Rh Rsh) (_ : IsLocalHom (algebraMap Rh Rsh)),
      HenselianLocalRing Rsh ∧
      IsSepClosed (ResidueField Rsh) ∧
      (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R Rsh) ∧
      (maximalIdeal R).map (algebraMap R Rsh) = maximalIdeal Rsh ∧
      ∃ e : κsep ≃+* ResidueField Rsh, ∀ x : R,
        e (algebraMap (ResidueField R) κsep (residue R x)) = residue Rsh (algebraMap R Rsh x)

Stacks.StrictHenselization.exists_isStrictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/ExistenceData.lean, line 164. The attribute's comment: “The five properties of the source's conclusion are bundled into the predicate Stacks.StrictHenselization.IsStrictHenselization, and the henselization R^h, which the sibling statement in StrictHenselization.Existence carries as a hypothesis, is produced here by IsLocalRing.exists_henselization rather than assumed; so this is the source's existential form. The separable algebraic closure is taken over (maximalIdeal R).ResidueField, the spelling IsStrictHenselization uses, and may lie in a universe independent of R.”. References: EGA IV (18.8.7); EGA IV (18.8.8); SGA 4 VIII (4.4).

Existence of the strict henselization (Stacks 04GP). A local ring (R, 𝔪, κ) together with a separable algebraic closure κ ⊆ κ^sep of its residue field admits a local R-algebra R^{sh} which is a strict henselization of R with respect to κ ⊆ κ^sep, that is: it is strictly henselian, R → R^{sh} is a local ring map realizing R^{sh} as a filtered colimit of étale R-algebras, 𝔪 R^{sh} is the maximal ideal of R^{sh}, and the residue field of R^{sh} is identified with κ^sep compatibly with κ ⊆ κ^sep.

public theorem exists_isStrictHenselization (R : Type u) [CommRing R] [IsLocalRing R]
    (κ : Type v) [Field κ] [Algebra (maximalIdeal R).ResidueField κ]
    [IsSepClosure (maximalIdeal R).ResidueField κ] :
    ∃ (Rsh : Type u) (_ : CommRing Rsh) (_ : IsLocalRing Rsh) (_ : Algebra R Rsh),
      Nonempty (IsStrictHenselization R κ Rsh)

Tag 04GQ, a definition

Tag 04GQ in the Stacks Project.

IsLocalRing.IsHenselization, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/Defs.lean, line 169. The attribute's comment: “One predicate for the source's three items: part (1) is IsHenselization R (ResidueField R) Rh, part (2) is IsHenselization R κsep Rsh for κ ⊆ κ^sep a separable algebraic closure, and part (3) is the isomorphism invariance of the three fields, which by Lemma 08HT makes them equivalent to being isomorphic to a ring Lemma 04GP constructs. Rh being a filtered colimit of étale R-algebras is (CommAlgCat.etale R).ind, as in Lemmas 04GN and 04GP, and the residue field condition is item (5) of Lemma 04GP. Locality of R → Rh and 𝔪 Rh = 𝔪_{Rh} are consequences, not fields. See the module docstring.”. References: EGA IV (18.8.7).

Henselization of a local ring (Stacks 04GQ). Let (R, 𝔪, κ) be a local ring and let κ ⊆ L be an extension of its residue field. A local R-algebra Rh is a henselization of R with residue field L if Rh is henselian, is a filtered colimit of étale R-algebras, and has residue field L compatibly with κ ⊆ L. For L = κ this is the henselization R → R^h of Lemma 04GN, and for L = κ^sep a separable algebraic closure of κ it is a strict henselization R → R^{sh} of R with respect to κ ⊆ κ^sep, in the sense of Lemma 04GP; by Lemma 08HT such an Rh is unique up to a unique R-algebra isomorphism over L.

public class IsLocalRing.IsHenselization (R : Type u) [CommRing R] [IsLocalRing R]
    (L : Type v) [Field L] [Algebra (ResidueField R) L]
    (Rh : Type w) [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh] : Prop

Tag 0BSL, a remark

Tag 0BSL in the Stacks Project.

IsLocalRing.IsHenselization.exists_strictHenselization_iUnion_finiteEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/OfHenselization.lean, line 604. The attribute's comment: “The rings R^h(κ') are local Rh-algebras A κ' with injective embeddings ι into Rsh exhausting it, which is the union of the source. The transition maps are pinned as the unique maps compatible with the inclusions of residue fields, and each A κ' is unique up to a unique isomorphism inducing the identity of κ'. That Rsh is the strict henselization is IsHenselization over Rh and over R with residue field κsep.”.

The strict henselization as a union of finite étale extensions of the henselization (Stacks 0BSL). Let R → Rh be a henselization of the local ring R and let κsep be a separable algebraic closure of the residue field κ of R, identified with that of Rh by e. For every finite subextension κ ⊆ κ' ⊆ κsep there is a finite étale local extension Rh ⊆ Rh(κ') with residue field extension κ ⊆ κ', unique up to unique isomorphism; for κ' ⊆ κ'' there is exactly one map Rh(κ') → Rh(κ'') compatible with κ' ⊆ κ''; and the union Rsh of the resulting directed system is strictly henselian, and is a strict henselization of Rh and of R.

theorem IsLocalRing.IsHenselization.exists_strictHenselization_iUnion_finiteEtale
    (R : Type u) [CommRing R] [IsLocalRing R] (Rh : Type u) [CommRing Rh] [IsLocalRing Rh]
    [Algebra R Rh] [IsHenselization R (ResidueField R) Rh] (κsep : Type u) [Field κsep]
    [Algebra (ResidueField R) κsep] [IsSepClosure (ResidueField R) κsep] :
    ∃ e : ResidueField R ≃+* ResidueField Rh,
      (∀ x : R, e (residue R x) = residue Rh (algebraMap R Rh x)) ∧
      letI : Algebra (ResidueField Rh) κsep :=
        ((algebraMap (ResidueField R) κsep).comp e.symm.toRingHom).toAlgebra
      IsSepClosure (ResidueField Rh) κsep ∧
      ∃ (Rsh : Type u) (_ : CommRing Rsh) (_ : IsLocalRing Rsh) (_ : Algebra R Rsh)
        (_ : Algebra Rh Rsh) (_ : IsScalarTower R Rh Rsh)
        (A : ∀ L, FiniteEtaleLocalResidueLift.{u, u, u} R Rh κsep e L)
        (map : ∀ {L L'}, L ≤ L' → A L →ₐ[Rh] A L') (ι : ∀ L, A L →ₐ[Rh] Rsh),
        (∀ L L' (h : L ≤ L') (f : A L →ₐ[Rh] A L'), f = map h ↔
          ∀ a, residue _ (f a) = residueMap (A L) (A L') (IntermediateField.inclusion h)
            (residue _ a)) ∧
        (∀ L, map (le_refl L) = AlgHom.id Rh (A L)) ∧
        (∀ L₁ L₂ L₃ (h₁₂ : L₁ ≤ L₂) (h₂₃ : L₂ ≤ L₃),
          (map h₂₃).comp (map h₁₂) = map (h₁₂.trans h₂₃)) ∧
        (∀ L (B : FiniteEtaleLocalResidueLift.{u, u, t} R Rh κsep e L),
          ∃! f : A L ≃ₐ[Rh] B,
            ∀ a, residue B (f a) = residueMap (A L) B (RingHom.id L) (residue _ a)) ∧
        (∀ L L' (h : L ≤ L') a, ι L' (map h a) = ι L a) ∧
        (∀ L, Function.Injective (ι L)) ∧ (∀ x, ∃ L a, ι L a = x) ∧
        HenselianLocalRing Rsh ∧ IsSepClosed (ResidueField Rsh) ∧
        IsHenselization Rh κsep Rsh ∧ IsHenselization R κsep Rsh

Tag 04GR, a lemma

Tag 04GR in the Stacks Project.

existsUnique_ringHom_to_henselian_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/HenselizationUniversalProperty.lean, line 543. References: EGA IV (18.5.11), “special case”; EGA IV (18.5.12), “special case”; EGA IV (18.5.17), “affine étale morphisms”; EGA IV (18.6.2); EGA IV (18.8.1), “(a)⇒(c), special case”; EGA IV (18.8.4), “special case”; SGA 1 I (6.2), “special case”; SGA 3 XI (1.11), “special case”; SGA 4 VIII (4.1), “(iii)”.

Stacks Tag 04GR. Let R, S, Sh be local rings, R → S (rs) a local ring homomorphism, and S → Sh (ssh) a local ring homomorphism into a henselian local ring Sh. Let R → A be étale and let q ⊆ A be a prime lying over the maximal ideal of R whose induced residue-field map R/𝔪_R → κ(q) is bijective. Then there is a unique ring homomorphism f : A → Sh that is R-linear (f ∘ algebraMap R A = ssh ∘ rs) and satisfies (maximalIdeal Sh).comap f = q.

theorem existsUnique_ringHom_to_henselian_of_etale
    (R S Sh A : Type*)
    [CommRing R] [CommRing S] [CommRing Sh] [CommRing A]
    [IsLocalRing R] [IsLocalRing S]
    [Algebra R A] [Algebra.Etale R A]
    (rs : R →+* S) [IsLocalHom rs]
    (ssh : S →+* Sh) [IsLocalHom ssh] [HenselianLocalRing Sh]
    (q : Ideal A) [q.IsPrime] [q.LiesOver (maximalIdeal R)]
    (hres : Function.Bijective
      (Ideal.ResidueField.map (maximalIdeal R) q (algebraMap R A)
        Ideal.LiesOver.over)) :
    ∃! f : A →+* Sh,
      f.comp (algebraMap R A) = ssh.comp rs ∧ (maximalIdeal Sh).comap f = q

Tag 04GS, a lemma

Tag 04GS in the Stacks Project.

HenselianLocalRing.indEtaleAlgHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/HenselizationUniversalProperty.lean, line 376. The attribute's comment: “The map of the universal property of R^h: the target is an arbitrary henselian local ring Sh with R → Sh local, since the source's S enters only through the composite R → S → S^h. Of the henselization R → Rh only the two items of Lemma 04GN that the proof uses are assumed — ind-étale, (CommAlgCat.etale R).ind, and surjectivity on residue fields. The commutative square is the R-algebra structure of the map. isLocalHom_indEtaleAlgHom and indEtaleAlgHom_unique are its defining property and its uniqueness. See the module docstring.”.

The map given by the universal property of the henselization (Stacks 04GS). Let (R, 𝔪, κ) be a local ring, let Rh be a local R-algebra with R → Rh local which is a filtered colimit of étale R-algebras and has residue field κ, and let Sh be a henselian local ring with R → Sh local. This is the R-algebra map Rh → Sh that is a local ring map, unique as such by indEtaleAlgHom_unique. Applied to the henselizations Rh = R^h and Sh = S^h of a local map of local rings R → S, it is the local ring map R^h → S^h over R → S that makes the henselization a functor.

noncomputable def HenselianLocalRing.indEtaleAlgHom
    {R : Type u} {Rh : Type v} {Sh : Type w} [CommRing R] [CommRing Rh] [CommRing Sh]
    [IsLocalRing R]
    [IsLocalRing Rh] [HenselianLocalRing Sh] [Algebra R Rh] [Algebra R Sh]
    [IsLocalHom (algebraMap R Rh)] [IsLocalHom (algebraMap R Sh)]
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rh)))
    (hres : Function.Surjective (ResidueField.map (algebraMap R Rh))) :
    Rh →ₐ[R] Sh

HenselianLocalRing.isLocalHom_indEtaleAlgHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/HenselizationUniversalProperty.lean, line 390. The attribute's comment: “the defining property of indEtaleAlgHom”.

HenselianLocalRing.indEtaleAlgHom is a local ring map.

public theorem HenselianLocalRing.isLocalHom_indEtaleAlgHom
    {R : Type u} {Rh : Type v} {Sh : Type w} [CommRing R] [CommRing Rh] [CommRing Sh]
    [IsLocalRing R]
    [IsLocalRing Rh] [HenselianLocalRing Sh] [Algebra R Rh] [Algebra R Sh]
    [IsLocalHom (algebraMap R Rh)] [IsLocalHom (algebraMap R Sh)]
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rh)))
    (hres : Function.Surjective (ResidueField.map (algebraMap R Rh))) :
    IsLocalHom (HenselianLocalRing.indEtaleAlgHom (Sh := Sh) hind hres)

HenselianLocalRing.indEtaleAlgHom_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/HenselizationUniversalProperty.lean, line 404. The attribute's comment: “uniqueness of indEtaleAlgHom”.

HenselianLocalRing.indEtaleAlgHom is the only local R-algebra map Rh → Sh.

public theorem HenselianLocalRing.indEtaleAlgHom_unique
    {R : Type u} {Rh : Type v} {Sh : Type w} [CommRing R] [CommRing Rh] [CommRing Sh]
    [IsLocalRing R]
    [IsLocalRing Rh] [HenselianLocalRing Sh] [Algebra R Rh] [Algebra R Sh]
    [IsLocalHom (algebraMap R Rh)] [IsLocalHom (algebraMap R Sh)]
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rh)))
    (hres : Function.Surjective (ResidueField.map (algebraMap R Rh)))
    (f : Rh →ₐ[R] Sh) (hf : IsLocalHom f) :
    f = HenselianLocalRing.indEtaleAlgHom hind hres

Tag 04GV, a lemma

Tag 04GV in the Stacks Project.

IsLocalRing.IsHenselization.isFiltered_etaleNeighborhood_and_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/EtaleNeighborhood.lean, line 333. The attribute's comment: “Étale neighborhoods (S, q) with κ(p) = κ(q) are étale R-algebras with an augmentation to κ(p), whose kernel is q. canonically is the characterization of the colimit maps S → (R_p)^h: the unique family inducing the identity of κ(p) = κ((R_p)^h) on residue fields; the maps S_q → (R_p)^h are pinned by extending them along S → S_q. The henselization is IsHenselization with residue field κ(p).”. References: SGA 4 VIII (4.1), “more general”.

The henselization as a colimit of étale neighborhoods (Stacks 04GV). Let p be a prime of R and let Rh be a henselization of R_p. The category of étale neighborhoods (S, q) of p with κ(q) = κ(p) is filtered, and Rh is canonically the colimit of the algebras S and also of the local rings S_q. The canonical maps S → Rh are the unique R-algebra maps inducing κ(q) = κ(p) ≅ κ(Rh) on residue fields, and the maps S_q → Rh extend them.

theorem isFiltered_etaleNeighborhood_and_isColimit :
    IsFiltered (EtaleNeighborhood p) ∧
      ∃ ι : EtaleNeighborhood.forget p ⟶ (Functor.const _).obj (CommAlgCat.of R Rh),
        (∀ A x, residue Rh ((ι.app A).hom x) =
          ResidueField.map (algebraMap (Localization.AtPrime p) Rh) (A.hom.hom x)) ∧
        (∀ ι' : EtaleNeighborhood.forget p ⟶ (Functor.const _).obj (CommAlgCat.of R Rh),
          (∀ A x, residue Rh ((ι'.app A).hom x) =
            ResidueField.map (algebraMap (Localization.AtPrime p) Rh) (A.hom.hom x)) → ι' = ι) ∧
        Nonempty (IsColimit (Cocone.mk _ ι)) ∧
        ∃ ιLoc : EtaleNeighborhood.localization p ⟶ (Functor.const _).obj (CommAlgCat.of R Rh),
          (∀ A, (EtaleNeighborhood.toLocalization p).app A ≫ ιLoc.app A = ι.app A) ∧
          Nonempty (IsColimit (Cocone.mk _ ιLoc))

Tag 08HU, a lemma

Tag 08HU in the Stacks Project.

IsLocalRing.IsHenselization.exists_unique_prime_isHenselization_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/TensorProduct.lean, line 366. The attribute's comment: “The map R^h → S^h of 04GS is pinned as the unique local R-algebra map f compatible with R_p → S_q. The prime is characterized by its two contractions, with uniqueness, and equals g⁻¹(𝔪_{S^h}) for the map g induced by f; that S^h is the henselization of (R^h ⊗_R S)_Q is IsHenselization with residue field κ(Q), through an algebra structure extending g. All rings share one universe, as IsHenselization requires.”.

The henselization after a ring map (Stacks 08HU). Let R → S be a ring map and let q ⊆ S lie over p ⊆ R. Let Rh and Sh be henselizations of R_p and S_q. The local ring map f : Rh → Sh of Lemma 04GS (the unique local map over R_p → S_q) identifies Sh with the henselization of Rh ⊗[R] S at the unique prime Q lying over 𝔪_Rh and q: here Q is the inverse image of 𝔪_Sh under the map g : Rh ⊗[R] S → Sh induced by f, and Sh is a henselization of (Rh ⊗[R] S)_Q through an algebra structure extending g.

theorem exists_unique_prime_isHenselization_tensorProduct [Algebra R Sq] [Algebra Rp Sq]
    [IsScalarTower R S Sq] [IsScalarTower R Rp Sq] [IsHenselization Rp (ResidueField Rp) Rh]
    [Algebra Rp Sh] [IsScalarTower Rp Sq Sh] [IsHenselization Sq (ResidueField Sq) Sh] :
    ∃ f : Rh →ₐ[R] Sh, IsLocalHom f ∧
      f.toRingHom.comp (algebraMap Rp Rh) = algebraMap Rp Sh ∧
      (∀ f' : Rh →ₐ[R] Sh, IsLocalHom f' →
        f'.toRingHom.comp (algebraMap Rp Rh) = algebraMap Rp Sh → f' = f) ∧
      let g : Rh ⊗[R] S →ₐ[R] Sh :=
        Algebra.TensorProduct.lift f (IsScalarTower.toAlgHom R S Sh) fun _ _ => .all _ _
      ∃ (Q : Ideal (Rh ⊗[R] S)) (_ : Q.IsPrime),
        Q.comap (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := Rh) (B := S)) =
          maximalIdeal Rh ∧
        Q.comap (Algebra.TensorProduct.includeRight (R := R) (A := Rh) (B := S)).toRingHom = q ∧
        Q = (maximalIdeal Sh).comap g.toRingHom ∧
        (∀ Q' : Ideal (Rh ⊗[R] S), Q'.IsPrime →
          Q'.comap (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := Rh) (B := S)) =
            maximalIdeal Rh →
          Q'.comap (Algebra.TensorProduct.includeRight (R := R) (A := Rh) (B := S)).toRingHom =
            q → Q' = Q) ∧
        ∃ _ : Algebra (Localization.AtPrime Q) Sh,
          IsLocalHom (algebraMap (Localization.AtPrime Q) Sh) ∧
          IsHenselization (Localization.AtPrime Q) (ResidueField (Localization.AtPrime Q)) Sh ∧
          (algebraMap (Localization.AtPrime Q) Sh).comp
            (algebraMap (Rh ⊗[R] S) (Localization.AtPrime Q)) = g.toRingHom

StacksDraft.henselization_tensorProduct_at_unique_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HenselizationUniverse/TensorProduct.lean, line 287. The attribute's comment: “Stated over six independent universes, as the source requires: the tag's six rings R, R_p, R^h, S, S_q, S^h are unconstrained relative to one another.”.

Henselization after a ring map (Stacks 08HU), at six independent universes. For primes q over p, the canonical local map between henselizations of R_p and S_q identifies the latter with the henselization of Rh ⊗[R] S at its unique prime lying over both the maximal ideal of Rh and q. The final equality says that the henselization map is induced by the canonical map from the tensor product.

This is the source-strength form of tag 08HU, and the provider of that tag. The weaker single-universe statement IsLocalRing.IsHenselization.exists_unique_prime_isHenselization_tensorProduct pins all six rings to one Type u; its @[stacks 08HU] attribute is dropped in favour of this one. See the module docstring.

theorem henselization_tensorProduct_at_unique_prime
    {R : Type uR} {Rp : Type uRp} {Rh : Type uRh}
    {S : Type uS} {Sq : Type uSq} {Sh : Type uSh}
    [CommRing R] [CommRing S] [Algebra R S]
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p]
    [CommRing Rp] [IsLocalRing Rp] [Algebra R Rp] [IsLocalization.AtPrime Rp p]
    [CommRing Sq] [IsLocalRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q]
    [Algebra R Sq] [Algebra Rp Sq] [IsScalarTower R S Sq] [IsScalarTower R Rp Sq]
    [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh] [Algebra Rp Rh]
    [IsScalarTower R Rp Rh] [IsHenselization Rp (ResidueField Rp) Rh]
    [CommRing Sh] [IsLocalRing Sh] [Algebra R Sh] [Algebra S Sh] [Algebra Rp Sh]
    [Algebra Sq Sh] [IsScalarTower R S Sh] [IsScalarTower S Sq Sh]
    [IsScalarTower Rp Sq Sh] [IsHenselization Sq (ResidueField Sq) Sh] :
    ∃ f : Rh →ₐ[R] Sh,
      IsLocalHom f ∧
      f.toRingHom.comp (algebraMap Rp Rh) = algebraMap Rp Sh ∧
      (∀ f' : Rh →ₐ[R] Sh, IsLocalHom f' →
        f'.toRingHom.comp (algebraMap Rp Rh) = algebraMap Rp Sh → f' = f) ∧
      let g : Rh ⊗[R] S →ₐ[R] Sh :=
        Algebra.TensorProduct.lift f (IsScalarTower.toAlgHom R S Sh)
          (fun _ _ => Commute.all _ _)
      ∃ (Q : Ideal (Rh ⊗[R] S)) (_hQ : Q.IsPrime),
        Q.comap (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := Rh) (B := S)) =
            maximalIdeal Rh ∧
        Q.comap (Algebra.TensorProduct.includeRight (R := R) (A := Rh) (B := S)).toRingHom = q ∧
        Q = (maximalIdeal Sh).comap g.toRingHom ∧
        (∀ (Q' : Ideal (Rh ⊗[R] S)), Q'.IsPrime →
          Q'.comap (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := Rh) (B := S)) =
              maximalIdeal Rh →
          Q'.comap (Algebra.TensorProduct.includeRight (R := R) (A := Rh) (B := S)).toRingHom =
              q → Q' = Q) ∧
        ∃ alg : Algebra (Localization.AtPrime Q) Sh,
          letI : Algebra (Localization.AtPrime Q) Sh := alg
          ∃ _ : IsLocalHom (algebraMap (Localization.AtPrime Q) Sh),
            IsHenselization (Localization.AtPrime Q)
                (ResidueField (Localization.AtPrime Q)) Sh ∧
              (algebraMap (Localization.AtPrime Q) Sh).comp
                  (algebraMap (Rh ⊗[R] S) (Localization.AtPrime Q)) = g.toRingHom

Tag 04GT, a lemma

Tag 04GT in the Stacks Project.

Stacks.StrictHenselization.strict_henselization_universal_property, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization.lean, line 1104.

Theorem (Stacks Tag 04GT). Let φ : R → S be a local ring map of local rings, let κ(S) ⊂ κsep be a separable algebraic closure of the residue field of S, and let S → Ssh be a strict henselization of S with respect to it. Let R → A be an étale ring map and q a prime of A lying over m_R. Given a residue field point φbar : κ(q) → κsep making the residue field square commute, there is a unique ring map f : A → Ssh compatible over the base, with f⁻¹(m_{Ssh}) = q, and inducing φbar on residue fields (via the identification κ(Ssh) ≅ κsep).

theorem strict_henselization_universal_property
    -- Local rings and the local base map `φ : R → S`.
    {R S : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    (φ : R →+* S) [IsLocalHom φ]
    -- A separable algebraic closure `κ(S) ⊂ κsep` of the residue field of `S` (Definition 2).
    (κsep : Type*) [Field κsep] [Algebra (maximalIdeal S).ResidueField κsep]
      [IsSepClosure (maximalIdeal S).ResidueField κsep]
    -- The strict henselization `S → Ssh` (Definition 3).
    {Ssh : Type*} [CommRing Ssh] [IsLocalRing Ssh] [Algebra S Ssh]
    (hsh : IsStrictHenselization S κsep Ssh)
    -- An étale `R`-algebra `A` and a prime `q` lying over `m_R`.
    {A : Type*} [CommRing A] [Algebra R A] [Algebra.Etale R A]
    (q : Ideal A) [q.IsPrime] (hq : maximalIdeal R = q.comap (algebraMap R A))
    -- The given residue field point `φbar : κ(q) → κsep`.
    (φbar : q.ResidueField →+* κsep)
    -- Compatibility of the residue square:
    --   `φbar ∘ (κ(R) → κ(q)) = (κ(S) → κsep) ∘ (κ(R) → κ(S))`.
    (hsquare :
      φbar.comp (Ideal.ResidueField.map (maximalIdeal R) q (algebraMap R A) hq)
        =
      (algebraMap (maximalIdeal S).ResidueField κsep).comp
        (Ideal.ResidueField.map (maximalIdeal R) (maximalIdeal S) φ
          (maximalIdeal_comap φ).symm)) :
    ∃! f : A →+* Ssh,
      -- (1) Compatibility over the base.
      (f.comp (algebraMap R A) = (algebraMap S Ssh).comp φ) ∧
      -- (2) Prime condition: `f⁻¹(m_{Ssh}) = q`.
      (∃ hf : q = (maximalIdeal Ssh).comap f,
        -- (3) Residue field condition: the induced `κ(q) → κ(Ssh)` equals
        --     `κ(q) --φbar--> κsep ≃ κ(Ssh)`.
        Ideal.ResidueField.map q (maximalIdeal Ssh) f hf
          = (hsh.residueFieldEquiv : κsep →+* (maximalIdeal Ssh).ResidueField).comp φbar)

Tag 04GU, a lemma

Tag 04GU in the Stacks Project.

HenselianLocalRing.indEtaleAlgHomOfResidue, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization.lean, line 392. The attribute's comment: “The map of the universal property: the target is an arbitrary henselian local R-algebra Ssh, since the source's S enters only through the composite R → S → S^sh, and of R^sh only locality and ind-étaleness — (CommAlgCat.etale R).ind, the spelling of Lemma 04GP(3) — are used. The source's square of residue fields is hφ, stated at the level of R; R local and both structure maps local are consequences of it, not hypotheses. isLocalHom_indEtaleAlgHomOfResidue, comp_residue_indEtaleAlgHomOfResidue and indEtaleAlgHomOfResidue_unique are its two properties and its uniqueness. See the module docstring.”. References: EGA IV (18.8.8.1), “existence of A^hs->B”; EGA IV (18.8.8).

The map given by functoriality of the strict henselization (Stacks 04GU). Let R be a ring, let Rsh be a local R-algebra which is a filtered colimit of étale R-algebras, let Ssh be a henselian local R-algebra, and let φ : ResidueField Rsh →+* ResidueField Ssh be compatible with the residue maps of R → Rsh and R → Ssh. This is the R-algebra map f : Rsh → Ssh inducing φ on residue fields; it is a local ring map, and is the only such map. Applied to strict henselizations Rsh = R^sh and Ssh = S^sh of a local map of local rings R → S, and to a map φ : κ₁^sep → κ₂^sep of separable algebraic closures over the residue field map of R → S, it is the local ring map R^sh → S^sh over R → S inducing φ.

noncomputable def HenselianLocalRing.indEtaleAlgHomOfResidue
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rsh)))
    (φ : ResidueField Rsh →+* ResidueField Ssh)
    (hφ : φ.comp ((residue Rsh).comp (algebraMap R Rsh))
      = (residue Ssh).comp (algebraMap R Ssh)) :
    Rsh →ₐ[R] Ssh

HenselianLocalRing.comp_residue_indEtaleAlgHomOfResidue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization.lean, line 405. The attribute's comment: “the defining property of indEtaleAlgHomOfResidue”. References: EGA IV (18.8.8.1), “induces \psi on residues”; EGA IV (18.8.4), “partial”.

HenselianLocalRing.indEtaleAlgHomOfResidue induces φ on residue fields.

public theorem HenselianLocalRing.comp_residue_indEtaleAlgHomOfResidue
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rsh)))
    (φ : ResidueField Rsh →+* ResidueField Ssh)
    (hφ : φ.comp ((residue Rsh).comp (algebraMap R Rsh))
      = (residue Ssh).comp (algebraMap R Ssh)) :
    (residue Ssh).comp
        (HenselianLocalRing.indEtaleAlgHomOfResidue hind φ hφ : Rsh →+* Ssh)
      = φ.comp (residue Rsh)

HenselianLocalRing.isLocalHom_indEtaleAlgHomOfResidue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization.lean, line 420. The attribute's comment: “indEtaleAlgHomOfResidue is local, which the source asserts”. References: EGA IV (18.8.8.1), “locality of A^hs->B”.

HenselianLocalRing.indEtaleAlgHomOfResidue is a local ring map.

public theorem HenselianLocalRing.isLocalHom_indEtaleAlgHomOfResidue
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rsh)))
    (φ : ResidueField Rsh →+* ResidueField Ssh)
    (hφ : φ.comp ((residue Rsh).comp (algebraMap R Rsh))
      = (residue Ssh).comp (algebraMap R Ssh)) :
    IsLocalHom (HenselianLocalRing.indEtaleAlgHomOfResidue hind φ hφ)

HenselianLocalRing.indEtaleAlgHomOfResidue_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization.lean, line 433. The attribute's comment: “uniqueness of indEtaleAlgHomOfResidue”. References: EGA IV (18.8.8.1), “uniqueness of A^hs->B”.

HenselianLocalRing.indEtaleAlgHomOfResidue is the only local R-algebra map Rsh → Ssh inducing φ on residue fields.

public theorem HenselianLocalRing.indEtaleAlgHomOfResidue_unique
    (hind : (CommAlgCat.etale.{max u v} R).ind.{max u v}
      (CommAlgCat.of R (ULift.{u} Rsh)))
    (φ : ResidueField Rsh →+* ResidueField Ssh)
    (hφ : φ.comp ((residue Rsh).comp (algebraMap R Rsh))
      = (residue Ssh).comp (algebraMap R Ssh))
    (f : Rsh →ₐ[R] Ssh) (hfloc : IsLocalHom f)
    (hf : (residue Ssh).comp (f : Rsh →+* Ssh) = φ.comp (residue Rsh)) :
    f = HenselianLocalRing.indEtaleAlgHomOfResidue hind φ hφ

Stacks.StrictHenselization.IsStrictHenselization.existsUnique_algHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/StrictlyHenselianTarget.lean, line 167. The attribute's comment: “The universal property read off IsStrictHenselization: the residue datum is a map out of the chosen separable closure κ^sep rather than out of IsLocalRing.ResidueField R, the convention HenselianLocalRing.indEtaleAlgHomOfResidue is phrased in, and the target is an arbitrary henselian local A-algebra as there. Existence and uniqueness among local A-algebra maps are the source's two assertions.”. References: EGA IV (18.8.8), “more general”; EGA IV (18.8.9), “special case”; SGA 4 VIII (4.4), “more general”.

The universal property of the strict henselization against a henselian local algebra (Stacks 04GU). Let A be a local ring, let κ^sep be a separable algebraic closure of its residue field and let R be a strict henselization of A with respect to it. Let C be a henselian local A-algebra, and let χ : κ^sep → κ(C) be a ring map compatible with the residue maps of A → R and A → C (the square of fields of the source). Then there is exactly one local A-algebra map R → C inducing χ on residue fields.

The source states this for C a strict henselization of a local ring S receiving a local map from A; Lemma 04GU uses of C only that it is a henselian local A-algebra, and that is the form taken here, since the target that this is applied to is known to be strictly henselian before it is known to be a strict henselization.

theorem IsStrictHenselization.existsUnique_algHom (hR : IsStrictHenselization A κsep R)
    {C : Type*} [CommRing C] [HenselianLocalRing C] [Algebra A C]
    (χ : κsep →+* ResidueField C)
    (hχ : ∀ a : A, χ (algebraMap (maximalIdeal A).ResidueField κsep
        (algebraMap A (maximalIdeal A).ResidueField a))
      = residue C (algebraMap A C a)) :
    ∃! f : R →ₐ[A] C, IsLocalHom f ∧
      (residue C).comp (f : R →+* C) = (χ.comp hR.residueFieldHom).comp (residue R)

Stacks.StrictHenselization.IsStrictHenselization.exists_algHom_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/StrictlyHenselianTarget.lean, line 200. The attribute's comment: “The source's map, in the case where the target's residue field is only known to be separably closed rather than identified with a chosen separable closure: the residue datum is then not part of the input but produced by IsSepClosed.lift, and only existence survives.”. References: EGA IV (18.8.8), “(ii)”.

A strictly henselian local algebra receives a local map from the strict henselization. Let A be a local ring, let κ^sep be a separable algebraic closure of its residue field and let R be a strict henselization of A with respect to it. Let C be a henselian local A-algebra with separably closed residue field whose structure map is local. Then there is a local A-algebra map R → C.

No residue datum has to be supplied: κ^sep is separable over κ_A and κ(C) is a separably closed field over κ_A through the residue map of A → C, so IsSepClosed.lift produces one, and existsUnique_algHom turns it into the map. Uniqueness is not asserted, and genuinely fails: the local maps R → C over A are permuted by the automorphisms of κ^sep over κ_A, and it is the residue datum that singles one out.

theorem IsStrictHenselization.exists_algHom_of_isSepClosed (hR : IsStrictHenselization A κsep R)
    (C : Type*) [CommRing C] [HenselianLocalRing C] [Algebra A C]
    [IsLocalHom (algebraMap A C)] (hC : IsSepClosed (ResidueField C)) :
    ∃ f : R →ₐ[A] C, IsLocalHom f

Tag 04GW, a lemma

Tag 04GW in the Stacks Project.

IsLocalRing.IsHenselization.isFiltered_augmentedEtale_and_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselizationColimit.lean, line 324. The attribute's comment: “A triple (S, q, φ) is an étale R-algebra with an R-algebra map to κ^sep, whose kernel is q. The strict henselization of R_p with respect to κ^sep is IsHenselization (Localization.AtPrime p) κsep Rsh; the statement is proved for any extension L of κ(p). canonically is the characterization of the colimit maps S → Rsh: given the identification e : κ^sep ≅ κ(Rsh), they are the unique maps reducing to S → κ^sep ≅ κ(Rsh); the maps S_q → Rsh extend them along S → S_q.”.

The strict henselization as a colimit of étale algebras (Stacks 04GW). Let p be a prime of R, let L be an extension of κ(p) (a separable algebraic closure κ^sep, in the source), let Rsh be a henselization of R_p with residue field L (the strict henselization (R_p)^{sh}), and fix an isomorphism e : L ≅ κ(Rsh) compatible with the maps from R. The category of étale R-algebras S with an R-algebra map S → L — the triples (S, q, φ) — is filtered, and Rsh is canonically the colimit of the algebras S and also of the local rings S_q, where q is the kernel of S → L. The canonical maps S → Rsh are the unique R-algebra maps whose reduction is S → L ≅ κ(Rsh), and the maps S_q → Rsh extend them.

theorem isFiltered_augmentedEtale_and_isColimit [IsScalarTower R (Localization.AtPrime p) Rsh] :
    IsFiltered (AugmentedEtale R L) ∧
      ∃ ι : forget R L ⟶ (Functor.const _).obj (CommAlgCat.of R Rsh),
        (∀ A x, residue Rsh ((ι.app A).hom x) = e (A.hom.hom x)) ∧
        (∀ ι' : forget R L ⟶ (Functor.const _).obj (CommAlgCat.of R Rsh),
          (∀ A x, residue Rsh ((ι'.app A).hom x) = e (A.hom.hom x)) → ι' = ι) ∧
        Nonempty (IsColimit (Cocone.mk _ ι)) ∧
        ∃ ιLoc : localization R L ⟶ (Functor.const _).obj (CommAlgCat.of R Rsh),
          (∀ A, (toLocalization R L).app A ≫ ιLoc.app A = ι.app A) ∧
          Nonempty (IsColimit (Cocone.mk _ ιLoc))

Tag 08HV, a lemma

Tag 08HV in the Stacks Project.

IsLocalRing.IsHenselization.exists_prime_isStrictHenselization_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/TensorProduct.lean, line 70. The attribute's comment: “The separable algebraic closures are the residue fields of R^sh and S^sh, and the commutative square is the compatibility hphi of φ with the residue maps out of R. The map of 04GU is pinned as the unique local R-algebra map inducing φ. The prime is g⁻¹(𝔪_{S^sh}) with its two contractions; that S^sh is the strict henselization of (R^sh ⊗_R S)_Q is IsHenselization with residue field κ(S^sh), separably closed over κ(Q). All rings share one universe, as IsHenselization requires.”.

The strict henselization after a ring map (Stacks 08HV). Let R → S be a ring map and let q ⊆ S lie over p ⊆ R. Let Rsh and Ssh be strict henselizations of R_p and S_q, with respect to the separable algebraic closures κ(Rsh) of κ(p) and κ(Ssh) of κ(q), and let φ : κ(Rsh) → κ(Ssh) be compatible with the residue maps out of R. The local map f : Rsh → Ssh of Lemma 04GU inducing φ identifies Ssh with the strict henselization of Rsh ⊗[R] S at the prime Q = g⁻¹(𝔪_Ssh), where g : Rsh ⊗[R] S → Ssh is induced by f; Q lies over 𝔪_Rsh and over q.

theorem exists_prime_isStrictHenselization_tensorProduct [Algebra R Sq] [Algebra Rp Sq]
    [IsScalarTower R S Sq] [IsScalarTower R Rp Sq] [Algebra Rp Ssh] [IsScalarTower R Rp Ssh]
    [IsScalarTower Rp Sq Ssh] (phi : ResidueField Rsh →+* ResidueField Ssh)
    (hphi : phi.comp ((residue Rsh).comp (algebraMap R Rsh)) =
      (residue Ssh).comp (algebraMap R Ssh)) :
    ∃ f : Rsh →ₐ[R] Ssh, IsLocalHom f ∧
      (residue Ssh).comp f.toRingHom = phi.comp (residue Rsh) ∧
      (∀ f' : Rsh →ₐ[R] Ssh, IsLocalHom f' →
        (residue Ssh).comp f'.toRingHom = phi.comp (residue Rsh) → f' = f) ∧
      let g : Rsh ⊗[R] S →ₐ[R] Ssh :=
        Algebra.TensorProduct.lift f (IsScalarTower.toAlgHom R S Ssh) fun _ _ => .all _ _
      ∃ (Q : Ideal (Rsh ⊗[R] S)) (_ : Q.IsPrime),
        Q.comap (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := Rsh) (B := S)) =
          maximalIdeal Rsh ∧
        Q.comap (Algebra.TensorProduct.includeRight (R := R) (A := Rsh) (B := S)).toRingHom = q ∧
        Q = (maximalIdeal Ssh).comap g.toRingHom ∧
        ∃ _ : Algebra (Localization.AtPrime Q) Ssh,
          IsLocalHom (algebraMap (Localization.AtPrime Q) Ssh) ∧
          ∃ _ : Algebra (ResidueField (Localization.AtPrime Q)) (ResidueField Ssh),
            IsSepClosure (ResidueField (Localization.AtPrime Q)) (ResidueField Ssh) ∧
            IsHenselization (Localization.AtPrime Q) (ResidueField Ssh) Ssh ∧
            (∀ x, algebraMap (ResidueField (Localization.AtPrime Q)) (ResidueField Ssh)
              (residue (Localization.AtPrime Q) x) =
                residue Ssh (algebraMap (Localization.AtPrime Q) Ssh x)) ∧
            (algebraMap (Localization.AtPrime Q) Ssh).comp
              (algebraMap (Rsh ⊗[R] S) (Localization.AtPrime Q)) = g.toRingHom

StacksDraft.strictHenselization_tensorProduct_at_induced_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HenselizationUniverse/StrictTensorProduct.lean, line 76. The attribute's comment: “Stated over six independent universes, as the source requires: the tag's six rings R, R_p, R^sh, S, S_q, S^sh are unconstrained relative to one another.”.

Strict henselization after a ring map (Stacks 08HV), at six independent universes. For primes q over p and compatible separable closures of their residue fields, the canonical local map between strict henselizations identifies the target with the strict henselization of Rsh ⊗[R] S at the prime induced by that map.

This is the source-strength form of tag 08HV, and the provider of that tag. The weaker single-universe statement IsLocalRing.IsHenselization.exists_prime_isStrictHenselization_tensorProduct pins all six rings to one Type u; its @[stacks 08HV] attribute is dropped in favour of this one. See the module docstring.

theorem strictHenselization_tensorProduct_at_induced_prime
    {R : Type uR} {Rp : Type uRp} {Rsh : Type uRsh}
    {S : Type uS} {Sq : Type uSq} {Ssh : Type uSsh}
    [CommRing R] [CommRing S] [Algebra R S]
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p]
    [CommRing Rp] [IsLocalRing Rp] [Algebra R Rp] [IsLocalization.AtPrime Rp p]
    [CommRing Sq] [IsLocalRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q]
    [Algebra R Sq] [Algebra Rp Sq] [IsScalarTower R S Sq] [IsScalarTower R Rp Sq]
    [CommRing Rsh] [IsLocalRing Rsh] [Algebra R Rsh] [Algebra Rp Rsh]
    [IsScalarTower R Rp Rsh]
    [Algebra (ResidueField Rp) (ResidueField Rsh)]
    [IsSepClosure (ResidueField Rp) (ResidueField Rsh)]
    [IsHenselization Rp (ResidueField Rsh) Rsh]
    [CommRing Ssh] [IsLocalRing Ssh] [Algebra R Ssh] [Algebra S Ssh] [Algebra Rp Ssh]
    [Algebra Sq Ssh] [IsScalarTower R S Ssh] [IsScalarTower S Sq Ssh]
    [IsScalarTower R Rp Ssh] [IsScalarTower Rp Sq Ssh]
    [Algebra (ResidueField Sq) (ResidueField Ssh)]
    [IsSepClosure (ResidueField Sq) (ResidueField Ssh)]
    [IsHenselization Sq (ResidueField Ssh) Ssh]
    (phi : ResidueField Rsh →+* ResidueField Ssh)
    (hphi : phi.comp ((residue Rsh).comp (algebraMap R Rsh)) =
      (residue Ssh).comp (algebraMap R Ssh)) :
    ∃ f : Rsh →ₐ[R] Ssh,
      IsLocalHom f ∧
      (residue Ssh).comp f.toRingHom = phi.comp (residue Rsh) ∧
      (∀ f' : Rsh →ₐ[R] Ssh, IsLocalHom f' →
        (residue Ssh).comp f'.toRingHom = phi.comp (residue Rsh) → f' = f) ∧
      let g : Rsh ⊗[R] S →ₐ[R] Ssh :=
        Algebra.TensorProduct.lift f (IsScalarTower.toAlgHom R S Ssh)
          (fun _ _ => Commute.all _ _)
      ∃ (Q : Ideal (Rsh ⊗[R] S)) (_hQ : Q.IsPrime),
        Q.comap (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := Rsh) (B := S)) =
            maximalIdeal Rsh ∧
        Q.comap (Algebra.TensorProduct.includeRight (R := R) (A := Rsh) (B := S)).toRingHom = q ∧
        Q = (maximalIdeal Ssh).comap g.toRingHom ∧
        ∃ alg : Algebra (Localization.AtPrime Q) Ssh,
          letI : Algebra (Localization.AtPrime Q) Ssh := alg
          ∃ _ : IsLocalHom (algebraMap (Localization.AtPrime Q) Ssh),
            ∃ algRes : Algebra (ResidueField (Localization.AtPrime Q)) (ResidueField Ssh),
              letI : Algebra (ResidueField (Localization.AtPrime Q)) (ResidueField Ssh) := algRes
              IsSepClosure (ResidueField (Localization.AtPrime Q)) (ResidueField Ssh) ∧
                IsHenselization (Localization.AtPrime Q) (ResidueField Ssh) Ssh ∧
                (∀ x : Localization.AtPrime Q,
                  algebraMap (ResidueField (Localization.AtPrime Q)) (ResidueField Ssh)
                      (residue (Localization.AtPrime Q) x) =
                    residue Ssh (algebraMap (Localization.AtPrime Q) Ssh x)) ∧
                (algebraMap (Localization.AtPrime Q) Ssh).comp
                    (algebraMap (Rsh ⊗[R] S) (Localization.AtPrime Q)) = g.toRingHom

Tag 0C2Z, a lemma

Tag 0C2Z in the Stacks Project.

IsLocalRing.IsHenselization.exists_algEquiv_tensorProduct_strictHenselization_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/BaseChange.lean, line 689. The attribute's comment: “The equality of the source is an isomorphism of (S_q)^h-algebras Ssh ≃ₐ[Sh] Sh ⊗[Rh] Rsh compatible with the local map Rsh → Ssh over Rh inducing the identity of κ^sep (via eRsh, eSsh), which is part of the statement. Henselizations and strict henselizations are IsHenselization with residue field κ and κ^sep. All seven carriers — R, S, κ^sep, (R_p)^h, (S_q)^h, (R_p)^{sh}, (S_q)^{sh} — lie in mutually independent universes.”.

The strict henselization as a base change of the henselization (Stacks 0C2Z). Let R → S be a ring map and let q be a prime of S lying over the prime p of R such that κ(p) → κ(q) is an isomorphism, and let κ^sep be a separable algebraic closure of κ(p) = κ(q). Let (R_p)^h → (S_q)^h be henselizations over R_p → S_q and let (R_p)^{sh}, (S_q)^{sh} be strict henselizations with respect to κ^sep. Then the local map (R_p)^{sh} → (S_q)^{sh} over (R_p)^h inducing the identity of κ^sep identifies (S_q)^{sh} with (S_q)^h ⊗_{(R_p)^h} (R_p)^{sh}.

theorem IsLocalRing.IsHenselization.exists_algEquiv_tensorProduct_strictHenselization_atPrime
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S)
    [p.IsPrime] [q.IsPrime] [q.LiesOver p]
    [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
    [Localization.AtPrime.IsLiesOverAlgebra p q]
    (hres : Function.Bijective
      (ResidueField.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))))
    (ksep : Type w) [Field ksep] [Algebra (ResidueField (Localization.AtPrime p)) ksep]
    [Algebra (ResidueField (Localization.AtPrime q)) ksep]
    [IsSepClosure (ResidueField (Localization.AtPrime p)) ksep]
    [IsSepClosure (ResidueField (Localization.AtPrime q)) ksep]
    (hksep : ∀ a, algebraMap (ResidueField (Localization.AtPrime q)) ksep
      (ResidueField.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) a) =
        algebraMap (ResidueField (Localization.AtPrime p)) ksep a)
    (Rh : Type x) [CommRing Rh] [IsLocalRing Rh] [Algebra (Localization.AtPrime p) Rh]
    [IsHenselization (Localization.AtPrime p) (ResidueField (Localization.AtPrime p)) Rh]
    (Sh : Type y) [CommRing Sh] [IsLocalRing Sh] [Algebra (Localization.AtPrime q) Sh]
    [IsHenselization (Localization.AtPrime q) (ResidueField (Localization.AtPrime q)) Sh]
    [Algebra (Localization.AtPrime p) Sh] [Algebra Rh Sh]
    [IsScalarTower (Localization.AtPrime p) Rh Sh]
    [IsScalarTower (Localization.AtPrime p) (Localization.AtPrime q) Sh]
    [IsLocalHom (algebraMap Rh Sh)]
    (Rsh : Type z) [CommRing Rsh] [IsLocalRing Rsh] [Algebra (Localization.AtPrime p) Rsh]
    [Algebra Rh Rsh] [IsScalarTower (Localization.AtPrime p) Rh Rsh]
    [IsHenselization (Localization.AtPrime p) ksep Rsh]
    (Ssh : Type t) [CommRing Ssh] [IsLocalRing Ssh] [Algebra (Localization.AtPrime q) Ssh]
    [Algebra Sh Ssh] [Algebra (Localization.AtPrime p) Ssh] [Algebra Rh Ssh]
    [IsScalarTower (Localization.AtPrime q) Sh Ssh]
    [IsScalarTower (Localization.AtPrime p) (Localization.AtPrime q) Ssh]
    [IsScalarTower (Localization.AtPrime p) Rh Ssh] [IsScalarTower Rh Sh Ssh]
    [IsHenselization (Localization.AtPrime q) ksep Ssh]
    (eRsh : ksep ≃+* ResidueField Rsh)
    (heRsh : ∀ a, eRsh (algebraMap (ResidueField (Localization.AtPrime p)) ksep
      (residue (Localization.AtPrime p) a)) =
        residue Rsh (algebraMap (Localization.AtPrime p) Rsh a))
    (eSsh : ksep ≃+* ResidueField Ssh)
    (heSsh : ∀ b, eSsh (algebraMap (ResidueField (Localization.AtPrime q)) ksep
      (residue (Localization.AtPrime q) b)) =
        residue Ssh (algebraMap (Localization.AtPrime q) Ssh b)) :
    ∃ g : Rsh →ₐ[Rh] Ssh, IsLocalHom g ∧
      (∀ a, eSsh.symm (residue Ssh (g a)) = eRsh.symm (residue Rsh a)) ∧
      ∃ e : Ssh ≃ₐ[Sh] Sh ⊗[Rh] Rsh, ∀ a, e (g a) = Algebra.TensorProduct.includeRight a

Sources

• Section 10.155, Tag 0BSK
• AxiomMath/Stacks at 5ed82d14

LeanIsLocalRing.exists_henselization · IsLocalRing.exists_strictHenselization · Stacks.StrictHenselization.exists_isStrictHenselization · IsLocalRing.IsHenselization · IsLocalRing.IsHenselization.exists_strictHenselization_iUnion_finiteEtale · existsUnique_ringHom_to_henselian_of_etale · HenselianLocalRing.indEtaleAlgHom · HenselianLocalRing.isLocalHom_indEtaleAlgHom

Section10.156 Henselization and quasi-finite ring maps#

Section 10.156 of the Stacks Project, Tag 0GIN. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05WP, a lemma

Tag 05WP in the Stacks Project.

IsLocalRing.IsHenselization.isLocalization_and_finite_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/QuasiFiniteRingMaps.lean, line 219. The attribute's comment: “The square of Lemma 04GS is the algebra structure algebraMap Rh Sh, local and compatible with R_p → S_q → S_q^h — conditions which by Lemma 04GS determine it — and the tensor product is any Algebra.IsPushout Rp Sq Rh T, whose map to S_q^h is the algebra structure algebraMap T Sh compatible with Rh and S_q. The prime generated by q is 𝔪_{S_q} T. Quasi-finiteness at q is Algebra.FiniteType R S with Algebra.QuasiFiniteAt R q, as in Lemma 04GH. See the module docstring.”.

Henselization and quasi-finite ring maps (Stacks 05WP). Let R → S be of finite type, let q be a prime of S lying over p, and assume R → S is quasi-finite at q. Let Rh and Sh be henselizations of R_p and S_q, let Rh → Sh be the local ring map over R_p → S_q of Lemma 04GS, and let T = Rh ⊗_{R_p} S_q, mapping to Sh through the square. Then the ideal 𝔪_{S_q} T generated by q is prime, Sh is the localization of T at it, and Sh is finite over Rh.

theorem isLocalization_and_finite_of_quasiFiniteAt
    [Algebra.FiniteType R S] [Algebra.QuasiFiniteAt R q] :
    ∃ _ : ((maximalIdeal Sq).map (algebraMap Sq T)).IsPrime,
      IsLocalization.AtPrime Sh ((maximalIdeal Sq).map (algebraMap Sq T)) ∧
        Module.Finite Rh Sh

Tag 05WQ, a lemma

Tag 05WQ in the Stacks Project.

IsLocalRing.henselization_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/HenselizationQuotient.lean, line 260. The attribute's comment: “"Rh is the henselization of R" is the four-item package of Lemma 04GN, in the spelling of IsLocalRing.exists_henselization, both as hypothesis and as conclusion; I R^h is I.map (algebraMap R Rh), and the R/I-algebra structure on Rh/I Rh is the induced one, Ideal.Quotient.algebraQuotientOfLEComap Ideal.le_comap_map. See the module docstring.”.

Henselization is compatible with quotients (Stacks 05WQ). Let (R, 𝔪, κ) be a local ring and let R → Rh be a henselization of R, that is: Rh is a henselian local ring, it is a filtered colimit of étale R-algebras, 𝔪 Rh is its maximal ideal, and its residue field is κ. Let I ⊆ 𝔪 be an ideal. Then Rh/I Rh is a henselization of R/I, for the induced R/I-algebra structure: it is a henselian local ring, it is a filtered colimit of étale R/I-algebras, the ideal generated by the image of 𝔪/I is its maximal ideal, and its residue field is again κ.

public theorem IsLocalRing.henselization_quotient {R Rh : Type u} [CommRing R] [CommRing Rh]
    [IsLocalRing R] [Algebra R Rh] [HenselianLocalRing Rh] [IsLocalHom (algebraMap R Rh)]
    (hind : (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R Rh))
    (hmax : (maximalIdeal R).map (algebraMap R Rh) = maximalIdeal Rh)
    (hres : Function.Bijective (ResidueField.map (algebraMap R Rh)))
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    letI : Algebra (R ⧸ I) (Rh ⧸ I.map (algebraMap R Rh)) :=
      Ideal.Quotient.algebraQuotientOfLEComap Ideal.le_comap_map
    ∃ (_ : IsLocalRing (R ⧸ I)) (_ : IsLocalRing (Rh ⧸ I.map (algebraMap R Rh)))
        (_ : IsLocalHom (algebraMap (R ⧸ I) (Rh ⧸ I.map (algebraMap R Rh)))),
      HenselianLocalRing (Rh ⧸ I.map (algebraMap R Rh)) ∧
      (CommAlgCat.etale.{u} (R ⧸ I)).ind.{u}
        (CommAlgCat.of (R ⧸ I) (Rh ⧸ I.map (algebraMap R Rh))) ∧
      (maximalIdeal (R ⧸ I)).map (algebraMap (R ⧸ I) (Rh ⧸ I.map (algebraMap R Rh))) =
        maximalIdeal (Rh ⧸ I.map (algebraMap R Rh)) ∧
      Function.Bijective
        (ResidueField.map (algebraMap (R ⧸ I) (Rh ⧸ I.map (algebraMap R Rh))))

Tag 05WR, a lemma

Tag 05WR in the Stacks Project.

Algebra.IsPushout.strictHenselization_and_finite_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/QuasiFinite.lean, line 556. The attribute's comment: “Stated as the construction of S_q^{sh}: Ssh is the localization of the base change T at the prime ker π, and the conclusion is that it is a strict henselization of S_q — the items of Lemma 04GP, as in Lemmas 05WP and 05WS — with residue field κ₂, finite and local over R_p^{sh}, and that κ₂/κ₁ is finite purely inseparable. With the uniqueness of Lemma 08HT, which the source's proof invokes here too, this is the source's identification of S_q^{sh} with that localization; the top arrow of the source's square is algebraMap Rsh Ssh. κ₁ is ResidueField Rsh, and that its image in κ₂ is the separable subfield of Lemma 030K is a consequence, not a hypothesis. See the module docstring.”.

The strict henselization of S_q for a quasi-finite ring map (Stacks 05WR). Let R → S be of finite type, let q be a prime of S lying over p at which R → S is quasi-finite, and let Rp, Sq be the localizations. Let Rsh be a strict henselization of Rp: henselian, ind-étale over Rp, with maximal ideal generated by 𝔪_{R_p} and residue field κ₁ a separable algebraic closure of κ(p). Let κ₂ be a separable algebraic closure of κ(q) containing κ₁, let T be the base change Rsh ⊗_{Rp} Sq and let π : T → κ₂ be the map induced by Rsh → κ₁ → κ₂ and Sq → κ(q) → κ₂. Let Ssh be the localization of T at the prime ker π. Then Ssh is finite over Rsh by a local ring map, Sq → Ssh is a strict henselization of Sq whose residue field is κ₂, and κ₂/κ₁ is finite and purely inseparable.

theorem Algebra.IsPushout.strictHenselization_and_finite_of_quasiFiniteAt
    {R S Rp Sq Rsh T Ssh κ₂ : Type u}
    [CommRing R] [CommRing S] [CommRing Rp] [CommRing Sq] [CommRing Rsh] [CommRing T]
    [CommRing Ssh] [Field κ₂] [Algebra R S]
    (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p]
    [Algebra.FiniteType R S] [Algebra.QuasiFiniteAt R q]
    [Algebra R Rp] [IsLocalRing Rp] [IsLocalization.AtPrime Rp p]
    [Algebra S Sq] [IsLocalRing Sq] [IsLocalization.AtPrime Sq q]
    [Algebra R Sq] [Algebra Rp Sq] [IsScalarTower R S Sq] [IsScalarTower R Rp Sq]
    [Algebra Rp Rsh] [HenselianLocalRing Rsh] [IsLocalHom (algebraMap Rp Rsh)]
    [IsSepClosure (ResidueField Rp) (ResidueField Rsh)]
    (hind : (CommAlgCat.etale.{u} Rp).ind.{u} (CommAlgCat.of Rp Rsh))
    (hmax : (maximalIdeal Rp).map (algebraMap Rp Rsh) = maximalIdeal Rsh)
    [Algebra (ResidueField Sq) κ₂] [IsSepClosure (ResidueField Sq) κ₂]
    [Algebra (ResidueField Rsh) κ₂]
    [Algebra Rp T] [Algebra Rsh T] [Algebra Sq T]
    [IsScalarTower Rp Rsh T] [IsScalarTower Rp Sq T]
    (hT : Algebra.IsPushout Rp Sq Rsh T)
    (π : T →+* κ₂)
    (hπRsh : π.comp (algebraMap Rsh T) = (algebraMap (ResidueField Rsh) κ₂).comp (residue Rsh))
    (hπSq : π.comp (algebraMap Sq T) = (algebraMap (ResidueField Sq) κ₂).comp (residue Sq))
    [(RingHom.ker π).IsPrime]
    [Algebra T Ssh] [IsLocalRing Ssh] [IsLocalization.AtPrime Ssh (RingHom.ker π)]
    [Algebra Sq Ssh] [Algebra Rsh Ssh] [IsScalarTower Sq T Ssh] [IsScalarTower Rsh T Ssh] :
    ∃ _ : IsLocalHom (algebraMap Sq Ssh),
      Module.Finite Rsh Ssh ∧ IsLocalHom (algebraMap Rsh Ssh) ∧ HenselianLocalRing Ssh ∧
        (CommAlgCat.etale.{u} Sq).ind.{u} (CommAlgCat.of Sq Ssh) ∧
        (maximalIdeal Sq).map (algebraMap Sq Ssh) = maximalIdeal Ssh ∧
        IsSepClosure (ResidueField Sq) (ResidueField Ssh) ∧
        (∃ e : ResidueField Ssh ≃+* κ₂,
          (e : ResidueField Ssh →+* κ₂).comp ((residue Ssh).comp (algebraMap T Ssh)) = π) ∧
        Module.Finite (ResidueField Rsh) κ₂ ∧ IsPurelyInseparable (ResidueField Rsh) κ₂

Tag 05WS, a lemma

Tag 05WS in the Stacks Project.

IsLocalRing.strictHenselization_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/StrictHenselization/Quotient.lean, line 319. The attribute's comment: “"Rsh is a strict henselization of R" is the package of Lemma 04GP, in the shape IsLocalRing.exists_henselization (04GN) gives the henselization package, both as hypothesis and as conclusion; IsSepClosure κ κ_sh is items (2) and (5) together. I R^{sh} is I.map (algebraMap R Rsh), and the R/I-algebra structure on Rsh/I Rsh is Mathlib's induced one. See the module docstring.”.

Strict henselization is compatible with quotients (Stacks 05WS). Let (R, 𝔪, κ) be a local ring and let R → Rsh be a strict henselization of R, that is: Rsh is a henselian local ring whose residue field is a separable algebraic closure κ^{sep} of κ, it is a filtered colimit of étale R-algebras, and 𝔪 Rsh is its maximal ideal. Let I ⊆ 𝔪 be an ideal. Then Rsh/I Rsh is a strict henselization of R/I, for the induced R/I-algebra structure: it is a henselian local ring, it is a filtered colimit of étale R/I-algebras, the ideal generated by the image of 𝔪/I is its maximal ideal, and its residue field is again a separable algebraic closure of κ.

public theorem IsLocalRing.strictHenselization_quotient {R Rsh : Type u} [CommRing R]
    [CommRing Rsh] [IsLocalRing R] [Algebra R Rsh] [HenselianLocalRing Rsh]
    [IsLocalHom (algebraMap R Rsh)] [IsSepClosure (ResidueField R) (ResidueField Rsh)]
    (hind : (CommAlgCat.etale.{u} R).ind.{u} (CommAlgCat.of R Rsh))
    (hmax : (maximalIdeal R).map (algebraMap R Rsh) = maximalIdeal Rsh)
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    ∃ (_ : IsLocalRing (R ⧸ I)) (_ : IsLocalRing (Rsh ⧸ I.map (algebraMap R Rsh)))
        (_ : IsLocalHom (algebraMap (R ⧸ I) (Rsh ⧸ I.map (algebraMap R Rsh)))),
      HenselianLocalRing (Rsh ⧸ I.map (algebraMap R Rsh)) ∧
      (CommAlgCat.etale.{u} (R ⧸ I)).ind.{u}
        (CommAlgCat.of (R ⧸ I) (Rsh ⧸ I.map (algebraMap R Rsh))) ∧
      (maximalIdeal (R ⧸ I)).map (algebraMap (R ⧸ I) (Rsh ⧸ I.map (algebraMap R Rsh))) =
        maximalIdeal (Rsh ⧸ I.map (algebraMap R Rsh)) ∧
      IsSepClosure (ResidueField (R ⧸ I))
        (ResidueField (Rsh ⧸ I.map (algebraMap R Rsh)))

Tag 092Y, a lemma

Tag 092Y in the Stacks Project.

isLocalRing_tensorProduct_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorProduct/LocalAlgebra.lean, line 497. References: EGA 0 (22.5.5), “partial”.

Stacks Tag 092Y. Let A → B and A → C be local homomorphisms of local rings, with A → C integral and at least one of the induced residue field extensions κ(m_C)/κ(m_A), κ(m_B)/κ(m_A) purely inseparable. Then D = B ⊗_A C is a local ring and the canonical maps B → D, C → D are local homomorphisms.

theorem isLocalRing_tensorProduct_of_isIntegral
    (A B C : Type*) [CommRing A] [CommRing B] [CommRing C]
    [IsLocalRing A] [IsLocalRing B] [IsLocalRing C]
    [Algebra A B] [Algebra A C]
    [IsLocalHom (algebraMap A B)] [IsLocalHom (algebraMap A C)]
    [Algebra.IsIntegral A C]
    (hins :
      @IsPurelyInseparable (ResidueField A) (ResidueField C) _ _
        (IsLocalRing.ResidueField.map (algebraMap A C)).toAlgebra ∨
      @IsPurelyInseparable (ResidueField A) (ResidueField B) _ _
        (IsLocalRing.ResidueField.map (algebraMap A B)).toAlgebra) :
    IsLocalRing (TensorProduct A B C) ∧
      IsLocalHom (Algebra.TensorProduct.includeLeftRingHom : B →+* TensorProduct A B C) ∧
      IsLocalHom ((Algebra.TensorProduct.includeRight : C →ₐ[A] TensorProduct A B
          C).toRingHom)

Tag 0GIP, a lemma

Tag 0GIP in the Stacks Project.

IsLocalRing.IsHenselization.bijective_tensorProduct_lift_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/QuasiFiniteRingMaps.lean, line 1132. The attribute's comment: “(1). The field κ is replaced by the prime P = ker(D → κ) of D: the statement is proved for all strict henselizations A^sh, B^sh, C^sh, D^sh of the localizations at the contractions of P and all local maps between them forming a commutative square over A → B, C → D, which includes the maps of Lemma 04GU attached to the embeddings of the residue fields in κ. The isomorphism is the bijectivity of Algebra.TensorProduct.lift of the two maps into D^sh, and D = B ⊗_A C is any Algebra.IsPushout A B C D. Quasi-finiteness at P ∩ B is Algebra.FiniteType A B with Algebra.QuasiFiniteAt A (P.under B), as in Lemma 04GH. See the module docstring.”.

Strict henselization and tensor products, quasi-finite case (Stacks 0GIP (1)). Let D = B ⊗_A C and let P be a prime of D, with contractions to A, B, C. Let A^sh, B^sh, C^sh, D^sh be strict henselizations of the localizations of A, B, C, D at these primes, with local ring maps forming a commutative square over the square A → B, C → D. If A → B is of finite type and quasi-finite at P ∩ B, then B^sh ⊗_{A^sh} C^sh → D^sh is an isomorphism.

theorem bijective_tensorProduct_lift_of_quasiFiniteAt
    {Ap : Type u} [CommRing Ap] [IsLocalRing Ap] [Algebra A Ap]
    [IsLocalization.AtPrime Ap (P.under A)]
    [Algebra Ap Ash] [IsScalarTower A Ap Ash] [IsLocalHom (algebraMap Ap Ash)]
    [IsSepClosure (ResidueField Ap) (ResidueField Ash)] [IsHenselization Ap (ResidueField Ash) Ash]
    [IsSepClosure (ResidueField Bp) (ResidueField Bsh)]
    [IsLocalHom (algebraMap Ash Bsh)] [IsLocalHom (algebraMap Ash Csh)]
    [IsLocalHom (algebraMap Csh Dsh)]
    [Algebra.FiniteType A B] [Algebra.QuasiFiniteAt A (P.under B)] :
    Function.Bijective (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom Ash Bsh Dsh)
      (IsScalarTower.toAlgHom Ash Csh Dsh) fun _ _ => .all _ _)

IsLocalRing.IsHenselization.bijective_tensorProduct_lift_of_ind_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/QuasiFiniteRingMaps.lean, line 1215. The attribute's comment: “(2). The field κ is replaced by the prime P = ker(D → κ) of D: the statement is proved for all strict henselizations A^sh, B^sh, C^sh, D^sh of the localizations at the contractions of P and all local maps between them forming a commutative square over A → B, C → D, which includes the maps of Lemma 04GU attached to the embeddings of the residue fields in κ. The isomorphism is the bijectivity of Algebra.TensorProduct.lift of the two maps into D^sh, and D = B ⊗_A C is any Algebra.IsPushout A B C D. "Filtered colimit of quasi-finite A-algebras" is ObjectProperty.ind in CommAlgCat A of Algebra.FiniteType A X ∧ Algebra.QuasiFinite A X. See the module docstring.”.

Strict henselization and tensor products, colimit case (Stacks 0GIP (2)). In the situation of Lemma 0GIP, if B is a filtered colimit of quasi-finite A-algebras, then B^sh ⊗_{A^sh} C^sh → D^sh is an isomorphism.

theorem bijective_tensorProduct_lift_of_ind_quasiFinite
    {Ap : Type u} [CommRing Ap] [IsLocalRing Ap] [Algebra A Ap]
    [IsLocalization.AtPrime Ap (P.under A)]
    [Algebra Ap Ash] [IsScalarTower A Ap Ash] [IsLocalHom (algebraMap Ap Ash)]
    [IsSepClosure (ResidueField Ap) (ResidueField Ash)] [IsHenselization Ap (ResidueField Ash) Ash]
    [IsSepClosure (ResidueField Bp) (ResidueField Bsh)]
    [IsLocalHom (algebraMap Ash Bsh)] [IsLocalHom (algebraMap Ash Csh)]
    [IsLocalHom (algebraMap Csh Dsh)]
    (hB : (ObjectProperty.ind.{u} fun X : CommAlgCat.{u} A =>
      Algebra.FiniteType A X ∧ Algebra.QuasiFinite A X) (CommAlgCat.of A B)) :
    Function.Bijective (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom Ash Bsh Dsh)
      (IsScalarTower.toAlgHom Ash Csh Dsh) fun _ _ => .all _ _)

IsLocalRing.IsHenselization.bijective_tensorProduct_lift_of_ind_quasiFinite_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/QuasiFiniteRingMaps.lean, line 1244. The attribute's comment: “(3). The field κ is replaced by the prime P = ker(D → κ) of D: the statement is proved for all strict henselizations A^sh, B^sh, C^sh, D^sh of the localizations at the contractions of P and all local maps between them forming a commutative square over A → B, C → D, which includes the maps of Lemma 04GU attached to the embeddings of the residue fields in κ. The isomorphism is the bijectivity of Algebra.TensorProduct.lift of the two maps into D^sh, and D = B ⊗_A C is any Algebra.IsPushout A B C D. The filtered colimit is ObjectProperty.ind in CommAlgCat A_p of Algebra.FiniteType ∧ Algebra.QuasiFinite, for the given A_p-algebra structure on B_p over A → B. See the module docstring.”.

Strict henselization and tensor products, local colimit case (Stacks 0GIP (3)). In the situation of Lemma 0GIP, if B_{P ∩ B} is a filtered colimit of quasi-finite algebras over A_{P ∩ A}, then B^sh ⊗_{A^sh} C^sh → D^sh is an isomorphism.

theorem bijective_tensorProduct_lift_of_ind_quasiFinite_localization
    {Ap : Type u} [CommRing Ap] [IsLocalRing Ap] [Algebra A Ap]
    [IsLocalization.AtPrime Ap (P.under A)]
    [Algebra Ap Ash] [IsScalarTower A Ap Ash] [IsLocalHom (algebraMap Ap Ash)]
    [IsSepClosure (ResidueField Ap) (ResidueField Ash)] [IsHenselization Ap (ResidueField Ash) Ash]
    [IsSepClosure (ResidueField Bp) (ResidueField Bsh)]
    [IsLocalHom (algebraMap Ash Bsh)] [IsLocalHom (algebraMap Ash Csh)]
    [IsLocalHom (algebraMap Csh Dsh)]
    [Algebra Ap Bp] [Algebra A Bp] [IsScalarTower A Ap Bp] [IsScalarTower A B Bp]
    (hB : (ObjectProperty.ind.{u} fun X : CommAlgCat.{u} Ap =>
      Algebra.FiniteType Ap X ∧ Algebra.QuasiFinite Ap X) (CommAlgCat.of Ap Bp)) :
    Function.Bijective (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom Ash Bsh Dsh)
      (IsScalarTower.toAlgHom Ash Csh Dsh) fun _ _ => .all _ _)

IsLocalRing.IsHenselization.bijective_tensorProduct_lift_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/QuasiFiniteRingMaps.lean, line 1345. The attribute's comment: “(4). The field κ is replaced by the prime P = ker(D → κ) of D: the statement is proved for all strict henselizations A^sh, B^sh, C^sh, D^sh of the localizations at the contractions of P and all local maps between them forming a commutative square over A → B, C → D, which includes the maps of Lemma 04GU attached to the embeddings of the residue fields in κ. The isomorphism is the bijectivity of Algebra.TensorProduct.lift of the two maps into D^sh, and D = B ⊗_A C is any Algebra.IsPushout A B C D. See the module docstring.”.

Strict henselization and tensor products, integral case (Stacks 0GIP (4)). In the situation of Lemma 0GIP, if B is integral over A, then B^sh ⊗_{A^sh} C^sh → D^sh is an isomorphism.

theorem bijective_tensorProduct_lift_of_isIntegral
    {Ap : Type u} [CommRing Ap] [IsLocalRing Ap] [Algebra A Ap]
    [IsLocalization.AtPrime Ap (P.under A)]
    [Algebra Ap Ash] [IsScalarTower A Ap Ash] [IsLocalHom (algebraMap Ap Ash)]
    [IsSepClosure (ResidueField Ap) (ResidueField Ash)] [IsHenselization Ap (ResidueField Ash) Ash]
    [IsSepClosure (ResidueField Bp) (ResidueField Bsh)]
    [IsLocalHom (algebraMap Ash Bsh)] [IsLocalHom (algebraMap Ash Csh)]
    [IsLocalHom (algebraMap Csh Dsh)] [Algebra.IsIntegral A B] :
    Function.Bijective (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom Ash Bsh Dsh)
      (IsScalarTower.toAlgHom Ash Csh Dsh) fun _ _ => .all _ _)

Sources

• Section 10.156, Tag 0GIN
• AxiomMath/Stacks at 5ed82d14

LeanIsLocalRing.IsHenselization.isLocalization_and_finite_of_quasiFiniteAt · IsLocalRing.henselization_quotient · Algebra.IsPushout.strictHenselization_and_finite_of_quasiFiniteAt · IsLocalRing.strictHenselization_quotient · isLocalRing_tensorProduct_of_isIntegral · IsLocalRing.IsHenselization.bijective_tensorProduct_lift_of_quasiFiniteAt · IsLocalRing.IsHenselization.bijective_tensorProduct_lift_of_ind_quasiFinite · IsLocalRing.IsHenselization.bijective_tensorProduct_lift_of_ind_quasiFinite_localization

Section10.157 Serre's criterion for normality#

Section 10.157 of the Stacks Project, Tag 031O. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 031P, a definition

Tag 031P in the Stacks Project.

HasPropertyRk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/Defs.lean, line 104. The attribute's comment: “Rk”. References: EGA IV (5.8.2), “affine case”; EGA IV (7.5.3), “partial”.

Property (Rₖ): every prime 𝔭 of A of height at most k has regular localization A_𝔭. As height 𝔭 = dim A_𝔭, this is regularity of A in codimension at most k.

def HasPropertyRk (A : Type*) [CommRing A] (k : ℕ) : Prop

PropertySkRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/Defs.lean, line 113. The attribute's comment: “Sk ring”. References: EGA IV (5.7.2), “special case”; EGA IV (5.7.3), “special case”; EGA IV (7.5.3).

Property (Sₖ) for a Noetherian commutative ring R: at every prime 𝔭 the depth of the localization R_𝔭 is at least min(k, dim R_𝔭).

def PropertySkRing (R : Type*) [CommRing R] [IsNoetherianRing R] (k : ℕ) : Prop

PropertySkModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/Defs.lean, line 124. The attribute's comment: “Sk module”. References: EGA IV (5.7.2), “special case”; EGA IV (5.7.3); EGA IV (7.5.3), “more general”.

Property (Sₖ) for a finite module M over a Noetherian commutative ring R: at every prime 𝔭 the depth of the localization M_𝔭 is at least min(k, dim Supp(M_𝔭)).

def PropertySkModule (R : Type*) [CommRing R] [IsNoetherianRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] (k : ℕ) : Prop

propertySkRing_of_ringEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/RingEquiv.lean, line 71. The attribute's comment: “Sk ring, isomorphism invariance”.

Serre's condition (Sₖ) is invariant under an isomorphism of rings. A prime of the target pulls back along the isomorphism, Localization.localRingEquiv identifies the two localizations, and both the Krull dimension and the depth are invariant under that isomorphism.

public theorem propertySkRing_of_ringEquiv {A : Type u} {B : Type v}
    [CommRing A] [CommRing B] [IsNoetherianRing A] [IsNoetherianRing B]
    (e : A ≃+* B) (k : ℕ) (h : PropertySkRing A k) : PropertySkRing B k

Tag 031Q, a lemma

Tag 031Q in the Stacks Project.

Module.forall_minimal_mem_associatedPrimes_iff_min_one_supportDim_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/Defs.lean, line 356. The attribute's comment: “Property (S₁) is spelled out as the inequality min{1, dim Supp(M_𝔭)} ≤ depth_{𝔭R_𝔭}(M_𝔭) of Definition 031P at k = 1 rather than as PropertySkModule R M 1, whose depth and dimension truncate the conventions this statement needs; having no embedded associated prime is spelled out with Minimal, as in tag 02M6; and the localizations are the canonical models Localization.AtPrime and LocalizedModule, indexed by PrimeSpectrum R as in Definition 0AAH. See the module docstring.”.

Let R be a Noetherian ring and let M be a finite R-module. Then M has no embedded associated prime — that is, every associated prime of M is minimal among the associated primes of M — if and only if M has property (S₁): for every prime 𝔭 of R the depth of the R_𝔭-module M_𝔭 along 𝔭R_𝔭 is at least min{1, dim Supp(M_𝔭)}, the inequality being read in WithBot ℕ∞. Concretely the right-hand side says that depth(M_𝔭) ≥ 1 at every prime 𝔭 with dim Supp(M_𝔭) ≥ 1.

public theorem forall_minimal_mem_associatedPrimes_iff_min_one_supportDim_le_depth
    {R : Type*} [CommRing R] [IsNoetherianRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    (∀ p ∈ associatedPrimes R M, Minimal (· ∈ associatedPrimes R M) p) ↔
      ∀ p : PrimeSpectrum R,
        min 1 (supportDim (Localization.AtPrime p.asIdeal)
            (LocalizedModule p.asIdeal.primeCompl M)) ≤
          (depth (Localization.AtPrime p.asIdeal)
            (IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl M) : WithBot ℕ∞)

Tag 031R, a lemma

Tag 031R in the Stacks Project.

isReduced_iff_hasR0_and_hasS1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/Reduced.lean, line 405. References: EGA IV (12.1.8), “more general”; EGA IV (3.2.1), “a), special case”; EGA IV (5.8.5), “special case”; EGA IV (7.3.9), “(i), special case”.

Stacks Tag 031R (Lemma 10.157.3, Serre's criterion). A Noetherian ring R is reduced if and only if it has both property (R_0) and property (S_1).

theorem isReduced_iff_hasR0_and_hasS1 (R : Type*) [CommRing R] [IsNoetherianRing R] :
    IsReduced R ↔ HasR0 R ∧ HasS1 R

Tag 031S, a lemma

Tag 031S in the Stacks Project.

isDomain_and_isIntegrallyClosed_atPrime_iff_isRegularLocalRing_and_min_two_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/Criterion.lean, line 886. The attribute's comment: “Normality is inlined as IsDomain plus IsIntegrallyClosed on Localization.AtPrime 𝔭 for every prime 𝔭, as in item (1) of tag 030C, Mathlib having no predicate for a normal ring; properties (R_1) and (S_2) are spelled out from Definition 031P at k = 1 and k = 2 with Ideal.height, IsRegularLocalRing, ringKrullDim and Module.depth (tag 00LI), the depth inequality being read in WithBot ℕ∞. See the module docstring.”. References: EGA IV (5.8.6), “affine case”; SGA 2 XI (3.11), “more general”.

Stacks Tag 031S (Serre's criterion for normality). Let R be a Noetherian ring. Then R is a normal ring — every localization R_𝔭 at a prime is a domain integrally closed in its fraction field — if and only if R has properties (R_1) and (S_2): the local ring R_𝔭 is regular for every prime 𝔭 of height ≤ 1, and depth(R_𝔭) ≥ min{2, dim(R_𝔭)} for every prime 𝔭, the latter inequality being read in WithBot ℕ∞.

public theorem isDomain_and_isIntegrallyClosed_atPrime_iff_isRegularLocalRing_and_min_two_le_depth
    {R : Type*} [CommRing R] [IsNoetherianRing R] :
    (∀ (p : Ideal R) [p.IsPrime],
        IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) ↔
      (∀ (p : Ideal R) [p.IsPrime], p.height ≤ 1 →
          IsRegularLocalRing (Localization.AtPrime p)) ∧
        ∀ (p : Ideal R) [p.IsPrime],
          min 2 (ringKrullDim (Localization.AtPrime p)) ≤
            (Module.depth (Localization.AtPrime p)
              (IsLocalRing.maximalIdeal (Localization.AtPrime p))
              (Localization.AtPrime p) : WithBot ℕ∞)

Tag 0567, a lemma

Tag 0567 in the Stacks Project.

main_theorem0567, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/Stability.lean, line 64. References: EGA II (7.1.6), “more general”; EGA IV (6.13.1), “special case”; EGA IV (7.3.9), “(i): (iv) implies (vii)”.

A regular ring is normal.

theorem main_theorem0567 (R : Type*) [CommRing R] [IsRegularRing R] :
    IsNormalRing R

Tag 031T, a lemma

Tag 031T in the Stacks Project.

associatedPrimes_minimal_and_height_eq_one_and_iInf_localization_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/Defs.lean, line 552. The attribute's comment: “A normal domain is IsDomain plus IsIntegrallyClosed, as in Definition 0309; having no embedded primes is spelled with Minimal, as in tags 02M6 and 031Q; item (2) is the equality ⨅ 𝔭, R_𝔭 = ⊥ of R-subalgebras of K, as in IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot; and R ∩ xR is the pullback of xR ⊆ K along Algebra.linearMap R K. See the module docstring.”. References: EGA 0 (23.2.9), “A normal (A = A')”; EGA IV (7.8.3), “(viii), special case”.

Let R be a Noetherian normal domain with fraction field K. Then (1) for every nonzero a : R each associated prime of R/aR is minimal among the associated primes of R/aR — that is, R/aR has no embedded primes — and has height 1; (2) R is the intersection, inside K, of the subalgebras R_𝔭 over the primes 𝔭 of height 1; and (3) the same as (1) for the ideal R ∩ xR attached to a nonzero x : K.

public theorem associatedPrimes_minimal_and_height_eq_one_and_iInf_localization_eq_bot
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K] :
    (∀ a : R, a ≠ 0 → ∀ p ∈ associatedPrimes R (R ⧸ Ideal.span {a}),
        Minimal (· ∈ associatedPrimes R (R ⧸ Ideal.span {a})) p ∧ p.height = 1) ∧
      ((⨅ p : PrimeSpectrum R, ⨅ _ : p.asIdeal.height = 1,
          Localization.subalgebra.ofField K _ p.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥) ∧
      (∀ x : K, x ≠ 0 →
        ∀ p ∈ associatedPrimes R
            (R ⧸ ((Submodule.span R {x}).comap (Algebra.linearMap R K) : Ideal R)),
          Minimal (· ∈ associatedPrimes R
              (R ⧸ ((Submodule.span R {x}).comap (Algebra.linearMap R K) : Ideal R))) p ∧
            p.height = 1)

Sources

• Section 10.157, Tag 031O
• AxiomMath/Stacks at 5ed82d14

LeanHasPropertyRk · PropertySkRing · PropertySkModule · propertySkRing_of_ringEquiv · Module.forall_minimal_mem_associatedPrimes_iff_min_one_supportDim_le_depth · isReduced_iff_hasR0_and_hasS1 · isDomain_and_isIntegrallyClosed_atPrime_iff_isRegularLocalRing_and_min_two_le_depth · main_theorem0567

Section10.158 Formal smoothness of fields#

Section 10.158 of the Stacks Project, Tag 031U. 11 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 090W, a lemma

Tag 090W in the Stacks Project.

Algebra.FormallyUnramified.tfae_isSeparable_unramified_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Field.lean, line 244. The attribute's comment: “The six items are the entries, in the source's order, of one List.TFAE. A finitely generated field extension is Algebra.EssFiniteType, Ω[K⁄k] = 0 is Subsingleton Ω[K⁄k], and étale is Mathlib's formally étale plus finite presentation, which is the source's Definition 00U1 by its Lemma 00UR. See the module docstring.”. References: EGA 0 (21.7.4), “more general”; EGA 0 (19.10.3), “(iii)”; EGA IV (17.4.2), “field extension K/k”; EGA IV (17.4.1), “field extension case”; EGA IV (17.15.11), “X = Spec of a field”; EGA 0 (21.7.4), “more general”; SGA 1 I (3.1), “(i)<=>(ii), field ext”; SGA 3 XI (1.3), “field extension case”.

Stacks 090W. Let K/k be a finitely generated field extension. The following are equivalent:

1. K is a finite separable field extension of k;
2. Ω[K⁄k] = 0;
3. K is formally unramified over k;
4. K is unramified over k;
5. K is formally étale over k;
6. K is étale over k.

public theorem Algebra.FormallyUnramified.tfae_isSeparable_unramified_etale
    (k K : Type*) [Field k] [Field K] [Algebra k K] [Algebra.EssFiniteType k K] :
    List.TFAE
      [Module.Finite k K ∧ Algebra.IsSeparable k K,
       Subsingleton Ω[K⁄k],
       Algebra.FormallyUnramified k K,
       Algebra.Unramified k K,
       Algebra.FormallyEtale k K,
       Algebra.Etale k K]

Tag 031W, a lemma

Tag 031W in the Stacks Project.

KaehlerDifferential.D_eq_zero_iff_exists_pow_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/PerfectField.lean, line 237. The attribute's comment: “The source's d a = 0 in Ω_{K/k} is KaehlerDifferential.D k K a = 0 and a is a p-th power is ∃ b, b ^ p = a; characteristic p > 0 is [Fact p.Prime] [CharP k p] on the base. See the module docstring.”. References: EGA 0 (21.4.4), “more general”; EGA 0 (21.4.6), “(a) ⇔ (b), special case”.

Vanishing differentials over a perfect field are p-th powers. Let k be a perfect field of characteristic p > 0, let K/k be a field extension and let a : K. Then d a = 0 in Ω[K⁄k] if and only if a is a p-th power in K. Equivalently, the kernel of the universal k-derivation d : K → Ω[K⁄k] is the subfield of p-th powers of K.

public theorem KaehlerDifferential.D_eq_zero_iff_exists_pow_eq {k K : Type*} [Field k] [Field K]
    [Algebra k K] [PerfectField k] (p : ℕ) [Fact p.Prime] [CharP k p] (a : K) :
    KaehlerDifferential.D k K a = 0 ↔ ∃ b : K, b ^ p = a

Tag 07DZ, a lemma

Tag 07DZ in the Stacks Project.

IntermediateField.finrank_adjoin_eq_pow_of_linearIndependent_D, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/PthRoots.lean, line 196. The attribute's comment: “The source's Ω_{k/𝔽_p} is Ω[k⁄ZMod p], characteristic p > 0 is [Fact p.Prime] [Algebra (ZMod p) k], and k(a_1^{1/p}, …, a_n^{1/p}) is IntermediateField.adjoin k (Set.range b) for a family b of p-th roots in an ambient extension K/k, which is unique since Frobenius is injective. See the module docstring.”.

Adjoining p-th roots of elements with independent differentials. Let k be a field of characteristic p > 0 and let a : ι → k be a finite family such that the differentials d aᵢ are linearly independent in Ω[k⁄𝔽_p]. If b : ι → K is a family of p-th roots of the aᵢ in an extension field K/k, then the field extension k(a_1^{1/p}, …, a_n^{1/p}) = k(bᵢ : i) has degree p ^ #ι over k.

public theorem IntermediateField.finrank_adjoin_eq_pow_of_linearIndependent_D {k K : Type*}
    [Field k] [Field K] (p : ℕ) [Fact p.Prime] [Algebra (ZMod p) k] [Algebra k K] {ι : Type*}
    [Fintype ι] (a : ι → k) (b : ι → K) (hb : ∀ i, b i ^ p = algebraMap k K (a i))
    (h : LinearIndependent k fun i ↦ KaehlerDifferential.D (ZMod p) k (a i)) :
    Module.finrank k (IntermediateField.adjoin k (Set.range b)) = p ^ Fintype.card ι

Tag 031X, a lemma

Tag 031X in the Stacks Project.

Algebra.isSeparableExtension_iff_injective_mapBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/FieldTheory/KaehlerDifferential/Separable.lean, line 411. The attribute's comment: “Differentials are taken over 𝐙, which for a field of characteristic p is the source's 𝐅_p, and the characteristic hypothesis is dropped: both conditions hold outright in characteristic zero, and the consumers (Lemmas 031Y, 0321 and Proposition 0322) are stated for all characteristics. See the module docstring.”. References: EGA 0 (20.6.3).

A field extension K/k is separable in the sense of Algebra.IsSeparableExtension if and only if the canonical map K ⊗_k Ω_{k/𝐙} → Ω_{K/𝐙} is injective.

public theorem Algebra.isSeparableExtension_iff_injective_mapBaseChange (k K : Type*) [Field k]
    [Field K] [Algebra k K] :
    Algebra.IsSeparableExtension k K ↔
      Function.Injective (KaehlerDifferential.mapBaseChange ℤ k K)

Tag 031Y, a lemma

Tag 031Y in the Stacks Project.

Algebra.FormallySmooth.isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Field.lean, line 261. The attribute's comment: “Separability is Algebra.IsSeparableExtension (Definition 030O(2)), not Mathlib's Algebra.IsSeparable, which asks the extension to be algebraic and would make the statement false for purely transcendental extensions. See the module docstring.”. References: EGA 0 (19.6.1), “necessity”; EGA 0 (19.0.2), “necessity”.

Let K/k be an extension of fields. If K is formally smooth over k, then K is a separable extension of k: every subextension of K/k finitely generated over k has a separating transcendence basis.

public theorem Algebra.FormallySmooth.isSeparableExtension (k K : Type*) [Field k] [Field K]
    [Algebra k K] [Algebra.FormallySmooth k K] : Algebra.IsSeparableExtension k K

Tag 031Z, a lemma

Tag 031Z in the Stacks Project.

Algebra.formallySmooth_iff_subsingleton_h1Cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/FieldCotangent.lean, line 56. The attribute's comment: “Stated for a field K over an arbitrary commutative base ring R; the source's base field k is the case R := k, and no hypothesis on the base is used. H_1(L_{K/k}) = 0 is Subsingleton (Algebra.H1Cotangent R K). See the module docstring.”.

A field K which is an algebra over a commutative ring R is formally smooth over R if and only if H¹(L_{K/R}) = 0.

public theorem Algebra.formallySmooth_iff_subsingleton_h1Cotangent
    (R K : Type*) [CommRing R] [Field K] [Algebra R K] :
    Algebra.FormallySmooth R K ↔ Subsingleton (Algebra.H1Cotangent R K)

Tag 0320, a lemma

Tag 0320 in the Stacks Project.

Algebra.FormallySmooth.of_algebraicIndependent_and_of_isSeparable_and_of_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Field.lean, line 223. The attribute's comment: “The source's parts (1), (2), (3) are the conjuncts .1, .2.1, .2.2. Purely transcendental is AlgebraicIndependent together with IntermediateField.adjoin k s = ⊤, as in the Mathlib sibling Algebra.FormallySmooth.of_algebraicIndependent; separable algebraic is Algebra.IsSeparable; separable is Algebra.IsSeparableExtension, Definition 030O(2), which does not presuppose algebraicity. See the module docstring.”. References: EGA 0 (19.6.1), “sufficiency”; EGA 0 (21.5.1), “more general”; EGA 0 (21.5.1), “more general”; EGA 0 (19.0.2), “sufficiency”; EGA 0 (22.2.1), “special case”.

Let K/k be an extension of fields. Then K is formally smooth over k in each of the following three cases: (1) K is purely transcendental over k, that is, K is generated as an intermediate field by an algebraically independent set; (2) K is separable algebraic over k; (3) K is separable over k in the sense of Algebra.IsSeparableExtension.

public theorem
    Algebra.FormallySmooth.of_algebraicIndependent_and_of_isSeparable_and_of_isSeparableExtension
    (k K : Type*) [Field k] [Field K] [Algebra k K] :
    (∀ s : Set K, AlgebraicIndependent k ((↑) : s → K) → IntermediateField.adjoin k s = ⊤ →
        Algebra.FormallySmooth k K) ∧
      (Algebra.IsSeparable k K → Algebra.FormallySmooth k K) ∧
      (Algebra.IsSeparableExtension k K → Algebra.FormallySmooth k K)

Tag 0321, a lemma

Tag 0321 in the Stacks Project.

Algebra.FormallySmooth.iff_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Field.lean, line 294. The attribute's comment: “Separability is Algebra.IsSeparableExtension, Definition 030O (2), which does not presuppose algebraicity and so is not Algebra.IsSeparable; formal smoothness is Algebra.FormallySmooth, Definition 00TI. The characteristic split is dropped: both implications hold in every characteristic (the source's proof is combine Lemmas 031Y and 0320, neither of which mentions the characteristic), so part (2) is this equivalence and part (1) is it together with the characteristic-zero case of Lemma 030Z. See the module docstring.”. References: EGA 0 (19.6.1); EGA 0 (21.5.1), “more general”; EGA 0 (21.5.1), “more general”; EGA 0 (19.0.2).

A field extension K/k is formally smooth over k if and only if it is separable over k in the sense of Algebra.IsSeparableExtension.

public theorem Algebra.FormallySmooth.iff_isSeparableExtension (k K : Type*) [Field k] [Field K]
    [Algebra k K] : Algebra.FormallySmooth k K ↔ Algebra.IsSeparableExtension k K

Tag 0322, a proposition

Tag 0322 in the Stacks Project.

Algebra.isSeparableExtension_of_charZero_and_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Field.lean, line 509. The attribute's comment: “The equivalences are stated uniformly in the characteristic: k^{1/p} is AdjoinPthRoots k for the exponential characteristic, which in characteristic zero makes the second condition, hence all of them, automatic, and the source's characteristic-zero list is recovered. Differentials are taken over 𝐙 in both characteristics. See the module docstring.”. References: EGA 0 (20.6.3).

Let K/k be a field extension. If the characteristic of k is zero then K is separable over k; and, in any characteristic, the following are equivalent: K is separable over k, the ring K ⊗_k k^{1/p} is reduced for the exponential characteristic p of k, K is geometrically reduced over k, the map K ⊗_k Ω_{k/𝐙} → Ω_{K/𝐙} is injective, H_1(L_{K/k}) = 0, and K is formally smooth over k.

public theorem Algebra.isSeparableExtension_of_charZero_and_tfae (k K : Type*) [Field k] [Field K]
    [Algebra k K] :
    (CharZero k → Algebra.IsSeparableExtension k K) ∧
      List.TFAE
        [Algebra.IsSeparableExtension k K,
          IsReduced (K ⊗[k] AdjoinPthRoots k),
          Algebra.IsGeometricallyReduced k K,
          Function.Injective (KaehlerDifferential.mapBaseChange ℤ k K),
          Subsingleton (Algebra.H1Cotangent k K),
          Algebra.FormallySmooth k K]

Tag 037X, a lemma

Tag 037X in the Stacks Project.

Algebra.IsSeparableExtension.tfae_exists_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Field.lean, line 318. References: SGA 1 II (5.7), “partial”.

A finitely generated field extension is separable if and only if it is the localization of a smooth algebra. For a finitely generated field extension K/k the following are equivalent: K/k is separable; some smooth k-subalgebra of K has K as its fraction field; some smooth k-algebra has K as a localization.

public theorem Algebra.IsSeparableExtension.tfae_exists_smooth
    (k : Type*) (K : Type v) [Field k] [Field K] [Algebra k K] [Algebra.EssFiniteType k K] :
    List.TFAE
      [Algebra.IsSeparableExtension k K,
        ∃ R : Subalgebra k K, Algebra.Smooth k R ∧ IsFractionRing R K,
        ∃ (R : Type v) (_ : CommRing R) (_ : Algebra k R) (_ : Algebra R K)
          (_ : IsScalarTower k R K) (S : Submonoid R),
          Algebra.Smooth k R ∧ IsLocalization S K]

Tag 07BV, a lemma

Tag 07BV in the Stacks Project.

Subalgebra.directedOn_isGlobalCompleteIntersectionOver_and_exists_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/FieldExtensionCompleteIntersectionColimit.lean, line 472. The attribute's comment: “First part. The filtered colimit is the directed union of the global complete intersection k-subalgebras of K; see the module docstring.”.

Stacks 07BV, first part. Every field extension K/k is a filtered colimit of global complete intersection algebras over k: the k-subalgebras of K that are global complete intersections over k form a directed family whose union is K.

theorem Subalgebra.directedOn_isGlobalCompleteIntersectionOver_and_exists_mem
    (k K : Type*) [Field k] [Field K] [Algebra k K] :
    DirectedOn (· ≤ ·) {A : Subalgebra k K | IsGlobalCompleteIntersectionOver k A} ∧
      ∀ x : K, ∃ A ∈ {A : Subalgebra k K | IsGlobalCompleteIntersectionOver k A}, x ∈ A

Subalgebra.directedOn_smooth_and_exists_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/FieldExtensionCompleteIntersectionColimit.lean, line 484. The attribute's comment: “Second part. The filtered colimit is the directed union of the smooth k-subalgebras of K; see the module docstring.”.

Stacks 07BV, second part. A separable field extension K/k is a filtered colimit of smooth k-algebras: the smooth k-subalgebras of K form a directed family whose union is K.

theorem Subalgebra.directedOn_smooth_and_exists_mem
    (k K : Type*) [Field k] [Field K] [Algebra k K] [Algebra.IsSeparableExtension k K] :
    DirectedOn (· ≤ ·) {A : Subalgebra k K | Algebra.Smooth k A} ∧
      ∀ x : K, ∃ A ∈ {A : Subalgebra k K | Algebra.Smooth k A}, x ∈ A

Sources

• Section 10.158, Tag 031U
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.FormallyUnramified.tfae_isSeparable_unramified_etale · KaehlerDifferential.D_eq_zero_iff_exists_pow_eq · IntermediateField.finrank_adjoin_eq_pow_of_linearIndependent_D · Algebra.isSeparableExtension_iff_injective_mapBaseChange · Algebra.FormallySmooth.isSeparableExtension · Algebra.formallySmooth_iff_subsingleton_h1Cotangent · Algebra.FormallySmooth.of_algebraicIndependent_and_of_isSeparable_and_of_isSeparableExtension · Algebra.FormallySmooth.iff_isSeparableExtension

Section10.159 Constructing flat ring maps#

Section 10.159 of the Stacks Project, Tag 03C2. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03C3, a lemma

Tag 03C3 in the Stacks Project.

IsLocalRing.exists_flat_residueField_algEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FiniteFreeResidueExtension.lean, line 965. The attribute's comment: “The lemma's preamble, a local ring R' and a local ring map R → R', is the Algebra R R', IsLocalRing R' and IsLocalHom (algebraMap R R') binders; the conjuncts are flatness, 𝔪' = 𝔪 R' as Ideal.map, and k' ≅ K as an extension of k as an ≃ₐ[ResidueField R]. K is allowed to live in a universe of its own, the source's case being v = u. See the module docstring.”. References: EGA 0 (10.3.1), “flat local ext, k'≅K”; EGA III (4.3.4), “partial”; SGA 3 V (4.1.2), “first assertion”.

A residue field extension is realized by a flat local ring map (Stacks 03C3). Let (R, 𝔪, k) be a local ring and let K be a field extension of k. Then there is a local ring (R', 𝔪', k') and a local ring map R → R' such that R' is flat over R, 𝔪' = 𝔪 R', and k' is isomorphic to K as an extension of k.

theorem IsLocalRing.exists_flat_residueField_algEquiv (R : Type u) [CommRing R]
    [IsLocalRing R] (K : Type v) [Field K] [Algebra (ResidueField R) K] :
    ∃ (R' : Type (max u v)) (_ : CommRing R') (_ : Algebra R R') (_ : IsLocalRing R')
      (_ : IsLocalHom (algebraMap R R')),
      Module.Flat R R' ∧
      (maximalIdeal R).map (algebraMap R R') = maximalIdeal R' ∧
      Nonempty (ResidueField R' ≃ₐ[ResidueField R] K)

Tag 09E0, a lemma

Tag 09E0 in the Stacks Project.

IsLocalRing.exists_finiteEtale_directed_residueField_algEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/ResidueFieldColimit.lean, line 1111. The attribute's comment: “The source's directed set I and system of finite étale extensions R ⊂ R_i with R' = colim R_i appear as a directed family 𝒮 of finite étale local R-subalgebras of R' covering R', which is equivalent since the transition maps of such a system are injective. K is allowed to live in a universe of its own, the source's case being v = u. See the module docstring.”. References: EGA IV (18.8.6), “(18.8.6.2)”.

A separable algebraic residue field extension is realized by a colimit of finite étale extensions (Stacks 09E0). Let (R, 𝔪, k) be a local ring and let K be a separable algebraic extension of k. Then there are a local ring R', a local ring map R → R', and a directed family 𝒮 of R-subalgebras of R' whose union is R', each a local ring finite étale over R, such that the residue field of R' is isomorphic to K as an extension of k.

public theorem IsLocalRing.exists_finiteEtale_directed_residueField_algEquiv (R : Type u)
    [CommRing R] [IsLocalRing R] (K : Type v) [Field K] [Algebra (ResidueField R) K]
    [Algebra.IsSeparable (ResidueField R) K] :
    ∃ (R' : Type (max u v)) (_ : CommRing R') (_ : Algebra R R') (_ : IsLocalRing R')
      (_ : IsLocalHom (algebraMap R R')) (𝒮 : Set (Subalgebra R R')),
      DirectedOn (· ≤ ·) 𝒮 ∧
      (∀ x : R', ∃ S ∈ 𝒮, x ∈ S) ∧
      (∀ S ∈ 𝒮, Module.Finite R S ∧ Algebra.Etale R S ∧ IsLocalRing S) ∧
      Nonempty (ResidueField R' ≃ₐ[ResidueField R] K)

Tag 07NE, a lemma

Tag 07NE in the Stacks Project.

exists_isFiniteFree_residueField_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FiniteFreeResidueExtension.lean, line 651. References: SGA 3 V (4.1.2), “finite K/k case”.

Stacks Tag 07NE (Lemma 10.159.3). Given a commutative ring R, a prime p, and a finite field extension L / κ(p), there exist a commutative ring S and a finite free ring map φ : R →+* S such that, with q := pS = Ideal.map φ p: * q is prime; * q lies over p (p = q.comap φ); * the induced residue field extension κ(q) / κ(p) is κ(p)-isomorphic to L / κ(p), i.e. there is a ring isomorphism Φ : κ(q) ≃+* L whose composite with the induced map κ(p) → κ(q) equals the structure map κ(p) → L.

theorem exists_isFiniteFree_residueField_equiv.{u, v}
    (R : Type u) [CommRing R] (p : Ideal R) [hp : p.IsPrime]
    (L : Type v) [Field L] [Algebra (ResidueFieldAtPrime R p) L]
    [Module.Finite (ResidueFieldAtPrime R p) L] :
    ∃ (S : Type u) (_ : CommRing S) (φ : R →+* S),
      IsFiniteFree φ ∧
      ∃ (_ : (Ideal.map φ p).IsPrime) (hpq : p = (Ideal.map φ p).comap φ),
        ∃ (Φ : ResidueFieldAtPrime S (Ideal.map φ p) ≃+* L),
          (Φ.toRingHom.comp (inducedResidueMap φ p (Ideal.map φ p) hpq) :
            ResidueFieldAtPrime R p →+* L) = algebraMap (ResidueFieldAtPrime R p) L

Tag 0GIL, a lemma

Tag 0GIL in the Stacks Project.

Stacks.Flatness.SmallSubalgebras.directedOn_flatSmallSubalgebras, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Colimit.lean, line 357.

(Directedness). The family F of flat A-subalgebras of cardinality ≤ κ is directed under inclusion.

theorem directedOn_flatSmallSubalgebras
    (hB : Module.Flat A B) :
    DirectedOn (· ≤ ·) (flatSmallSubalgebras A B)

Stacks.Flatness.SmallSubalgebras.sSup_flatSmallSubalgebras, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Colimit.lean, line 387.

(Covering, supremum form). The supremum (union) of the family F is all of B.

theorem sSup_flatSmallSubalgebras
    (hB : Module.Flat A B) :
    sSup (flatSmallSubalgebras A B) = ⊤

Stacks.Flatness.SmallSubalgebras.faithfullyFlat_of_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/Colimit.lean, line 398.

(Corollary / remark). Any member of F is faithfully flat over A whenever B is faithfully flat over A.

theorem faithfullyFlat_of_mem
    (hB : Module.FaithfullyFlat A B)
    (B' : Subalgebra A B) (hB' : B' ∈ flatSmallSubalgebras A B) :
    Module.FaithfullyFlat A B'

Sources

• Section 10.159, Tag 03C2
• AxiomMath/Stacks at 5ed82d14

LeanIsLocalRing.exists_flat_residueField_algEquiv · IsLocalRing.exists_finiteEtale_directed_residueField_algEquiv · exists_isFiniteFree_residueField_equiv · Stacks.Flatness.SmallSubalgebras.directedOn_flatSmallSubalgebras · Stacks.Flatness.SmallSubalgebras.sSup_flatSmallSubalgebras · Stacks.Flatness.SmallSubalgebras.faithfullyFlat_of_mem

Section10.160 The Cohen structure theorem#

Section 10.160 of the Stacks Project, Tag 0323. 12 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0323, the section

Tag 0323 in the Stacks Project.

IsLocalRing.isAdicComplete_maximalIdeal_iff_forall_compatible_existsUnique_mk_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/InverseLimitCharacterization.lean, line 122. The attribute's comment: “0323 is the label of the heading \section{The Cohen structure theorem}, not of a mathematical statement: it has no hypotheses and no conclusion, so NO single theorem can be a faithful formalization of it, and this attribute is placed under the project's rule that a tag which is not a statement as written is carried in corrected form with the correction recorded. The correction: 0323 is carried here, on the section's OPENING NOTION — the section begins Here is a fundamental notion in commutative algebra and then states Definition 0324, the definition of a complete local ring, which is what this declaration characterizes — and the section's remaining eleven labelled items are carried at their own tags elsewhere in this library, not here. Namely: 032A, the Cohen structure theorem itself, on IsLocalRing.exists_isCoefficientRing_and_exists_surjective_mvPowerSeries in StacksFrontier.RingTheory.CompleteLocalRing.CohenStructureTheorem; 032D on IsLocalRing.exists_injective_finite_mvPowerSeries in the same module; 0C0S, the power series description of a regular complete local ring, on IsRegularLocalRing.nonempty_ringEquiv_and_algEquiv_mvPowerSeries in StacksFrontier.RingTheory.CompleteLocalRing.Regular; 0325 on quotient_isNoetherianCompleteLocalRing and finite_isProduct_isNoetherianCompleteLocalRing, and 032B on complete_local_ring_noetherian, all in StacksFrontier.RingTheory.CompleteLocalRing.Noetherian; 0326 on LocalSubring.IsCoefficientRing in StacksFrontier.RingTheory.CompleteLocalRing.CoefficientRing; 0327 on the class IsCohenRing, 0328 on IsCohenRing.exists_residueField_ringEquiv and 0329 on IsCohenRing.formallySmooth_quotient_span_pow, all in StacksFrontier.RingTheory.CohenRing; and 032C on isUniversallyCatenary_of_isPrecomplete_maximalIdeal in StacksFrontier.RingTheory.Catenary.Formal. With 0324 carried here, every labelled item of the section now has a carrier and only the heading itself had none.”.

A local ring is complete exactly when it is the inverse limit of its adic truncations.

Let (R, 𝔪) be a local ring. Then R is 𝔪-adically complete if and only if for every family f of residues f n : R ⧸ 𝔪ⁿ that is compatible with the truncation maps R ⧸ 𝔪ⁿ → R ⧸ 𝔪ᵏ for k ≤ n, there is a unique r : R whose residue modulo 𝔪ⁿ is f n for every n.

This is the Stacks project's definition of a complete local ring: a compatible family is an element of lim_n R / 𝔪ⁿ, existence of r says the canonical map R → lim_n R / 𝔪ⁿ is surjective, and uniqueness says it is injective, so the two together say that this ring map is an isomorphism. Uniqueness for the zero family is the separatedness ⋂ₙ 𝔪ⁿ = (0) that the source's footnote insists on; it corresponds to the IsHausdorff half of IsAdicComplete, while existence corresponds to the IsPrecomplete half.

theorem IsLocalRing.isAdicComplete_maximalIdeal_iff_forall_compatible_existsUnique_mk_eq
    (R : Type u) [CommRing R] [IsLocalRing R] :
    IsAdicComplete (maximalIdeal R) R ↔
      ∀ f : (n : ℕ) → R ⧸ maximalIdeal R ^ n,
        (∀ (k n : ℕ) (h : k ≤ n),
            Ideal.Quotient.factor (Ideal.pow_le_pow_right h) (f n) = f k) →
          ∃! r : R, ∀ n : ℕ, Ideal.Quotient.mk (maximalIdeal R ^ n) r = f n

Tag 0324, a definition

Tag 0324 in the Stacks Project.

IsLocalRing.isAdicComplete_maximalIdeal_iff_forall_compatible_existsUnique_mk_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/InverseLimitCharacterization.lean, line 122. The attribute's comment: “The source defines (R, 𝔪) to be a complete local ring when the canonical map R ⟶ lim_n R / 𝔪ⁿ is an isomorphism. This library has no definition of its own for that: completeness of a local ring is spelled IsAdicComplete (IsLocalRing.maximalIdeal R) R everywhere downstream (for instance in 032A, 032D and 0C0S), and introducing a second name for it would shadow canonical Mathlib API. So the definition is carried as the CHARACTERIZATION theorem that identifies the library's spelling with the source's: IsAdicComplete holds iff every compatible family of residues modulo 𝔪ⁿ comes from a unique element of R, i.e. iff the canonical ring map into the inverse limit is bijective, hence an isomorphism. lim_n R/𝔪ⁿ is not named as an object; it is spelled by its universal property, with the source's own truncations Ideal.Quotient.mk (𝔪ⁿ) and transition maps Ideal.Quotient.factor, so the statement does not depend on a model of the limit. The source's footnote — that this includes ⋂ 𝔪ⁿ = (0), R complete AND separated — is the uniqueness half of the ∃!, applied to the zero family; it matches the IsHausdorff component of IsAdicComplete, existence matching IsPrecomplete. The footnote's three cross-references (05JC, 05GG, 05GH) are remarks on when the completion is itself complete and Noetherian; they are separate tags and are not claimed here.”.

A local ring is complete exactly when it is the inverse limit of its adic truncations.

Let (R, 𝔪) be a local ring. Then R is 𝔪-adically complete if and only if for every family f of residues f n : R ⧸ 𝔪ⁿ that is compatible with the truncation maps R ⧸ 𝔪ⁿ → R ⧸ 𝔪ᵏ for k ≤ n, there is a unique r : R whose residue modulo 𝔪ⁿ is f n for every n.

This is the Stacks project's definition of a complete local ring: a compatible family is an element of lim_n R / 𝔪ⁿ, existence of r says the canonical map R → lim_n R / 𝔪ⁿ is surjective, and uniqueness says it is injective, so the two together say that this ring map is an isomorphism. Uniqueness for the zero family is the separatedness ⋂ₙ 𝔪ⁿ = (0) that the source's footnote insists on; it corresponds to the IsHausdorff half of IsAdicComplete, while existence corresponds to the IsPrecomplete half.

theorem IsLocalRing.isAdicComplete_maximalIdeal_iff_forall_compatible_existsUnique_mk_eq
    (R : Type u) [CommRing R] [IsLocalRing R] :
    IsAdicComplete (maximalIdeal R) R ↔
      ∀ f : (n : ℕ) → R ⧸ maximalIdeal R ^ n,
        (∀ (k n : ℕ) (h : k ≤ n),
            Ideal.Quotient.factor (Ideal.pow_le_pow_right h) (f n) = f k) →
          ∃! r : R, ∀ n : ℕ, Ideal.Quotient.mk (maximalIdeal R ^ n) r = f n

Tag 0325, a lemma

Tag 0325 in the Stacks Project.

quotient_isNoetherianCompleteLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/Noetherian/FiniteProduct.lean, line 91. References: EGA 0 (20.7.20), “special case”; EGA IV (18.5.16), “special case”.

If R is a Noetherian complete local ring and J is a proper ideal of R, then the quotient R / J is again a Noetherian complete local ring.

theorem quotient_isNoetherianCompleteLocalRing
    {R : Type*} [CommRing R] (hR : IsNoetherianCompleteLocalRing R)
    (J : Ideal R) (hJ : J ≠ ⊤) :
    IsNoetherianCompleteLocalRing (R ⧸ J)

finite_isProduct_isNoetherianCompleteLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/Noetherian/FiniteProduct.lean, line 657. References: EGA 0 (22.3.1), “special case”; EGA IV (18.5.9), “(ii), special case”; EGA IV (5.4.3), “special case”; SGA 1 III (1.4), “special case”; SGA 3 VIIB (0.1.1), “special case”; SGA 3 XV (1.5), “partial”; SGA 3 XV (3.9); SGA 4 VIII (4.1), “(i), special case”.

If R is a Noetherian complete local ring and R → S is a finite ring map, then S is a finite product of Noetherian complete local rings: there exist finitely many rings T 0, ..., T (m-1), each a Noetherian complete local ring, together with a ring isomorphism S ≃+* Π i, T i.

theorem finite_isProduct_isNoetherianCompleteLocalRing
    {R : Type u} [CommRing R] (hR : IsNoetherianCompleteLocalRing R)
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] :
    ∃ (m : ℕ) (T : Fin m → Type v) (_ : ∀ i, CommRing (T i)),
      (∀ i, IsNoetherianCompleteLocalRing (T i)) ∧
      Nonempty (S ≃+* (Π i, T i))

Tag 032B, a lemma

Tag 032B in the Stacks Project.

complete_local_ring_noetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/Noetherian/FGMaximalIdeal.lean, line 541. References: EGA 0 (7.2.6), “special case”; EGA I (10.6.4), “special case”.

A local ring R that is complete for its maximal-ideal-adic topology and whose maximal ideal is finitely generated is Noetherian.

theorem complete_local_ring_noetherian
    (R : Type*) [CommRing R] [IsLocalRing R]
    (hcomplete : IsAdicComplete (IsLocalRing.maximalIdeal R) R)
    (hfg : (IsLocalRing.maximalIdeal R).FG) :
    IsNoetherianRing R

Tag 0326, a definition

Tag 0326 in the Stacks Project.

LocalSubring.IsCoefficientRing, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/CoefficientRing.lean, line 100.

A coefficient ring of a local ring (R, 𝔪) is a local subring Λ ⊆ R such that Λ is complete with maximal ideal Λ ∩ 𝔪, the residue field of Λ maps isomorphically onto the residue field of R, and Λ ∩ 𝔪 = pΛ, where p is the characteristic of the residue field of R.

public structure LocalSubring.IsCoefficientRing (Λ : LocalSubring R) : Prop

Tag 0327, a definition

Tag 0327 in the Stacks Project.

IsCohenRing, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenRing.lean, line 46. References: EGA 0 (19.8.4), “partial”; SGA 7 I (0.5.3).

A Cohen ring is a complete discrete valuation ring whose uniformizer is a (rational) prime number p. Concretely, R is a domain, it is a discrete valuation ring, it is complete for the maximal-ideal-adic topology, and there is a prime number p ∈ ℕ such that the maximal ideal of R is generated by the image of p in R.

This is a class extending IsDiscreteValuationRing and IsAdicComplete for the maximal ideal, so that both the valuation-theoretic and the completeness API of a Cohen ring are available to instance search without unfolding the definition, and only the arithmetic condition on the uniformizer is a field of its own.

class IsCohenRing (R : Type*) [CommRing R] [IsDomain R] : Prop extends
    IsDiscreteValuationRing R, IsAdicComplete (IsLocalRing.maximalIdeal R) R

Tag 0328, a lemma

Tag 0328 in the Stacks Project.

IsCohenRing.exists_residueField_ringEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenRing.lean, line 348. The attribute's comment: “The source's Λ/pΛ ≅ k is the conjunction of maximalIdeal Λ = pΛ, pinning the uniformizer to the prime p that IsCohenRing (Stacks 0327) only asserts to exist, with a ring isomorphism ResidueField Λ ≃+* k, ResidueField Λ being Λ ⧸ maximalIdeal Λ. The ring Λ is asked for in the universe of k. See the module docstring.”. References: EGA 0 (19.8.6), “(ii), special case”.

Cohen rings exist (Stacks 0328). Let p be a prime number and let k be a field of characteristic p. Then there is a Cohen ring Λ whose uniformizer is p, i.e. with maximalIdeal Λ = pΛ, and whose residue field Λ/pΛ is isomorphic to k.

public theorem IsCohenRing.exists_residueField_ringEquiv (p : ℕ) (hp : p.Prime) (k : Type u)
    [Field k] [CharP k p] :
    ∃ (Λ : Type u) (_ : CommRing Λ) (_ : IsDomain Λ) (_ : IsCohenRing Λ),
      maximalIdeal Λ = Ideal.span {(p : Λ)} ∧ Nonempty (ResidueField Λ ≃+* k)

Tag 0329, a lemma

Tag 0329 in the Stacks Project.

IsCohenRing.formallySmooth_quotient_span_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenRing.lean, line 666. The attribute's comment: “The source's p > 0 prime and p a uniformizer are consequences of CharP (ResidueField Λ) p for a Cohen ring, so only the latter is assumed, and n ≥ 1 is dropped because n = 0 gives the zero ring on both sides. The ZMod (p ^ n)-algebra structure is assumed rather than synthesized; it is unique where it exists, so this pins the source's map ℤ/pⁿℤ → Λ/pⁿΛ. See the module docstring.”.

Let Λ be a Cohen ring whose residue field has characteristic p, so that p is a uniformizer of Λ. For every n the ring map ℤ/pⁿℤ → Λ/pⁿΛ is formally smooth (Stacks 0329).

public theorem IsCohenRing.formallySmooth_quotient_span_pow (p n : ℕ) (Λ : Type*) [CommRing Λ]
    [IsDomain Λ] [IsCohenRing Λ] [CharP (ResidueField Λ) p]
    [Algebra (ZMod (p ^ n)) (Λ ⧸ Ideal.span {(p : Λ) ^ n})] :
    Algebra.FormallySmooth (ZMod (p ^ n)) (Λ ⧸ Ideal.span {(p : Λ) ^ n})

Tag 032A, a theorem

Tag 032A in the Stacks Project.

IsLocalRing.exists_isCoefficientRing_and_exists_surjective_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/CohenStructureTheorem/CoefficientRing.lean, line 672. The attribute's comment: “Completeness of R is IsAdicComplete (maximalIdeal R) R, the source's R ≅ lim_n R/𝔪ⁿ. The two parts are the two conjuncts, the second guarded by its own hypothesis so that part (1) keeps the source's generality, and its R ≅ Λ[[x_1, …, x_n]]/I is stated as the existence of a surjection MvPowerSeries (Fin n) Λ →+* R with kernel I. See the module docstring.”. References: EGA 0 (19.8.8), “(i)”.

Cohen structure theorem (Stacks 032A). Let (R, 𝔪) be a complete local ring. 1. R has a coefficient ring: a local subring Λ ⊆ R which is complete with maximal ideal Λ ∩ 𝔪, whose residue field maps isomorphically onto that of R, and with Λ ∩ 𝔪 = pΛ for p the residue characteristic of R. 2. If 𝔪 is a finitely generated ideal, then R is isomorphic to a quotient Λ[[x_1, …, x_n]]/I where Λ is either a field or a Cohen ring; equivalently, there is a surjective ring homomorphism Λ[[x_1, …, x_n]] → R, whose kernel is I.

public theorem IsLocalRing.exists_isCoefficientRing_and_exists_surjective_mvPowerSeries
    (R : Type u) [CommRing R] [IsLocalRing R] [IsAdicComplete (maximalIdeal R) R] :
    (∃ Λ : LocalSubring R, Λ.IsCoefficientRing) ∧
      ((maximalIdeal R).FG →
        ∃ (n : ℕ) (Λ : Type u) (_ : CommRing Λ) (_ : IsDomain Λ),
          (IsField Λ ∨ IsCohenRing Λ) ∧
            ∃ f : MvPowerSeries (Fin n) Λ →+* R, Function.Surjective f)

Tag 032C, a remark

Tag 032C in the Stacks Project.

isUniversallyCatenary_of_isPrecomplete_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Catenary/Formal.lean, line 293. The attribute's comment: “universally catenary”. References: EGA IV (5.2.5), “special case”; EGA IV (5.6.4), “special case”; EGA IV (7.1.11), “clause (i), special case”; EGA IV (7.5.3), “more general”.

Stacks Project, Tag 032C. A Noetherian complete local ring is universally catenary.

By the Cohen structure theorem it is a quotient of a power series ring over a field or over a Cohen ring, hence of a regular local ring; a regular local ring is Cohen-Macaulay with full support, so [Stacks, Tag 00NM] applies, and universal catenarity passes to quotients.

Completeness is asked for as precompleteness for the maximal ideal, as in [Stacks, Tag 07PJ]; the Hausdorff half is automatic for a Noetherian local ring, so a ring carrying IsAdicComplete (IsLocalRing.maximalIdeal R) R satisfies the hypothesis by inference.

theorem isUniversallyCatenary_of_isPrecomplete_maximalIdeal
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) R] : Ring.IsUniversallyCatenary R

Tag 0C0S, a lemma

Tag 0C0S in the Stacks Project.

IsRegularLocalRing.nonempty_ringEquiv_and_algEquiv_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/Regular.lean, line 362. The attribute's comment: “The source's Noetherian complete local regular ring is IsRegularLocalRing R with IsAdicComplete (maximalIdeal R) R. R contains 𝐅_p or 𝐐 iff it contains a field, which is how the first part is hypothesized; the number of variables is pinned to the embedding dimension, the d of the source's proof. The two parts are the two conjuncts, each guarded by its own hypothesis. See the module docstring.”. References: EGA 0 (19.6.3), “a)⇒c), regular case”; EGA 0 (19.6.5), “Â ≅ K[[T_1,...,T_n]]”; EGA 0 (19.6.4), “special case”; EGA 0 (19.8.8), “(i), special case”.

Let (R, 𝔪) be a Noetherian complete local ring which is regular, and let d be its embedding dimension dim_{R/𝔪} 𝔪/𝔪², which equals dim R. 1. If R contains a field — equivalently 𝐅_p or 𝐐 — then R is isomorphic to the power series ring in d variables over its residue field. 2. If k is a field and k → R is a ring map inducing an isomorphism k → R/𝔪, then R is isomorphic as a k-algebra to the power series ring in d variables over k. (Stacks 0C0S)

public theorem IsRegularLocalRing.nonempty_ringEquiv_and_algEquiv_mvPowerSeries (R : Type u)
    [CommRing R] [IsRegularLocalRing R] [IsAdicComplete (maximalIdeal R) R] (d : ℕ)
    (hd : Module.finrank (ResidueField R) (CotangentSpace R) = d) :
    (∀ (F : Type v) [Field F] [Algebra F R],
        Nonempty (R ≃+* MvPowerSeries (Fin d) (ResidueField R))) ∧
      (∀ (k : Type w) [Field k] [Algebra k R],
        Function.Bijective ((residue R).comp (algebraMap k R)) →
          Nonempty (R ≃ₐ[k] MvPowerSeries (Fin d) k))

Tag 032D, a lemma

Tag 032D in the Stacks Project.

IsLocalRing.exists_injective_finite_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/CohenStructureTheorem/RegularSubring.lean, line 569. The attribute's comment: “The subring R₀ ⊆ R is presented as an injective ring homomorphism f from the power series ring it is isomorphic to, so that items (1) and (3) are statements about MvPowerSeries (Fin d) Λ and item (2) is one about f: f.Finite for finiteness and Function.Surjective ((residue R).comp f) for the isomorphism on residue fields. See the module docstring.”. References: EGA 0 (19.8.8), “(ii)”.

Let (R, 𝔪) be a Noetherian complete local domain. Then there is a subring R₀ ⊆ R which is a regular complete local ring, over which R is finite, which induces an isomorphism on residue fields, and which is a power series ring Λ[[X_1, …, X_d]] over a field or over a Cohen ring Λ. The subring is presented as the image of an injective ring homomorphism f : Λ[[X_1, …, X_d]] → R, finite and with R/𝔪 generated by the image of f. (Stacks 032D)

public theorem IsLocalRing.exists_injective_finite_mvPowerSeries (R : Type u) [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] [IsAdicComplete (maximalIdeal R) R] :
    ∃ (d : ℕ) (Λ : Type u) (_ : CommRing Λ) (_ : IsDomain Λ),
      (IsField Λ ∨ IsCohenRing Λ) ∧
        ∃ _ : IsRegularLocalRing (MvPowerSeries (Fin d) Λ),
          IsAdicComplete (maximalIdeal (MvPowerSeries (Fin d) Λ)) (MvPowerSeries (Fin d) Λ) ∧
            ∃ f : MvPowerSeries (Fin d) Λ →+* R,
              Function.Injective f ∧ f.Finite ∧ Function.Surjective ((residue R).comp f)

Sources

• Section 10.160, Tag 0323
• AxiomMath/Stacks at 5ed82d14

LeanIsLocalRing.isAdicComplete_maximalIdeal_iff_forall_compatible_existsUnique_mk_eq · quotient_isNoetherianCompleteLocalRing · finite_isProduct_isNoetherianCompleteLocalRing · complete_local_ring_noetherian · LocalSubring.IsCoefficientRing · IsCohenRing · IsCohenRing.exists_residueField_ringEquiv · IsCohenRing.formallySmooth_quotient_span_pow

Section10.161 Japanese rings#

Section 10.161 of the Stacks Project, Tag 0BI1. 15 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 032F, a definition

Tag 032F in the Stacks Project.

IsN1, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Defs.lean, line 100. The attribute's comment: “(1)”.

A domain R is N-1 if the integral closure of R in its field of fractions is a finite R-module.

The field of fractions is FractionRing R; see the module docstring for the formulation with an arbitrary field of fractions. As with IsIntegrallyClosed, R is not required to be a domain: for a general commutative ring FractionRing R is the total ring of fractions, and the condition reads the same.

abbrev IsN1 (R : Type*) [CommRing R] : Prop

IsJapaneseRing, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Defs.lean, line 109. The attribute's comment: “(2)”. References: EGA 0 (23.1.1), “def. of Japanese”.

A domain R is N-2, or Japanese, if for every finite field extension L of its field of fractions K = Frac(R), the integral closure of R in L is a finite R-module.

The extension is presented as a field L that is a K-algebra, finite dimensional over K, whose R-algebra structure is the composite of R → K with K → L.

class IsJapaneseRing (R : Type u) [CommRing R] [IsDomain R] : Prop

Tag 032G, a lemma

Tag 032G in the Stacks Project.

isN1_and_isJapaneseRing_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/JapaneseCriteria.lean, line 151.

N-1 and N-2 pass to a localization. Stacks Tag 032G: if a domain R is N-1 then so is every localization of R which is again a domain, and the same for N-2.

theorem isN1_and_isJapaneseRing_of_isLocalization {R : Type u} [CommRing R] [IsDomain R]
    (M : Submonoid R) (Rₛ : Type u) [CommRing Rₛ] [IsDomain Rₛ] [Algebra R Rₛ]
    [IsLocalization M Rₛ] :
    (IsN1 R → IsN1 Rₛ) ∧ (IsJapaneseRing R → IsJapaneseRing Rₛ)

Tag 032H, a lemma

Tag 032H in the Stacks Project.

isN1_and_isJapaneseRing_of_localizationSpan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/JapaneseCriteria.lean, line 265.

N-1 and N-2 descend along a principal open cover. Stacks Tag 032H: let R be a domain and let t ⊆ R generate the unit ideal. If the localization R_g is N-1 for every g ∈ t then so is R, and the same for N-2.

theorem isN1_and_isJapaneseRing_of_localizationSpan {R : Type u} [CommRing R] [IsDomain R]
    (t : Set R) (ht : Ideal.span t = ⊤)
    {Rₚ : ∀ _ : t, Type u} [∀ g, CommRing (Rₚ g)] [∀ g, IsDomain (Rₚ g)]
    [∀ g, Algebra R (Rₚ g)] [∀ g, IsLocalization.Away g.val (Rₚ g)] :
    ((∀ g, IsN1 (Rₚ g)) → IsN1 R) ∧
      ((∀ g, IsJapaneseRing (Rₚ g)) → IsJapaneseRing R)

Tag 032I, a lemma

Tag 032I in the Stacks Project.

isJapaneseRing_of_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/JapaneseCriteria.lean, line 484.

N-2 ascends along a quasi-finite extension of domains. Stacks Tag 032I: let R ⊆ S be a quasi-finite extension of domains with R Noetherian and N-2. Then S is N-2.

Zariski's main theorem covers Spec S by principal opens on which S agrees with a subalgebra module-finite over R; N-2 ascends to such a subalgebra, passes to its localizations (Tag 032G), and descends from the cover (Tag 032H).

theorem isJapaneseRing_of_quasiFinite {R S : Type u} [CommRing R] [IsDomain R] [CommRing S]
    [IsDomain S] [Algebra R S] [FaithfulSMul R S] [IsNoetherianRing R] [Algebra.FiniteType R S]
    [Algebra.QuasiFinite R S] (hR : IsJapaneseRing R) : IsJapaneseRing S

Tag 032J, a lemma

Tag 032J in the Stacks Project.

main_theorem_032j, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Basic.lean, line 610.

Theorem (Stacks Tag 032J). Let R be a Noetherian domain. If the Laurent polynomial ring R[z, z^{-1}] is N-1, then R is N-1.

theorem main_theorem_032j (R : Type*) [CommRing R] [IsDomain R] [IsNoetherianRing R]
    (h : IsN1 (LaurentPolynomial R)) : IsN1 R

Tag 032K, a lemma

Tag 032K in the Stacks Project.

isN1_of_finite_of_isN1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Basic.lean, line 702. The attribute's comment: “(1)”.

Statement 1 (N-1 descends, part of Stacks Tag 032K). Let R be a Noetherian domain and R ⊂ S a finite extension of domains (modelled by an injective algebra map R → S with S finite over R). If S is N-1, then R is N-1.

theorem isN1_of_finite_of_isN1
    (R S : Type*) [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [CommRing S] [IsDomain S] [Algebra R S]
    (hinj : Function.Injective (algebraMap R S))
    (hfin : Module.Finite R S)
    (hS : IsN1 S) : IsN1 R

isN2_of_finite_of_isN2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Basic.lean, line 818. The attribute's comment: “(2)”.

Statement 2 (N-2 descends, part of Stacks Tag 032K). Let R be a Noetherian domain and R ⊂ S a finite extension of domains (modelled by an injective algebra map R → S with S finite over R). If S is N-2, then R is N-2.

theorem isN2_of_finite_of_isN2
    (R S : Type*) [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [CommRing S] [IsDomain S] [Algebra R S]
    (hinj : Function.Injective (algebraMap R S))
    (hfin : Module.Finite R S)
    (hS : IsN2_032k S) : IsN2_032k R

Tag 032L, a lemma

Tag 032L in the Stacks Project.

Noetherian_normal_domain_finite_separable_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Basic.lean, line 908. References: EGA II (6.3.10), “special case”; EGA II (7.3.12), “special case”; EGA IV (14.5.5), “finiteness of A₁ over A”; EGA IV (18.10.15), “partial”.

The integral closure of a Noetherian normal domain in a finite separable extension is finite over the base ring.

theorem Noetherian_normal_domain_finite_separable_extension
    (R : Type*) [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
    (L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Algebra R L] [IsScalarTower R K L] :
    Module.Finite R (integralClosure R L)

Tag 0AE0, a lemma

Tag 0AE0 in the Stacks Project.

Stacks.Nagata.PurelyInseparable.integralClosure_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/PurelyInseparable.lean, line 713.

Stacks 0AE0. The integral closure of R in L = K[x]/(x^p - a) is finite over R. Given the finitely generated R-module N ⊇ integral closure from exists_fg_le, the integral closure is a submodule of the f.g. module N over the Noetherian ring R, hence itself f.g. (Submodule.FG.of_le), hence finite (Module.Finite.of_fg).

theorem integralClosure_finite
    (h : ∃ D : Derivation ℤ K K,
      (∀ r : R, ∃ s : R, D (algebraMap R K r) = algebraMap R K s) ∧ D a ≠ 0) :
    Module.Finite R (integralClosure R (Lext p a))

Tag 032M, a lemma

Tag 032M in the Stacks Project.

N1_iff_N2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Basic.lean, line 868. References: EGA 0 (23.1.2), “special case”.

Stacks Tag 032M, Lemma 10.161.11. For a Noetherian domain R whose fraction field K has characteristic zero, R is N-1 if and only if R is N-2 (Japanese).

theorem N1_iff_N2 (R K : Type u) [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] :
    IsN1_032m R K ↔ IsN2_032m R K

Tag 032N, a lemma

Tag 032N in the Stacks Project.

isJapaneseRing_iff_finite_integralClosure_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/JapaneseCriteria.lean, line 380. References: EGA 0 (23.1.2).

N-2 is tested on purely inseparable extensions. Stacks Tag 032N: a Noetherian domain R is N-2 if and only if the integral closure of R in every finite purely inseparable extension of its field of fractions is a finite R-module.

The source states this for a field of fractions of characteristic p > 0; the characteristic plays no role in the argument, which factors a finite normal extension of K as a purely inseparable extension followed by a separable one (Tag 030M) and is vacuously about L = K in characteristic zero, so no characteristic hypothesis is imposed.

theorem isJapaneseRing_iff_finite_integralClosure_isPurelyInseparable (R : Type u) [CommRing R]
    [IsDomain R] [IsNoetherianRing R] :
    IsJapaneseRing R ↔
      ∀ (L : Type u) [Field L] [Algebra R L] [Algebra (FractionRing R) L]
        [IsScalarTower R (FractionRing R) L] [FiniteDimensional (FractionRing R) L]
        [IsPurelyInseparable (FractionRing R) L],
        Module.Finite R (integralClosure R L)

Tag 032O, a lemma

Tag 032O in the Stacks Project.

Polynomial.isN1_and_isJapaneseRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Polynomial.lean, line 687.

N-1 and N-2 ascend to a polynomial ring. Let R be a domain. If the integral closure of R in Frac(R) is a finite R-module, then the integral closure of R[x] in Frac(R[x]) is a finite R[x]-module; and if R is Noetherian and N-2 (Japanese), then R[x] is N-2.

The Noetherian hypothesis of Tag 032O is attached to the N-2 conjunct only, the N-1 conjunct not using it; see the module docstring.

public theorem Polynomial.isN1_and_isJapaneseRing (R : Type u) [CommRing R] [IsDomain R] :
    (IsN1 R → IsN1 (Polynomial R)) ∧
      (IsNoetherianRing R → IsJapaneseRing R → IsJapaneseRing (Polynomial R))

Tag 0332, a lemma

Tag 0332 in the Stacks Project.

PrimeSpectrum.isOpen_setOf_isIntegrallyClosed_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NormalLocus/Open.lean, line 558. The attribute's comment: “Normality of a localization is spelled IsIntegrallyClosed, Mathlib having no predicate for a normal ring; the IsDomain conjunct of the spelling used for tags 030C (1) and 031S is automatic here because R is a domain. R_f is the canonical model Localization.Away f. See the module docstring.”.

Stacks Tag 0332. Let R be a Noetherian domain. If there is a nonzero f ∈ R such that R_f is normal, then the set of primes 𝔭 of R with R_𝔭 a normal domain is open in Spec(R).

public theorem PrimeSpectrum.isOpen_setOf_isIntegrallyClosed_atPrime
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] {f : R} (hf : f ≠ 0)
    (hf' : IsIntegrallyClosed (Localization.Away f)) :
    IsOpen {p : PrimeSpectrum R | IsIntegrallyClosed (Localization.AtPrime p.asIdeal)}

Tag 0333, a lemma

Tag 0333 in the Stacks Project.

isN1_iff_exists_isIntegrallyClosed_away_and_forall_isN1_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/N1.lean, line 476. The attribute's comment: “R_f normal is IsIntegrallyClosed (Localization.Away f), normality of a domain being integral closedness in its field of fractions; the localizations are the concrete models Localization.Away f and Localization.AtPrime 𝔪. See the module docstring.”.

A Noetherian domain R is N-1 — its integral closure in Frac R is a finite R-module — if and only if R_f is normal for some nonzero f ∈ R and R_𝔪 is N-1 for every maximal ideal 𝔪 ⊆ R.

Normality of the domain R_f is IsIntegrallyClosed (Localization.Away f); see the module docstring.

public theorem isN1_iff_exists_isIntegrallyClosed_away_and_forall_isN1_atPrime
    (R : Type*) [CommRing R] [IsDomain R] [IsNoetherianRing R] :
    IsN1 R ↔
      (∃ f : R, f ≠ 0 ∧ IsIntegrallyClosed (Localization.Away f)) ∧
        ∀ (𝔪 : Ideal R) [𝔪.IsMaximal], IsN1 (Localization.AtPrime 𝔪)

Tag 032P, a lemma

Tag 032P in the Stacks Project.

IsJapaneseRing.of_quotient_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Tate.lean, line 623. References: EGA 0 (23.1.3).

Tate's theorem. Let R be a Noetherian integrally closed (i.e. normal) domain and let x ∈ R generate a prime ideal, so that R ⧸ xR is a domain. If R ⧸ xR is N-2 (Japanese) and R is x-adically complete, then R is N-2.

Completeness is asked for as IsPrecomplete (Ideal.span {x}) R; the Hausdorff half of IsAdicComplete is automatic here, see the module docstring.

public theorem IsJapaneseRing.of_quotient_span_singleton {R : Type u} [CommRing R] [IsDomain R]
    [IsNoetherianRing R] [IsIntegrallyClosed R] (x : R) [(Ideal.span {x}).IsPrime]
    [IsPrecomplete (Ideal.span {x}) R] (h : IsJapaneseRing (R ⧸ Ideal.span {x})) :
    IsJapaneseRing R

Tag 032Q, a lemma

Tag 032Q in the Stacks Project.

PowerSeries.isJapaneseRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/PowerSeries.lean, line 261. References: EGA 0 (23.1.4), “case r = 1”.

Tag 032Q. If R is a Noetherian N-2 (Japanese) domain, then so is the formal power series ring R⟦X⟧: the integral closure of R⟦X⟧ in every finite extension of Frac R⟦X⟧ is a finite R⟦X⟧-module.

Together with PowerSeries.instIsNoetherianRing and PowerSeries.instIsDomain this says that R⟦X⟧ is a Noetherian N-2 domain.

public theorem isJapaneseRing {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    (hR : IsJapaneseRing R) : IsJapaneseRing R⟦X⟧

Sources

• Section 10.161, Tag 0BI1
• AxiomMath/Stacks at 5ed82d14

LeanIsN1 · IsJapaneseRing · isN1_and_isJapaneseRing_of_isLocalization · isN1_and_isJapaneseRing_of_localizationSpan · isJapaneseRing_of_quasiFinite · main_theorem_032j · isN1_of_finite_of_isN1 · isN2_of_finite_of_isN2

Section10.162 Nagata rings#

Section 10.162 of the Stacks Project, Tag 032E. 17 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 032R, a definition

Tag 032R in the Stacks Project.

IsUniversallyJapaneseRing, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Defs.lean, line 119. The attribute's comment: “(1)”. References: EGA 0 (23.1.1); EGA IV (7.7.1).

A ring R is universally Japanese if for every finite-type ring map R → S with S a domain, the domain S is N-2 (Japanese), i.e. satisfies IsJapaneseRing.

class IsUniversallyJapaneseRing (R : Type u) [CommRing R] : Prop

IsNagataRing, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Defs.lean, line 129. The attribute's comment: “(2)”.

A ring R is a Nagata ring if R is Noetherian and for every prime ideal p ⊆ R the quotient domain R ⧸ p is N-2 (Japanese), i.e. satisfies IsJapaneseRing.

class IsNagataRing (R : Type u) [CommRing R] : Prop

Tag 03GH, a lemma

Tag 03GH in the Stacks Project.

IsIntegralClosure.finite_of_essFiniteType_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/IntegralClosure.lean, line 264. References: EGA II (6.3.10), “special case”.

A Nagata ring has finite integral closure in a reduced algebra essentially of finite type.

Let R be a Nagata ring, that is, a Noetherian ring such that R ⧸ p is N-2 (Japanese) for every prime p, and let S be a reduced R-algebra essentially of finite type. Then the integral closure A of R in S is a finite R-module.

public theorem IsIntegralClosure.finite_of_essFiniteType_of_isReduced
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {S : Type u} [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [IsReduced S]
    {A : Type v} [CommRing A] [Algebra R A] [Algebra A S] [IsScalarTower R A S]
    [IsIntegralClosure A R S]
    (hR : ∀ (p : Ideal R) [p.IsPrime], IsJapaneseRing (R ⧸ p)) :
    Module.Finite R A

Tag 0351, a lemma

Tag 0351 in the Stacks Project.

isUniversallyJapanese_of_finiteType_isN1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Japanese/N1Criterion.lean, line 258. References: EGA IV (7.7.1), “N-1 ⇒ univ. Japanese”.

Stacks Tag 0351. Let R be a ring such that for every finite type ring map R → S with S a domain, the domain S is N-1. Then R is universally Japanese.

theorem isUniversallyJapanese_of_finiteType_isN1 (R : Type u) [CommRing R]
    (H : ∀ (S : Type u) [CommRing S] [IsDomain S] [Algebra R S] [Algebra.FiniteType R S], IsN1 S) :
    IsUniversallyJapaneseRing R

Tag 032S, a lemma

Tag 032S in the Stacks Project.

isUniversallyJapanese_of_isEssentiallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Japanese/EssFiniteType.lean, line 372. References: EGA IV (7.7.2), “moreover clause”.

(Stacks Tag 032S, Lemma 10.162.4) If R is universally Japanese then any R-algebra A essentially of finite type over R is universally Japanese.

theorem isUniversallyJapanese_of_isEssentiallyOfFiniteType (R : Type u) [CommRing R] (A : Type u)
    [CommRing A] [Algebra R A] (hR : IsUniversallyJapanese R)
    (hA : IsEssentiallyOfFiniteType R A (algebraMap R A)) : IsUniversallyJapanese A

Tag 032T, a lemma

Tag 032T in the Stacks Project.

isNagataRing_of_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/QuasiFinite.lean, line 154.

A quasi-finite algebra over a Nagata ring is a Nagata ring. If R is a Nagata ring — Noetherian, with every quotient R ⧸ p by a prime N-2 — and R → S is quasi-finite, that is of finite type with finite-dimensional fibres (for example module-finite), then S is a Nagata ring.

Quasi-finiteness in the sense of [Stacks, Tag 00PL] is the conjunction [Algebra.FiniteType R S] [Algebra.QuasiFinite R S], Mathlib's Algebra.QuasiFinite omitting the finite type condition. No injectivity is required: the map R → S is arbitrary.

public theorem isNagataRing_of_quasiFinite {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FiniteType R S] [Algebra.QuasiFinite R S] (hR : IsNagataRing R) :
    IsNagataRing S

Tag 032U, a lemma

Tag 032U in the Stacks Project.

isNagata_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Japanese/Localization.lean, line 211. References: EGA IV (7.7.2).

(Stacks Tag 032U) A localization of a Nagata ring is a Nagata ring.

Here T is an arbitrary R-algebra realizing T = M⁻¹R for a submonoid M ⊆ R (IsLocalization M T), which is exactly Definition 4 of a localization. The single-element case R_f (M = {1, f, f², …}) and the prime case R_p (M = R ∖ p) are special cases.

Proof structure (Stacks: "clear from Tag 032G"): * Noetherianity of T is IsLocalization.isNoetherianRing M T hR.isNoetherianRing. * For a prime q ⊆ T, set p := q.comap (R → T) (prime by Ideal.comap_isPrime). Then R/p is N-2 (hR.isJapaneseRing_quotient p), and T/q ≅ M̄⁻¹(R/p) is a localization of the domain R/p at the image M̄ of M, which lies in the nonzerodivisors of R/p. By isN2_of_isLocalization_domain, T/q is N-2. Hence T is Nagata.

theorem isNagata_of_isLocalization (R : Type u) [CommRing R] (M : Submonoid R) (T : Type u)
    [CommRing T] [Algebra R T] [IsLocalization M T] (hR : IsNagataRing R) :
    IsNagataRing T

Tag 032V, a lemma

Tag 032V in the Stacks Project.

isUniversallyJapaneseRing_and_isNagataRing_of_localizationSpan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Descent.lean, line 288.

Universally Japanese and Nagata descend along a principal open cover. Let t ⊆ R generate the unit ideal and for g ∈ t let Rₚ g be a localization of R away from g. If every Rₚ g is universally Japanese then so is R, and if every Rₚ g is a Nagata ring then so is R.

The source states the two parts for finitely many f₁, …, f_n; they are the two conjuncts here, and an arbitrary spanning set is the same hypothesis.

public theorem isUniversallyJapaneseRing_and_isNagataRing_of_localizationSpan {R : Type u}
    [CommRing R] (t : Set R) (ht : Ideal.span t = ⊤) (Rₚ : ∀ _ : t, Type u)
    [∀ g, CommRing (Rₚ g)] [∀ g, Algebra R (Rₚ g)] [∀ g, IsLocalization.Away g.val (Rₚ g)] :
    ((∀ g, IsUniversallyJapaneseRing (Rₚ g)) → IsUniversallyJapaneseRing R) ∧
      ((∀ g, IsNagataRing (Rₚ g)) → IsNagataRing R)

Tag 032W, a lemma

Tag 032W in the Stacks Project.

IsNagataRing.of_isPrecomplete_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/CompleteLocalRing.lean, line 290. References: EGA 0 (23.1.5), “more general”.

A Noetherian complete local ring is a Nagata ring. If R is Noetherian, local, and complete for the topology defined by its maximal ideal m, then R is a Nagata ring: for every prime p ⊆ R the quotient domain R ⧸ p is N-2 (Japanese).

Completeness is asked for as IsPrecomplete (IsLocalRing.maximalIdeal R) R; the Hausdorff half of IsAdicComplete is automatic for a Noetherian local ring, so a ring with IsAdicComplete (IsLocalRing.maximalIdeal R) R satisfies the hypothesis by inference.

public theorem IsNagataRing.of_isPrecomplete_maximalIdeal {R : Type u} [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] [IsPrecomplete (IsLocalRing.maximalIdeal R) R] :
    IsNagataRing R

Tag 032X, a definition

Tag 032X in the Stacks Project.

IsAnalyticallyUnramified, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Defs.lean, line 107. References: SGA 1 I (9.4).

A local ring R with maximal ideal m is analytically unramified if its completion R^ = lim_n R ⧸ mⁿ is reduced.

The source asks for R Noetherian; that hypothesis is not needed to state the condition and is carried by the lemmas about it. A prime ideal p ⊂ R is analytically unramified when the local ring R ⧸ p is, i.e. when IsAnalyticallyUnramified (R ⧸ p) holds.

public def IsAnalyticallyUnramified (R : Type*) [CommRing R] [IsLocalRing R] : Prop

Tag 032Y, a lemma

Tag 032Y in the Stacks Project.

isAnalyticallyUnramified_iff_minimalPrimes_and_isN1, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Criteria/MinimalPrimes.lean, line 638.

Tag 032Y. Let (R, m) be a Noetherian local ring. Then R is analytically unramified if and only if R is reduced and each of its minimal primes q is analytically unramified, i.e. each local ring R ⧸ q is; and an analytically unramified R is N-1, i.e. the integral closure of R in its total ring of fractions Q(R) is a finite R-module.

The first conjunct is parts (1), (2) and (3) of the source, the forward direction being (1) and (2) and the converse being (3); the second conjunct is part (4), and part (5) is that conjunct with [IsDomain R] adjoined.

public theorem isAnalyticallyUnramified_iff_minimalPrimes_and_isN1 (R : Type*) [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] :
    (IsAnalyticallyUnramified R ↔
        IsReduced R ∧
          ∀ q ∈ minimalPrimes R, ∀ [IsLocalRing (R ⧸ q)], IsAnalyticallyUnramified (R ⧸ q)) ∧
      (IsAnalyticallyUnramified R → IsN1 R)

Tag 032Z, a lemma

Tag 032Z in the Stacks Project.

exists_isDiscreteValuationRing_atPrime_of_analyticallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/AnalyticallyUnramified.lean, line 1235.

Stacks Tag 032Z. Let R be a Noetherian local ring and p ⊂ R a prime ideal such that the localization R_p is a discrete valuation ring and p is analytically unramified (R^ / p R^ is reduced). Then for every associated prime q of the R^-module R^ / p R^, the local ring (R^)_q is a discrete valuation ring.

theorem exists_isDiscreteValuationRing_atPrime_of_analyticallyUnramified {R : Type*} [CommRing R]
  [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R)
    [p.IsPrime]
    -- (1) `R_p` is a discrete valuation ring (hence a domain).
    [IsDomain (Localization.AtPrime p)] (hdvr : IsDiscreteValuationRing (Localization.AtPrime p))
    -- (2) `p` is analytically unramified: `R^ / p R^` is reduced.
    (hunr : AnalyticallyUnramifiedPrime p)
    -- `q` is an associated prime of the `R^`-module `R^ / p R^`.
    (q : Ideal (mCompletion R)) (hq : IsAssociatedPrime q (mCompletion R ⧸ pCompletion p)) :
    -- Conclusion: `(R^)_q` is a discrete valuation ring (in particular a domain).
    ∃ (_ : q.IsPrime) (_ : IsDomain (Localization.AtPrime q)),
      IsDiscreteValuationRing (Localization.AtPrime q)

Tag 0330, a lemma

Tag 0330 in the Stacks Project.

IsAnalyticallyUnramified.of_associatedPrimes_quotient_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Criteria/CuttingByNonzerodivisor.lean, line 507. The attribute's comment: “The source's R a domain with x ≠ 0 is generalized to x a nonzerodivisor, which is all the proof uses; R ⧸ xR having no embedded primes is spelled as every associated prime of R ⧸ xR being minimal over xR, there being no predicate for it in this library.”.

Stacks Tag 0330. Let (R, 𝔪) be a Noetherian local ring and let x ∈ 𝔪 be a nonzerodivisor. If R ⧸ xR has no embedded primes — every associated prime of the module R ⧸ xR is minimal over xR — and every associated prime 𝔭 of R ⧸ xR has R_𝔭 regular and is analytically unramified, then R is analytically unramified.

The source assumes R a domain and x ≠ 0; only x ∈ nonZeroDivisors R is used, and it is what those two amount to.

public theorem IsAnalyticallyUnramified.of_associatedPrimes_quotient_span_singleton {R : Type*}
    [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {x : R} (hx : x ∈ nonZeroDivisors R)
    (hxm : x ∈ maximalIdeal R)
    (hemb : associatedPrimes R (R ⧸ Ideal.span {x}) ⊆ (Ideal.span {x}).minimalPrimes)
    (hp :
      ∀ (p : Ideal R) [p.IsPrime] [IsLocalRing (R ⧸ p)],
        p ∈ associatedPrimes R (R ⧸ Ideal.span {x}) →
          IsRegularLocalRing (Localization.AtPrime p) ∧ IsAnalyticallyUnramified (R ⧸ p)) :
    IsAnalyticallyUnramified R

Tag 0331, a lemma

Tag 0331 in the Stacks Project.

IsAnalyticallyUnramified.of_isNagataRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AnalyticallyUnramified/Criteria/NagataDomain.lean, line 316. The attribute's comment: “Nagata is IsNagataRing of Definition 032R(2), whose first conjunct is IsNoetherianRing R, so the source's Noetherian hypothesis is absorbed rather than restated; analytically unramified is the predicate of Tag 032X, reducedness of the 𝔪-adic completion.”.

Stacks Tag 0331. A local ring (R, 𝔪) which is a domain and a Nagata ring is analytically unramified: its completion R^ = lim_n R ⧸ 𝔪ⁿ is reduced.

The source also assumes R Noetherian; that is the first conjunct of IsNagataRing R.

public theorem IsAnalyticallyUnramified.of_isNagataRing {R : Type*} [CommRing R] [IsLocalRing R]
    [IsDomain R] (hR : IsNagataRing R) : IsAnalyticallyUnramified R

Tag 0BI2, a lemma

Tag 0BI2 in the Stacks Project.

isNagataRing_tfae_isAnalyticallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/AnalyticallyUnramified.lean, line 236.

Stacks 0BI2. For a Noetherian local ring R, the following are equivalent:

1. R is a Nagata ring;
2. for every finite R-algebra S which is a domain and every maximal ideal 𝔪' of S, the localization S_{𝔪'} is analytically unramified;
3. for every finite local homomorphism R → S to a local domain S, the ring S is analytically unramified.

theorem isNagataRing_tfae_isAnalyticallyUnramified {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    [IsNagataRing R,
      ∀ (S : Type (max u v)) [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S]
        (m' : Ideal S) [m'.IsMaximal], IsAnalyticallyUnramified (Localization.AtPrime m'),
      ∀ (S : Type (max u w)) [CommRing S] [IsDomain S] [IsLocalRing S] [Algebra R S]
        [Module.Finite R S] [IsLocalHom (algebraMap R S)], IsAnalyticallyUnramified S].TFAE

Tag 0334, a proposition

Tag 0334 in the Stacks Project.

isNagataRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/FiniteType.lean, line 478. The attribute's comment: “Items (1)-(3) as a List.TFAE. Nagata is IsNagataRing (032R(2)) and universally Japanese is IsUniversallyJapaneseRing (032R(1)); item (2), the condition the source's proof calls universally Nagata, is stated as the quantification over finite-type R-algebras rather than through a predicate of its own. See the module docstring.”. References: EGA IV (7.7.2), “a) <=> b)”; EGA IV (10.4.10), “more general”.

Nagata's theorem. For a ring R the following are equivalent: R is a Nagata ring; every finite-type R-algebra is a Nagata ring; R is universally Japanese and Noetherian.

In particular an algebra of finite type over a Nagata ring is a Nagata ring. Nagata is IsNagataRing and universally Japanese is IsUniversallyJapaneseRing, the two conditions of Definition 032R.

public theorem isNagataRing_tfae {R : Type u} [CommRing R] :
    List.TFAE
      [ IsNagataRing R,
        ∀ (S : Type u) [CommRing S] [Algebra R S] [Algebra.FiniteType R S], IsNagataRing S,
        IsUniversallyJapaneseRing R ∧ IsNoetherianRing R ]

Tag 0335, a proposition

Tag 0335 in the Stacks Project.

isNagataRing_field_and_int_and_isDedekindDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Examples.lean, line 128. The attribute's comment: “Items (1), (3) and (4) as one conjunction, since they share one proof; each is available separately as IsNagataRing.of_field, Int.isNagataRing and IsNagataRing.of_isDedekindDomain_of_charZero. Item (2) is Tag 032W and item (5) with the closing clause "and in particular universally Japanese" is Tag 0334, both tagged 0335 below. Nagata is IsNagataRing (032R(2)) and universally Japanese is IsUniversallyJapaneseRing (032R(1)). See the module docstring.”.

Fields, ℤ and Dedekind domains whose fraction field has characteristic zero are Nagata rings, hence in particular universally Japanese. These are items (1), (3) and (4) of the source, in its order; they share the one argument that inspects R ⧸ 𝔭 for each prime 𝔭.

The three classes on their own are IsNagataRing.of_field, Int.isNagataRing and IsNagataRing.of_isDedekindDomain_of_charZero, which is how they are applied; see the module docstring.

public theorem isNagataRing_field_and_int_and_isDedekindDomain :
    (∀ (K : Type u) [Field K], IsNagataRing K) ∧
    IsNagataRing ℤ ∧
    ∀ (R : Type u) [CommRing R] [IsDedekindDomain R] [CharZero R], IsNagataRing R

IsNagataRing.of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Examples.lean, line 138. The attribute's comment: “(1) Fields.”.

Stacks 0335 (1). A field is a Nagata ring, hence in particular universally Japanese: the only prime of a field K is 0, and K ⧸ 0 = K is N-2 because the integral closure of K in a finite extension L of K is L itself, a finite K-module.

public theorem IsNagataRing.of_field {K : Type u} [Field K] : IsNagataRing K

Int.isNagataRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Examples.lean, line 146. The attribute's comment: “(3) The ring ℤ.”. References: EGA IV (7.7.4), “in particular Z”; EGA IV (7.8.3), “(vi), special case”.

Stacks 0335 (3). The ring ℤ is a Nagata ring, hence in particular universally Japanese. This is the case R = ℤ of IsNagataRing.of_isDedekindDomain_of_charZero.

public theorem Int.isNagataRing : IsNagataRing ℤ

IsNagataRing.of_isDedekindDomain_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/Examples.lean, line 162. The attribute's comment: “(4) Dedekind domains with fraction field of characteristic zero, the latter read as CharZero R.”. References: EGA IV (7.7.4), “Dedekind char 0”; EGA IV (7.8.3), “(vi), special case”; EGA IV (7.8.4), “special case”.

Stacks 0335 (4). A Dedekind domain whose fraction field has characteristic zero is a Nagata ring, hence in particular universally Japanese. For a prime 𝔭 ≠ 0 the quotient R ⧸ 𝔭 is a field and so is N-2; for 𝔭 = 0 the quotient is R itself, which is N-1 because it is integrally closed, and N-1 implies N-2 in characteristic zero (Tag 032M).

The condition on the fraction field is stated as CharZero R, which for a domain R is equivalent since R → Frac R is injective. It cannot be dropped: a one-dimensional Noetherian integrally closed domain in characteristic p need not be N-2.

public theorem IsNagataRing.of_isDedekindDomain_of_charZero {R : Type u} [CommRing R]
    [IsDedekindDomain R] [CharZero R] : IsNagataRing R

Declarations registered for the tag:

• IsNagataRing.of_isPrecomplete_maximalIdeal, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Nagata/Examples.lean, line 170 (StacksFrontier): “(2) Noetherian complete local rings, which is Tag 032W.”.
• isNagataRing_tfae, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Nagata/Examples.lean, line 177 (StacksFrontier): “(5) Finite type ring extensions of any of the above, which is the implication (1) ⇒ (2) of Tag 0334, and the closing clause "and in particular universally Japanese", which is its implication (1) ⇒ (3).”.

Tag 09E2, a lemma

Tag 09E2 in the Stacks Project.

IsNagataRing.exists_pow_eq_iff_exists_pow_eq_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/PthRoot.lean, line 479. The attribute's comment: “Stated as a biconditional, the reverse implication being map_pow on the completion map. Noetherian is absorbed into IsNagataRing (Definition 032R(2)), primality of p into p ≠ 0 over a domain (CharP.char_is_prime_or_zero), and the characteristic of Frac A is read off A. The completion is AdicCompletion (maximalIdeal A) A as in Tag 032X.”.

Stacks Tag 09E2. Let (A, 𝔪) be a local domain which is a Nagata ring and has characteristic p ≠ 0, and let A^ = lim_n A ⧸ 𝔪ⁿ be its completion. An element a : A has a p-th root in A if and only if it has one in A^.

The source also assumes A Noetherian, which is the first conjunct of IsNagataRing A, and assumes p prime, which follows from p ≠ 0 because A is a domain. The source's characteristic assumption is on the fraction field of A; that is the same condition as CharP A p.

public theorem IsNagataRing.exists_pow_eq_iff_exists_pow_eq_adicCompletion {A : Type*}
    [CommRing A] [IsLocalRing A] [IsDomain A] (hA : IsNagataRing A) {p : ℕ} [CharP A p]
    (hp : p ≠ 0) (a : A) :
    (∃ b : A, b ^ p = a) ↔
      ∃ α : AdicCompletion (IsLocalRing.maximalIdeal A) A,
        α ^ p = algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A) a

Sources

• Section 10.162, Tag 032E
• AxiomMath/Stacks at 5ed82d14

LeanIsUniversallyJapaneseRing · IsNagataRing · IsIntegralClosure.finite_of_essFiniteType_of_isReduced · isUniversallyJapanese_of_finiteType_isN1 · isUniversallyJapanese_of_isEssentiallyOfFiniteType · isNagataRing_of_quasiFinite · isNagata_of_isLocalization · isUniversallyJapaneseRing_and_isNagataRing_of_localizationSpan

Section10.163 Ascending properties#

Section 10.163 of the Stacks Project, Tag 0336. 10 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0338, a lemma

Tag 0338 in the Stacks Project.

Module.depth_tensorProduct_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/FlatLocalHom.lean, line 814. The attribute's comment: “The fibre N/𝔪_R N has its depth taken over S along 𝔪_S rather than over S/𝔪_R S, which is the same value, and the tensor product is written with N on the left.”. References: EGA IV (6.3.1); EGA IV (6.3.1); EGA IV (6.3.4), “more general”; SGA 2 III (2.11), “special case”.

Depth is additive along a flat local homomorphism. Let R → S be a local homomorphism of Noetherian local rings, let M be a finite R-module and let N be a finite S-module flat over R. Then depth_S(N ⊗_R M) = depth_R(M) + depth_S(N/𝔪_R N).

public theorem depth_tensorProduct_of_flat {R S M N : Type*} [CommRing R] [CommRing S]
    [IsNoetherianRing R] [IsNoetherianRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [AddCommGroup M] [Module R M] [Module.Finite R M]
    [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] [Module.Finite S N]
    [Module.Flat R N] :
    depth S (maximalIdeal S) (N ⊗[R] M) = depth R (maximalIdeal R) M +
      depth S (maximalIdeal S)
        (N ⧸ ((maximalIdeal R).map (algebraMap R S) • (⊤ : Submodule S N)))

Tag 0337, a lemma

Tag 0337 in the Stacks Project.

Module.depth_self_eq_depth_self_add_depth_quotient_map_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/FlatLocalHom.lean, line 880. The attribute's comment: “Stated for Module.depth along the maximal ideals (Tag 00LI), with the fibre ring spelled as the S-module S ⧸ 𝔪_R S, of the same depth as the local ring S/𝔪_R S, and with IsNoetherianRing R dropped, being a consequence of faithful flatness. See the module docstring.”. References: EGA IV (6.3.1), “case M = R, N = S”; SGA 2 III (2.11), “M = A”.

Depth is additive along a flat local homomorphism. Let R → S be a flat local homomorphism of local rings with S Noetherian, with maximal ideals 𝔪_R and 𝔪_S. Then depth_{𝔪_S}(S) = depth_{𝔪_R}(R) + depth_{𝔪_S}(S/𝔪_R S), where 𝔪_R S is the ideal of S generated by the image of 𝔪_R. The depth of the fibre S/𝔪_R S is taken over S along 𝔪_S, which is its depth as a local ring in its own right.

public theorem depth_self_eq_depth_self_add_depth_quotient_map_maximalIdeal (R S : Type*)
    [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [Module.Flat R S] :
    depth S (IsLocalRing.maximalIdeal S) S =
      depth R (IsLocalRing.maximalIdeal R) R +
        depth S (IsLocalRing.maximalIdeal S)
          (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))

Tag 045J, a lemma

Tag 045J in the Stacks Project.

Module.isMaximalCohenMacaulay_self_iff_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/FlatLocalHom.lean, line 455. The attribute's comment: “Cohen-Macaulayness of a Noetherian local ring A (Definition 00N8) is Module.IsMaximalCohenMacaulay A A, i.e. depth_{𝔪_A}(A) = dim A; for the fibre that equation is written out, with its depth taken over S along 𝔪_S as in Tag 0337, since a quotient of a local ring carries no IsLocalRing instance. IsNoetherianRing R is dropped, being a consequence of faithful flatness. See the module docstring.”. References: EGA IV (6.3.5), “CM clauses of (i),(ii)”; EGA IV (15.4.2), “partial”; EGA IV (6.3.3), “Case M = A”.

Cohen–Macaulayness along a flat local homomorphism. Let R → S be a flat local homomorphism of local rings with S Noetherian. Then S is Cohen–Macaulay, that is depth_{𝔪_S}(S) = dim(S), if and only if R is Cohen–Macaulay and the fibre ring S/𝔪_R S is Cohen–Macaulay, the latter written as depth_{𝔪_S}(S/𝔪_R S) = dim(S/𝔪_R S) with the depth taken over S, which is the depth of S/𝔪_R S as a local ring in its own right.

public theorem isMaximalCohenMacaulay_self_iff_of_flat (R S : Type*) [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] [Module.Flat R S] :
    IsMaximalCohenMacaulay S S ↔
      IsMaximalCohenMacaulay R R ∧
        (depth S (IsLocalRing.maximalIdeal S)
              (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S)) : WithBot ℕ∞) =
          ringKrullDim (S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))

Tag 0339, a lemma

Tag 0339 in the Stacks Project.

min_le_depth_atPrime_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/FlatAscent.lean, line 872. The attribute's comment: “Property (S_k) is spelled out from Definition 031P as the inequality min{k, dim(A_𝔮)} ≤ depth(A_𝔮) at every prime, with Module.depth (Tag 00LI) along the maximal ideal of Localization.AtPrime 𝔮 and ringKrullDim for the dimension, as in Tags 031Q, 031S and 0352, the inequality being read in WithBot ℕ∞; the fibre ring S ⊗_R κ(𝔭) is Ideal.Fiber 𝔭 S, and the ring map is an Algebra R S instance with Module.Flat R S. See the module docstring.”. References: EGA IV (6.4.1), “(ii), affine E=O,F=O”; EGA IV (12.1.5), “(i), F=O_X, G=O_Y”.

Stacks Tag 0339. Let R → S be a flat ring map of Noetherian rings. If every fibre ring κ(𝔭) ⊗_R S has Serre's property (S_k) and R has (S_k), then S has (S_k), property (S_k) of a ring meaning that the depth of its localization at any prime is at least the minimum of k and the dimension of that localization. The inequalities are read in WithBot ℕ∞.

public theorem min_le_depth_atPrime_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [IsNoetherianRing R] [IsNoetherianRing S] [Module.Flat R S] {k : ℕ}
    (hfibre : ∀ (p : Ideal R) [p.IsPrime] (Q : Ideal (p.Fiber S)) [Q.IsPrime],
      min (k : WithBot ℕ∞) (ringKrullDim (Localization.AtPrime Q)) ≤
        (Module.depth (Localization.AtPrime Q)
          (IsLocalRing.maximalIdeal (Localization.AtPrime Q)) (Localization.AtPrime Q) :
            WithBot ℕ∞))
    (hR : ∀ (p : Ideal R) [p.IsPrime],
      min (k : WithBot ℕ∞) (ringKrullDim (Localization.AtPrime p)) ≤
        (Module.depth (Localization.AtPrime p)
          (IsLocalRing.maximalIdeal (Localization.AtPrime p)) (Localization.AtPrime p) :
            WithBot ℕ∞)) :
    ∀ (q : Ideal S) [q.IsPrime],
      min (k : WithBot ℕ∞) (ringKrullDim (Localization.AtPrime q)) ≤
        (Module.depth (Localization.AtPrime q)
          (IsLocalRing.maximalIdeal (Localization.AtPrime q)) (Localization.AtPrime q) :
            WithBot ℕ∞)

Tag 033A, a lemma

Tag 033A in the Stacks Project.

property_Rk_of_flat_of_fibre_of_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/FlatAscent.lean, line 371. References: EGA IV (6.5.3), “(ii), affine case”; EGA IV (17.5.8), “(iii)”; EGA IV (7.3.8), “(v_n), special case”; SGA 6 X (7.7), “special case”.

Let φ : R → S be a flat ring map between Noetherian rings and fix k ≥ 0. If every fibre ring S ⊗[R] κ(p) has property (R_k) and R has property (R_k), then S has property (R_k).

theorem property_Rk_of_flat_of_fibre_of_base
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] [Module.Flat R S]
    (k : ℕ)
    (hfib : ∀ (p : Ideal R) [p.IsPrime], HasPropertyRk (fibreRing R S p) k)
    (hR : HasPropertyRk R k) :
    HasPropertyRk S k

Tag 0C21, a lemma

Tag 0C21 in the Stacks Project.

isReduced_of_flat_of_isReduced_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/ReducedFibres.lean, line 143. The attribute's comment: “The ring map is an Algebra R S instance with Module.Flat R S, and the fibre ring S ⊗_R κ(𝔭) is Mathlib's Ideal.Fiber 𝔭 S, as in the statements of Tags 0339 and 033A. Reducedness is Mathlib's IsReduced, and the fibre hypothesis is reducedness, not geometric reducedness, so this is not an affine instance of Mathlib's AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian. See the module docstring.”. References: EGA IV (3.3.5), “affine case”; EGA IV (11.3.13), “(ii) reduced, Noetherian”.

Let R → S be a flat ring map of Noetherian rings. If R is reduced and every fibre ring κ(𝔭) ⊗_R S is reduced, then S is reduced.

public theorem isReduced_of_flat_of_isReduced_fiber {R : Type u} {S : Type v} [CommRing R]
    [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsNoetherianRing S] [Module.Flat R S]
    [IsReduced R] (hfibre : ∀ (p : Ideal R) [p.IsPrime], IsReduced (p.Fiber S)) :
    IsReduced S

Tag 033B, a lemma

Tag 033B in the Stacks Project.

Algebra.isReduced_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Reduced.lean, line 230. The attribute's comment: “The ring map is an Algebra R S instance and smoothness of it is Mathlib's Algebra.Smooth R S (equivalently (algebraMap R S).Smooth, by RingHom.smooth_algebraMap); reducedness is IsReduced. No Noetherian hypothesis, so this is not an instance of Mathlib's AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian. See the module docstring.”. References: SGA 1 II (3.1), “reduced, O_y ⇒ O_x”.

Stacks Tag 033B. Let R → S be a smooth ring map. If R is reduced, then S is reduced.

public theorem Algebra.isReduced_of_smooth (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.Smooth R S] [IsReduced R] : IsReduced S

Tag 0C22, a lemma

Tag 0C22 in the Stacks Project.

isNormalRing_of_flat_of_isNormalRing_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/NormalFibres.lean, line 395. The attribute's comment: “The ring map is an Algebra R S instance with Module.Flat R S, and the fibre ring S ⊗_R κ(𝔭) is Mathlib's Ideal.Fiber 𝔭 S, as in the companion statements 0C21 and 0339. Normality is the library's IsNormalRing (Definition 00GV), definitionally the IsDomain plus IsIntegrallyClosed condition on Localization.AtPrime 𝔮 that tags 030C(1), 031S and 033G write out, and the fibre hypothesis is normality, not geometric normality. Mathlib has neither a normal-ring predicate nor this ascent. See the module docstring.”. References: EGA IV (6.5.4), “(ii), affine case”; EGA IV (6.5.4), “(ii), affine case”.

Stacks Tag 0C22. Let R → S be a flat ring map of Noetherian rings. If R is a normal ring and every fibre ring κ(𝔭) ⊗_R S is a normal ring, then S is a normal ring.

public theorem isNormalRing_of_flat_of_isNormalRing_fiber {R : Type u} {S : Type v} [CommRing R]
    [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsNoetherianRing S] [Module.Flat R S]
    (hR : IsNormalRing R) (hfibre : ∀ (p : Ideal R) [p.IsPrime], IsNormalRing (p.Fiber S)) :
    IsNormalRing S

Tag 033C, a lemma

Tag 033C in the Stacks Project.

Algebra.isNormalRing_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Normal.lean, line 60. References: SGA 1 II (3.1), “normal, O_y ⇒ O_x”.

Stacks 033C. A smooth algebra over a normal ring is a normal ring.

theorem Algebra.isNormalRing_of_smooth (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.Smooth R S] (hR : IsNormalRing R) : IsNormalRing S

Tag 07NF, a lemma

Tag 07NF in the Stacks Project.

Algebra.isRegularRing_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/RegularRing.lean, line 189. The attribute's comment: “The ring map is an Algebra R S instance and smoothness of it is Mathlib's Algebra.Smooth R S (equivalently (algebraMap R S).Smooth, by RingHom.smooth_algebraMap), as in the companion statements 033B and 033C; regularity is Mathlib's IsRegularRing, Definition 00OD verbatim, which already contains Noetherianness, so the source's standing convention that a regular ring is Noetherian is carried by the predicate on both sides. Mathlib has the polynomial case and transport along ring equivalences, but no ascent along a smooth map. See the module docstring.”. References: SGA 1 II (3.1), “regular, O_y ⇒ O_x”.

Regularity ascends along smooth maps of rings (Stacks Tag 07NF). Let R → S be a smooth ring map. If R is a regular ring, then S is a regular ring.

public theorem Algebra.isRegularRing_of_smooth (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.Smooth R S] [IsRegularRing R] : IsRegularRing S

Sources

• Section 10.163, Tag 0336
• AxiomMath/Stacks at 5ed82d14

LeanModule.depth_tensorProduct_of_flat · Module.depth_self_eq_depth_self_add_depth_quotient_map_maximalIdeal · Module.isMaximalCohenMacaulay_self_iff_of_flat · min_le_depth_atPrime_of_flat · property_Rk_of_flat_of_fibre_of_base · isReduced_of_flat_of_isReduced_fiber · Algebra.isReduced_of_smooth · isNormalRing_of_flat_of_isNormalRing_fiber

Section10.164 Descending properties#

Section 10.164 of the Stacks Project, Tag 033D. 7 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 033E, a lemma

Tag 033E in the Stacks Project.

descent_noetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 300. References: EGA 0 (6.5.2), “special case”; EGA IV (2.2.14), “affine source and target”.

Stacks 033E. If φ : R → S is faithfully flat and S is Noetherian, then R is Noetherian.

theorem descent_noetherian {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    (hφ : φ.FaithfullyFlat) (hS : IsNoetherianRing S) : IsNoetherianRing R

Tag 033F, a lemma

Tag 033F in the Stacks Project.

RingHom.FaithfullyFlat.isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/FaithfullyFlat/Descent.lean, line 309. References: EGA IV (11.3.13), “(i), reduced case”.

Stacks 033F. If φ : R → S is a faithfully flat ring map and S is reduced, then R is reduced.

theorem RingHom.FaithfullyFlat.isReduced {R S : Type*} [CommRing R] [CommRing S] {φ : R →+* S}
    (hφ : φ.FaithfullyFlat) [IsReduced S] : IsReduced R

Tag 033G, a lemma

Tag 033G in the Stacks Project.

isDomain_and_isIntegrallyClosed_atPrime_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegrallyClosed/FaithfullyFlatDescent.lean, line 232. The attribute's comment: “Normality is inlined as IsDomain plus IsIntegrallyClosed on Localization.AtPrime 𝔭 for every prime 𝔭, as in item (1) of tag 030C and in tag 031S, Mathlib having no predicate for a normal ring; the ring map R → S is an Algebra R S instance and its faithful flatness is Module.FaithfullyFlat R S. See the module docstring.”. References: EGA IV (6.5.4), “(i), affine case”; EGA IV (2.1.13), “special case”; EGA IV (7.5.3), “(vi)”.

Stacks 033G. Let R → S be a faithfully flat ring map. If S is a normal ring, i.e. all its localizations at primes are normal domains, then so is R.

public theorem isDomain_and_isIntegrallyClosed_atPrime_of_faithfullyFlat {R : Type*} [CommRing R]
    {S : Type*} [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
    (hS : ∀ (q : Ideal S) [q.IsPrime],
      IsDomain (Localization.AtPrime q) ∧ IsIntegrallyClosed (Localization.AtPrime q)) :
    ∀ (p : Ideal R) [p.IsPrime],
      IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)

Tag 07NG, a lemma

Tag 07NG in the Stacks Project.

IsRegularRing.of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RegularRing/FaithfullyFlatDescent.lean, line 173. The attribute's comment: “The source's "regular ring" is Mathlib's class IsRegularRing (Definition 00OD), which already includes Noetherianness, so the Noetherianness of R that the source derives from Lemma 033E is part of the conclusion; the ring map R → S is an Algebra R S instance and its faithful flatness is Module.FaithfullyFlat R S, equal to (algebraMap R S).FaithfullyFlat by RingHom.faithfullyFlat_algebraMap_iff. See the module docstring.”.

Regularity descends along a faithfully flat ring map (Stacks 07NG). Let R → S be a ring map. If it is faithfully flat and S is a regular ring, then R is a regular ring.

public theorem IsRegularRing.of_faithfullyFlat {R : Type u} (S : Type v) [CommRing R] [CommRing S]
    [Algebra R S] [Module.FaithfullyFlat R S] [IsRegularRing S] : IsRegularRing R

Tag 0352, a lemma

Tag 0352 in the Stacks Project.

isNoetherianRing_and_min_le_depth_atPrime_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/FaithfullyFlatDescent.lean, line 332. The attribute's comment: “Property (S_k) is spelled out from Definition 031P as the inequality min{k, dim(R_𝔭)} ≤ depth(R_𝔭) at every prime, with Module.depth (tag 00LI) along the maximal ideal of Localization.AtPrime 𝔭 and ringKrullDim for the dimension, as in tags 031Q and 031S, the inequality being read in WithBot ℕ∞; the ring map R → S is an Algebra R S instance and its faithful flatness is Module.FaithfullyFlat R S. See the module docstring.”. References: EGA IV (6.4.1), “(i), affine E=O,F=O”.

Stacks Tag 0352. Let R → S be a ring map. If it is faithfully flat and S is Noetherian with property (S_k) — the depth of S_𝔮 is at least min{k, dim(S_𝔮)} for every prime 𝔮 — then R is Noetherian and has property (S_k). The depth inequalities are read in WithBot ℕ∞.

public theorem isNoetherianRing_and_min_le_depth_atPrime_of_faithfullyFlat
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [Module.FaithfullyFlat R S] [IsNoetherianRing S] {k : ℕ}
    (hS : ∀ (q : Ideal S) [q.IsPrime],
      min (k : WithBot ℕ∞) (ringKrullDim (Localization.AtPrime q)) ≤
        (Module.depth (Localization.AtPrime q)
          (IsLocalRing.maximalIdeal (Localization.AtPrime q)) (Localization.AtPrime q) :
            WithBot ℕ∞)) :
    IsNoetherianRing R ∧
      ∀ (p : Ideal R) [p.IsPrime],
        min (k : WithBot ℕ∞) (ringKrullDim (Localization.AtPrime p)) ≤
          (Module.depth (Localization.AtPrime p)
            (IsLocalRing.maximalIdeal (Localization.AtPrime p)) (Localization.AtPrime p) :
              WithBot ℕ∞)

Tag 0353, a lemma

Tag 0353 in the Stacks Project.

isNoetherianRing_and_isRegularLocalRing_atPrime_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/FaithfullyFlatDescent.lean, line 544. The attribute's comment: “Property (R_k) is spelled out from Definition 031P as the implication height 𝔭 ≤ k → IsRegularLocalRing (Localization.AtPrime 𝔭), with Ideal.height and IsRegularLocalRing, as in tag 031S; the source's dim(R_𝔭) ≤ k is Ideal.height 𝔭 ≤ k by IsLocalization.AtPrime.ringKrullDim_eq_height. The bound k is generalized from a non-negative integer to an element of ℕ∞, whose top value recovers tag 07NG. The ring map R → S is an Algebra R S instance and its faithful flatness is Module.FaithfullyFlat R S. See the module docstring.”. References: EGA IV (6.5.3), “(i), affine case”.

Stacks Tag 0353. Let R → S be a ring map. If it is faithfully flat and S is Noetherian with property (R_k) — the local ring S_𝔮 is regular for every prime 𝔮 of height at most k — then R is Noetherian and has property (R_k). The bound k ranges over ℕ∞, the value ⊤ giving the descent of regularity itself (tag 07NG).

public theorem isNoetherianRing_and_isRegularLocalRing_atPrime_of_faithfullyFlat
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [Module.FaithfullyFlat R S] [IsNoetherianRing S] {k : ℕ∞}
    (hS : ∀ (q : Ideal S) [q.IsPrime], q.height ≤ k →
      IsRegularLocalRing (Localization.AtPrime q)) :
    IsNoetherianRing R ∧
      ∀ (p : Ideal R) [p.IsPrime], p.height ≤ k →
        IsRegularLocalRing (Localization.AtPrime p)

Tag 0354, a lemma

Tag 0354 in the Stacks Project.

IsNagataRing.of_smooth_of_comap_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Nagata/SmoothDescent.lean, line 266. The attribute's comment: “Smoothness of the ring map R → S is Algebra.Smooth R S (Definition 00T2) for an Algebra R S instance, and surjectivity on spectra is surjectivity of PrimeSpectrum.comap (algebraMap R S); the pair is equivalent to smooth plus Module.FaithfullyFlat R S. Nagata is IsNagataRing of Definition 032R(2), whose Noetherian clause is part of the conclusion rather than a hypothesis on R. See the module docstring.”.

Stacks Tag 0354. Let R → S be a ring map. If it is smooth and the induced map Spec S → Spec R is surjective, and S is a Nagata ring — Noetherian, with every quotient S ⧸ q by a prime N-2 — then R is a Nagata ring.

Smoothness is Algebra.Smooth (Definition 00T2), and together with surjectivity on spectra it is equivalent to R → S being smooth and faithfully flat, by Algebra.Smooth.flat and Module.FaithfullyFlat.of_comap_surjective.

public theorem IsNagataRing.of_smooth_of_comap_surjective {R S : Type u} [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.Smooth R S]
    (hsurj : Function.Surjective (PrimeSpectrum.comap (algebraMap R S)))
    (hS : IsNagataRing S) : IsNagataRing R

Sources

• Section 10.164, Tag 033D
• AxiomMath/Stacks at 5ed82d14

Leandescent_noetherian · RingHom.FaithfullyFlat.isReduced · isDomain_and_isIntegrallyClosed_atPrime_of_faithfullyFlat · IsRegularRing.of_faithfullyFlat · isNoetherianRing_and_min_le_depth_atPrime_of_faithfullyFlat · isNoetherianRing_and_isRegularLocalRing_atPrime_of_faithfullyFlat · IsNagataRing.of_smooth_of_comap_surjective

Section10.165 Geometrically normal algebras#

Section 10.165 of the Stacks Project, Tag 037Y. 6 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 037Z, a lemma

Tag 037Z in the Stacks Project.

Algebra.isNormalRing_tensorProduct_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyNormal/TFAE.lean, line 608. The attribute's comment: “The source's four conditions in its order, with a normal ring spelled by the library's IsNormalRing (Definition 00GV), a finitely generated field extension by Algebra.EssFiniteType, and the perfect closure taken abstractly, as IsPerfectClosure.”.

Stacks 037Z. Let k be a field of exponential characteristic p and let A be a commutative k-algebra. The following are equivalent: (1) k' ⊗[k] A is a normal ring for every field extension k'/k; (2) k' ⊗[k] A is a normal ring for every finitely generated field extension k'/k; (3) k' ⊗[k] A is a normal ring for every finite purely inseparable extension k'/k; (4) k^{perf} ⊗[k] A is a normal ring, for a perfect closure k^{perf} of k.

public theorem isNormalRing_tensorProduct_tfae
    (k : Type u) [Field k] (p : ℕ) [ExpChar k p] (A : Type v) [CommRing A] [Algebra k A]
    (kperf : Type w) [Field kperf] [Algebra k kperf] [ExpChar kperf p] [PerfectRing kperf p]
    [IsPerfectClosure (algebraMap k kperf) p] :
    [∀ (k' : Type u) [Field k'] [Algebra k k'], IsNormalRing (k' ⊗[k] A),
      ∀ (k' : Type u) [Field k'] [Algebra k k'] [EssFiniteType k k'],
        IsNormalRing (k' ⊗[k] A),
      ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
        [IsPurelyInseparable k k'], IsNormalRing (k' ⊗[k] A),
      IsNormalRing (kperf ⊗[k] A)].TFAE

Tag 0380, a definition

Tag 0380 in the Stacks Project.

Algebra.IsGeometricallyNormal, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyNormal/Defs.lean, line 111. The attribute's comment: “The first of the four equivalent conditions of Lemma 037Z, a normal ring being spelled by the library's IsNormalRing (Definition 00GV); the other three are criteria for it, through Algebra.isNormalRing_tensorProduct_tfae.”. References: EGA IV (6.7.6).

A commutative algebra A over a field k is geometrically normal over k if the base change k' ⊗[k] A is a normal ring for every field extension k'/k. By Lemma 037Z it is enough to ask this for the finitely generated extensions, or for the finite purely inseparable ones, or for a single perfect closure of k.

public class IsGeometricallyNormal (k : Type u) (A : Type v) [Field k] [CommRing A]
    [Algebra k A] : Prop

Tag 06DE, a lemma

Tag 06DE in the Stacks Project.

Algebra.IsGeometricallyNormal.of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyNormal/Localization.lean, line 81. The attribute's comment: “The source's S⁻¹A is spelled abstractly as an A-algebra A' with IsLocalization S A' and IsScalarTower k A A', so that the fraction field of a domain and the localizations at primes are instances of the statement rather than transports of it.”.

A localization of a geometrically normal algebra over a field is geometrically normal: if A is geometrically normal over the field k and A' is the localization of A at a submonoid S ⊆ A, regarded as a k-algebra through A, then A' is geometrically normal over k.

public theorem IsGeometricallyNormal.of_isLocalization {k : Type u} {A : Type v} {A' : Type w}
    [Field k] [CommRing A] [CommRing A'] [Algebra k A] [Algebra k A'] [Algebra A A']
    [IsScalarTower k A A'] [IsGeometricallyNormal k A] (S : Submonoid A) [IsLocalization S A'] :
    IsGeometricallyNormal k A'

Tag 0C30, a lemma

Tag 0C30 in the Stacks Project.

Algebra.IsGeometricallyNormal.of_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyNormal/Separable.lean, line 216. The attribute's comment: “Separability is the source's Definition 030O (2), Algebra.IsSeparableExtension, which does not require K/k algebraic, and not Mathlib's Algebra.IsSeparable; the converse implication is Proposition 0322 and is not part of this tag.”. References: EGA IV (6.7.6), “separable ⇒ geom normal”.

A separable field extension is geometrically normal: if K/k is a field extension all of whose finitely generated subextensions are separably generated (Definition 030O (2)), then k' ⊗[k] K is a normal ring for every field extension k'/k.

public theorem IsGeometricallyNormal.of_isSeparableExtension {k K : Type*} [Field k] [Field K]
    [Algebra k K] [IsSeparableExtension k K] : IsGeometricallyNormal k K

Tag 06DF, a lemma

Tag 06DF in the Stacks Project.

Algebra.IsGeometricallyNormal.isNormalRing_tensorProduct_of_isNormalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyNormal/TensorProduct.lean, line 468. References: EGA IV (21.14.4), “special case”.

Stacks 06DF. The tensor product over a field k of a geometrically normal k-algebra and a normal k-algebra is a normal ring.

theorem Algebra.IsGeometricallyNormal.isNormalRing_tensorProduct_of_isNormalRing (k : Type u)
    (A : Type v) (B : Type w) [Field k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B]
    [Algebra.IsGeometricallyNormal k A] (hB : IsNormalRing B) : IsNormalRing (A ⊗[k] B)

Tag 0C31, a lemma

Tag 0C31 in the Stacks Project.

Algebra.isGeometricallyNormal_iff_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyNormal/Separable.lean, line 228. The attribute's comment: “Separable algebraic is Mathlib's Algebra.IsSeparable k k', which includes algebraicity; the k-algebra structure of A is the restriction of its k'-algebra structure.”.

Stacks 0C31. For a separable algebraic field extension k'/k, a k'-algebra A is geometrically normal over k if and only if it is geometrically normal over k'. Both directions are tested on finite purely inseparable extensions L (Lemma 037Z). Over k', the ring L ⊗[k'] A is a localization of L ⊗[k] A (Lemma 0C2X). Over k, the ring k' ⊗[k] L is a field and L ⊗[k] A = (k' ⊗[k] L) ⊗[k'] A.

public theorem isGeometricallyNormal_iff_of_isSeparable (k k' A : Type*) [Field k] [Field k']
    [CommRing A] [Algebra k k'] [Algebra k A] [Algebra k' A] [IsScalarTower k k' A]
    [Algebra.IsSeparable k k'] : IsGeometricallyNormal k A ↔ IsGeometricallyNormal k' A

Sources

• Section 10.165, Tag 037Y
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.isNormalRing_tensorProduct_tfae · Algebra.IsGeometricallyNormal · Algebra.IsGeometricallyNormal.of_isLocalization · Algebra.IsGeometricallyNormal.of_isSeparableExtension · Algebra.IsGeometricallyNormal.isNormalRing_tensorProduct_of_isNormalRing · Algebra.isGeometricallyNormal_iff_of_isSeparable

Section10.166 Geometrically regular algebras#

Section 10.166 of the Stacks Project, Tag 045K. 6 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0381, a lemma

Tag 0381 in the Stacks Project.

Algebra.forall_isRegularRing_tensorProduct_essFiniteType_iff_finite_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FieldExtension.lean, line 160. The attribute's comment: “Regular ring is Definition 00OD, that is Mathlib's IsRegularRing, which already contains Noetherianness; a finitely generated field extension is Algebra.EssFiniteType (IntermediateField.fg_top_iff) and a finite purely inseparable one is Module.Finite together with IsPurelyInseparable. The source's hypothesis that A be Noetherian is not assumed: it is implied by either side, since A ≃ₐ[k] k ⊗[k] A. The extension fields range over a single free universe, w := u giving the source's statement in full. See the module docstring.”. References: EGA 0 (22.5.8), “b) ⇔ b')”; EGA IV (6.7.7), “(b) ⇔ (c), special case”.

Regularity of all base changes to finitely generated field extensions is detected by the finite purely inseparable ones. Let k be a field and A a k-algebra. Then K ⊗[k] A is a regular ring (Definition 00OD) for every finitely generated field extension K/k if and only if k' ⊗[k] A is a regular ring for every finite purely inseparable extension k'/k.

public theorem forall_isRegularRing_tensorProduct_essFiniteType_iff_finite_isPurelyInseparable
    (k : Type u) (A : Type v) [Field k] [CommRing A] [Algebra k A] :
    (∀ (K : Type w) [Field K] [Algebra k K] [Algebra.EssFiniteType k K],
        IsRegularRing (K ⊗[k] A)) ↔
      ∀ (K : Type w) [Field K] [Algebra k K] [Module.Finite k K] [IsPurelyInseparable k K],
        IsRegularRing (K ⊗[k] A)

Tag 0382, a definition

Tag 0382 in the Stacks Project.

Algebra.IsGeometricallyRegular, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/Defs.lean, line 140. The attribute's comment: “Stated as condition (1) of Lemma 0381; condition (2) follows by instance resolution and the converse is that lemma. Regular ring is Definition 00OD, that is Mathlib's IsRegularRing, which already contains Noetherianness, so the source's hypothesis that R be Noetherian is not assumed but implied (take K := k). A finitely generated field extension is Algebra.EssFiniteType (IntermediateField.essFiniteType_iff), and the test field ranges over the universe of k, which is the source's condition for extensions in every universe. See the module docstring.”. References: EGA IV (6.7.6).

A k-algebra R over a field k is geometrically regular over k if K ⊗[k] R is a regular ring (Definition 00OD) for every finitely generated field extension K/k. By Lemma 0381 it is enough to require this for the finite purely inseparable extensions k'/k.

public class IsGeometricallyRegular (k : Type u) (R : Type v) [Field k] [CommRing R]
    [Algebra k R] : Prop

Tag 07NH, a lemma

Tag 07NH in the Stacks Project.

Algebra.IsGeometricallyRegular.of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/FaithfullyFlatDescent.lean, line 79. The attribute's comment: “The source's faithfully flat k-algebra map A → B is Algebra A B with IsScalarTower k A B and Module.FaithfullyFlat A B, the latter being (algebraMap A B).FaithfullyFlat by RingHom.faithfullyFlat_algebraMap_iff; geometric regularity is Algebra.IsGeometricallyRegular (Definition 0382), which already implies the Noetherianness the source assumes. Named after the sibling 07NG, IsRegularRing.of_faithfullyFlat. See the module docstring.”.

Geometric regularity descends through faithfully flat maps of algebras. Let k be a field and let A → B be a faithfully flat map of k-algebras. If B is geometrically regular over k, then so is A.

public theorem IsGeometricallyRegular.of_faithfullyFlat {k : Type u} {A : Type v} (B : Type w)
    [Field k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B]
    [IsScalarTower k A B] [Module.FaithfullyFlat A B] [IsGeometricallyRegular k B] :
    IsGeometricallyRegular k A

Tag 07QF, a lemma

Tag 07QF in the Stacks Project.

Algebra.IsGeometricallyRegular.of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/Smooth.lean, line 89. The attribute's comment: “The source's smooth k-algebra map A → B is Algebra A B with IsScalarTower k A B and Algebra.Smooth A B, the latter being (algebraMap A B).Smooth by RingHom.smooth_algebraMap and being Definition 00T2 by Proposition 00TN; geometric regularity is Algebra.IsGeometricallyRegular (Definition 0382), which already implies the Noetherianness Definition 0382 assumes. Named after the sibling 07NH, IsGeometricallyRegular.of_faithfullyFlat. See the module docstring.”.

Geometric regularity ascends along smooth maps of algebras. Let k be a field and let A → B be a smooth map of k-algebras. If A is geometrically regular over k, then so is B.

public theorem IsGeometricallyRegular.of_smooth {k : Type u} (A : Type v) {B : Type w}
    [Field k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [Algebra A B]
    [IsScalarTower k A B] [Algebra.Smooth A B] [IsGeometricallyRegular k A] :
    IsGeometricallyRegular k B

Tag 07QG, a lemma

Tag 07QG in the Stacks Project.

Algebra.IsGeometricallyRegular.of_directed_of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/Colimit.lean, line 171. The attribute's comment: “The source's k = colim k_i over subfields is a directed family t : ι → Subfield k with ⨆ i, t i = ⊤, equivalently (Subfield.mem_iSup_of_directed) every element of k lying in some t i; Nonempty ι is necessary, since for ι empty and k a prime field the supremum is ⊤ and the hypothesis vacuous. A is a t i-algebra by restriction of scalars along t i ↪ k (IsScalarTower ↥(t i) k A), and geometric regularity is Algebra.IsGeometricallyRegular (Definition 0382), which already implies the Noetherianness Definition 0382 assumes. See the module docstring.”.

Let k be a field, A a k-algebra, and let t : ι → Subfield k be a nonempty directed family of subfields of k with ⨆ i, t i = ⊤, that is, k = colim (t i). If A is geometrically regular over every t i, then A is geometrically regular over k.

public theorem IsGeometricallyRegular.of_directed_of_iSup_eq_top {k : Type u} {A : Type v}
    {ι : Type w} [Nonempty ι] [Field k] [CommRing A] [Algebra k A] (t : ι → Subfield k)
    (dir : Directed (· ≤ ·) t) (htop : ⨆ i, t i = ⊤)
    [∀ i, IsGeometricallyRegular (t i) A] :
    IsGeometricallyRegular k A

Tag 07QH, a lemma

Tag 07QH in the Stacks Project.

Algebra.isGeometricallyRegular_iff_tower_top_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyRegular/BaseFieldExtension.lean, line 219. The attribute's comment: “The source's separable algebraic extension k'/k is Algebra.IsSeparable k k', which already contains algebraicity (Algebra.IsSeparable.isAlgebraic); no finiteness is assumed, the reduction to the finite case being internal to the proof (Lemma 07QG). A being an algebra over k' and over k at once is IsScalarTower k k' A, which pins the k-structure to be the restriction of the k'-structure. Geometric regularity is Algebra.IsGeometricallyRegular (Definition 0382), which already implies the Noetherianness Definition 0382 assumes. Named after Mathlib's Algebra.isSeparable_tower_top_of_isSeparable, tower_top naming the right-hand side. See the module docstring.”.

Let k'/k be a separable algebraic field extension and let A be a k'-algebra, viewed as a k-algebra by restriction of scalars. Then A is geometrically regular over k if and only if it is geometrically regular over k'.

public theorem isGeometricallyRegular_iff_tower_top_of_isSeparable (k : Type u) (k' : Type v)
    (A : Type w) [Field k] [Field k'] [CommRing A] [Algebra k k'] [Algebra k A] [Algebra k' A]
    [IsScalarTower k k' A] [Algebra.IsSeparable k k'] :
    IsGeometricallyRegular k A ↔ IsGeometricallyRegular k' A

Sources

• Section 10.166, Tag 045K
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.forall_isRegularRing_tensorProduct_essFiniteType_iff_finite_isPurelyInseparable · Algebra.IsGeometricallyRegular · Algebra.IsGeometricallyRegular.of_faithfullyFlat · Algebra.IsGeometricallyRegular.of_smooth · Algebra.IsGeometricallyRegular.of_directed_of_iSup_eq_top · Algebra.isGeometricallyRegular_iff_tower_top_of_isSeparable

Section10.167 Geometrically Cohen-Macaulay algebras#

Section 10.167 of the Stacks Project, Tag 045L. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 045M, a lemma

Tag 045M in the Stacks Project.

Algebra.TensorProduct.isNoetherianRing_and_isCohenMacaulay_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/FieldExtension.lean, line 403. The attribute's comment: “Finite generation of a field extension is Algebra.EssFiniteType (IntermediateField.fg_top_iff), and "one of them" is the disjunction h. Cohen-Macaulayness of the ring (Definition 00NC) is Module.IsCohenMacaulay R R for R = K ⊗[k] L, the notion of tag 0AAH for R over itself, which at each prime is Cohen-Macaulayness of R_𝔭. See the module docstring.”. References: EGA IV (6.7.1.1).

Stacks 045M. Let k be a field and let K/k and L/k be field extensions one of which is of finite type as a field extension. Then K ⊗[k] L is a Noetherian Cohen–Macaulay ring.

public theorem Algebra.TensorProduct.isNoetherianRing_and_isCohenMacaulay_of_essFiniteType
    (k K L : Type*) [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L]
    (h : Algebra.EssFiniteType k K ∨ Algebra.EssFiniteType k L) :
    IsNoetherianRing (K ⊗[k] L) ∧ Module.IsCohenMacaulay (K ⊗[k] L) (K ⊗[k] L)

Tag 045N, a lemma

Tag 045N in the Stacks Project.

Algebra.TensorProduct.isMaximalCohenMacaulay_self_iff_of_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/FieldExtension.lean, line 772. The attribute's comment: “Cohen-Macaulayness of a Noetherian local ring (Definition 00N8) is Module.IsMaximalCohenMacaulay A A (Tag 00NF); finite generation of the field extension is Algebra.EssFiniteType k K (IntermediateField.fg_top_iff), as in Tag 045M; both localisations are abstract IsLocalization.AtPrimes as in Tag 00ND; lying over is contraction along Algebra.TensorProduct.includeRight, there being no Algebra S (K ⊗[k] S) instance; and IsNoetherianRing (K ⊗[k] S) is not assumed, being a consequence by Tag 045I. See the module docstring.”. References: EGA IV (6.7.1), “(i), CM, affine”; EGA IV (6.7.1.1), “more general”.

Stacks 045N. Let k be a field, S a Noetherian k-algebra and K/k a finitely generated field extension. Let 𝔮 ⊆ S be a prime and let 𝔮_K ⊆ K ⊗[k] S be a prime lying over it along s ↦ 1 ⊗ s. Then the local ring S_𝔮 is Cohen–Macaulay, that is depth_{𝔪}(S_𝔮) = dim S_𝔮, if and only if the local ring (K ⊗[k] S)_{𝔮_K} is.

public theorem Algebra.TensorProduct.isMaximalCohenMacaulay_self_iff_of_essFiniteType
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [IsNoetherianRing S]
    {K : Type*} [Field K] [Algebra k K] [Algebra.EssFiniteType k K]
    (q : Ideal S) [q.IsPrime] (qK : Ideal (K ⊗[k] S)) [qK.IsPrime]
    (hqK : q = qK.comap Algebra.TensorProduct.includeRight.toRingHom)
    (Sq : Type*) [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q] [IsLocalRing Sq]
    (SKqK : Type*) [CommRing SKqK] [Algebra (K ⊗[k] S) SKqK]
    [IsLocalization.AtPrime SKqK qK] [IsLocalRing SKqK] :
    Module.IsMaximalCohenMacaulay Sq Sq ↔ Module.IsMaximalCohenMacaulay SKqK SKqK

Sources

• Section 10.167, Tag 045L
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.TensorProduct.isNoetherianRing_and_isCohenMacaulay_of_essFiniteType · Algebra.TensorProduct.isMaximalCohenMacaulay_self_iff_of_essFiniteType

Section10.168 Colimits and maps of finite presentation, II#

Section 10.168 of the Stacks Project, Tag 07RF. 10 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02JO, a lemma

Tag 02JO in the Stacks Project.

Module.Flat.eventually_flat_of_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/FlatModel/DirectedModel.lean, line 786. The attribute's comment: “(3)”. References: EGA IV (11.2.6), “affine case, (ii)”; EGA IV (11.2.6.1), “(ii) necessity”.

Stacks 02JO (3). Let R → S be of finite presentation and let M be a finitely presented S-module which is flat over R. Let (R → S, M) = colim_λ (R_λ → S_λ, M_λ) be a directed colimit such that R_μ ⊗_{R_λ} S_λ → S_μ and S_μ ⊗_{S_λ} M_λ → M_μ are isomorphisms for μ ≥ λ, each R_λ → S_λ is of finite presentation and each M_λ is a finitely presented S_λ-module. Then M_λ is flat over R_λ for all sufficiently large λ.

theorem Module.Flat.eventually_flat_of_directed {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.FinitePresentation R S] (M : Type w) [AddCommGroup M] [Module R M]
    [Module S M] [IsScalarTower R S M] [Module.FinitePresentation S M] [Module.Flat R M]
    {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
    {A B : ι → Type v} [∀ i, CommRing (A i)] [∀ i, CommRing (B i)] [∀ i, Algebra (A i) (B i)]
    {N : ι → Type*} [∀ i, AddCommGroup (N i)] [∀ i, Module (B i) (N i)]
    (a : ∀ i j, i ≤ j → A i →+* A j) (b : ∀ i j, i ≤ j → B i →+* B j)
    (n : ∀ i j (h : i ≤ j), N i →ₛₗ[b i j h] N j)
    [DirectedSystem A fun i j h => a i j h] [DirectedSystem B fun i j h => b i j h]
    [DirectedSystem N fun i j h => n i j h]
    (hab : ∀ i j (h : i ≤ j),
      (b i j h).comp (algebraMap (A i) (B i)) = (algebraMap (A j) (B j)).comp (a i j h))
    (ρ : ∀ i, A i →+* R) (σ : ∀ i, B i →+* S) (ν : ∀ i, N i →ₛₗ[σ i] M)
    (hρ : ∀ i j (h : i ≤ j) x, ρ j (a i j h x) = ρ i x)
    (hσ : ∀ i j (h : i ≤ j) x, σ j (b i j h x) = σ i x)
    (hν : ∀ i j (h : i ≤ j) x, ν j (n i j h x) = ν i x)
    (hρσ : ∀ i, (σ i).comp (algebraMap (A i) (B i)) = (algebraMap R S).comp (ρ i))
    (hρs : ∀ r, ∃ i x, ρ i x = r) (hρz : ∀ i x, ρ i x = 0 → ∃ j, ∃ h : i ≤ j, a i j h x = 0)
    (hσs : ∀ s, ∃ i x, σ i x = s) (hσz : ∀ i x, σ i x = 0 → ∃ j, ∃ h : i ≤ j, b i j h x = 0)
    (hνs : ∀ m, ∃ i x, ν i x = m) (hνz : ∀ i x, ν i x = 0 → ∃ j, ∃ h : i ≤ j, n i j h x = 0)
    (hpush : ∀ i j (h : i ≤ j), CategoryTheory.IsPushout (CommRingCat.ofHom (a i j h))
      (CommRingCat.ofHom (algebraMap (A i) (B i))) (CommRingCat.ofHom (algebraMap (A j) (B j)))
      (CommRingCat.ofHom (b i j h)))
    (hbc : ∀ i j (h : i ≤ j), letI := algebraB b h
      letI := Module.compHom (N j) (b i j h)
      haveI : IsScalarTower (B i) (B j) (N j) := .of_algebraMap_smul fun _ _ => rfl
      IsBaseChange (B j) (transLinear b n h))
    (hfp : ∀ i, Algebra.FinitePresentation (A i) (B i))
    (hfpN : ∀ i, Module.FinitePresentation (B i) (N i)) :
    ∃ i, ∀ j, i ≤ j →
      letI := Module.compHom (N j) (algebraMap (A j) (B j)); Module.Flat (A j) (N j)

Module.Flat.exists_finiteType_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/FlatModel/FiniteTypeModel.lean, line 254. The attribute's comment: “(1)”.

Stacks 02JO (1). Let R → S be of finite presentation and let M be a finitely presented S-module which is flat over R. Then there are a ring R₀ of finite type over ℤ, an R₀-algebra S₀ of finite type and a finite S₀-module M₀ flat over R₀, together with ring maps R₀ → R, S₀ → S and an S₀-linear map M₀ → M, such that S = R ⊗_{R₀} S₀ and M = S ⊗_{S₀} M₀.

theorem Module.Flat.exists_finiteType_model {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.FinitePresentation R S] (M : Type w) [AddCommGroup M] [Module R M]
    [Module S M] [IsScalarTower R S M] [Module.FinitePresentation S M] [Module.Flat R M] :
    ∃ (R₀ S₀ M₀ : Type u) (_ : CommRing R₀) (_ : CommRing S₀) (_ : Algebra R₀ S₀)
      (_ : Algebra R₀ R) (_ : Algebra S₀ S) (_ : Algebra R₀ S) (_ : IsScalarTower R₀ R S)
      (_ : IsScalarTower R₀ S₀ S) (_ : AddCommGroup M₀) (_ : Module S₀ M₀) (_ : Module R₀ M₀)
      (_ : IsScalarTower R₀ S₀ M₀) (_ : Module S₀ M) (_ : IsScalarTower S₀ S M)
      (f : M₀ →ₗ[S₀] M),
      Algebra.FiniteType ℤ R₀ ∧ Algebra.FiniteType R₀ S₀ ∧ Module.Finite S₀ M₀ ∧
        Module.Flat R₀ M₀ ∧ Algebra.IsPushout R₀ R S₀ S ∧ IsBaseChange S f

Module.Flat.exists_finitePresentation_model_of_directed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/FlatModel/FiniteTypeModel.lean, line 288. The attribute's comment: “(2)”. References: EGA IV (1.8.4.2).

Stacks 02JO (2). Let R → S be of finite presentation and let M be a finitely presented S-module which is flat over R. If R = colim_λ R_λ is a directed colimit, then there are λ, an R_λ-algebra S_λ of finite presentation and a finitely presented S_λ-module M_λ which is flat over R_λ, with an algebra map S_λ → S and an S_λ-linear map M_λ → M exhibiting S = R ⊗_{R_λ} S_λ and M = S ⊗_{S_λ} M_λ.

theorem Module.Flat.exists_finitePresentation_model_of_directed {R S : Type u} [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] (M : Type w) [AddCommGroup M]
    [Module R M] [Module S M] [IsScalarTower R S M] [Module.FinitePresentation S M]
    [Module.Flat R M] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
    {A : ι → Type v} [∀ i, CommRing (A i)] (a : ∀ i j, i ≤ j → A i →+* A j)
    [DirectedSystem A fun i j h => a i j h] (ρ : ∀ i, A i →+* R)
    (hρ : ∀ i j (h : i ≤ j) x, ρ j (a i j h x) = ρ i x) (hs : ∀ r, ∃ i x, ρ i x = r)
    (hz : ∀ i x, ρ i x = 0 → ∃ j, ∃ h : i ≤ j, a i j h x = 0) :
    ∃ i, letI := (ρ i).toAlgebra
      ∃ (T P : Type (max u v)) (_ : CommRing T) (_ : Algebra (A i) T) (_ : Algebra T S)
        (_ : Algebra (A i) S) (_ : IsScalarTower (A i) R S) (_ : IsScalarTower (A i) T S)
        (_ : AddCommGroup P) (_ : Module T P) (_ : Module (A i) P) (_ : IsScalarTower (A i) T P)
        (_ : Module T M) (_ : IsScalarTower T S M) (f : P →ₗ[T] M),
        Algebra.FinitePresentation (A i) T ∧ Module.FinitePresentation T P ∧
          Module.Flat (A i) P ∧ Algebra.IsPushout (A i) R T S ∧ IsBaseChange S f

Module.Flat.exists_flat_models_and_eventually_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/FlatModel/Packaged.lean, line 47.

Stacks 02JO. Let R → S be of finite presentation and let M be a finitely presented S-module which is flat over R. Then:

1. there are a ring R₀ of finite type over ℤ, an R₀-algebra S₀ of finite type and a finite S₀-module M₀ flat over R₀, with maps to R, S and M exhibiting S = R ⊗_{R₀} S₀ and M = S ⊗_{S₀} M₀;
2. if R = colim_λ R_λ is a directed colimit, such a model already exists over some R_λ, with R_λ → S_λ of finite presentation and M_λ a finitely presented S_λ-module;
3. if (R → S, M) = colim_λ (R_λ → S_λ, M_λ) is a directed colimit of finitely presented pairs with cartesian transition squares, then M_λ is flat over R_λ for all large λ.

This is the packaged three-part form of the tag, stated at the universe generality the source asserts: the index I, the three colimits R, S, M, the stage families A, B, N and the model R₀, S₀, M₀ of part (1) all live in independent universes. The three parts are also available separately as Module.Flat.exists_finiteType_model, Module.Flat.exists_finitePresentation_model_of_directed and Module.Flat.eventually_flat_of_directed, which are proved with R and S in one universe (and, in part (1), with the model in that universe); this statement is deduced from them by the universe transport of the previous section, with no repetition of the spreading-out argument.

theorem Module.Flat.exists_flat_models_and_eventually_flat
    {R : Type uR} {S : Type uS} {M : Type uM}
    [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.FinitePresentation S M] [Module.Flat R M] :
    (∃ (R₀ : Type uR₀) (S₀ : Type uS₀) (M₀ : Type uM₀)
        (_ : CommRing R₀) (_ : CommRing S₀) (_ : Algebra R₀ S₀)
        (_ : Algebra R₀ R) (_ : Algebra S₀ S) (_ : Algebra R₀ S)
        (_ : IsScalarTower R₀ R S) (_ : IsScalarTower R₀ S₀ S)
        (_ : AddCommGroup M₀) (_ : Module S₀ M₀) (_ : Module R₀ M₀)
        (_ : IsScalarTower R₀ S₀ M₀) (_ : Module S₀ M) (_ : IsScalarTower S₀ S M)
        (f : M₀ →ₗ[S₀] M),
      Algebra.FiniteType ℤ R₀ ∧ Algebra.FiniteType R₀ S₀ ∧ Module.Finite S₀ M₀ ∧
        Module.Flat R₀ M₀ ∧ Algebra.IsPushout R₀ R S₀ S ∧ IsBaseChange S f) ∧
    (∀ (I : Type uI) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
        (A : I → Type uA) (_ : ∀ i, CommRing (A i))
        (a : ∀ i j, i ≤ j → A i →+* A j)
        (_ : DirectedSystem A (fun i j h ↦ a i j h))
        (ρ : ∀ i, A i →+* R),
      (∀ i j (h : i ≤ j), ρ j ∘ a i j h = ρ i) →
      (∀ x : R, ∃ i y, ρ i y = x) →
      (∀ i y, ρ i y = 0 → ∃ (j : I) (h : i ≤ j), a i j h y = 0) →
      ∃ i : I,
        letI : Algebra (A i) R := (ρ i).toAlgebra
        ∃ (T : Type (max uA uS)) (P : Type (max (max uA uS) uM))
            (_ : CommRing T) (_ : Algebra (A i) T)
            (_ : Algebra T S) (_ : Algebra (A i) S)
            (_ : IsScalarTower (A i) R S) (_ : IsScalarTower (A i) T S)
            (_ : AddCommGroup P) (_ : Module T P) (_ : Module (A i) P)
            (_ : IsScalarTower (A i) T P) (_ : Module T M) (_ : IsScalarTower T S M)
            (f : P →ₗ[T] M),
          algebraMap (A i) R = ρ i ∧
            Algebra.FinitePresentation (A i) T ∧ Module.FinitePresentation T P ∧
            Module.Flat (A i) P ∧ Algebra.IsPushout (A i) R T S ∧ IsBaseChange S f) ∧
    (∀ (I : Type uI) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
        (A : I → Type uA) (B : I → Type uB) (N : I → Type uN)
        (_ : ∀ i, CommRing (A i)) (_ : ∀ i, CommRing (B i))
        (_ : ∀ i, AddCommGroup (N i)) (_ : ∀ i, Module (B i) (N i))
        (a : ∀ i j, i ≤ j → A i →+* A j)
        (b : ∀ i j, i ≤ j → B i →+* B j)
        (_ : DirectedSystem A (fun i j h ↦ a i j h))
        (_ : DirectedSystem B (fun i j h ↦ b i j h))
        (g : ∀ i, A i →+* B i)
        (n : ∀ i j, (h : i ≤ j) → N i →ₛₗ[b i j h] N j)
        (ρ : ∀ i, A i →+* R) (σ : ∀ i, B i →+* S)
        (ν : ∀ i, N i →+ M)
        (hg : ∀ i j (h : i ≤ j), (g j).comp (a i j h) = (b i j h).comp (g i)),
      (∀ i x, n i i le_rfl x = x) →
      (∀ i j k (hij : i ≤ j) (hjk : j ≤ k) x,
        n j k hjk (n i j hij x) = n i k (hij.trans hjk) x) →
      (∀ i j (h : i ≤ j), ρ j ∘ a i j h = ρ i) →
      (∀ i j (h : i ≤ j), σ j ∘ b i j h = σ i) →
      (∀ i j (h : i ≤ j) x, ν j (n i j h x) = ν i x) →
      (∀ i, (algebraMap R S).comp (ρ i) = (σ i).comp (g i)) →
      (∀ i x m, ν i (g i x • m) = ρ i x • ν i m) →
      (∀ i y m, ν i (y • m) = σ i y • ν i m) →
      (∀ x : R, ∃ i y, ρ i y = x) →
      (∀ i y, ρ i y = 0 → ∃ (j : I) (h : i ≤ j), a i j h y = 0) →
      (∀ x : S, ∃ i y, σ i y = x) →
      (∀ i y, σ i y = 0 → ∃ (j : I) (h : i ≤ j), b i j h y = 0) →
      (∀ x : M, ∃ i y, ν i y = x) →
      (∀ i y, ν i y = 0 → ∃ (j : I) (h : i ≤ j), n i j h y = 0) →
      (∀ i,
        letI : Algebra (A i) (B i) := (g i).toAlgebra
        Algebra.FinitePresentation (A i) (B i)) →
      (∀ i, Module.FinitePresentation (B i) (N i)) →
      (∀ i j (h : i ≤ j),
        letI : Algebra (A i) (B i) := (g i).toAlgebra
        letI : Algebra (A i) (A j) := (a i j h).toAlgebra
        letI : Algebra (B i) (B j) := (b i j h).toAlgebra
        letI : Algebra (A j) (B j) := (g j).toAlgebra
        letI : Algebra (A i) (B j) := ((g j).comp (a i j h)).toAlgebra
        letI : IsScalarTower (A i) (A j) (B j) :=
          IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
        letI : IsScalarTower (A i) (B i) (B j) :=
          IsScalarTower.of_algebraMap_smul fun x y ↦ by
            change b i j h (g i x) * y = g j (a i j h x) * y
            exact congrArg (fun z : B j ↦ z * y)
              (by simpa using (RingHom.congr_fun (hg i j h) x).symm)
        Algebra.IsPushout (A i) (A j) (B i) (B j)) →
      (∀ i j (h : i ≤ j),
        letI : Algebra (B i) (B j) := (b i j h).toAlgebra
        letI : Module (B i) (N j) := Module.compHom (N j) (b i j h)
        letI : IsScalarTower (B i) (B j) (N j) :=
          IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
        IsBaseChange (B j)
          (⟨(n i j h).toAddHom, fun x y ↦ (n i j h).map_smul' x y⟩ :
            N i →ₗ[B i] N j)) →
      ∃ i, ∀ j, i ≤ j →
        letI : Module (A j) (N j) := Module.compHom (N j) (g j)
        Module.Flat (A j) (N j))

Tag 034Y, a lemma

Tag 034Y in the Stacks Project.

Algebra.exists_faithfullyFlat_finitePresentation_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ColimitsII/FaithfullyFlatModel.lean, line 217. The attribute's comment: “The diagram is the data R → A₀ → A with IsScalarTower R A₀ A (the left square) and A₀ → B₀ → B, A₀ → A → B through a common A₀ → B (the right square); B = A ⊗_{A₀} B₀ is Algebra.IsPushout A₀ A B₀ B. The rings A₀, B₀ live in the universe of R, A and B.”.

Stacks 034Y. Let R → A → B be ring maps with A → B faithfully flat of finite presentation. Then there are an R-algebra A₀ of finite presentation and a faithfully flat A₀-algebra B₀ of finite presentation, with maps A₀ → A of R-algebras and B₀ → B compatible with A₀ → B₀ and A → B, such that B = A ⊗_{A₀} B₀.

theorem Algebra.exists_faithfullyFlat_finitePresentation_model {R : Type v} {A B : Type u}
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Module.FaithfullyFlat A B]
    [Algebra.FinitePresentation A B] :
    ∃ (A₀ B₀ : Type (max u v)) (_ : CommRing A₀) (_ : CommRing B₀) (_ : Algebra R A₀)
      (_ : Algebra A₀ B₀) (_ : Algebra A₀ A) (_ : IsScalarTower R A₀ A) (_ : Algebra B₀ B)
      (_ : Algebra A₀ B) (_ : IsScalarTower A₀ A B) (_ : IsScalarTower A₀ B₀ B),
      Algebra.FinitePresentation R A₀ ∧ Module.FaithfullyFlat A₀ B₀ ∧
        Algebra.FinitePresentation A₀ B₀ ∧ Algebra.IsPushout A₀ A B₀ B

Tag 07RG, a lemma

Tag 07RG in the Stacks Project.

Stacks.DirectLimit.FiniteDescent.finite_baseChange_of_colimit_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Algebra/DirectLimit/Descent/Finite.lean, line 526.

Let L be the directed colimit of a directed system of R-algebras (A i), and let φ : B →ₐ[R] C be a map of R-algebras of finite type. If the base change id_L ⊗ φ : L ⊗_R B → L ⊗_R C is a finite ring map, then there is an index i such that the base change id_{A i} ⊗ φ : A i ⊗_R B → A i ⊗_R C is a finite ring map.

theorem finite_baseChange_of_colimit_finite
    {A : ι → Type*} [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    {f : ∀ ⦃i j⦄, i ≤ j → A i →ₐ[R] A j}
    {L : Type*} [CommRing L] [Algebra R L]
    {g : ∀ i, A i →ₐ[R] L}
    (φ : B →ₐ[R] C)
    (hcolim : IsDirectedColimit A f L g)
    (hfin_type : φ.FiniteType)
    (hfin : (baseChange L φ).toRingHom.Finite) :
    ∃ i : ι, (baseChange (A i) φ).toRingHom.Finite

Tag 07RH, a lemma

Tag 07RH in the Stacks Project.

surjective_baseChange_of_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Algebra/DirectLimit/Descent/Surjective.lean, line 280. References: SGA 3 VIB (10.1), “special case”.

Let A = colim_i Aᵢ be a directed colimit of A₀-algebras, and let C₀ be an A₀-algebra that is of finite type over the A₀-algebra B₀ (via the structure map φ₀ : B₀ → C₀). If the base change id_A ⊗ φ₀ : A ⊗_{A₀} B₀ → A ⊗_{A₀} C₀ is surjective, then there is some index i for which the base change id_{Aᵢ} ⊗ φ₀ : Aᵢ ⊗_{A₀} B₀ → Aᵢ ⊗_{A₀} C₀ is already surjective.

theorem surjective_baseChange_of_colimit
    (hcolim : IsRingColimit A₀ Aᵢ f A g)
    (hsurj : Function.Surjective (baseChangeColim A₀ A B₀ C₀))
    (hft : Algebra.FiniteType B₀ C₀) :
    ∃ i : I, Function.Surjective (baseChange A₀ Aᵢ B₀ C₀ i)

Tag 0C4F, a lemma

Tag 0C4F in the Stacks Project.

Stacks.DirectLimit.UnramifiedDescent.colimit_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Algebra/DirectLimit/Descent/Unramified.lean, line 534.

If the base change Φ = id_A ⊗ φ₀ of φ₀ to the directed colimit A = colim_i Aᵢ is unramified and C₀ is of finite type over B₀ via φ₀, then the base change Φᵢ = id_{Aᵢ} ⊗ φ₀ is unramified at some finite stage i ≥ O, where G i is an A₀-algebra via f O i h.

theorem colimit_unramified
    (hΦ :
      letI : Algebra ((A G f) ⊗[G O] B₀) ((A G f) ⊗[G O] C₀) :=
        (phiColim G f O B₀ C₀ φ₀).toRingHom.toAlgebra
      Algebra.Unramified ((A G f) ⊗[G O] B₀) ((A G f) ⊗[G O] C₀))
    (hFT :
      letI : Algebra B₀ C₀ := φ₀.toRingHom.toAlgebra
      Algebra.FiniteType B₀ C₀) :
    ∃ i, ∃ (h : O ≤ i),
      letI : Algebra (G O) (G i) := (f O i h).toAlgebra
      letI φᵢ : (G i) ⊗[G O] B₀ →ₐ[G i] (G i) ⊗[G O] C₀ :=
        Algebra.TensorProduct.map (AlgHom.id (G i) (G i)) φ₀
      letI : Algebra ((G i) ⊗[G O] B₀) ((G i) ⊗[G O] C₀) := φᵢ.toRingHom.toAlgebra
      Algebra.Unramified ((G i) ⊗[G O] B₀) ((G i) ⊗[G O] C₀)

Tag 0C32, a lemma

Tag 0C32 in the Stacks Project.

Stacks.DirectLimit.FinitePresentationDescent.isIso_of_finitePresentation_colim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Algebra/DirectLimit/Descent/Bijective.lean, line 836.

Let A = colim_{i ∈ I} A_i be a directed colimit of commutative rings, fix an index i₀ ∈ I, and let φ₀ : B₀ → C₀ be a map of A i₀-algebras. If the base-changed map φ : A ⊗_{A i₀} B₀ → A ⊗_{A i₀} C₀ is bijective and φ₀ is of finite presentation, then there exists an index i ≥ i₀ such that the base-changed map φ_i : A_i ⊗_{A i₀} B₀ → A_i ⊗_{A i₀} C₀ is bijective.

theorem isIso_of_finitePresentation_colim
    (hfp : (φ₀ : B₀ →+* C₀).FinitePresentation)
    (hφ : Function.Bijective (phiColim A f i₀ B₀ C₀ φ₀)) :
    ∃ i : ι, ∃ h : i₀ ≤ i, Function.Bijective (phiAt A f i₀ B₀ C₀ φ₀ i h)

Tag 07RI, a lemma

Tag 07RI in the Stacks Project.

RingHom.Etale.exists_baseChange_etale_of_colimitPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/ColimitBaseChange.lean, line 380. The attribute's comment: “The source's A_0 is the base ring R and its index set restricted to i ≥ 0, which is cofinal, is the diagram; A = colim A_i is Limits.ColimitPresentation J A in CommAlgCat R over an arbitrary filtered J, together with the PreservesColimit instance saying the colimit is computed on underlying sets, and the base change of φ is Mathlib's Algebra.TensorProduct.map (AlgHom.id R _) φ. See the module docstring.”.

Étale spreads out in a filtered colimit of base rings. Let A be the colimit of a filtered diagram of R-algebras Aᵢ, computed on underlying sets, and let φ : B →ₐ[R] C be of finite presentation. If the base change 1 ⊗ φ : A ⊗[R] B → A ⊗[R] C is étale, then 1 ⊗ φ : Aᵢ ⊗[R] B → Aᵢ ⊗[R] C is étale for some i.

public theorem exists_baseChange_etale_of_colimitPresentation
    {R : Type u} [CommRing R] {J : Type w} [Category.{t} J] [IsFiltered J]
    {A : CommAlgCat.{v} R} (pres : ColimitPresentation J A)
    [PreservesColimit (pres.diag ⋙ forget₂ (CommAlgCat R) CommRingCat) (forget CommRingCat)]
    {B C : Type*} [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] (φ : B →ₐ[R] C)
    (hφ : φ.toRingHom.FinitePresentation)
    (hA : (Algebra.TensorProduct.map (AlgHom.id R ↥A) φ).toRingHom.Etale) :
    ∃ i : J, (Algebra.TensorProduct.map (AlgHom.id R ↥(pres.diag.obj i)) φ).toRingHom.Etale

Tag 0C0B, a lemma

Tag 0C0B in the Stacks Project.

RingHom.Smooth.exists_baseChange_smooth_of_colimitPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/Smooth.lean, line 1130. The attribute's comment: “The source's A_0 is the base ring R and its index set restricted to i ≥ 0, which is cofinal, is the diagram; A = colim A_i is Limits.ColimitPresentation J A in CommAlgCat R over a filtered J whose colimit is computed on underlying sets, and the base change of φ is Mathlib's Algebra.TensorProduct.map (AlgHom.id R _) φ. Smooth is RingHom.Smooth, the source's notion by Proposition 00TN. See the module docstring.”.

Smoothness spreads out in a filtered colimit of base rings. Let A be the colimit of a filtered diagram of R-algebras Aᵢ, computed on underlying sets, and let φ : B →ₐ[R] C be of finite presentation. If the base change 1 ⊗ φ : A ⊗[R] B → A ⊗[R] C is smooth, then 1 ⊗ φ : Aᵢ ⊗[R] B → Aᵢ ⊗[R] C is smooth for some i.

public theorem exists_baseChange_smooth_of_colimitPresentation
    {R : Type u} [CommRing R] {J : Type w} [Category.{t} J] [IsFiltered J]
    {A : CommAlgCat.{v} R} (pres : ColimitPresentation J A)
    [PreservesColimit (pres.diag ⋙ forget₂ (CommAlgCat.{v} R) CommRingCat.{v})
      (forget CommRingCat)]
    {B C : Type*} [CommRing B] [CommRing C] [Algebra R B] [Algebra R C] (φ : B →ₐ[R] C)
    (hφ : φ.toRingHom.FinitePresentation)
    (hA : (Algebra.TensorProduct.map (AlgHom.id R ↥A) φ).toRingHom.Smooth) :
    ∃ i : J, (Algebra.TensorProduct.map (AlgHom.id R ↥(pres.diag.obj i)) φ).toRingHom.Smooth

Tag 0C33, a lemma

Tag 0C33 in the Stacks Project.

Algebra.IsRelativeGlobalCompleteIntersection.exists_stage_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ColimitsII/TensorProductStage.lean, line 262. The attribute's comment: “The relative global complete intersection case. The colimit A is the ring R with the cocone ρ, given elementwise: every element of R comes from a stage, and an element of a stage dying in R dies at a later stage. The maps A_i ⊗ B₀ → A_i ⊗ C₀ are Algebra.TensorProduct.map id φ₀.”.

Stacks 0C33, relative global complete intersections. Let A = colim_i A_i be a directed colimit of rings, let 0 ≤ i be an index and φ₀ : B₀ → C₀ a map of A₀-algebras with C₀ of finite presentation over B₀. If A ⊗_{A₀} B₀ → A ⊗_{A₀} C₀ is a relative global complete intersection, then so is A_i ⊗_{A₀} B₀ → A_i ⊗_{A₀} C₀ for some i ≥ 0.

theorem Algebra.IsRelativeGlobalCompleteIntersection.exists_stage_tensorProduct
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
    {A : ι → Type u} [∀ i, CommRing (A i)] (a : ∀ i j, i ≤ j → A i →+* A j)
    [DirectedSystem A fun i j h => a i j h] {R : Type*} [CommRing R] (ρ : ∀ i, A i →+* R)
    (hρ : ∀ i j (h : i ≤ j) x, ρ j (a i j h x) = ρ i x) (hρs : ∀ r, ∃ i x, ρ i x = r)
    (hρz : ∀ i x, ρ i x = 0 → ∃ j, ∃ h : i ≤ j, a i j h x = 0)
    {i₀ : ι} {B₀ C₀ : Type v} [CommRing B₀] [CommRing C₀] [Algebra (A i₀) B₀] [Algebra (A i₀) C₀]
    (φ₀ : B₀ →ₐ[A i₀] C₀) (hfp : φ₀.FinitePresentation)
    (h : letI := (ρ i₀).toAlgebra
      letI := (Algebra.TensorProduct.map (AlgHom.id (A i₀) R) φ₀).toRingHom.toAlgebra
      Algebra.IsRelativeGlobalCompleteIntersection (R ⊗[A i₀] B₀) (R ⊗[A i₀] C₀)) :
    ∃ i, ∃ h : i₀ ≤ i, letI := (a i₀ i h).toAlgebra
      letI := (Algebra.TensorProduct.map (AlgHom.id (A i₀) (A i)) φ₀).toRingHom.toAlgebra
      Algebra.IsRelativeGlobalCompleteIntersection (A i ⊗[A i₀] B₀) (A i ⊗[A i₀] C₀)

Algebra.Syntomic.exists_stage_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ColimitsII/TensorProductStage.lean, line 284. The attribute's comment: “The syntomic case, with the conventions of the relative global complete intersection case.”.

Stacks 0C33, syntomic ring maps. Let A = colim_i A_i be a directed colimit of rings, let 0 ≤ i be an index and φ₀ : B₀ → C₀ a map of A₀-algebras with C₀ of finite presentation over B₀. If A ⊗_{A₀} B₀ → A ⊗_{A₀} C₀ is syntomic, then so is A_i ⊗_{A₀} B₀ → A_i ⊗_{A₀} C₀ for some i ≥ 0.

theorem Algebra.Syntomic.exists_stage_tensorProduct
    {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
    {A : ι → Type u} [∀ i, CommRing (A i)] (a : ∀ i j, i ≤ j → A i →+* A j)
    [DirectedSystem A fun i j h => a i j h] {R : Type*} [CommRing R] (ρ : ∀ i, A i →+* R)
    (hρ : ∀ i j (h : i ≤ j) x, ρ j (a i j h x) = ρ i x) (hρs : ∀ r, ∃ i x, ρ i x = r)
    (hρz : ∀ i x, ρ i x = 0 → ∃ j, ∃ h : i ≤ j, a i j h x = 0)
    {i₀ : ι} {B₀ C₀ : Type v} [CommRing B₀] [CommRing C₀] [Algebra (A i₀) B₀] [Algebra (A i₀) C₀]
    (φ₀ : B₀ →ₐ[A i₀] C₀) (hfp : φ₀.FinitePresentation)
    (h : letI := (ρ i₀).toAlgebra
      letI := (Algebra.TensorProduct.map (AlgHom.id (A i₀) R) φ₀).toRingHom.toAlgebra
      Algebra.Syntomic (R ⊗[A i₀] B₀) (R ⊗[A i₀] C₀)) :
    ∃ i, ∃ h : i₀ ≤ i, letI := (a i₀ i h).toAlgebra
      letI := (Algebra.TensorProduct.map (AlgHom.id (A i₀) (A i)) φ₀).toRingHom.toAlgebra
      Algebra.Syntomic (A i ⊗[A i₀] B₀) (A i ⊗[A i₀] C₀)

Tag 034Z, a lemma

Tag 034Z in the Stacks Project.

Algebra.exists_quasiFinite_faithfullyFlat_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/ColimitsII/QuasiFiniteFactorization.lean, line 535. The attribute's comment: “The commutative triangle is the data R → S → S' with IsScalarTower R S S'; quasi-finiteness (Definition 00PL) is Algebra.QuasiFinite, which omits the finite type clause of the source's definition, supplied here by Algebra.FinitePresentation. S' lives in the universe of R and S.”. References: EGA IV (17.16.2), “affine case”.

Stacks 034Z. Let R → S be a faithfully flat ring map of finite presentation. Then there is an S-algebra S' such that R → S' is quasi-finite, faithfully flat and of finite presentation.

theorem Algebra.exists_quasiFinite_faithfullyFlat_finitePresentation
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [Module.FaithfullyFlat R S] [Algebra.FinitePresentation R S] :
    ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Algebra S S')
      (_ : IsScalarTower R S S'), Algebra.QuasiFinite R S' ∧ Module.FaithfullyFlat R S' ∧
        Algebra.FinitePresentation R S'

Sources

• Section 10.168, Tag 07RF
• AxiomMath/Stacks at 5ed82d14

LeanModule.Flat.eventually_flat_of_directed · Module.Flat.exists_finiteType_model · Module.Flat.exists_finitePresentation_model_of_directed · Module.Flat.exists_flat_models_and_eventually_flat · Algebra.exists_faithfullyFlat_finitePresentation_model · Stacks.DirectLimit.FiniteDescent.finite_baseChange_of_colimit_finite · surjective_baseChange_of_colimit · Stacks.DirectLimit.UnramifiedDescent.colimit_unramified

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.