10.136 Syntomic morphisms to 10.153 Henselian local rings

Section10.136 Syntomic morphisms#

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

Tag 00SL, a definition

Tag 00SL in the Stacks Project.

Algebra.Syntomic, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/Defs.lean, line 70. The attribute's comment: “Stated for an R-algebra S, as Mathlib states Algebra.Smooth; for a ring map f : R →+* S it is Algebra.Syntomic R S at f.toAlgebra. The fibre ring is Mathlib's Ideal.Fiber p S = κ(p) ⊗[R] S, the source's S ⊗_R κ(p) with the factors exchanged so that the κ(p)-algebra structure is the one Mathlib puts on a tensor product. See the module docstring.”. References: EGA IV (19.3.6), “affine case”.

A ring map R → S is syntomic, and S is a flat local complete intersection over R, if it is flat, of finite presentation, and if all of its fibre rings S ⊗_R κ(p) are local complete intersections over κ(p) (IsLocalCompleteIntersection).

public class Algebra.Syntomic (R : Type*) [CommRing R] (S : Type*) [CommRing S] [Algebra R S] :
    Prop
Tag 00SM, a lemma

Tag 00SM in the Stacks Project.

Algebra.IsPushout.syntomic_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/BaseChange.lean, line 227. The attribute's comment: “The base change S' = R' ⊗_R S is an arbitrary pushout square Algebra.IsPushout R R' S S'; the source's literal form is inferInstance once Algebra.TensorProduct.rightAlgebra is a local instance. Faithful flatness is Module.FaithfullyFlat R R', the module-level form Mathlib's descent lemmas use. See the module docstring.”.

Let R → S be a ring map, let R → R' be faithfully flat and let S' be the base change of S along R → R', so S' = R' ⊗_R S. Then R' → S' is syntomic if and only if R → S is syntomic.

public theorem Algebra.IsPushout.syntomic_iff (R R' S S' : Type*) [CommRing R] [CommRing R']
    [CommRing S] [CommRing S'] [Algebra R R'] [Algebra R S] [Algebra R S'] [Algebra R' S']
    [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
    [Algebra.IsPushout R R' S S'] [Module.FaithfullyFlat R R'] :
    Algebra.Syntomic R' S' ↔ Algebra.Syntomic R S
Tag 00SN, a lemma

Tag 00SN in the Stacks Project.

Algebra.IsPushout.syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/BaseChange.lean, line 211. The attribute's comment: “The base change is an arbitrary pushout square Algebra.IsPushout R S R' S', the square RingHom.IsStableUnderBaseChange quantifies over and the orientation of Mathlib's Algebra.IsPushout.isIntegral; the source's literal S' = S ⊗_R R' is TensorProduct.isPushout. Nothing is assumed about R → R'. See the module docstring.”.

Any base change of a syntomic ring map is syntomic: if R → S is syntomic and S' is the base change of S along an arbitrary ring map R → R', so S' = S ⊗_R R', then R' → S' is syntomic.

public theorem Algebra.IsPushout.syntomic (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (R' S' : Type*) [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra R S'] [Algebra S S']
    [Algebra R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
    [Algebra.IsPushout R S R' S'] [Algebra.Syntomic R S] :
    Algebra.Syntomic R' S'
Tag 00SO, a lemma

Tag 00SO in the Stacks Project.

isSyntomic_of_isSyntomic_localization_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RingHom/FinitePresentation.lean, line 378.

Syntomic is local on the source: let R → S be a ring map and suppose there are elements g_1, …, g_m ∈ S generating the unit ideal of S such that for each i the composite R → S_{g_i} is syntomic. Then R → S is syntomic.

theorem isSyntomic_of_isSyntomic_localization_away
    (R : Type*) [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
    (m : ℕ) (g : Fin m → S) (hg : Ideal.span (Set.range g) = ⊤)
    (h : ∀ i, IsSyntomic R (Localization.Away (g i))) :
    IsSyntomic R S
Tag 00SP, a definition

Tag 00SP in the Stacks Project.

Algebra.Presentation.IsRelativeGlobalCompleteIntersection, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Defs.lean, line 245. The attribute's comment: “The source's displayed S = R[x_1, …, x_n]/(f_1, …, f_c), a presentation together with the dimension property of its fibres; Algebra.IsRelativeGlobalCompleteIntersection is the property of the ring map, defined through this one. Stated for arbitrary finite index types, with n = Nat.card ι and c = Nat.card σ. The fibre ring is Ideal.Fiber p S = κ(p) ⊗[R] S, and dim = n - c is written additively as ringKrullDim (p.Fiber S) + Nat.card σ = Nat.card ι in WithBot ℕ∞ rather than with the truncated subtraction Algebra.Presentation.dimension. See the module docstring.”.

A presentation S = R[x_1, …, x_n]/(f_1, …, f_c) of S over R is a relative global complete intersection if every nonempty fibre of Spec(S) → Spec(R) has dimension n - c.

The number of variables is n = Nat.card ι and the number of relations is c = Nat.card σ, the fibre over a prime p of R is the spectrum of p.Fiber S = κ(p) ⊗_R S, it is nonempty exactly when that ring is nonzero, and dim = n - c is written as the equation ringKrullDim (p.Fiber S) + c = n in WithBot ℕ∞.

public class Algebra.Presentation.IsRelativeGlobalCompleteIntersection {R S : Type*} [CommRing R]
    [CommRing S] [Algebra R S] {ι σ : Type*} [Finite ι] [Finite σ]
    (P : Algebra.Presentation R S ι σ) : Prop

Algebra.IsRelativeGlobalCompleteIntersection, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Defs.lean, line 264. The attribute's comment: “Stated for an R-algebra S, as Mathlib states Algebra.Smooth and as the sibling Algebra.Syntomic (00SL) is stated; for a ring map f : R →+* S it is Algebra.IsRelativeGlobalCompleteIntersection R S at f.toAlgebra. The presentation S = R[x_1, …, x_n]/(f_1, …, f_c) is Algebra.Presentation R S (Fin n) (Fin c) and the dimension condition on it is Algebra.Presentation.IsRelativeGlobalCompleteIntersection, through which this one is defined, as Mathlib defines Algebra.IsStandardSmoothOfRelativeDimension through Algebra.SubmersivePresentation. See the module docstring.”.

A ring map R → S is a relative global complete intersection if there is a presentation S = R[x_1, …, x_n]/(f_1, …, f_c) such that every nonempty fibre of Spec(S) → Spec(R) has dimension n - c, that is, a presentation satisfying Algebra.Presentation.IsRelativeGlobalCompleteIntersection.

public class Algebra.IsRelativeGlobalCompleteIntersection (R : Type*) [CommRing R] (S : Type*)
    [CommRing S] [Algebra R S] : Prop
Tag 07CF, a lemma

Tag 07CF in the Stacks Project.

Algebra.exists_presentation_basis_cotangent_of_free_cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Cotangent/FreeConormalPresentation.lean, line 42.

A finitely presented R-algebra S admitting a presentation S = R[x₁, …, xₙ]/I with I/I² free over S admits a presentation S = R[y₁, …, y_m]/(f₁, …, f_c) whose conormal module is free with basis the classes of f₁, …, f_c.

theorem exists_presentation_basis_cotangent_of_free_cotangent [FinitePresentation R S]
    (h : ∃ (ι : Type) (_ : Finite ι) (P : Generators R S ι),
      Module.Free S P.toExtension.Cotangent) :
    ∃ (ι σ : Type) (_ : Finite ι) (_ : Finite σ) (P : Presentation R S ι σ)
      (b : Module.Basis σ S P.toExtension.Cotangent),
      ∀ r, b r = Extension.Cotangent.mk ⟨P.relation r, P.relation_mem_ker r⟩
Tag 00SQ, an example

Tag 00SQ in the Stacks Project.

MvPolynomial.universalFactorizationMapBaseChangeAlgHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/UniversalFactorization.lean, line 79. The attribute's comment: “the source's k-algebra maps S_k → K are tuples β, γ with x^{n+m} + α_1 x^{n+m-1} + … = (x^n + β_1 x^{n-1} + …)(x^m + γ_1 x^{m-1} + …) in K; here for any K-algebra L over any base ring, the tuples being the monic factors of degrees m and k, the total degree being n = m + k”.

K-algebra maps from the fibre ring K ⊗_{R[a]} S of the universal factorization map φ : R[a] → S to a K-algebra L correspond to factorizations over L of the image x^n + α_{n-1} x^{n-1} + ⋯ + α_0 of the free monic polynomial into monic polynomials of degrees m and k. The factorization attached to f consists of the images under f of the two factors of the free monic polynomial over S.

noncomputable def universalFactorizationMapBaseChangeAlgHomEquiv (K L : Type*) [CommRing K]
    [CommRing L] [Algebra (MvPolynomial (Fin n) R) K] [Algebra K L]
    [Algebra (MvPolynomial (Fin n) R) L] [IsScalarTower (MvPolynomial (Fin n) R) K L] :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    (K ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) →ₐ[K] L) ≃
      {q : MonicDegreeEq L m × MonicDegreeEq L k //
        q.1.1 * q.2.1 = (freeMonic R n).map (algebraMap (MvPolynomial (Fin n) R) L)}

Polynomial.finite_monicDegreeEq_mul_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/UniversalFactorization.lean, line 137. The attribute's comment: “the source's finiteness of the set of tuples β, γ in a field K with x^{n+m} + α_1 x^{n+m-1} + … = (x^n + β_1 x^{n-1} + …)(x^m + γ_1 x^{m-1} + …); here for any polynomial over any field, with factor degrees m and k”.

Over a field L, a polynomial has only finitely many factorizations into monic polynomials of given degrees m and k.

theorem finite_monicDegreeEq_mul_eq (L : Type*) [Field L] (m k : ℕ) (p : L[X]) :
    Finite {q : MonicDegreeEq L m × MonicDegreeEq L k // q.1.1 * q.2.1 = p}

MvPolynomial.isIntegral_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/UniversalFactorization.lean, line 166. The attribute's comment: “the source's last paragraph: each of b_i, c_j is integral over R; here every element of S, over any base ring, the total degree being n = m + k”.

Every element of S is integral over R[a] under the universal factorization map.

theorem isIntegral_universalFactorizationMap :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Algebra.IsIntegral (MvPolynomial (Fin n) R)
      (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

MvPolynomial.finite_primeSpectrum_tensorProduct_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/UniversalFactorization.lean, line 192. The attribute's comment: “the source's statement that all fibres have finitely many closed points; here all points, over any base ring, the total degree being n = m + k”.

Every fibre K ⊗_{R[a]} S of the universal factorization map R[a] → S over a field K has finitely many points.

theorem finite_primeSpectrum_tensorProduct_universalFactorizationMap (K : Type*) [Field K]
    [Algebra (MvPolynomial (Fin n) R) K] :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Finite (PrimeSpectrum
      (K ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)))

MvPolynomial.ringKrullDim_tensorProduct_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/UniversalFactorization.lean, line 205. The attribute's comment: “the source's statement that all fibres have dimension 0, over any base ring, the total degree being n = m + k; the fibre over a prime p is the case K = κ(p)”.

Every nonempty fibre K ⊗_{R[a]} S of the universal factorization map R[a] → S over a field K has dimension 0.

theorem ringKrullDim_tensorProduct_universalFactorizationMap (K : Type*) [Field K]
    [Algebra (MvPolynomial (Fin n) R) K] :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Nontrivial
        (K ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) →
      ringKrullDim
        (K ⊗[MvPolynomial (Fin n) R] (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)) = 0

MvPolynomial.universalFactorizationMapPresentation_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/UniversalFactorization.lean, line 223. The attribute's comment: “the source's S is a relative global complete intersection over R, for the presentation by the b_i, c_j and the equations a_k = a_k(b_i, c_j), over any base ring, the total degree being n = m + k”.

The canonical presentation S = R[a][b, c]/(a_l - a_l(b, c)) of the universal factorization map, with m + k variables and n = m + k relations, is a relative global complete intersection.

theorem universalFactorizationMapPresentation_isRelativeGlobalCompleteIntersection :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Algebra.Presentation.IsRelativeGlobalCompleteIntersection
      (universalFactorizationMapPresentation R n m k hn).toPresentation

MvPolynomial.isRelativeGlobalCompleteIntersection_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/UniversalFactorization.lean, line 236. The attribute's comment: “the source's R → S is a relative global complete intersection, as a property of the ring map, over any base ring, the total degree being n = m + k”.

The universal factorization map R[a_0, …, a_{n-1}] → R[b] ⊗_R R[c] is a relative global complete intersection.

theorem isRelativeGlobalCompleteIntersection_universalFactorizationMap :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Algebra.IsRelativeGlobalCompleteIntersection (MvPolynomial (Fin n) R)
      (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Declarations registered for the tag:

Tag 00SS, a lemma

Tag 00SS in the Stacks Project.

Algebra.IsRelativeGlobalCompleteIntersection.baseChange_and_localization_away_and_localization_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Relative.lean, line 314. The attribute's comment: “The three parts are the three conjuncts, with the auxiliary rings quantified inside the statement so that each carries only its own data, and each part is available separately as baseChange, of_isLocalizationAway and localization_base. Part (1) is over an arbitrary pushout square Algebra.IsPushout R S R' S', the orientation of the sibling 00SN, with nothing assumed about R → R'; part (2) over an arbitrary IsLocalization.Away g S', the source's h restricting nothing since R[x_1, …, x_n] → S is surjective; part (3) over a localization at an arbitrary submonoid M ⊆ R rather than only at the powers of one f ∈ R, the factorization R → Rₘ → S being [Algebra Rₘ S] with [IsScalarTower R Rₘ S]. See the module docstring.”.

Let S = R[x_1, …, x_n]/(f_1, …, f_c) be a relative global complete intersection over R. Then

  1. for any ring map R → R' the base change S' = R' ⊗_R S is a relative global complete intersection over R', presented as R'[x_1, …, x_n]/(f_1, …, f_c);
  2. for any g ∈ S, the image of some h ∈ R[x_1, …, x_n], the localization S_g is a relative global complete intersection over R, presented as R[x_1, …, x_n, x_{n+1}]/(f_1, …, f_c, hx_{n+1} - 1);
  3. if R → S factors through a localization R_M of R, then S is a relative global complete intersection over R_M, presented as R_M[x_1, …, x_n]/(f_1, …, f_c).
public theorem baseChange_and_localization_away_and_localization_base (R : Type u) (S : Type v)
    [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.IsRelativeGlobalCompleteIntersection R S] :
    (∀ (R' : Type u') (S' : Type v') [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra R S']
        [Algebra S S'] [Algebra R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
        [Algebra.IsPushout R S R' S'], Algebra.IsRelativeGlobalCompleteIntersection R' S') ∧
      (∀ (g : S) (S' : Type w) [CommRing S'] [Algebra S S'] [Algebra R S'] [IsScalarTower R S S']
        [IsLocalization.Away g S'], Algebra.IsRelativeGlobalCompleteIntersection R S') ∧
      (∀ (M : Submonoid R) (Rₘ : Type t) [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ]
        [Algebra Rₘ S] [IsScalarTower R Rₘ S],
          Algebra.IsRelativeGlobalCompleteIntersection Rₘ S)

Algebra.IsRelativeGlobalCompleteIntersection.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Relative.lean, line 333. The attribute's comment: “Part (1), over an arbitrary pushout square Algebra.IsPushout R S R' S' — the orientation and binders of the sibling 00SN, Algebra.IsPushout.syntomic.”.

The base change of a relative global complete intersection is a relative global complete intersection: if S = R[x_1, …, x_n]/(f_1, …, f_c) is one over R and Algebra.IsPushout R S R' S', so that S' = R' ⊗_R S = R'[x_1, …, x_n]/(f_1, …, f_c), then S' is a relative global complete intersection over R'. Nothing is assumed about R → R'.

public theorem baseChange (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    (R' : Type u') (S' : Type v') [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra R S']
    [Algebra S S'] [Algebra R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
    [Algebra.IsPushout R S R' S'] [Algebra.IsRelativeGlobalCompleteIntersection R S] :
    Algebra.IsRelativeGlobalCompleteIntersection R' S'

Algebra.IsRelativeGlobalCompleteIntersection.of_isLocalizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Relative.lean, line 348. The attribute's comment: “Part (2), for an arbitrary localization away from g; the source's h restricts nothing, since R[x_1, …, x_n] → S is surjective. Binders as in Algebra.FinitePresentation.of_isLocalizationAway, the same statement for finite presentation.”.

A localization of a relative global complete intersection away from an element is a relative global complete intersection: if S = R[x_1, …, x_n]/(f_1, …, f_c) is one over R, g ∈ S is the image of h ∈ R[x_1, …, x_n], and S' is the localization S_g, then S' = R[x_1, …, x_n, x_{n+1}]/(f_1, …, f_c, hx_{n+1} - 1) is a relative global complete intersection over R.

public theorem of_isLocalizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsRelativeGlobalCompleteIntersection R S] (g : S) {S' : Type w}
    [CommRing S'] [Algebra S S'] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization.Away g S'] :
    Algebra.IsRelativeGlobalCompleteIntersection R S'

Algebra.IsRelativeGlobalCompleteIntersection.localization_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Relative.lean, line 361. The attribute's comment: “Part (3), for a localization at an arbitrary submonoid M ⊆ R rather than only at the powers of one f ∈ R; the factorization R → Rₘ → S is [Algebra Rₘ S] with [IsScalarTower R Rₘ S]. Binders as in Algebra.FormallySmooth.localization_base.”.

A relative global complete intersection over R whose structure map factors through a localization Rₘ of R is a relative global complete intersection over Rₘ: if S = R[x_1, …, x_n]/(f_1, …, f_c) is one over R and R → S factors as R → Rₘ → S, then S = Rₘ[x_1, …, x_n]/(f_1, …, f_c) is a relative global complete intersection over Rₘ.

public theorem localization_base {R : Type u} [CommRing R] (M : Submonoid R) {S : Type v}
    [CommRing S] [Algebra R S] [Algebra.IsRelativeGlobalCompleteIntersection R S] {Rₘ : Type t}
    [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra Rₘ S] [IsScalarTower R Rₘ S] :
    Algebra.IsRelativeGlobalCompleteIntersection Rₘ S
Tag 00ST, a lemma

Tag 00ST in the Stacks Project.

Algebra.Presentation.exists_sub_one_mem_map_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Relative.lean, line 538. The attribute's comment: “(1): the fibre of Spec(S/IS) → Spec(R/I) over 𝔭/I is the fibre κ(𝔭) ⊗_R S = 𝔭.Fiber S of Spec(S) → Spec(R) over 𝔭 ⊇ I, and only nonempty fibres are constrained, as in Definition 00SP; g ↦ 1 ∈ S/IS is g - 1 ∈ IS. The presentation of S_g is Algebra.Presentation.localizationAwayComp.”.

Let S = R[x_1, …, x_n]/(f_1, …, f_c), presented by P, and let I ⊆ R be an ideal such that the fibres of Spec(S/IS) → Spec(R/I) have dimension n - c, that is, every nonempty fibre of Spec(S) → Spec(R) over a prime 𝔭 ⊇ I has dimension n - c. Then there is an h ∈ R[x_1, …, x_n] whose image g ∈ S maps to 1 ∈ S/IS, such that S_g = R[x_1, …, x_n, x_{n+1}]/(f_1, …, f_c, h x_{n+1} - 1) is a relative global complete intersection with this presentation.

theorem Algebra.Presentation.exists_sub_one_mem_map_isRelativeGlobalCompleteIntersection
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {ι σ : Type*} [Finite ι] [Finite σ]
    (P : Algebra.Presentation R S ι σ) (I : Ideal R)
    (hI : ∀ (p : Ideal R) [p.IsPrime], I ≤ p → Nontrivial (p.Fiber S) →
      ringKrullDim (p.Fiber S) + ((Nat.card σ : ℕ) : WithBot ℕ∞) =
        ((Nat.card ι : ℕ) : WithBot ℕ∞)) :
    ∃ h : P.Ring, algebraMap P.Ring S h - 1 ∈ I.map (algebraMap R S) ∧
      (P.localizationAwayComp h
        (Localization.Away (algebraMap P.Ring S h))).IsRelativeGlobalCompleteIntersection

Algebra.Presentation.exists_isUnit_fiber_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Relative.lean, line 595. The attribute's comment: “(2): the fibre S ⊗_R κ(𝔭) is 𝔭.Fiber S = κ(𝔭) ⊗_R S, in which g is 1 ⊗ g, and dim = n - c is written additively as in Definition 00SP. The presentation of S_g is Algebra.Presentation.localizationAwayComp.”.

Let S = R[x_1, …, x_n]/(f_1, …, f_c), presented by P, and let 𝔭 be a prime of R with dim(S ⊗_R κ(𝔭)) = n - c. Then there is an h ∈ R[x_1, …, x_n] whose image g ∈ S maps to a unit of S ⊗_R κ(𝔭), such that S_g = R[x_1, …, x_n, x_{n+1}]/(f_1, …, f_c, h x_{n+1} - 1) is a relative global complete intersection with this presentation.

theorem Algebra.Presentation.exists_isUnit_fiber_isRelativeGlobalCompleteIntersection
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {ι σ : Type*} [Finite ι] [Finite σ]
    (P : Algebra.Presentation R S ι σ) (p : Ideal R) [p.IsPrime]
    (hp : ringKrullDim (p.Fiber S) + ((Nat.card σ : ℕ) : WithBot ℕ∞) =
      ((Nat.card ι : ℕ) : WithBot ℕ∞)) :
    ∃ h : P.Ring, IsUnit (Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField)
        (algebraMap P.Ring S h)) ∧
      (P.localizationAwayComp h
        (Localization.Away (algebraMap P.Ring S h))).IsRelativeGlobalCompleteIntersection

Algebra.Presentation.exists_notMem_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Relative.lean, line 641. The attribute's comment: “(3): the presentation of S_g is Algebra.Presentation.localizationAwayComp, the source's R[x_1, …, x_n, x_{n+1}]/(f_1, …, f_c, h x_{n+1} - 1), and dim_𝔮(S/R) = n - c is Algebra.relativeDimensionAt R 𝔮 + c = n (tag 00QD), written additively as in Definition 00SP. The numbers of variables and relations are Nat.card ι and Nat.card σ.”.

Let S = R[x_1, …, x_n]/(f_1, …, f_c), presented by P, and let 𝔮 be a prime of S with dim_𝔮(S/R) = n - c. Then there is an h ∈ R[x_1, …, x_n] whose image g ∈ S is not in 𝔮, such that S_g = R[x_1, …, x_n, x_{n+1}]/(f_1, …, f_c, h x_{n+1} - 1) is a relative global complete intersection with this presentation.

theorem Algebra.Presentation.exists_notMem_isRelativeGlobalCompleteIntersection
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {ι σ : Type*} [Finite ι] [Finite σ]
    (P : Algebra.Presentation R S ι σ) (q : Ideal S) [q.IsPrime]
    (hq : Algebra.relativeDimensionAt R q + ((Nat.card σ : ℕ) : WithBot ℕ∞) =
      ((Nat.card ι : ℕ) : WithBot ℕ∞)) :
    ∃ h : P.Ring, algebraMap P.Ring S h ∉ q ∧
      (P.localizationAwayComp h
        (Localization.Away (algebraMap P.Ring S h))).IsRelativeGlobalCompleteIntersection
Tag 00SU, a lemma

Tag 00SU in the Stacks Project.

Algebra.Presentation.exists_fg_isRelativeGlobalCompleteIntersection_naive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/Morphisms.lean, line 698. The attribute's comment: “The subalgebra is a finitely generated Subalgebra ℤ R, the relations over it are f₀ with MvPolynomial.map (algebraMap R₀ R) (f₀ k) = f_k, and S₀ is presented by Algebra.Presentation.naive. Stated for arbitrary finite index types.”.

Stacks 00SU. Let S = R[x_1, …, x_n]/(f_1, …, f_c) be a relative global complete intersection. There is a finite type ℤ-subalgebra R₀ ⊆ R with f_k ∈ R₀[x_1, …, x_n] such that S₀ = R₀[x_1, …, x_n]/(f_1, …, f_c) is a relative global complete intersection.

theorem Algebra.Presentation.exists_fg_isRelativeGlobalCompleteIntersection_naive
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {ι σ : Type*} [Finite ι] [Finite σ]
    (P : Algebra.Presentation R S ι σ) [P.IsRelativeGlobalCompleteIntersection] :
    ∃ (R₀ : Subalgebra ℤ R) (_ : R₀.FG) (f₀ : σ → MvPolynomial ι R₀),
      (∀ j, MvPolynomial.map (algebraMap R₀ R) (f₀ j) = P.relation j) ∧
        (Algebra.Presentation.naive (v := f₀)).IsRelativeGlobalCompleteIntersection
Tag 00SV, a lemma

Tag 00SV in the Stacks Project.

Algebra.Presentation.isRegular_localization_relation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RelativeConormal.lean, line 947. The attribute's comment: “(1): RingTheory.Sequence.IsRegular is Definition 00LF verbatim, nonvanishing clause included, for the list of images of f_1, …, f_c in Localization.AtPrime 𝔮', 𝔮' = 𝔮 ∩ R[x_1, …, x_n].”.

Stacks 00SV (1). Let S = R[x_1, …, x_n]/(f_1, …, f_c), presented by P, be a relative global complete intersection (Definition 00SP). For every prime 𝔮 of S, with corresponding prime 𝔮' of R[x_1, …, x_n], the relations f_1, …, f_c form a regular sequence in the local ring R[x_1, …, x_n]_{𝔮'}.

theorem Algebra.Presentation.isRegular_localization_relation {R : Type*} [CommRing R] {S : Type*}
    [CommRing S] [Algebra R S] {ι : Type*} [Finite ι] {c : ℕ}
    (P : Algebra.Presentation R S ι (Fin c)) [P.IsRelativeGlobalCompleteIntersection]
    (q : Ideal S) [q.IsPrime] :
    RingTheory.Sequence.IsRegular (Localization.AtPrime (q.comap (algebraMap P.Ring S)))
      ((List.ofFn P.relation).map
        (algebraMap P.Ring (Localization.AtPrime (q.comap (algebraMap P.Ring S)))))

Algebra.Presentation.flat_localization_quotient_relation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RelativeConormal.lean, line 964. The attribute's comment: “(2): R[x_1, …, x_n]_{𝔮'}/(f_1, …, f_i) is the quotient of Localization.AtPrime 𝔮' by the ideal generated by the first i images of the relations, for every i : ℕ (List.take saturates at c).”.

Stacks 00SV (2). Let S = R[x_1, …, x_n]/(f_1, …, f_c), presented by P, be a relative global complete intersection (Definition 00SP). For every prime 𝔮 of S, with corresponding prime 𝔮' of R[x_1, …, x_n], each of the rings R[x_1, …, x_n]_{𝔮'}/(f_1, …, f_i) is flat over R.

theorem Algebra.Presentation.flat_localization_quotient_relation {R : Type*} [CommRing R]
    {S : Type*} [CommRing S] [Algebra R S] {ι : Type*} [Finite ι] {c : ℕ}
    (P : Algebra.Presentation R S ι (Fin c)) [P.IsRelativeGlobalCompleteIntersection]
    (q : Ideal S) [q.IsPrime] (i : ℕ) :
    Module.Flat R (Localization.AtPrime (q.comap (algebraMap P.Ring S)) ⧸
      Ideal.ofList (((List.ofFn P.relation).map
        (algebraMap P.Ring (Localization.AtPrime (q.comap (algebraMap P.Ring S))))).take i))

Algebra.Presentation.exists_basis_cotangent_relation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/RelativeConormal.lean, line 981. The attribute's comment: “(3): the conormal module I/I² is P.toExtension.Cotangent, and the basis is pinned: its i-th vector is the class of the relation f_i.”.

Stacks 00SV (3). Let S = R[x_1, …, x_n]/(f_1, …, f_c), presented by P, be a relative global complete intersection (Definition 00SP). Then the conormal module I/I² of I = (f_1, …, f_c) is free over S on the classes of f_1, …, f_c.

theorem Algebra.Presentation.exists_basis_cotangent_relation {R : Type*} [CommRing R] {S : Type*}
    [CommRing S] [Algebra R S] {ι : Type*} [Finite ι] {c : ℕ}
    (P : Algebra.Presentation R S ι (Fin c)) [P.IsRelativeGlobalCompleteIntersection] :
    ∃ b : Module.Basis (Fin c) S P.toExtension.Cotangent,
      ∀ i, b i = Algebra.Extension.Cotangent.mk ⟨P.relation i, P.relation_mem_ker i⟩
Tag 00SW, a lemma

Tag 00SW in the Stacks Project.

Algebra.Syntomic.of_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/RelativeGlobalCompleteIntersection.lean, line 138. The attribute's comment: “Stated for the class Algebra.IsRelativeGlobalCompleteIntersection R S and concluding Algebra.Syntomic R S, the whole of Definition 00SL, not only the flatness that the source's "i.e., flat" singles out.”.

A relative global complete intersection is syntomic: if S = R[x_1, …, x_n]/(f_1, …, f_c) is a relative global complete intersection over R, then R → S is flat, of finite presentation, and its fibres are local complete intersections over the residue fields.

theorem Algebra.Syntomic.of_isRelativeGlobalCompleteIntersection (R S : Type*) [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.IsRelativeGlobalCompleteIntersection R S] :
    Algebra.Syntomic R S
Tag 03HS, a lemma

Tag 03HS in the Stacks Project.

Polynomial.Monic.exists_finite_free_faithfullyFlat_syntomic_map_eq_prod_X_sub_C, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/SplittingExtension.lean, line 287. The attribute's comment: “The source's finite free faithfully flat extension A ⊂ A': the injectivity of algebraMap A A' is not a conjunct, being FaithfulSMul.algebraMap_injective applied to Module.FaithfullyFlat A A'. The splitting is the explicit product over Fin P.natDegree, which names the roots the consumers use and is stronger than Polynomial.Splits. Unlike the Mathlib sibling Polynomial.Monic.exists_splits_map, no Nontrivial A is assumed and the extension is also faithfully flat and syntomic (Definition 00SL). See the module docstring.”.

Stacks 03HS. Let A be a ring and let P ∈ A[x] be monic. There is a finite free, faithfully flat, syntomic extension A ⊂ A' and elements β_1, …, β_n ∈ A', n = deg P, with P = ∏ (x - β_i) in A'[x]. The inclusion A ⊂ A' is the faithful flatness: it gives FaithfulSMul A A', hence algebraMap A A' injective.

public theorem Polynomial.Monic.exists_finite_free_faithfullyFlat_syntomic_map_eq_prod_X_sub_C
    {A : Type u} [CommRing A] {P : A[X]} (hP : P.Monic) :
    ∃ (A' : Type u) (_ : CommRing A') (_ : Algebra A A') (_ : Module.Finite A A')
      (_ : Module.Free A A') (_ : Module.FaithfullyFlat A A') (_ : Algebra.Syntomic A A')
      (β : Fin P.natDegree → A'), P.map (algebraMap A A') = ∏ i, (X - C (β i))
Tag 00SY, a lemma

Tag 00SY in the Stacks Project.

Algebra.exists_notMem_syntomic_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/SyntomicAt.lean, line 561. The attribute's comment: “The principal localization S_g is Localization.Away g, the local ring map R_𝔭 → S_𝔮 is Localization.localRingHom for the lying-over relation, and S_𝔮/𝔭S_𝔮 is the fibre 𝔭.Fiber S_𝔮 = κ(𝔭) ⊗_R S_𝔮, canonically a κ(𝔭)-algebra, which is S_𝔮/𝔭S_𝔮 because S_𝔮 is an R_𝔭-algebra.”.

Let R → S be a ring map and let 𝔮 be a prime of S lying over the prime 𝔭 of R. The following are equivalent:

  1. there is a g ∈ S, g ∉ 𝔮, such that R → S_g is syntomic;
  2. there is a g ∈ S, g ∉ 𝔮, such that S_g is a relative global complete intersection over R;
  3. there is a g ∈ S, g ∉ 𝔮, such that R → S_g is of finite presentation, the local ring map R_𝔭 → S_𝔮 is flat, and S_𝔮/𝔭S_𝔮 is a complete intersection over κ(𝔭).
theorem Algebra.exists_notMem_syntomic_tfae {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    List.TFAE
      [∃ g ∉ q, Algebra.Syntomic R (Localization.Away g),
        ∃ g ∉ q, Algebra.IsRelativeGlobalCompleteIntersection R (Localization.Away g),
        ∃ g ∉ q,
          Algebra.FinitePresentation R (Localization.Away g) ∧
            (letI : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
              (Localization.localRingHom p q (algebraMap R S) (q.over_def p)).toAlgebra
             Module.Flat (Localization.AtPrime p) (Localization.AtPrime q)) ∧
              IsCompleteIntersection p.ResidueField (p.Fiber (Localization.AtPrime q))]
Tag 07BT, a lemma

Tag 07BT in the Stacks Project.

Algebra.Generators.finite_and_projective_tensor_cotangent_of_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/Morphisms.lean, line 918. The attribute's comment: “The presentation R[x_1, …, x_n] → S is Algebra.Generators R S (Fin n), I/I² is its cotangent module P.toExtension.Cotangent, and (I/I²)_g is the base change T ⊗_S I/I² to a localization T of S away from g. The source's hypothesis that I is finitely generated is not needed.”.

Stacks 07BT. Let S = R[x_1, …, x_n]/I and let g ∈ S be such that S_g is syntomic over R. Then (I/I²)_g is a finite projective S_g-module.

theorem Algebra.Generators.finite_and_projective_tensor_cotangent_of_syntomic {R S T : Type*}
    [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T]
    [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] [Algebra.Syntomic R T] {n : ℕ}
    (P : Algebra.Generators R S (Fin n)) :
    Module.Finite T (T ⊗[S] P.toExtension.Cotangent) ∧
      Module.Projective T (T ⊗[S] P.toExtension.Cotangent)
Tag 00SZ, a lemma

Tag 00SZ in the Stacks Project.

Algebra.IsRelativeGlobalCompleteIntersection.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/Morphisms.lean, line 477. The attribute's comment: “(2). Stated for the class Algebra.IsRelativeGlobalCompleteIntersection along a scalar tower R → S → S'; the composite presentation is Algebra.Presentation.isRelativeGlobalCompleteIntersection_comp.”.

Stacks 00SZ (2). If R → S and S → S' are relative global complete intersections, then so is R → S'.

theorem Algebra.IsRelativeGlobalCompleteIntersection.comp (R S S' : Type*) [CommRing R]
    [CommRing S] [CommRing S'] [Algebra R S] [Algebra S S'] [Algebra R S'] [IsScalarTower R S S']
    [Algebra.IsRelativeGlobalCompleteIntersection R S]
    [Algebra.IsRelativeGlobalCompleteIntersection S S'] :
    Algebra.IsRelativeGlobalCompleteIntersection R S'

Algebra.Syntomic.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/Morphisms.lean, line 490. The attribute's comment: “(1). Stated for the class Algebra.Syntomic along a scalar tower R → S → S'.”.

Stacks 00SZ (1). If R → S and S → S' are syntomic, then so is R → S'.

theorem Algebra.Syntomic.comp (R S S' : Type*) [CommRing R] [CommRing S] [CommRing S']
    [Algebra R S] [Algebra S S'] [Algebra R S'] [IsScalarTower R S S'] [Algebra.Syntomic R S]
    [Algebra.Syntomic S S'] : Algebra.Syntomic R S'
Tag 00T0, a lemma

Tag 00T0 in the Stacks Project.

Algebra.Syntomic.exists_span_eq_top_algEquiv_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Syntomic/Morphisms.lean, line 852. The attribute's comment: “The syntomic R/I-algebra S̄ is an R-algebra through R → R/I, the elements ḡ_i are a set s with Ideal.span s = ⊤, and S̄_{ḡ_i} ≅ S_i/IS_i is an isomorphism of R-algebras.”.

Stacks 00T0. Let I ⊆ R be an ideal and let R/I → S̄ be syntomic. There are elements ḡ_i ∈ S̄ generating the unit ideal such that every S̄_{ḡ_i} is isomorphic to S_i/IS_i for a relative global complete intersection S_i over R.

theorem Algebra.Syntomic.exists_span_eq_top_algEquiv_quotient {R : Type u} [CommRing R]
    (I : Ideal R) {S : Type v} [CommRing S] [Algebra R S] [Algebra (R ⧸ I) S]
    [IsScalarTower R (R ⧸ I) S] [Algebra.Syntomic (R ⧸ I) S] :
    ∃ s : Set S, Ideal.span s = ⊤ ∧ ∀ g ∈ s, ∃ (T : Type u) (_ : CommRing T) (_ : Algebra R T),
      Algebra.IsRelativeGlobalCompleteIntersection R T ∧
        Nonempty ((T ⧸ I.map (algebraMap R T)) ≃ₐ[R] Localization.Away g)
Sources
LeanAlgebra.Syntomic · Algebra.IsPushout.syntomic_iff · Algebra.IsPushout.syntomic · isSyntomic_of_isSyntomic_localization_away · Algebra.Presentation.IsRelativeGlobalCompleteIntersection · Algebra.IsRelativeGlobalCompleteIntersection · Algebra.exists_presentation_basis_cotangent_of_free_cotangent · MvPolynomial.universalFactorizationMapBaseChangeAlgHomEquiv

Section10.137 Smooth ring maps#

Section 10.137 of the Stacks Project, Tag 00T1. 18 tags here are carried by 15 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00T3, a lemma

Tag 00T3 in the Stacks Project.

Algebra.Smooth.localization_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Localization.lean, line 141. The attribute's comment: “First assertion: any localization S_g is smooth over R. Algebra.Smooth is Mathlib's definition (formally smooth and of finite presentation), equivalent to 00T2 by 00TN. The localization is an abstract IsLocalization.Away g S'. See the module docstring.”.

Let R → S be a smooth ring map and let S' be a localization of S away from an element g : S. Then S' is smooth over R.

public theorem Algebra.Smooth.localization_away {R S S' : Type*} [CommRing R] [CommRing S]
    [CommRing S'] [Algebra R S] [Algebra R S'] [Algebra S S'] [IsScalarTower R S S']
    [Algebra.Smooth R S] (g : S) [IsLocalization.Away g S'] :
    Algebra.Smooth R S'

Algebra.Smooth.localization_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Localization.lean, line 157. The attribute's comment: “Second assertion: if f ∈ R maps to an invertible element of S then R_f → S is smooth. Stated as the Algebra.Smooth analogue of Algebra.FormallySmooth.localization_base: the base is localized at an arbitrary submonoid M, and the hypothesis on f is the pair [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]. Algebra.Smooth is Mathlib's definition (formally smooth and of finite presentation), equivalent to 00T2 by 00TN. See the module docstring.”.

Let M be a multiplicative subset of R and Rₘ a localization of R at M. Let Sₘ be an R-algebra which is smooth over R and which is an Rₘ-algebra compatibly with its R-algebra structure — for M the powers of f ∈ R this last condition says that f maps to an invertible element of Sₘ. Then Sₘ is smooth over Rₘ.

public theorem Algebra.Smooth.localization_base {R Rₘ Sₘ : Type*} [CommRing R] [CommRing Rₘ]
    [CommRing Sₘ] [Algebra R Rₘ] [Algebra R Sₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]
    (M : Submonoid R) [IsLocalization M Rₘ] [Algebra.Smooth R Sₘ] :
    Algebra.Smooth Rₘ Sₘ
Tag 00T4, a lemma

Tag 00T4 in the Stacks Project.

Declarations registered for the tag:

  • Algebra.Smooth.baseChange registered with add_to_stacks in StacksFrontier/RingTheory/Smooth/Basic.lean, line 61 (StacksFrontier): “smoothness is stable under base change”. References: EGA 0 (19.3.5), “(iii), special case”; EGA 0 (19.4.2), “Necessity, special case”; EGA 0 (19.4.6), “special case”; EGA IV (17.3.3), “(iii), special case”; EGA IV (17.7.3), “(ii)”; EGA IV (6.8.2), “special case”; EGA IV (6.8.3), “(iii), special case”; SGA 1 II (4.13), “affine ascent”; SGA 3 VIB (10.1), “smoothness, special case”; SGA 3 VIB (2.1.2), “special case”; SGA 6 VIII (1.6), “special case”; SGA 6 VIII (1.8), “affine case”; SGA 6 X (7.13.3), “special case”; SGA 1 II (1.3), “(ii), affine case”.
Tag 00T5, a lemma

Tag 00T5 in the Stacks Project.

isLocalCompleteIntersection_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/Smooth.lean, line 136. The attribute's comment: “The source's smooth (Definition 00T2) is Algebra.Smooth, by Proposition 00TN; its finite type hypothesis on S is not repeated, being Algebra.Smooth.finitePresentation. A local complete intersection over k (Definition 00S9 (2)) is IsLocalCompleteIntersection. See the module docstring.”.

A smooth algebra over a field is a local complete intersection. Let k be a field and let S be a smooth k-algebra. Then S is a local complete intersection over k: there is a family of elements of S generating the unit ideal — equivalently, whose standard opens cover Spec S — each of whose localizations S_g admits a presentation k[x₁, …, xₙ]/(f₁, …, f_c) with dim S_g = n - c.

public theorem isLocalCompleteIntersection_of_smooth (k : Type u) [Field k] (S : Type v)
    [CommRing S] [Algebra k S] [Algebra.Smooth k S] :
    IsLocalCompleteIntersection k S
Tag 00T6, a definition

Tag 00T6 in the Stacks Project.

Declarations registered for the tag:

Tag 00T7, a lemma

Tag 00T7 in the Stacks Project.

Algebra.SubmersivePresentation.smooth_and_free_and_isStandardSmooth_and_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/StandardSmoothProperties.lean, line 111. The attribute's comment: “The standard smooth algebra is a submersive presentation P (Definition 00T6 is Mathlib's Algebra.IsStandardSmooth). The source's x_1, …, x_c are the variables P.map j paired with the relations, so its dx_{c+1}, …, dx_n are the dx_i for i ∉ range P.map. I/I² is P.toExtension.Cotangent. In (6) the R_f-algebra structure on S is the one factoring R → S. (7) is stated for the presentation P itself.”.

Let S = R[x_1, …, x_n]/(f_1, …, f_c) be standard smooth, via a submersive presentation P. Then (1) R → S is smooth; (2) Ω_{S/R} is free on the dx_i for the variables x_i not paired with a relation; (3) I/I² is free on the classes of the f_j; (4) S_g is standard smooth over R for every g ∈ S; (5) R' ⊗_R S is standard smooth over R' for every R-algebra R'; (6) if f ∈ R maps to a unit of S, then S is standard smooth over R_f; (7) S is a relative global complete intersection over R.

theorem smooth_and_free_and_isStandardSmooth_and_isRelativeGlobalCompleteIntersection :
    Algebra.Smooth R S ∧
    (∃ b : Module.Basis ((Set.range P.map)ᶜ : Set ι) S Ω[S⁄R],
      ∀ i, b i = KaehlerDifferential.D R S (P.val i)) ∧
    (∃ b : Module.Basis σ S P.toExtension.Cotangent,
      ∀ j, b j = Extension.Cotangent.mk ⟨P.relation j, P.relation_mem_ker j⟩) ∧
    (∀ g : S, IsStandardSmooth R (Localization.Away g)) ∧
    (∀ (R' : Type*) [CommRing R'] [Algebra R R'], IsStandardSmooth R' (R' ⊗[R] S)) ∧
    (∀ (f : R) (hf : IsUnit (algebraMap R S f)),
      letI := (IsLocalization.Away.lift (S := Localization.Away f) f hf).toAlgebra
      IsStandardSmooth (Localization.Away f) S) ∧
    P.toPresentation.IsRelativeGlobalCompleteIntersection
Tag 00T8, an example

Tag 00T8 in the Stacks Project.

Stacks.StandardSmooth.isStandardSmooth_SAlg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/StandardSmooth.lean, line 409.

Theorem (Stacks Tag 00T8). With f : Fin c → R[x_0, ..., x_{n-1}], h = det(jacobianFirst f), and S = R[x_0, ..., x_n] / (f_0, ..., f_{c-1}, x_n * h - 1), the algebra S is standard smooth over R. The witnessing presentation reorders the variables so that the first c + 1 variables (in the chosen order) are x_0, ..., x_{c-1}, x_n, and uses the relations g_0, ..., g_c.

theorem isStandardSmooth_SAlg {n c : ℕ} (hc : c ≤ n) (f : Fin c → MvPolynomial (Fin n) R) :
    IsStandardSmooth (R := R) (SAlg hc f)
Tag 00T9, a lemma

Tag 00T9 in the Stacks Project.

Declarations registered for the tag:

Tag 00TA, a lemma

Tag 00TA in the Stacks Project.

Algebra.Smooth.exists_span_eq_top_isStandardSmooth_and_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Syntomic.lean, line 38. The attribute's comment: “The cover by standard opens D(g), g ∈ s, is Ideal.span s = ⊤. Syntomic is Algebra.Syntomic (Definition 00SL); it is derived here directly from Lemma 00T5 on the fibres rather than through Lemmas 00T7, 00SW and 00SO.”.

Stacks 00TA. Let R → S be a smooth ring map. There are g ∈ S whose standard opens D(g) cover Spec(S) and such that each S_g is standard smooth over R. In particular R → S is syntomic.

theorem exists_span_eq_top_isStandardSmooth_and_syntomic [Smooth R S] :
    (∃ s : Set S, Ideal.span s = ⊤ ∧ ∀ g ∈ s, IsStandardSmooth R (Localization.Away g)) ∧
      Syntomic R S
Tag 00TB, a definition

Tag 00TB in the Stacks Project.

Algebra.SmoothAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/SmoothAt.lean, line 19. References: SGA 1 II (1.1).

A ring map R → S is smooth at a prime q of S if there exists some g ∈ S with g ∉ q such that the induced map R → S_g is smooth.

def Algebra.SmoothAt (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (q : Ideal S) [q.IsPrime] : Prop
Tag 07BU, a lemma

Tag 07BU in the Stacks Project.

Algebra.isSmoothAt_tfae_h1Cotangent_and_kaehlerDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/NaiveCotangentCriterion.lean, line 244. The attribute's comment: “The localizations H_1(L_{S/R})_q and Ω_{S/R, q} are read on an arbitrary model Sq of S_q as Algebra.H1Cotangent R Sq and Ω[Sq⁄R], which is Lemma 00S7 and is witnessed by the instances Algebra.H1Cotangent.isLocalizedModule and KaehlerDifferential.isLocalizedModule_map; vanishing is Subsingleton and finite free is Module.Finite and Module.Free. Item (1) is Definition 00TB verbatim, and Mathlib's Algebra.IsSmoothAt is added as item (5). See the module docstring.”. References: EGA 0 (22.6.4), “special case”.

Smoothness at a prime is the vanishing of H_1 together with freeness of Ω (Stacks 07BU). Let R → S be of finite presentation, let q be a prime of S and let Sq be a model of S_q. The following are equivalent: (1) R → S is smooth at q, that is R → S_g is smooth for some g ∉ q; (2) H_1(L_{S/R})_q = 0 and Ω_{S/R, q} is a finite free S_q-module; (3) H_1(L_{S/R})_q = 0 and Ω_{S/R, q} is projective; (4) H_1(L_{S/R})_q = 0 and Ω_{S/R, q} is flat; (5) S_q is formally smooth over R.

public theorem Algebra.isSmoothAt_tfae_h1Cotangent_and_kaehlerDifferential
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S]
    (q : Ideal S) [q.IsPrime] (Sq : Type*) [CommRing Sq] [Algebra S Sq]
    [IsLocalization.AtPrime Sq q] [Algebra R Sq] [IsScalarTower R S Sq] :
    List.TFAE
      [∃ g ∉ q, Algebra.Smooth R (Localization.Away g),
       Subsingleton (Algebra.H1Cotangent R Sq) ∧
         Module.Finite Sq Ω[Sq⁄R] ∧ Module.Free Sq Ω[Sq⁄R],
       Subsingleton (Algebra.H1Cotangent R Sq) ∧ Module.Projective Sq Ω[Sq⁄R],
       Subsingleton (Algebra.H1Cotangent R Sq) ∧ Module.Flat Sq Ω[Sq⁄R],
       Algebra.IsSmoothAt R q]
Tag 00TC, a lemma

Tag 00TC in the Stacks Project.

Algebra.smooth_iff_forall_exists_notMem_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/SmoothAt.lean, line 199. The attribute's comment: “Smoothness at a prime q (Definition 00TB) is spelled out as ∃ g ∉ q, with Localization.Away g smooth over R — as in Mathlib's Algebra.IsSmoothAt.exists_notMem_smooth — and not as Mathlib's Algebra.IsSmoothAt, which is formal smoothness of S_q and makes the equivalence false for S not of finite presentation over R (witness: k[x_i : i ∈ ℕ] over k). Producing the finite presentation of S from the pointwise hypothesis is precisely the content of this lemma. Stated for algebras; RingHom.smooth_algebraMap gives the form for a bundled ring map. See the module docstring.”.

Smoothness is detected at the primes of the target. A ring map R → S is smooth if and only if it is smooth at every prime q of S, that is, if and only if for every prime q ⊂ S there is a g ∈ S, g ∉ q, with R → S_g smooth (Definition 00TB).

Beware that the right-hand side is the Stacks project's notion of smoothness at q, which is strictly stronger than Mathlib's Algebra.IsSmoothAt R q = Algebra.FormallySmooth R S_q when S is not of finite presentation over R; see the module docstring.

public theorem Algebra.smooth_iff_forall_exists_notMem_smooth (R : Type*) [CommRing R] (S : Type*)
    [CommRing S] [Algebra R S] :
    Algebra.Smooth R S ↔
      ∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, Algebra.Smooth R (Localization.Away g)
Tag 00TD, a lemma

Tag 00TD in the Stacks Project.

Declarations registered for the tag:

Tag 0GIF, a lemma

Tag 0GIF in the Stacks Project.

Algebra.Smooth.prod_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Pi.lean, line 256. The attribute's comment: “The product is the literal S' × S'', with the componentwise Prod.algebra structure; the abstract form (an S with S ≃ₐ[R] S' × S'') follows by transport, via Algebra.FormallySmooth.of_equiv and Algebra.FinitePresentation.equiv. The two factors are allowed to lie in different universes, so this is not an instance of Mathlib's Algebra.FormallySmooth.pi_iff; that lemma also settles only the formal smoothness half, the finite presentation of each factor of a finitely presented product being the content added here. See the module docstring.”.

A product of two algebras is smooth if and only if both factors are. Let R be a ring and let S = S' × S'' be a product of R-algebras. Then S is smooth over R if and only if both S' and S'' are smooth over R.

Each factor is the principal localization of S at one of the complementary idempotents (1, 0) and (0, 1), which is why the equivalence holds; see the module docstring.

public theorem Algebra.Smooth.prod_iff (R : Type*) [CommRing R] (S' : Type*) [CommRing S']
    [Algebra R S'] (S'' : Type*) [CommRing S''] [Algebra R S''] :
    Algebra.Smooth R (S' × S'') ↔ Algebra.Smooth R S' ∧ Algebra.Smooth R S''
Tag 00TE, a lemma

Tag 00TE in the Stacks Project.

Algebra.Presentation.isSmoothAt_iff_exists_jacobian_notMem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/JacobianCriterion.lean, line 386. The attribute's comment: “The subset I ⊆ {1, …, n} of cardinality c is an injection σ ↪ ι from the relations to the variables — that is, the extra datum of an Algebra.PreSubmersivePresentation — and the image of g_I in S is its jacobian. The hypothesis is placed on the given presentation P, not on the class Algebra.IsRelativeGlobalCompleteIntersection (00SP), since the criterion depends on P; it is verbatim the condition that class asserts of its chosen presentation. Index types are arbitrary finite ones rather than Fin n, Fin c, and smoothness at q is Algebra.IsSmoothAt (00TB). See the module docstring.”.

Jacobian criterion for smoothness at a prime. Let S = R[x_1, …, x_n]/(f_1, …, f_c) be a presentation of S over R such that every nonempty fibre of Spec(S) → Spec(R) has dimension n - c, i.e. a relative global complete intersection (Definition 00SP). Then R → S is smooth at a prime q ⊂ S if and only if there is a subset I ⊆ {1, …, n} of cardinality c such that g_I = det (∂f_j/∂x_i)_{j = 1, …, c, i ∈ I} does not map into q.

The subset I is an injection f : σ ↪ ι from the relations to the variables, and the image of g_I in S is the Algebra.PreSubmersivePresentation.jacobian of P equipped with f. See the module docstring.

public theorem Algebra.Presentation.isSmoothAt_iff_exists_jacobian_notMem {R S : Type*}
    [CommRing R] [CommRing S] [Algebra R S] {ι σ : Type*} [Finite ι] [Finite σ]
    (P : Algebra.Presentation R S ι σ)
    (hP : ∀ (p : Ideal R) [p.IsPrime], Nontrivial (p.Fiber S) →
      ringKrullDim (p.Fiber S) + Nat.card σ = Nat.card ι)
    (q : Ideal S) [q.IsPrime] :
    Algebra.IsSmoothAt R q ↔
      ∃ f : σ ↪ ι, (Algebra.PreSubmersivePresentation.mk P f f.injective).jacobian ∉ q
Tag 00TF, a lemma

Tag 00TF in the Stacks Project.

Algebra.exists_notMem_smooth_of_isSmoothAt_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/SmoothAt.lean, line 570. The attribute's comment: “Smoothness at q in the conclusion is spelled out as Definition 00TB, ∃ g ∉ q with Localization.Away g smooth over R, while smoothness of the fibre at Q is Mathlib's Algebra.IsSmoothAt; the two notions agree under hypothesis (1), so this is the weakest hypothesis with the strongest conclusion. The fibre is Ideal.Fiber and Q is pinned as the prime corresponding to q by hq, the inverse of PrimeSpectrum.preimageEquivFiber. Flatness of R_p → S_q is stated over R, which for the R_p-algebra S_q is the same condition (Module.flat_iff_of_isLocalization). This is the full generality of the tag; upstream's Algebra.IsSmoothAt.of_formallySmooth_fiber is the case of all three hypotheses imposed globally. See the module docstring.”. References: SGA 1 II (2.1), “(a) + (b) ⇒ smooth”; SGA 3 VIB (3.10), “special case”.

Flat with a smooth fibre implies smooth, at a prime. Let R → S be a ring map, let q be a prime of S and let Q be the prime of the fibre κ(p) ⊗_R S corresponding to q, where p is the prime of R under q. Assume that R → S_g is of finite presentation for some g ∉ q, that S_q is flat over R — equivalently, that the local homomorphism R_p → S_q is flat — and that the fibre is smooth over κ(p) at Q. Then R → S is smooth at q: there is a g ∈ S, g ∉ q, with R → S_g smooth (Definition 00TB).

Note that q lies over p automatically, this being part of hq.

public theorem Algebra.exists_notMem_smooth_of_isSmoothAt_fiber {R S : Type*} [CommRing R]
    [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Q : Ideal (p.Fiber S)) [Q.IsPrime]
    [Algebra.IsSmoothAt p.ResidueField Q] (q : Ideal S) [q.IsPrime]
    [Module.Flat R (Localization.AtPrime q)]
    (hq : Q.comap (Algebra.TensorProduct.includeRight : S →ₐ[R] p.Fiber S) = q)
    (hfp : ∃ g ∉ q, Algebra.FinitePresentation R (Localization.Away g)) :
    ∃ g ∉ q, Algebra.Smooth R (Localization.Away g)
Tag 00TG, a lemma

Tag 00TG in the Stacks Project.

Algebra.smoothLocus_comap_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/LocusBaseChange.lean, line 300. The attribute's comment: “The base change is the abstract one, Algebra.IsPushout R S R' S', and the two smooth loci are Mathlib's Algebra.smoothLocus, which for a finitely presented algebra is the source's set of primes at which the map is smooth (Definition 00TB, via Lemma 07BU). The equality is oriented as f⁻¹(U) = V, as in Algebra.smoothLocus_comap_of_isLocalization. See the module docstring.”. References: EGA IV (17.7.2), “(ii), affine case”; SGA 1 II (4.13), “affine case”.

The smooth locus is stable under flat base change (Stacks 00TG). Let R → S be of finite presentation, let R → R' be flat and let S' be the base change R' ⊗_R S. Then the set of primes of S' at which R' → S' is smooth is the inverse image, under f : Spec(S') → Spec(S), of the set of primes of S at which R → S is smooth.

public theorem Algebra.smoothLocus_comap_of_isPushout (R S R' S' : Type*) [CommRing R] [CommRing S]
    [CommRing R'] [CommRing S'] [Algebra R S] [Algebra R R'] [Algebra S S'] [Algebra R' S']
    [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
    [Algebra.IsPushout R S R' S'] [Algebra.FinitePresentation R S] [Module.Flat R R'] :
    PrimeSpectrum.comap (algebraMap S S') ⁻¹' Algebra.smoothLocus R S
      = Algebra.smoothLocus R' S'
Tag 02UQ, a lemma

Tag 02UQ in the Stacks Project.

Algebra.isSmoothAt_iff_isSmoothAt_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/LocusBaseChange.lean, line 461. The attribute's comment: “The source takes K/k a field extension; K is here an arbitrary commutative k-algebra, since only flatness of k → K is used and that is automatic over a field. The base change is the abstract one, Algebra.IsPushout k S K S', the prime correspondence is Ideal.LiesOver, and smoothness at a prime is Mathlib's Algebra.IsSmoothAt, which for a finite type algebra over a field is the source's Definition 00TB. See the module docstring.”.

Smoothness at a prime is insensitive to base field extension (Stacks 02UQ). Let k be a field, S a finite type k-algebra, K a k-algebra and S' the base change K ⊗_k S. Let q' be a prime of S' lying over the prime q of S. Then S is smooth over k at q if and only if S' is smooth over K at q'.

public theorem Algebra.isSmoothAt_iff_isSmoothAt_of_isPushout {k S K S' : Type*} [Field k]
    [CommRing S] [CommRing K] [CommRing S'] [Algebra k S] [Algebra k K] [Algebra S S']
    [Algebra K S'] [Algebra k S'] [IsScalarTower k K S'] [IsScalarTower k S S']
    [Algebra.IsPushout k S K S'] [Algebra.FiniteType k S] (q : Ideal S) (q' : Ideal S')
    [q.IsPrime] [q'.IsPrime] [q'.LiesOver q] :
    Algebra.IsSmoothAt k q ↔ Algebra.IsSmoothAt K q'
Tag 04B1, a lemma

Tag 04B1 in the Stacks Project.

Algebra.Smooth.exists_span_eq_top_isStandardSmooth_algEquiv_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/LocalStructure.lean, line 185. The attribute's comment: “The source's R/I → S̄ is stated for an arbitrary surjection R → R', which is what the proof uses (it lifts the relations along R[x] → R'[x]); the source's form is the case R' = R ⧸ I, by Ideal.Quotient.mk_surjective. The source's S_i/I S_i is the base change R' ⊗[R] S, identified with that quotient over R ⧸ I by Algebra.TensorProduct.quotIdealMapEquivQuotTensor. The parenthetical (standard) is taken as the assertion. See the module docstring.”.

Let R → R' be a surjective ring map (for instance R' = R ⧸ I) and let R' → S' be smooth. Then there are elements g ∈ S' generating the unit ideal of S' such that each S'_g is isomorphic as an R'-algebra to R' ⊗[R] S for some standard smooth R-algebra S; that is, S' is, locally on Spec S', a base change of a standard smooth R-algebra.

public theorem Algebra.Smooth.exists_span_eq_top_isStandardSmooth_algEquiv_tensorProduct
    (R : Type u) [CommRing R] (R' : Type v) [CommRing R'] [Algebra R R']
    (hsurj : Function.Surjective (algebraMap R R'))
    (S' : Type w) [CommRing S'] [Algebra R' S'] [Algebra.Smooth R' S'] :
    ∃ s : Set S', Ideal.span s = ⊤ ∧ ∀ g ∈ s,
      ∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S) (_ : Algebra.IsStandardSmooth R S),
        Nonempty (Localization.Away g ≃ₐ[R'] R' ⊗[R] S)
Sources
LeanAlgebra.Smooth.localization_away · Algebra.Smooth.localization_base · Algebra.Smooth.baseChange · isLocalCompleteIntersection_of_smooth · Algebra.SubmersivePresentation · Algebra.IsStandardSmooth · Algebra.SubmersivePresentation.smooth_and_free_and_isStandardSmooth_and_isRelativeGlobalCompleteIntersection · Stacks.StandardSmooth.isStandardSmooth_SAlg

Section10.138 Formally smooth maps#

Section 10.138 of the Stacks Project, Tag 00TH. 12 tags here are carried by 10 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00TJ, a lemma

Tag 00TJ in the Stacks Project.

Declarations registered for the tag:

Tag 031H, a lemma

Tag 031H in the Stacks Project.

Declarations registered for the tag:

Tag 00TK, a lemma

Tag 00TK in the Stacks Project.

Declarations registered for the tag:

Tag 00TL, a lemma

Tag 00TL in the Stacks Project.

Declarations registered for the tag:

Tag 031J, a proposition

Tag 031J in the Stacks Project.

Algebra.FormallySmooth.tfae_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormallySmooth/Presentation.lean, line 127. The attribute's comment: “Stated for a variable formally smooth presentation, giving the source's for some P and for all P forms at once; see the module docstring.”. References: EGA 0 (20.4.9), “discrete case”; EGA IV (17.2.3), “(i), affine case”.

Let R → S be a ring map, let P be a formally smooth R-algebra and let P → S be a surjection with kernel J. The following are equivalent:

  1. S is formally smooth over R;
  2. the surjection P ⧸ J² → S admits an R-algebra section;
  3. the sequence 0 → J/J² → S ⊗[P] Ω[P⁄R] → Ω[S⁄R] → 0 is split short exact, i.e. its first map is injective and its second map admits an S-linear section;
  4. Ω[S⁄R] is a projective S-module and H₁(NL_{S/R}) = 0.
public theorem Algebra.FormallySmooth.tfae_of_surjective
    {R : Type*} {S : Type*} {P : Type*} [CommRing R] [CommRing S] [CommRing P]
    [Algebra R S] [Algebra R P] [Algebra P S] [IsScalarTower R P S]
    [Algebra.FormallySmooth R P] (hf : Function.Surjective (algebraMap P S)) :
    List.TFAE
      [ Algebra.FormallySmooth R S,
        ∃ g, (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S,
        Function.Injective (kerCotangentToTensor R P S) ∧
          ∃ σ : Ω[S⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R], mapBaseChange R P S ∘ₗ σ = LinearMap.id,
        Module.Projective S Ω[S⁄R] ∧ Subsingleton (Algebra.H1Cotangent R S) ]
Tag 031K, a lemma

Tag 031K in the Stacks Project.

KaehlerDifferential.exists_retraction_mapBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/BaseChange.lean, line 200. The attribute's comment: “Split short exactness, i.e. the two assertions of the tag that are not already in Mathlib (exactness at Ω_{C/A} is KaehlerDifferential.exact_mapBaseChange_map and surjectivity is KaehlerDifferential.map_surjective), stated as the existence of a retraction of the injection: that is at once its injectivity and the splitting. See the module docstring.”. References: EGA 0 (20.5.7), “(ii), sufficiency”; EGA IV (17.2.3), “(ii), affine case”; EGA 0 (20.7.3), “discrete case, necessity”; EGA 0 (20.7.2), “sufficiency”; EGA 0 (20.5.7), “(ii), sufficiency”; SGA 1 II (4.3), “(i) inj., affine case”; SGA 1 II (4.4), “special case”; SGA 6 VIII (2.6), “partial”.

The sequence of differentials of a tower is split short exact. Let R → A → B be ring maps with A → B formally smooth. Then the canonical injection B ⊗_A Ω_{A/R} → Ω_{B/R} admits a B-linear retraction, so that 0 → B ⊗_A Ω_{A/R} → Ω_{B/R} → Ω_{B/A} → 0 is a split short exact sequence.

public theorem KaehlerDifferential.exists_retraction_mapBaseChange (R : Type*) [CommRing R]
    (A B : Type*) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B]
    [IsScalarTower R A B] [Algebra.FormallySmooth A B] :
    ∃ r : Ω[B⁄R] →ₗ[B] B ⊗[A] Ω[A⁄R],
      r ∘ₗ KaehlerDifferential.mapBaseChange R A B = LinearMap.id
Tag 06A6, a lemma

Tag 06A6 in the Stacks Project.

KaehlerDifferential.exists_retraction_kerCotangentToTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Conormal.lean, line 1110. The attribute's comment: “Split exactness, i.e. the two assertions of the tag that are not already in Mathlib (exactness at Ω_{B/A} ⊗_B C is KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange and surjectivity on the right is KaehlerDifferential.mapBaseChange_surjective), stated as the existence of a retraction of the injection J/J² → Ω_{B/A} ⊗_B C: that single datum is at once its injectivity and the splitting. See the module docstring.”. References: EGA 0 (20.5.14), “injectivity, splitting”; EGA IV (17.2.5), “injectivity, affine”; EGA 0 (22.4.6), “(22.4.6.1)”; EGA 0 (22.4.4.2), “partial”; SGA 3 III (4.25), “(ii) inj. + splitting”.

Stacks 06A6. If S is a formally smooth R-algebra and P → S is surjective with kernel J, then the canonical map J/J² → S ⊗[P] Ω[P⁄R] of Stacks 00RU admits a retraction, so that the sequence 0 → J/J² → S ⊗[P] Ω[P⁄R] → Ω[S⁄R] → 0 is split exact. Nothing is required of P.

public theorem KaehlerDifferential.exists_retraction_kerCotangentToTensor (R P S : Type*)
    [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S] [Algebra R S]
    [IsScalarTower R P S] [Algebra.FormallySmooth R S]
    (hf : Function.Surjective (algebraMap P S)) :
    ∃ l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent,
      l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
Tag 06A7, a lemma

Tag 06A7 in the Stacks Project.

Algebra.FormallySmooth.exists_retraction_mapCotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Conormal.lean, line 1602. The attribute's comment: “Split exactness, i.e. the part of the tag that is not already the neighbouring tag 065V, stated as the existence of a retraction of the injection I/I² → J/J²: given 065V's exactness that single datum is at once its injectivity and the splitting. Exactness at J/J² and surjectivity of KaehlerDifferential.kerCotangentToTensor A B C are 065V, hold with no hypothesis on A → B, and are not restated. See the module docstring.”.

Stacks 06A7. Let A → B → C be ring maps with A → C surjective and A → B formally smooth, and put I = ker (A → C) and J = ker (B → C). Then the map ι : I/I² → J/J² of Stacks 065V admits a retraction; in particular ι is injective, so that the sequence 0 → I/I² → J/J² → Ω[B⁄A] ⊗[B] B/J → 0 of Stacks 065V is split short exact.

public theorem Algebra.FormallySmooth.exists_retraction_mapCotangent
    (A B C : Type*) [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C]
    [Algebra A C] [IsScalarTower A B C] [Algebra.FormallySmooth A B]
    (h : Function.Surjective (algebraMap A C)) :
    ∃ ρ : (RingHom.ker (algebraMap B C)).Cotangent →ₗ[A]
        (RingHom.ker (algebraMap A C)).Cotangent,
      ρ ∘ₗ Ideal.mapCotangent (RingHom.ker (algebraMap A C))
        (RingHom.ker (algebraMap B C)) (Algebra.ofId A B)
        (((RingHom.comap_ker (algebraMap B C) (algebraMap A B)).trans
          (congrArg RingHom.ker (IsScalarTower.algebraMap_eq A B C).symm)).ge) =
        LinearMap.id
Tag 00TN, a proposition

Tag 00TN in the Stacks Project.

Declarations registered for the tag:

Tag 0CAQ, a lemma

Tag 0CAQ in the Stacks Project.

smooth_descends_to_filtered_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SpreadingOut/Smooth.lean, line 1351.

Stacks Tag 0CAQ (Lemma 10.138.15). Let I be a filtered category and F : I ⥤ CommRingCat a filtered system of commutative rings with colimit A = colimit F and structure maps ψ_i = colimit.ι F i. If A → B (given by a morphism f : colimit F ⟶ B) is a smooth ring map, then there exist an index i, a commutative ring B_i, and a smooth ring map g : A_i → B_i, such that B is isomorphic, as an A-algebra, to the base change B_i ⊗_{A_i} A of B_i along the structure map ψ_i : A_i → A.

theorem smooth_descends_to_filtered_colimit
    {I : Type u} [SmallCategory I] [IsFiltered I] (F : I ⥤ CommRingCat.{u})
    (B : CommRingCat.{u}) (f : colimit F ⟶ B) :
    letI : Algebra (↑(colimit F) : Type u) (↑B : Type u) := f.hom.toAlgebra
    RingHom.Smooth f.hom →
    ∃ (i : I) (Bi : CommRingCat.{u}) (g : F.obj i ⟶ Bi),
      letI : Algebra (↑(F.obj i) : Type u) (↑Bi : Type u) := g.hom.toAlgebra
      letI : Algebra (↑(F.obj i) : Type u) (↑(colimit F) : Type u) :=
        (colimit.ι F i).hom.toAlgebra
      RingHom.Smooth g.hom ∧
      (letI : Algebra (↑(colimit F) : Type u) (↑B : Type u) := f.hom.toAlgebra
       letI := Algebra.TensorProduct.rightAlgebra
         (R := (↑(F.obj i) : Type u)) (A := (↑Bi : Type u)) (B := (↑(colimit F) : Type u))
       Nonempty ((↑B : Type u) ≃ₐ[(↑(colimit F) : Type u)]
         TensorProduct (↑(F.obj i) : Type u) (↑Bi : Type u) (↑(colimit F) : Type u)))
Tag 06CM, a lemma

Tag 06CM in the Stacks Project.

Algebra.FormallySmooth.iff_tensorProduct_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/FaithfullyFlatDescent.lean, line 39. The attribute's comment: “The source's S' = S ⊗_R R' is written R' ⊗[R] S, Mathlib's order for a base change.”. References: EGA 0 (19.3.5), “(iii), special case”; EGA 0 (19.4.6), “special case”; SGA 3 XIX (2.1), “special case”.

Let R → R' be faithfully flat. Then S is formally smooth over R if and only if the base change R' ⊗_R S is formally smooth over R'.

theorem iff_tensorProduct_of_faithfullyFlat [Module.FaithfullyFlat R R'] :
    FormallySmooth R S ↔ FormallySmooth R' (R' ⊗[R] S)
Tag 07K4, a lemma

Tag 07K4 in the Stacks Project.

Stacks.Smooth.strongLifting_specMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/StrongLifting.lean, line 144. The attribute's comment: “the geometric form for the spectrum of a smooth ring map”.

The ring dictionary for the strong lifting property. The spectrum of a smooth ring map has the strong lifting property; the lift is the one produced by Algebra, Lemma 10.138.17.

theorem strongLifting_specMap {R A : CommRingCat.{u}} {ψ : R ⟶ A} (hψ : RingHom.Smooth ψ.hom) :
    StrongLifting (Spec.map ψ)

Stacks.Smooth.strongLifting_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/StrongLifting.lean, line 174. The attribute's comment: “the geometric form for a smooth morphism of affine schemes”.

A smooth morphism of affine schemes has the strong lifting property.

theorem strongLifting_of_isAffine {X S : Scheme.{u}} (f : X ⟶ S) [IsAffine X] [IsAffine S]
    [AlgebraicGeometry.Smooth f] : StrongLifting f

Stacks.Smooth.exists_lift_of_isClosedImmersion_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/StrongLifting.lean, line 193. The attribute's comment: “the lifting problem along a thickening of affine schemes”. References: SGA 3 III (2.5), “(a), special case”; SGA 3 IX (3.3), “special case”.

Lifting along a thickening for a smooth morphism of affine schemes. Let f : X ⟶ S be a smooth morphism of affine schemes, let i : T ⟶ T' be a closed immersion of schemes with T' affine which is surjective on points, and let a : T ⟶ X and h : T' ⟶ S present a lifting problem for f along i. Then there is a morphism b : T' ⟶ X with b ≫ f = h and i ≫ b = a.

The thickening is the spectrum of the surjection i.appTop on global sections, whose kernel is locally nilpotent by AlgebraicGeometry.isLocallyNilpotent_ker_appTop_of_surjective, so Stacks.Smooth.strongLifting_of_isAffine applies.

theorem exists_lift_of_isClosedImmersion_of_surjective {X S T T' : Scheme.{u}} (f : X ⟶ S)
    [IsAffine X] [IsAffine S] [AlgebraicGeometry.Smooth f] [IsAffine T'] {i : T ⟶ T'}
    [IsClosedImmersion i] (hi : Function.Surjective i.base) (a : T ⟶ X) (h : T' ⟶ S)
    (hcomm : a ≫ f = i ≫ h) :
    ∃ b : T' ⟶ X, b ≫ f = h ∧ i ≫ b = a

main_theorem07K4, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Lifting.lean, line 130. References: EGA 0 (19.0.1), “special case”; EGA 0 (19.3.10.1), “special case”; EGA 0 (19.5.6.4), “special case”; EGA IV (17.14.2), “partial”; SGA 1 III (5.2), “special case”; SGA 3 III (0.17), “special case”; SGA 3 III (2.3), “(a), special case”; SGA 3 III (2.5), “(a), special case”; SGA 3 IX (3.3), “special case”; SGA 3 XI (1.5), “partial”.

Smooth strong lifting: a smooth ring map R → S has the lifting property with respect to locally nilpotent ideals. For any commutative R-algebra A with a locally nilpotent ideal I, every R-algebra map S → A ⧸ I lifts to an R-algebra map S → A.

theorem main_theorem07K4
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Algebra.Smooth R S]
    (A : Type*) [CommRing A] [Algebra R A] (I : Ideal A)
    (hI : Ideal.IsLocallyNilpotent I)
    (g : S →ₐ[R] A ⧸ I) :
    ∃ f : S →ₐ[R] A, (Ideal.Quotient.mkₐ R I).comp f = g
Sources
LeanAlgebra.FormallySmooth.instTensorProduct · Algebra.FormallySmooth.comp · Algebra.instFormallySmoothMvPolynomial · Algebra.FormallySmooth.iff_split_surjection · Algebra.FormallySmooth.tfae_of_surjective · KaehlerDifferential.exists_retraction_mapBaseChange · KaehlerDifferential.exists_retraction_kerCotangentToTensor · Algebra.FormallySmooth.exists_retraction_mapCotangent

Section10.139 Smoothness and differentials#

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

Tag 04B2, a lemma

Tag 04B2 in the Stacks Project.

KaehlerDifferential.mapBaseChange_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/JacobiZariski.lean, line 167. The attribute's comment: “Exactness at C ⊗_B Ω_{B/A}, the one node of the sequence that is not already in Mathlib; the other two are KaehlerDifferential.exact_mapBaseChange_map and KaehlerDifferential.map_surjective. Stated under H₁(L_{C/B}) = 0, the hypothesis the source's second proof uses, which the tag's smoothness gives by instance inference. See the module docstring.”. References: SGA 6 VIII (2.6), “partial”.

The sequence of differentials of a tower is exact on the left: let R → A → B be ring maps such that H₁(L_{B/A}) = 0, for instance with A → B smooth. Then the canonical map B ⊗_A Ω_{A/R} → Ω_{B/R} is injective, so that 0 → B ⊗_A Ω_{A/R} → Ω_{B/R} → Ω_{B/A} → 0 is a short exact sequence.

public theorem KaehlerDifferential.mapBaseChange_injective (R : Type*) [CommRing R]
    (A B : Type*) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B]
    [IsScalarTower R A B] [Subsingleton (Algebra.H1Cotangent A B)] :
    Function.Injective (KaehlerDifferential.mapBaseChange R A B)
Tag 06A8, a lemma

Tag 06A8 in the Stacks Project.

KaehlerDifferential.split_exact_kerCotangentToTensor_mapBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Conormal.lean, line 1160. The attribute's comment: “Stated for a formally smooth R → S, which is the source's own generalisation 06A6, and with no hypothesis on P. Split exactness is recorded as injectivity of the left hand map together with an S-linear section of the right hand map, the exactness of the sequence of 00RU in the middle and on the right being Mathlib's KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange and KaehlerDifferential.mapBaseChange_surjective. See the module docstring.”. References: EGA 0 (20.5.14), “injectivity, splitting”; EGA IV (17.2.5), “affine case”; EGA 0 (20.5.14), “injectivity, splitting”; EGA 0 (20.6.22), “partial”; EGA 0 (22.4.4.2), “partial”; SGA 3 III (4.25), “(ii) inj. + splitting”.

Stacks 06A8. Let R → P → S be ring maps with R → S smooth and P → S surjective with kernel J. Then the exact sequence 0 → J/J² → S ⊗[P] Ω[P⁄R] → Ω[S⁄R] → 0 of Stacks 00RU is split short exact: its left hand map J/J² → S ⊗[P] Ω[P⁄R] is injective and its right hand map S ⊗[P] Ω[P⁄R] → Ω[S⁄R] admits an S-linear section. Only formal smoothness of R → S is used, and nothing is required of P.

theorem KaehlerDifferential.split_exact_kerCotangentToTensor_mapBaseChange
    (R P S : Type*) [CommRing R] [CommRing P] [CommRing S] [Algebra R P] [Algebra P S]
    [Algebra R S] [IsScalarTower R P S] [Algebra.FormallySmooth R S]
    (hf : Function.Surjective (algebraMap P S)) :
    Function.Injective (kerCotangentToTensor R P S) ∧
      ∃ σ : Ω[S⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R], mapBaseChange R P S ∘ₗ σ = LinearMap.id
Tag 06A9, a lemma

Tag 06A9 in the Stacks Project.

Algebra.FormallySmooth.exists_leftInverse_mapCotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Conormal.lean, line 1225. The attribute's comment: “Stated for a formally smooth A → B, which is the source's own generalisation 06A7, and with the retraction that generalisation asserts rather than bare injectivity, the latter following by Function.LeftInverse.injective. Exactness at J/J² and surjectivity of KaehlerDifferential.kerCotangentToTensor A B C are the neighbouring tag 065V and are not restated. See the module docstring.”.

Stacks 06A9. Let A → B → C be ring maps with A → C surjective and A → B smooth, and put I = ker (A → C) and J = ker (B → C). Then the map I/I² → J/J² of Stacks 065V admits an A-linear left inverse; in particular it is injective, so that the sequence 0 → I/I² → J/J² → Ω[B⁄A] ⊗[B] B/J → 0 of Stacks 065V is exact, indeed split exact. Only formal smoothness of A → B is used.

theorem Algebra.FormallySmooth.exists_leftInverse_mapCotangent
    (A B C : Type*) [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C]
    [Algebra A C] [IsScalarTower A B C] [Algebra.FormallySmooth A B]
    (h : Function.Surjective (algebraMap A C)) :
    ∃ ρ : (RingHom.ker (algebraMap B C)).Cotangent →ₗ[A]
        (RingHom.ker (algebraMap A C)).Cotangent,
      ρ ∘ₗ Ideal.mapCotangent (RingHom.ker (algebraMap A C))
        (RingHom.ker (algebraMap B C)) (Algebra.ofId A B)
        (((RingHom.comap_ker (algebraMap B C) (algebraMap A B)).trans
          (congrArg RingHom.ker (IsScalarTower.algebraMap_eq A B C).symm)).ge) =
        LinearMap.id
Tag 05D5, a lemma

Tag 05D5 in the Stacks Project.

conormal_finite_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Conormal.lean, line 188. The attribute's comment: “(1)”. References: EGA 0 (19.5.3), “(i), special case”; EGA 0 (19.5.4.1), “a), special case”; EGA 0 (19.5.7), “Clause (i), special case”; EGA 0 (22.1.1), “(ii), condition α”; EGA IV (17.10.4), “special case”; SGA 1 II (4.10), “(iv)”; SGA 3 III (4.25), “(ii), special case”; SGA 3 VIB (1.6), “special case”; SGA 6 VII (1.6), “special case”; SGA 6 VIII (2.4), “special case”; SGA 6 X (7.1), “special case”.

Part (1) of Stacks tag 05D5: the conormal module is finite locally free. If S is a smooth R-algebra and σ : S →ₐ[R] R, then the conormal module I/I² of I = Ker(σ) is a finitely generated projective R-module.

theorem conormal_finite_projective (h : Algebra.Smooth R S) :
    Module.Finite R (RingHom.ker σ).Cotangent ∧
      Module.Projective R (RingHom.ker σ).Cotangent

adicCompletion_algEquiv_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Conormal.lean, line 1068. The attribute's comment: “(2)”. References: EGA 0 (19.0.2), “special case”; EGA 0 (19.5.4), “a) ⇒ c)”; EGA 0 (19.5.4.4), “partial”; EGA 0 (21.9.2), “special case”; EGA IV (17.5.3), “partial”; SGA 1 II (4.17), “affine case, (i)⇒(iii)”; SGA 1 III (1.5), “necessity, special case”; SGA 3 VIIB (5.5.2), “partial”; SGA 3 XI (1.2), “(ii), special case”.

Part (2) of Stacks tag 05D5: the completion is a power series ring when the conormal module is free. If S is a smooth R-algebra, σ : S →ₐ[R] R, and the conormal module I/I² of I = Ker(σ) is free (necessarily of finite rank d := Module.finrank R (I/I²) by (1)), then the I-adic completion S^∧ is isomorphic, as an R-algebra, to the formal power series R-algebra in d variables R[[t_1, …, t_d]].

theorem adicCompletion_algEquiv_mvPowerSeries (h : Algebra.Smooth R S)
    (hfree : Module.Free R (RingHom.ker σ).Cotangent) :
    Nonempty (AdicCompletion (RingHom.ker σ) S ≃ₐ[R]
      MvPowerSeries (Fin (Module.finrank R (RingHom.ker σ).Cotangent)) R)
Sources
LeanKaehlerDifferential.mapBaseChange_injective · KaehlerDifferential.split_exact_kerCotangentToTensor_mapBaseChange · Algebra.FormallySmooth.exists_leftInverse_mapCotangent · conormal_finite_projective · adicCompletion_algEquiv_mvPowerSeries

Section10.140 Smooth algebras over fields#

Section 10.140 of the Stacks Project, Tag 00TQ. 8 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00TR, a lemma

Tag 00TR in the Stacks Project.

finrank_kaehler_baseChange_eq_finrank_cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/CotangentAtMaximalIdeal.lean, line 199.

For an algebraically closed field \(k\), a finite type \(k\)-algebra \(S\), and a maximal ideal \(\mathfrak{m} \subset S\), the dimension over the residue field \(\kappa(\mathfrak{m}) = S/\mathfrak{m}\) of the cotangent space \(\Omega_{S/k} \otimes_S \kappa(\mathfrak{m})\) equals the dimension of \(\mathfrak{m}/\mathfrak{m}^2\).

theorem finrank_kaehler_baseChange_eq_finrank_cotangent
    (k S : Type*) [Field k] [IsAlgClosed k] [CommRing S] [Algebra k S]
    [Algebra.FiniteType k S] (𝔪 : Ideal S) [𝔪.IsMaximal] :
    Module.finrank (S ⧸ 𝔪) ((S ⧸ 𝔪) ⊗[S] KaehlerDifferential k S) =
      Module.finrank (S ⧸ 𝔪) 𝔪.Cotangent
Tag 00TS, a lemma

Tag 00TS in the Stacks Project.

Algebra.isSmoothAt_tfae_of_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/RegularLocalRing/ClosedPointRegularity.lean, line 719. The attribute's comment: “The residue field κ(𝔪) is S ⧸ 𝔪, and the fibre Ω_{S/k} ⊗_S κ(𝔪) is the base change (S ⧸ 𝔪) ⊗[S] Ω[S⁄k], whose factors are transposed so that the left one carries the scalar action making it a κ(𝔪)-vector space. dim S_𝔪 is ringKrullDim Sₘ for an arbitrary model Sₘ of the localization, matching Mathlib's IsRegularLocalRing. The source's item (4) is stated twice, as the existential and as Mathlib's Algebra.IsSmoothAt; those are items 4 and 5. See the module docstring.”. References: EGA 0 (22.6.7), “alg. closed k, max ideal”; EGA IV (17.15.5), “affine, k alg closed”; EGA IV (17.15.9), “k alg closed, closed pt”; SGA 1 II (5.3), “alg. closed k, max ideal”; SGA 1 II (5.5), “alg closed k, closed pt”; SGA 1 II (5.9), “k alg closed, closed pt”.

Regularity at a closed point equals smoothness, over an algebraically closed field (Stacks 00TS). For an algebraically closed field k, a finite type k-algebra S, a maximal ideal 𝔪 ⊆ S and a model Sₘ of S_𝔪, the following are equivalent: (1) S_𝔪 is a regular local ring; (2) dim_{κ(𝔪)} Ω_{S/k} ⊗_S κ(𝔪) ≤ dim S_𝔪; (3) the same with equality; (4) there is a g ∈ S, g ∉ 𝔪, with S_g smooth over k; (5) in other words, S/k is smooth at 𝔪.

public theorem Algebra.isSmoothAt_tfae_of_isAlgClosed {k S : Type*} [Field k] [IsAlgClosed k]
    [CommRing S] [Algebra k S] [Algebra.FiniteType k S] (𝔪 : Ideal S) [𝔪.IsMaximal]
    (Sₘ : Type*) [CommRing Sₘ] [Algebra S Sₘ] [IsLocalization.AtPrime Sₘ 𝔪] :
    List.TFAE
      [IsRegularLocalRing Sₘ,
       (Module.finrank (S ⧸ 𝔪) ((S ⧸ 𝔪) ⊗[S] Ω[S⁄k]) : WithBot ℕ∞) ≤ ringKrullDim Sₘ,
       (Module.finrank (S ⧸ 𝔪) ((S ⧸ 𝔪) ⊗[S] Ω[S⁄k]) : WithBot ℕ∞) = ringKrullDim Sₘ,
       ∃ g ∉ 𝔪, Algebra.Smooth k (Localization.Away g),
       Algebra.IsSmoothAt k 𝔪]
Tag 00TT, a lemma

Tag 00TT in the Stacks Project.

Algebra.isSmoothAt_tfae_localKrullDim_and_isRegularLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/RegularLocalRing/LocalDimensionCriterion.lean, line 379. The attribute's comment: “𝔮 and x are one datum x : PrimeSpectrum S with 𝔮 = x.asIdeal; dim_x X is TopologicalSpace.localKrullDim, Topology Definition 0055 (4); κ(𝔮) is Ideal.ResidueField x.asIdeal and the fibre Ω_{S/k} ⊗_S κ(𝔮) is the base change κ(𝔮) ⊗[S] Ω[S⁄k], whose factors are transposed so that the left one carries the scalar action making it a κ(𝔮)-vector space; S_𝔮 is an arbitrary model Sq. The source's moreover is the final conjunct and not a fourth equivalent item, regularity being strictly weaker than smoothness over a nonperfect field. See the module docstring.”. References: EGA IV (17.15.5), “affine case”; SGA 1 II (5.3), “first assertion”; SGA 1 II (5.5), “affine (i)<=>(ii bis)”.

Smoothness at a point is the differential fibre having the local dimension (Stacks 00TT). Let k be a field, let S be a finite type k-algebra, let X = Spec S, let x ∈ X be a point with prime ideal 𝔮 = x.asIdeal, and let Sq be a model of S_𝔮. The following are equivalent: (1) S is smooth at 𝔮 over k; (2) dim_{κ(𝔮)} Ω_{S/k} ⊗_S κ(𝔮) ≤ dim_x X; (3) the same with equality. Moreover, in this case the local ring S_𝔮 is regular.

public theorem Algebra.isSmoothAt_tfae_localKrullDim_and_isRegularLocalRing
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (x : PrimeSpectrum S) (Sq : Type*) [CommRing Sq] [Algebra S Sq]
    [IsLocalization.AtPrime Sq x.asIdeal] :
    List.TFAE
      [Algebra.IsSmoothAt k x.asIdeal,
       (Module.finrank x.asIdeal.ResidueField (x.asIdeal.ResidueField ⊗[S] Ω[S⁄k]) : WithBot ℕ∞) ≤
         localKrullDim (PrimeSpectrum S) x,
       (Module.finrank x.asIdeal.ResidueField (x.asIdeal.ResidueField ⊗[S] Ω[S⁄k]) : WithBot ℕ∞) =
         localKrullDim (PrimeSpectrum S) x] ∧
      (Algebra.IsSmoothAt k x.asIdeal → IsRegularLocalRing Sq)
Tag 00TU, a lemma

Tag 00TU in the Stacks Project.

KaehlerDifferential.kerCotangentToTensor_injective_of_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/Separable.lean, line 199. The attribute's comment: “d is KaehlerDifferential.kerCotangentToTensor k R B, whose domain (RingHom.ker (algebraMap R B)).Cotangent is I/I² and whose codomain B ⊗[R] Ω[R⁄k] has the factors of the source's Ω_{R/k} ⊗_R κ transposed, so that the left one carries the B-vector space structure. Finitely generated separable is Algebra.EssFiniteType together with the notion of Stacks 030O (2). Generalized: the quotient is an arbitrary surjection onto a field rather than the residue field of a local ring, and R is not assumed Noetherian; the source's statement is the case B := IsLocalRing.ResidueField R. See the module docstring.”.

The differential is injective on I/I² for a separable field quotient (Stacks 00TU). Let k be a field, let R be a k-algebra and let R → B be a surjection onto a field B which is a finitely generated separable extension of k. Then d : I/I² → Ω_{R/k} ⊗_R B, x ↦ 1 ⊗ dx, is injective, where I = ker(R → B). For R local and B = R/𝔪 this is injectivity of d on 𝔪/𝔪².

public theorem KaehlerDifferential.kerCotangentToTensor_injective_of_isSeparableExtension
    (k R B : Type*) [Field k] [CommRing R] [Field B] [Algebra k R] [Algebra R B] [Algebra k B]
    [IsScalarTower k R B] [Algebra.EssFiniteType k B] [Algebra.IsSeparableExtension k B]
    (h : Function.Surjective (algebraMap R B)) :
    Function.Injective (kerCotangentToTensor k R B)
Tag 00TV, a lemma

Tag 00TV in the Stacks Project.

Algebra.isSmoothAt_iff_isRegularLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/RegularLocalRing/SeparableResidueRegular.lean, line 409. The attribute's comment: “κ(𝔮) is Ideal.ResidueField q, and its separability over k is Algebra.IsSeparableExtension, Definition 030O (2); that does not presuppose algebraicity, so it is not Algebra.IsSeparable. S_𝔮 is an arbitrary model Sq, pinned by IsLocalization.AtPrime Sq q; regularity is IsRegularLocalRing (Definition 00KU) and smoothness at 𝔮 is Algebra.IsSmoothAt. The two-item enumeration is an Iff. Finite generation of κ(𝔮)/k is not assumed, being a consequence of Algebra.FiniteType k S. See the module docstring.”. References: EGA IV (17.15.1), “last assertion”; EGA 0 (22.6.7), “separable residue field”; EGA IV (17.15.9), “a)”; SGA 1 II (5.4), “affine local, κ(q)/k sep”; SGA 1 II (5.10), “affine case”; SGA 1 II (5.3), “regular ⇒ smooth”; SGA 1 II (5.9), “(i) <=> smooth in (ii)”.

Smoothness at a prime with separable residue field is regularity (Stacks 00TV). Let k be a field, let S be a finite type k-algebra, let 𝔮 ⊆ S be a prime whose residue field κ(𝔮) is separable over k, and let Sq be a model of S_𝔮. Then S is smooth at 𝔮 over k if and only if S_𝔮 is a regular local ring.

public theorem Algebra.isSmoothAt_iff_isRegularLocalRing
    {k S : Type*} [Field k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (q : Ideal S) [q.IsPrime] [Algebra.IsSeparableExtension k q.ResidueField]
    (Sq : Type*) [CommRing Sq] [Algebra S Sq] [IsLocalization.AtPrime Sq q] :
    Algebra.IsSmoothAt k q ↔ IsRegularLocalRing Sq
Tag 00TW, a lemma

Tag 00TW in the Stacks Project.

not_isNilpotent_of_hasFreeSummandDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/CotangentAtMaximalIdeal.lean, line 257. The attribute's comment: “(1)”.

Let R → S be a map of ℚ-algebras with S nonzero, and let f ∈ S be such that Ω[S⁄R] = S·df ⊕ C with df a free generator of S·df. Then f is not nilpotent.

theorem not_isNilpotent_of_hasFreeSummandDifferential
    (R S : Type*) [CommRing R] [CommRing S]
    [Algebra ℚ R] [Algebra ℚ S] [Algebra R S] [IsScalarTower ℚ R S] [Nontrivial S]
    (f : S) (hf : HasFreeSummandDifferential R S f) :
    ¬ IsNilpotent f

nonzerodivisor_of_hasFreeSummandDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/CotangentAtMaximalIdeal.lean, line 286. The attribute's comment: “(2)”.

Let R → S be a map of ℚ-algebras with S a Noetherian local ring, and let f ∈ S be such that Ω[S⁄R] = S·df ⊕ C with df a free generator of S·df. Then f is a nonzerodivisor: f * a = 0 → a = 0.

theorem nonzerodivisor_of_hasFreeSummandDifferential
    (R S : Type*) [CommRing R] [CommRing S]
    [Algebra ℚ R] [Algebra ℚ S] [Algebra R S] [IsScalarTower ℚ R S]
    [IsNoetherianRing S] [IsLocalRing S]
    (f : S) (hf : HasFreeSummandDifferential R S f) :
    ∀ a : S, f * a = 0 → a = 0
Tag 00TX, a lemma

Tag 00TX in the Stacks Project.

Algebra.isSmoothAt_tfae_free_kaehlerDifferential_isRegularLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/RegularLocalRing/CharZeroRegularity.lean, line 607. The attribute's comment: “The localized module Ω_{S/k, 𝔮} is Ω[Sq⁄k], which by KaehlerDifferential.isLocalizedModule_map is the localization of Ω[S⁄k] at q.primeCompl, the identification the source's own proof uses. The source's parenthetical (finite) is not a conjunct: Module.Finite Sq Ω[Sq⁄k] holds unconditionally here. S_𝔮 is an arbitrary model Sq, pinned by IsLocalization.AtPrime Sq q and IsScalarTower k S Sq, as in the siblings 00TT and 00TV; regularity is IsRegularLocalRing (Definition 00KU (2)) and smoothness at 𝔮 is Algebra.IsSmoothAt. The three-item enumeration is a List.TFAE. See the module docstring.”. References: EGA IV (17.15.7), “affine case”; EGA IV (17.15.5), “affine, char 0”; SGA 1 II (5.7), “char 0, local at prime”; SGA 1 II (5.4), “char 0, affine local”; SGA 1 II (5.5), “char 0, affine, k'=k”; SGA 1 II (5.9), “characteristic zero”; SGA 1 III (5.2), “special case”.

Smoothness, free differentials and regularity agree in characteristic zero (Stacks 00TX). Let k be a field of characteristic 0, let S be a finite type k-algebra, let 𝔮 ⊆ S be a prime and let Sq be a model of S_𝔮. The following are equivalent: (1) S is smooth at 𝔮 over k; (2) the S_𝔮-module Ω_{S/k, 𝔮} is free; (3) the local ring S_𝔮 is regular.

public theorem Algebra.isSmoothAt_tfae_free_kaehlerDifferential_isRegularLocalRing
    {k S : Type*} [Field k] [CharZero k] [CommRing S] [Algebra k S] [Algebra.FiniteType k S]
    (q : Ideal S) [q.IsPrime] (Sq : Type*) [CommRing Sq] [Algebra k Sq] [Algebra S Sq]
    [IsScalarTower k S Sq] [IsLocalization.AtPrime Sq q] :
    List.TFAE
      [Algebra.IsSmoothAt k q,
       Module.Free Sq Ω[Sq⁄k],
       IsRegularLocalRing Sq]
Tag 07ND, a lemma

Tag 07ND in the Stacks Project.

Algebra.isSmoothAt_bot_iff_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/Field.lean, line 208. The attribute's comment: “Smoothness at (0) is Algebra.IsSmoothAt R (⊥ : Ideal S), as in the sibling 00TV; separability of the possibly transcendental extension L/K is Algebra.IsSeparableExtension, Definition 030O (2), not Algebra.IsSeparable. The fraction fields are abstract, pinned by IsFractionRing, and the source's injectivity of R → S is implied by the compatible K-algebra structure on L rather than assumed. See the module docstring.”.

Smoothness at the generic point is separability of the fraction field extension (Stacks 07ND). Let R → S be a finite type map of domains, let K and L be the fraction fields of R and S, and let L be a K-algebra compatibly with both towers — which forces R → S to be injective. Then S is smooth over R at 𝔮 = (0) if and only if L/K is separable.

public theorem Algebra.isSmoothAt_bot_iff_isSeparableExtension (R S K L : Type*)
    [CommRing R] [CommRing S] [Field K] [Field L] [IsDomain R] [IsDomain S]
    [Algebra R S] [Algebra.FiniteType R S] [Algebra R K] [IsFractionRing R K]
    [Algebra S L] [IsFractionRing S L] [Algebra R L] [Algebra K L]
    [IsScalarTower R S L] [IsScalarTower R K L] :
    Algebra.IsSmoothAt R (⊥ : Ideal S) ↔ Algebra.IsSeparableExtension K L
Sources
Leanfinrank_kaehler_baseChange_eq_finrank_cotangent · Algebra.isSmoothAt_tfae_of_isAlgClosed · Algebra.isSmoothAt_tfae_localKrullDim_and_isRegularLocalRing · KaehlerDifferential.kerCotangentToTensor_injective_of_isSeparableExtension · Algebra.isSmoothAt_iff_isRegularLocalRing · not_isNilpotent_of_hasFreeSummandDifferential · nonzerodivisor_of_hasFreeSummandDifferential · Algebra.isSmoothAt_tfae_free_kaehlerDifferential_isRegularLocalRing

Section10.141 Smooth ring maps in the Noetherian case#

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

Tag 02HS, a definition

Tag 02HS in the Stacks Project.

InfinitesimalLifting.IsSmallExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Smooth/InfinitesimalLifting.lean, line 129. References: SGA 7 VI (1.4), “more general”.

A ring map φ : B' → B is a small extension (Stacks tag 02HS) if B' and B are local Artinian rings, φ is surjective, and the kernel ker φ has length 1 as a B'-module.

def IsSmallExtension {B' B : CommRingCat.{u}} (φ : B' ⟶ B) : Prop
Tag 02HT, a lemma

Tag 02HT in the Stacks Project.

Algebra.isSmoothAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Kaehler/SmoothRingMapsInTheNoetherianCase.lean, line 480. The attribute's comment: “Smoothness at q is Algebra.IsSmoothAt, the source's Definition 02HN by the finite presentation of S. A small extension (Definition 02HS) is a surjection f : B' →ₐ[R] B of Artinian local rings with IsSimpleModule B' (ker f), and κ(q) ≅ κ(𝔪) is surjectivity of Ideal.ResidueField.mapₐ q (maximalIdeal B) g, the canonical map out of the residue field of S_q — not of S → κ(𝔪), which would force q maximal. The source's prime 𝔭 under q is not used. See the module docstring.”.

Let R be a Noetherian ring, let S be an R-algebra of finite type and let q be a prime of S. The following are equivalent:

  1. R → S is smooth at q;
  2. for every surjection f : B' → B of local R-algebras whose kernel has square zero and every R-algebra map g : S → B with q the contraction of the maximal ideal of B, there is an R-algebra map g' : S → B' with f ∘ g' = g;
  3. the same, with f ranging over small extensions, that is, surjections of Artinian local rings whose kernel is a simple B'-module (equivalently, has length 1);
  4. the same, with f ranging over small extensions along which g additionally induces an isomorphism κ(q) ≅ κ(𝔪), that is, along which the canonical map κ(q) → κ(𝔪) attached to q = g⁻¹(𝔪) is surjective.
theorem isSmoothAt_tfae {R : Type u} {S : Type v} [CommRing R] [IsNoetherianRing R]
    [CommRing S] [Algebra R S] [Algebra.FiniteType R S] (q : Ideal S) [q.IsPrime] :
    List.TFAE
      [ Algebra.IsSmoothAt R q,
        ∀ (B' B : Type max u v) [CommRing B'] [CommRing B] [IsLocalRing B'] [IsLocalRing B]
          [Algebra R B'] [Algebra R B] (f : B' →ₐ[R] B), Function.Surjective f →
          RingHom.ker (f : B' →+* B) ^ 2 = ⊥ →
          ∀ g : S →ₐ[R] B, (maximalIdeal B).comap (g : S →+* B) = q →
            ∃ g' : S →ₐ[R] B', f.comp g' = g,
        ∀ (B' B : Type max u v) [CommRing B'] [CommRing B] [IsLocalRing B'] [IsLocalRing B]
          [IsArtinianRing B'] [IsArtinianRing B] [Algebra R B'] [Algebra R B]
          (f : B' →ₐ[R] B), Function.Surjective f →
          IsSimpleModule B' (RingHom.ker (f : B' →+* B)) →
          ∀ g : S →ₐ[R] B, (maximalIdeal B).comap (g : S →+* B) = q →
            ∃ g' : S →ₐ[R] B', f.comp g' = g,
        ∀ (B' B : Type max u v) [CommRing B'] [CommRing B] [IsLocalRing B'] [IsLocalRing B]
          [IsArtinianRing B'] [IsArtinianRing B] [Algebra R B'] [Algebra R B]
          (f : B' →ₐ[R] B), Function.Surjective f →
          IsSimpleModule B' (RingHom.ker (f : B' →+* B)) →
          ∀ (g : S →ₐ[R] B) (hq : (maximalIdeal B).comap (g : S →+* B) = q),
            Function.Surjective (Ideal.ResidueField.mapₐ q (maximalIdeal B) g hq.symm) →
            ∃ g' : S →ₐ[R] B', f.comp g' = g ]
Sources
LeanInfinitesimalLifting.IsSmallExtension · Algebra.isSmoothAt_tfae

Section10.143 Étale ring maps#

Section 10.143 of the Stacks Project, Tag 00U0. 11 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00U9, a lemma

Tag 00U9 in the Stacks Project.

Declarations registered for the tag:

Tag 00U2, a lemma

Tag 00U2 in the Stacks Project.

Algebra.etaleLocus_eq_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 406. The attribute's comment: “(5). Stated for Algebra.etaleLocus, hence without the tag's hypothesis that R → S be of finite presentation, which neither the conclusion nor the proof uses; with that hypothesis the two loci are the tag's. The base change is the abstract Algebra.IsPushout. See the module docstring, which also records where in Mathlib the other ten items live.”.

Let R → S be a ring map, let R → R' be flat and let S' be the base change of S along R → R'. Then the set of primes of S' where R' → S' is étale is the inverse image, under Spec S' → Spec S, of the set of primes of S where R → S is étale.

theorem Algebra.etaleLocus_eq_of_isPushout
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (R' S' : Type*) [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] [Algebra R' S']
    [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S']
    [Algebra.IsPushout R S R' S'] [Module.Flat R R'] :
    Algebra.etaleLocus R' S' =
      PrimeSpectrum.comap (algebraMap S S') ⁻¹' Algebra.etaleLocus R S

Algebra.Etale.exists_etale_stage_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FilteredColimitStage.lean, line 105. The attribute's comment: “(9) The filtered colimit A = colim A_i is an arbitrary filtered diagram F : J ⥤ CommRingCat together with a colimiting cocone c with vertex A, plus the instance saying the colimit is computed on underlying sets; the stages A_i are F.obj i and the comparison maps are the legs c.ι.app i, which are also the A_i-algebra structure of A in the conclusion. The isomorphism B ≅ A ⊗_{A_i} B_i is one of A-algebras, with the tensor product as the model of the base change. The existing registration of item (5) is Algebra.etaleLocus_eq_of_isPushout; item (8), which this is deduced from, is Mathlib's Algebra.Etale.exists_subalgebra_fg. See the module docstring.”.

Item (9) of Stacks 00U2. Let A = colim_{i ∈ J} A_i be a filtered colimit of rings, computed on underlying sets, and let B be an étale A-algebra. Then there are an index i and an étale A_i-algebra B_i with B ≅ A ⊗_{A_i} B_i as A-algebras, the A_i-algebra structure of A being the comparison map A_i → A.

theorem Algebra.Etale.exists_etale_stage_of_isColimit {J : Type w} [Category.{t} J] [IsFiltered J]
    (F : J ⥤ CommRingCat.{u}) {c : Cocone F} (hc : IsColimit c)
    [PreservesColimit F (forget CommRingCat)]
    (B : Type*) [CommRing B] [Algebra (c.pt : Type u) B] [Algebra.Etale (c.pt : Type u) B] :
    ∃ (i : J) (Bᵢ : Type u) (_ : CommRing Bᵢ) (_ : Algebra (F.obj i : Type u) Bᵢ),
      Algebra.Etale (F.obj i : Type u) Bᵢ ∧
        (letI : Algebra (F.obj i : Type u) (c.pt : Type u) := (c.ι.app i).hom.toAlgebra;
          Nonempty (B ≃ₐ[(c.pt : Type u)] (c.pt : Type u) ⊗[(F.obj i : Type u)] Bᵢ))
Tag 00U3, a lemma

Tag 00U3 in the Stacks Project.

Declarations registered for the tag:

  • Algebra.Etale.iff_exists_algEquiv_prod registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch10.lean, line 253 (StacksFrontier). References: EGA III (7.8.6); EGA IV (17.6.2), “a ⇔ c', special case”; EGA IV (17.15.11), “a ⇔ c, affine case”; EGA IV (18.2.3); EGA IV (18.3.3); SGA 1 I (10.1), “special case”; SGA 1 IX (1.2), “special case”; SGA 1 IX (1.8), “more general”; SGA 1 IX (1.9); SGA 1 XIII (2.0), “more general”; SGA 3 VIIB (1.6), “special case”; SGA 3 VIIB (1.6.E), “special case”; SGA 3 VIIB (2.5), “special case”; SGA 3 XVII (5.2.1), “partial”; SGA 4½ Arcata (2.1.2); SGA 4½ Arcata (2.4.2); SGA 4½ Sommes trig (4.5), “partial”; SGA 4½ Sommes trig (6.1), “partial”.
Tag 00U4, a lemma

Tag 00U4 in the Stacks Project.

Algebra.IsEtaleAt.map_eq_maximalIdeal_and_finite_isSeparable_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/ResidueFieldExtension.lean, line 637. The attribute's comment: “The source's hypothesis that R → S be étale at q is taken in the weaker form of its two consequences: Algebra.IsEtaleAt R q, and S_q essentially of finite type over R (rather than finite presentation of S over R). Item (1) is recorded as p S_q = m_{S_q}; the source's other half q S_q = m_{S_q} holds for any prime and is Localization.AtPrime.map_eq_maximalIdeal. See the module docstring, which also records that the unramified version of this statement is the separate tag 00UW.”. References: SGA 1 I (3.1), “(i)”.

Stacks 00U4. Let R → S be a ring map and let q be a prime of S lying over a prime p of R. If R → S is étale at q then (1) the ideal p S_q is the maximal ideal of the local ring S_q, hence equals q S_q, and (2) the residue field extension κ(q)/κ(p) is finite separable.

public theorem Algebra.IsEtaleAt.map_eq_maximalIdeal_and_finite_isSeparable_residueField
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
    [Localization.AtPrime.IsLiesOverAlgebra p q]
    [Algebra.EssFiniteType R (Localization.AtPrime q)] [Algebra.IsEtaleAt R q] :
    p.map (algebraMap R (Localization.AtPrime q)) = maximalIdeal (Localization.AtPrime q) ∧
      Module.Finite p.ResidueField q.ResidueField ∧
      Algebra.IsSeparable p.ResidueField q.ResidueField
Tag 00U5, a lemma

Tag 00U5 in the Stacks Project.

RingHom.Etale.quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 195.

An étale ring map is quasi-finite: every fibre κ(P) ⊗ S is a finite κ(P)-algebra.

theorem RingHom.Etale.quasiFinite
    {R S : Type*} [CommRing R] [CommRing S]
    (f : R →+* S) (hf : f.Etale) :
    f.QuasiFinite
Tag 00U6, a lemma

Tag 00U6 in the Stacks Project.

Algebra.IsEtaleAt.of_flat_of_map_eq_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 347. The attribute's comment: “"Étale at q" is Algebra.IsEtaleAt R q, which under hypothesis (1) is the source's Definition 00U1 (Algebra.exists_etale_of_isEtaleAt in one direction, Algebra.basicOpen_subset_etaleLocus_iff_etale in the other). Hypothesis (3) is recorded as p S_q = m_{S_q}; the source's p S_q = q S_q follows by Localization.AtPrime.map_eq_maximalIdeal. The finiteness half of (4) is stated because the source states it, and is implied by the rest; see the module docstring.”. References: EGA IV (18.2.3), “a') ⇒ a)”; SGA 1 IX (1.2), “converse direction”.

Let R → S be a ring map and let q be a prime of S lying over a prime p of R. If (1) R → S is of finite presentation, (2) R_p → S_q is flat, (3) p S_q is the maximal ideal of the local ring S_q, and (4) the field extension κ(q)/κ(p) is finite separable, then R → S is étale at q.

theorem Algebra.IsEtaleAt.of_flat_of_map_eq_maximalIdeal
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
    [Localization.AtPrime.IsLiesOverAlgebra p q]
    [Module.Flat (Localization.AtPrime p) (Localization.AtPrime q)]
    [Module.Finite p.ResidueField q.ResidueField]
    [Algebra.IsSeparable p.ResidueField q.ResidueField]
    (h : p.map (algebraMap R (Localization.AtPrime q)) =
      IsLocalRing.maximalIdeal (Localization.AtPrime q)) :
    Algebra.IsEtaleAt R q
Tag 00U7, a lemma

Tag 00U7 in the Stacks Project.

RingHom.Etale.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 267. The attribute's comment: “Stated for ring maps and their composite rather than for a tower of algebras: the source quantifies over R-algebra maps S → T, for which RingHom.Etale is the predicate, and the sibling RingHom.FormallyEtale.of_comp is stated that way. The hypothesis that R → S be étale is weakened to the two properties the mathematics uses, formal unramifiedness and finite type; see the module docstring for a witness that the generalization is strict.”.

Let f : R →+* S and g : S →+* T be ring maps, so that g is a map of R-algebras for the R-algebra structure g ∘ f on T. If f is formally unramified and of finite type and g ∘ f is étale, then g is étale. In particular a map between two étale R-algebras is étale.

theorem RingHom.Etale.of_comp {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
    {f : R →+* S} {g : S →+* T} (hf : f.FormallyUnramified) (hf' : f.FiniteType)
    (h : (g.comp f).Etale) : g.Etale
Tag 00U8, a lemma

Tag 00U8 in the Stacks Project.

Algebra.exists_isIdempotentElem_isLocalizationAway_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 219.

A surjective, flat, finitely presented ring map R → S exhibits S as the localization of R at an idempotent e: the kernel of algebraMap R S is the ideal (1 - e), and S is the localization of R away from e.

theorem Algebra.exists_isIdempotentElem_isLocalizationAway_of_surjective
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (hsurj : Function.Surjective (algebraMap R S))
    [Module.Flat R S] [Algebra.FinitePresentation R S] :
    ∃ e : R, IsIdempotentElem e ∧
      RingHom.ker (algebraMap R S) = Ideal.span {1 - e} ∧
      IsLocalization.Away e S
Tag 04D1, a lemma

Tag 04D1 in the Stacks Project.

etale_lift_along_surjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Lifting.lean, line 287. References: EGA IV (18.1.1), “special case”.

Étale ring maps lift along surjections of rings: if A' → A is a surjection of commutative rings with kernel I and B is an étale A-algebra, then B is the reduction of an étale A'-algebra, in the sense that there are an étale A'-algebra C and a surjection of A'-algebras ψ : C → B with RingHom.ker ψ = I C.

theorem etale_lift_along_surjection (A' : Type u) (A : Type v) (B : Type w)
    [CommRing A'] [CommRing A] [CommRing B] [Algebra A' A] [Algebra A B] [Algebra A' B]
    [IsScalarTower A' A B] (hA : Function.Surjective (algebraMap A' A)) [Algebra.Etale A B] :
    ∃ (C : Type u) (_ : CommRing C) (_ : Algebra A' C), Algebra.Etale A' C ∧
      ∃ ψ : C →ₐ[A'] B, Function.Surjective ψ ∧
        RingHom.ker (ψ : C →+* B) = (RingHom.ker (algebraMap A' A)).map (algebraMap A' C)
Tag 05YT, a lemma

Tag 05YT in the Stacks Project.

Stacks.Thickenings.etale_of_isKerBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Etale.lean, line 120. The attribute's comment: “The scheme-level form: on a commutative square of schemes with closed immersions i : X ⟶ X' and j : Y ⟶ Y', square-zero kernel ideal sheaf for j and the kernel ideal of i the base change along f' of that of j, étaleness of f gives étaleness of f'. The affine-local content on each pair of affine opens is the lemma itself, which is already proved for ring maps as Algebra.Etale.of_ker_sq_eq_bot_of_isBaseChange; what is proved here is the reduction of the scheme statement to it.”.

Let

X --f--→ Y
|        |
i        j
↓        ↓
X' -f'-→ Y'

be a commutative square of schemes with i and j closed immersions. If the kernel ideal sheaf of j has square zero, the kernel ideal sheaf of i is the base change along f' of the kernel ideal sheaf of j, and f is étale, then f' is étale. The two hypotheses on j together say that j is a first-order thickening, Stacks.Thickenings.IsFirstOrderThickening; nothing is assumed about the order of i, nor that either closed immersion is surjective on points.

theorem etale_of_isKerBaseChange {i : X ⟶ X'} {f : X ⟶ Y} {f' : X' ⟶ Y'} {j : Y ⟶ Y'}
    [IsClosedImmersion i] [IsClosedImmersion j] (hcomm : i ≫ f' = f ≫ j) (hj : j.ker ^ 2 = ⊥)
    (hbc : IsKerBaseChange i f' j) [Etale f] : Etale f'

Algebra.Etale.of_ker_sq_eq_bot_of_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 599. The attribute's comment: “The source's J = I ⊗_A B is spelled as bijectivity of the canonical map B' ⊗[A'] I → J, i.e. as IsBaseChange B' f for the map f : I → J induced by A' → B'; tensoring over A' rather than A avoids the A-module structure on I, which is unavailable to typeclass inference, and asks for the same thing (see the module docstring). The source's hypothesis J ^ 2 = ⊥ is dropped: it follows from hI and the surjectivity half of hbc.”.

Let A' → A and B' → B be surjective ring maps forming a commutative square with A' → B' and A → B, and write I = ker (A' → A), J = ker (B' → B). If I has square zero, A → B is étale, and J is the base change of I along A' → B' (J = I ⊗_A B), then A' → B' is étale.

theorem Algebra.Etale.of_ker_sq_eq_bot_of_isBaseChange
    {A' A B' B : Type*} [CommRing A'] [CommRing A] [CommRing B'] [CommRing B]
    [Algebra A' A] [Algebra A' B'] [Algebra A' B] [Algebra A B] [Algebra B' B]
    [IsScalarTower A' A B] [IsScalarTower A' B' B] [Algebra.Etale A B]
    (hA : Function.Surjective (algebraMap A' A)) (hB : Function.Surjective (algebraMap B' B))
    (hI : RingHom.ker (algebraMap A' A) ^ 2 = ⊥)
    (f : RingHom.ker (algebraMap A' A) →ₗ[A'] RingHom.ker (algebraMap B' B))
    (hf : ∀ x, (f x : B') = algebraMap A' B' (x : A')) (hbc : IsBaseChange B' f) :
    Algebra.Etale A' B'
Tag 00UA, an example

Tag 00UA in the Stacks Project.

MvPolynomial.surjective_aeval_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 145. The attribute's comment: “The symbolic presentation S = R[b, c]/(a_k(b, c) - a_k): the map from R[b, c] is surjective.”.

The R[a]-algebra map R[a][b, c] → S sending bᵢ ↦ bᵢ and cⱼ ↦ cⱼ is surjective.

theorem surjective_aeval_universalFactorizationMap :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Function.Surjective (aeval (R := MvPolynomial (Fin n) R) (S₁ := 𝓢)
      (Sum.elim (fun i ↦ X i ⊗ₜ[R] 1) fun j ↦ 1 ⊗ₜ[R] X j))

MvPolynomial.ker_aeval_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 156. The attribute's comment: “The symbolic presentation S = R[b, c]/(a_k(b, c) - a_k): the kernel. The polynomial a_k(b, c) is the image of a_k under R[a] → S ≃ R[b, c].”.

The kernel of R[a][b, c] → S is generated by the relations aⱼ(b, c) - aⱼ, where aⱼ(b, c) is the image of aⱼ written as a polynomial in the b's and c's.

theorem ker_aeval_universalFactorizationMap :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    RingHom.ker (aeval (R := MvPolynomial (Fin n) R) (S₁ := 𝓢)
      (Sum.elim (fun i ↦ X i ⊗ₜ[R] 1) fun j ↦ 1 ⊗ₜ[R] X j)) =
    Ideal.span (Set.range fun j : Fin n ↦
      (tensorEquivSum R (Fin m) (Fin k) R (universalFactorizationMap R n m k hn (X j))).map C -
        C (X j))

MvPolynomial.pderiv_universalFactorizationMap_eq_sylvester, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 175. The attribute's comment: “The matrix of partial derivatives is the Sylvester matrix of g and h. Mathlib's Polynomial.sylvester is the transpose of the source's matrix, and the variables are ordered by increasing degree; see the module docstring.”.

The matrix of partial derivatives of the relations aⱼ(b, c) - aⱼ with respect to the variables bᵢ, cⱼ is the transpose of the Sylvester matrix of the generic monic polynomials g and h over R[a][b, c]. Its rows are indexed by the variables and its columns by the relations.

theorem pderiv_universalFactorizationMap_eq_sylvester :
    (Matrix.of fun (i : Fin m ⊕ Fin k) (j : Fin n) ↦ pderiv i
      ((tensorEquivSum R (Fin m) (Fin k) R (universalFactorizationMap R n m k hn (X j))).map C -
        C (X j))) =
    ((Polynomial.sylvester
      ((Polynomial.freeMonic R m).map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp
        (rename Sum.inl)).toRingHom)
      ((Polynomial.freeMonic R k).map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp
        (rename Sum.inr)).toRingHom) m k).submatrix (finCongr hn) finSumFinEquiv)ᵀ

MvPolynomial.aeval_pderiv_universalFactorizationMap_eq_transpose_toMatrix_sylvesterMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 229. The attribute's comment: “The Sylvester matrix is the transpose of the matrix of the linear map S[x]_{<m} ⊕ S[x]_{<n} → S[x]_{<n+m}, a ⊕ b ↦ ag + bh, stated for the matrix of partial derivatives with entries in S. Mathlib's Polynomial.sylvesterMap lists the two summands in the other order; see the module docstring.”.

In S, the matrix of partial derivatives of the relations aⱼ(b, c) - aⱼ is the transpose of the matrix of the S-linear map S[x]_{<m} × S[x]_{<k} → S[x]_{<m+k}, (p, q) ↦ g q + h p, in the monomial bases.

theorem aeval_pderiv_universalFactorizationMap_eq_transpose_toMatrix_sylvesterMap :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    (Matrix.of fun (i : Fin m ⊕ Fin k) (j : Fin n) ↦
      aeval (R := MvPolynomial (Fin n) R) (S₁ := 𝓢)
        (Sum.elim (fun i ↦ X i ⊗ₜ[R] 1) fun j ↦ 1 ⊗ₜ[R] X j) (pderiv i
          ((tensorEquivSum R (Fin m) (Fin k) R
            (universalFactorizationMap R n m k hn (X j))).map C - C (X j)))) =
    ((LinearMap.toMatrix
      (((Polynomial.degreeLT.basis 𝓢 m).prod (Polynomial.degreeLT.basis 𝓢 k)).reindex
        finSumFinEquiv)
      (Polynomial.degreeLT.basis 𝓢 (m + k))
      (Polynomial.sylvesterMap 𝐠 𝐡 (Polynomial.natDegree_map_freeMonic_le m _)
        (Polynomial.natDegree_map_freeMonic_le k _))).submatrix (finCongr hn) finSumFinEquiv)ᵀ

MvPolynomial.aeval_det_pderiv_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 256. The attribute's comment: “The determinant Δ of the matrix of partial derivatives is the resultant Res_x(g, h).”.

The determinant Δ of the matrix of partial derivatives of the relations aⱼ(b, c) - aⱼ, with the variables b₀, …, bₘ₋₁, c₀, …, cₖ₋₁ in this order, is in S the resultant Res(g, h).

theorem aeval_det_pderiv_universalFactorizationMap :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    aeval (R := MvPolynomial (Fin n) R) (S₁ := 𝓢)
      (Sum.elim (fun i ↦ X i ⊗ₜ[R] 1) fun j ↦ 1 ⊗ₜ[R] X j)
      (Matrix.of fun i j : Fin n ↦ pderiv (finSumFinEquiv.symm (finCongr hn i))
        ((tensorEquivSum R (Fin m) (Fin k) R
          (universalFactorizationMap R n m k hn (X j))).map C - C (X j))).det =
    Polynomial.resultant 𝐠 𝐡

MvPolynomial.etale_localizationAway_resultant_universalFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 283. The attribute's comment: “The conclusion: R → S[1/Δ] = S[1/Res_x(g, h)] is étale.”.

R[a] → S[1/Δ] is étale, where Δ = Res(g, h).

theorem etale_localizationAway_resultant_universalFactorizationMap :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Algebra.Etale (MvPolynomial (Fin n) R) (Localization.Away (Polynomial.resultant 𝐠 𝐡))

MvPolynomial.tfae_universalFactorizationMap_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 330. The attribute's comment: “For a prime q ⊂ S: (1) R → S is étale at q, (2) Δ = Res_x(g, h) ∉ q, (3) the images of g, h in κ(q)[x] are relatively prime, are equivalent. Étale at q is the source's definition, ∃ f ∉ q, Algebra.Etale R (Localization.Away f).”.

For a prime q of S the following are equivalent: R[a] → S is étale at q, that is, R[a] → S_f is étale for some f ∉ q; Δ = Res(g, h) ∉ q; the images of g and h in κ(q)[x] are coprime.

theorem tfae_universalFactorizationMap_etale (q : Ideal 𝓢) [q.IsPrime] :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    List.TFAE [∃ f ∉ q, Algebra.Etale (MvPolynomial (Fin n) R) (Localization.Away f),
      Polynomial.resultant 𝐠 𝐡 ∉ q,
      IsCoprime (𝐠.map (algebraMap 𝓢 q.ResidueField)) (𝐡.map (algebraMap 𝓢 q.ResidueField))]

MvPolynomial.exists_mulVec_sylvester_map_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 353. The attribute's comment: “The reason given for (2) ⇔ (3): the image of the Sylvester matrix in Mat(n + m, κ(q)) has a kernel if and only if ḡ, h̄ have a factor in common. Mathlib's Polynomial.sylvester is the transpose of the source's matrix; a square matrix over a field and its transpose have a nonzero kernel simultaneously.”.

For a prime q of S, the Sylvester matrix of the images of g and h in κ(q)[x] has a nonzero kernel if and only if these images have a common factor which is not a unit.

theorem exists_mulVec_sylvester_map_eq_zero_iff (q : Ideal 𝓢) [q.IsPrime] :
    (∃ v ≠ 0, Polynomial.sylvester (𝐠.map (algebraMap 𝓢 q.ResidueField))
      (𝐡.map (algebraMap 𝓢 q.ResidueField)) m k *ᵥ v = 0) ↔
    ∃ d, d ∣ 𝐠.map (algebraMap 𝓢 q.ResidueField) ∧ d ∣ 𝐡.map (algebraMap 𝓢 q.ResidueField) ∧
      ¬IsUnit d

MvPolynomial.isEtaleAt_universalFactorizationMap_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/UniversalFactorizationResultant.lean, line 377. The attribute's comment: “(1) ⇔ (2), with étale at q read as Mathlib's Algebra.IsEtaleAt, which agrees with the source's definition since S is of finite presentation over R.”.

R[a] → S is étale at a prime q of S in the sense of Algebra.IsEtaleAt if and only if Δ = Res(g, h) ∉ q.

theorem isEtaleAt_universalFactorizationMap_iff (q : Ideal 𝓢) [q.IsPrime] :
    letI := (universalFactorizationMap R n m k hn).toAlgebra
    Algebra.IsEtaleAt (MvPolynomial (Fin n) R) q ↔ Polynomial.resultant 𝐠 𝐡 ∉ q
Sources
LeanAlgebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero · Algebra.etaleLocus_eq_of_isPushout · Algebra.Etale.exists_etale_stage_of_isColimit · Algebra.Etale.iff_exists_algEquiv_prod · Algebra.IsEtaleAt.map_eq_maximalIdeal_and_finite_isSeparable_residueField · RingHom.Etale.quasiFinite · Algebra.IsEtaleAt.of_flat_of_map_eq_maximalIdeal · RingHom.Etale.of_comp

Section10.144 Local structure of étale ring maps#

Section 10.144 of the Stacks Project, Tag 0G1A. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00UB, a definition

Tag 00UB in the Stacks Project.

Declarations registered for the tag:

Tag 00UC, a lemma

Tag 00UC in the Stacks Project.

standardEtalePair_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/StandardEtale.lean, line 240. The attribute's comment: “(1)”. References: EGA IV (18.4.3), “(F)”; SGA 1 I (7.3), “partial”; SGA 1 I (7.4), “partial”.

For an explicit standard étale pair (f, g) over R, the canonical map R → R[x]_g/(f) is étale.

theorem standardEtalePair_isEtale {R : Type*} [CommRing R] (P : StandardEtalePair R) :
    Algebra.Etale R P.Ring

standardEtalePair_baseChange_isStandardEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/StandardEtale.lean, line 260. The attribute's comment: “(2)”. References: SGA 1 IX (1.3), “standard étale case”.

The base change T ⊗[R] (R[x]_g/(f)) is standard étale over T.

theorem standardEtalePair_baseChange_isStandardEtale {R T : Type*} [CommRing R]
    [CommRing T] [Algebra R T] (P : StandardEtalePair R) :
    Algebra.IsStandardEtale T (T ⊗[R] P.Ring)

standardEtalePair_localizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/StandardEtale.lean, line 270. The attribute's comment: “(3)”.

For a standard étale pair (f, g) over R with ring A = R[x]_g/(f) and any α : A, the composite R → A → A[1/α] is standard étale.

theorem standardEtalePair_localizationAway {R : Type*} [CommRing R]
    (P : StandardEtalePair R) (α : P.Ring)
    (Aα : Type*) [CommRing Aα] [Algebra P.Ring Aα] [Algebra R Aα]
    [IsScalarTower R P.Ring Aα] [IsLocalization.Away α Aα] :
    Algebra.IsStandardEtale R Aα

standardEtale_not_isStableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/StandardEtale.lean, line 512. The attribute's comment: “(4)”.

There exist commutative rings R, S, T with algebra structures forming a scalar tower R → S → T such that R → S and S → T are standard étale but the composite R → T is not.

theorem standardEtale_not_isStableUnderComposition :
    ∃ (R S T : Type) (_ : CommRing R) (_ : CommRing S) (_ : CommRing T)
      (_ : Algebra R S) (_ : Algebra S T) (_ : Algebra R T) (_ : IsScalarTower R S T),
      Algebra.IsStandardEtale R S ∧ Algebra.IsStandardEtale S T ∧
        ¬ Algebra.IsStandardEtale R T
Tag 00UD, a lemma

Tag 00UD in the Stacks Project.

Algebra.exists_etale_liesOver_residueFieldRingEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/ResidueFieldExtension.lean, line 428. The attribute's comment: “The isomorphism of extensions κ(p')/κ(p) ≅ κ(p) ⊂ L is pinned as a ring isomorphism e : κ(p') ≃+* L with e ∘ Ideal.ResidueField.map p p' (algebraMap R R') = algebraMap κ(p) L. Only Algebra.Etale R R' is asserted, as in the source's statement; that R' may be taken standard étale is Proposition 00UE. See the module docstring.”. References: SGA 2 XIV (3.4), “affine case”.

Stacks 00UD. Let R be a ring, p a prime of R and L/κ(p) a finite separable field extension. Then there are an étale ring map R → R' and a prime p' of R' lying over p together with an isomorphism κ(p') ≃ L of extensions of κ(p), i.e. one carrying the canonical map κ(p) → κ(p') induced by R → R' to the structure map κ(p) → L.

public theorem exists_etale_liesOver_residueFieldRingEquiv {R : Type u} [CommRing R] (p : Ideal R)
    [p.IsPrime] (L : Type v) [Field L] [Algebra p.ResidueField L]
    [Module.Finite p.ResidueField L] [Algebra.IsSeparable p.ResidueField L] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R')
      (p' : Ideal R') (_ : p'.IsPrime) (_ : p'.LiesOver p) (e : p'.ResidueField ≃+* L),
      (e : p'.ResidueField →+* L).comp
        (Ideal.ResidueField.map p p' (algebraMap R R') (p'.over_def p)) =
          algebraMap p.ResidueField L
Tag 00UE, a proposition

Tag 00UE in the Stacks Project.

Algebra.exists_isStandardEtale_of_exists_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/StandardEtale.lean, line 149. The attribute's comment: “The hypothesis "étale at q" is Definition 00U1 verbatim, ∃ g ∉ Q, Algebra.Etale R (Localization.Away g), rather than Mathlib's Algebra.IsEtaleAt, which is Algebra.FormallyEtale R S_Q and agrees with it only for S finitely presented over R; the source assumes no finiteness on S, so this is strictly more general than Mathlib's Algebra.IsEtaleAt.exists_isStandardEtale and implies it. S_g is Localization.Away g with its R-algebra structure the composite R → S → S_g. See the module docstring.”.

Let R → S be a ring map and q ⊂ S a prime. If R → S is étale at q, that is, if R → S_g is étale for some g ∈ S with g ∉ q, then there is a g ∈ S, g ∉ q, such that R → S_g is standard étale.

public theorem Algebra.exists_isStandardEtale_of_exists_etale {R : Type u} {S : Type v}
    [CommRing R] [CommRing S] [Algebra R S] (Q : Ideal S) [Q.IsPrime]
    (hQ : ∃ g ∉ Q, Algebra.Etale R (Localization.Away g)) :
    ∃ g ∉ Q, Algebra.IsStandardEtale R (Localization.Away g)
Tag 00UF, a lemma

Tag 00UF in the Stacks Project.

Algebra.IsStandardEtale.exists_finite_faithfullyFlat_forall_exists_comp_eq_comap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FiniteFlatCover.lean, line 373. The attribute's comment: “Conditions (1) and (2) are Module.Finite, Algebra.FinitePresentation and Module.FaithfullyFlat over R, faithful flatness being flatness plus surjectivity of Spec(S') → Spec(R); S'_{g'} is an arbitrary localization of S' away from g'; lying over a common prime is the equation between contractions, and the factorization is pinned by an equation between the canonical maps R → S'_{g'}. See the module docstring.”.

Stacks 00UF. Let R → S be a standard étale ring map. Then there is a finite, finitely presented, faithfully flat R-algebra S' — equivalently, S' is finite projective over R and Spec(S') → Spec(R) is surjective — such that for every prime q ⊂ S and every prime q' ⊂ S' lying over the same prime of R there are g' ∈ S', g' ∉ q', and a factorization of the canonical map R → S'_{g'} through a ring map φ : S → S'_{g'} with φ⁻¹(q'S'_{g'}) = q.

public theorem Algebra.IsStandardEtale.exists_finite_faithfullyFlat_forall_exists_comp_eq_comap_eq
    (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
    [Algebra.IsStandardEtale R S] :
    ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Algebra.FinitePresentation R S') (_ : Module.FaithfullyFlat R S'),
      ∀ (q : Ideal S) (_ : q.IsPrime) (q' : Ideal S') (_ : q'.IsPrime),
        q.under R = q'.under R → ∃ g' ∉ q', ∀ (B : Type w) (_ : CommRing B) (_ : Algebra S' B)
          (_ : IsLocalization.Away g' B), ∃ φ : S →+* B,
            φ.comp (algebraMap R S) = (algebraMap S' B).comp (algebraMap R S') ∧
              (q'.map (algebraMap S' B)).comap φ = q
Tag 00UG, a lemma

Tag 00UG in the Stacks Project.

Algebra.Etale.exists_finite_faithfullyFlat_forall_exists_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FiniteFlatCover.lean, line 689. The attribute's comment: “Hypotheses (1) and (2) are Algebra.Etale and Module.FaithfullyFlat over R, faithful flatness being flatness — which étale supplies — plus surjectivity of Spec(S) → Spec(R); conclusions (1) and (2) are likewise Module.Finite, Algebra.FinitePresentation and Module.FaithfullyFlat over R. S'_{g'} is an arbitrary localization of S' away from g', and the factorization in (3) is pinned by an equation between the canonical maps R → S'_{g'}. See the module docstring.”.

Stacks 00UG. Let R → S be a ring map which is étale and surjective on spectra. Then there is a finite, finitely presented, faithfully flat R-algebra S' — equivalently, S' is finite projective over R and Spec(S') → Spec(R) is surjective — such that for every prime q' ⊂ S' there is a g' ∈ S', g' ∉ q', for which the canonical map R → S'_{g'} factors as R → S → S'_{g'}.

public theorem Algebra.Etale.exists_finite_faithfullyFlat_forall_exists_comp_eq
    (R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
    [Algebra.Etale R S] [Module.FaithfullyFlat R S] :
    ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Algebra.FinitePresentation R S') (_ : Module.FaithfullyFlat R S'),
      ∀ (q' : Ideal S') (_ : q'.IsPrime), ∃ g' ∉ q', ∀ (B : Type w) (_ : CommRing B)
        (_ : Algebra S' B) (_ : IsLocalization.Away g' B), ∃ φ : S →+* B,
          φ.comp (algebraMap R S) = (algebraMap S' B).comp (algebraMap R S')
Sources
LeanAlgebra.IsStandardEtale · StandardEtalePair · StandardEtalePair.equivAwayQuotient · standardEtalePair_isEtale · standardEtalePair_baseChange_isStandardEtale · standardEtalePair_localizationAway · standardEtale_not_isStableUnderComposition · Algebra.exists_etale_liesOver_residueFieldRingEquiv

Section10.145 Étale local structure of quasi-finite ring maps#

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

Tag 00UK, a lemma

Tag 00UK in the Stacks Project.

Algebra.exists_etale_completeOrthogonalIdempotents_finite_not_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalStructure.lean, line 561. The attribute's comment: “The product decomposition is given by complete orthogonal idempotents e : Fin (n + 1) → R' ⊗[R] S, the factors being (R' ⊗[R] S)[1/e i], and the primes of a factor are named by the primes of R' ⊗[R] S avoiding the corresponding idempotent. See the module docstring.”.

Étale local structure of a finite type algebra along a fibre (Stacks 00UK). Let S be a finite type R-algebra and p a prime of R. There are an étale R-algebra R', a prime p' of R' lying over p with κ(p) = κ(p'), and a decomposition R' ⊗[R] S = A₁ × ⋯ × Aₙ × B — given by complete orthogonal idempotents e 0, …, e n, with Aᵢ = (R' ⊗[R] S)[1/e i] and B = (R' ⊗[R] S)[1/e n] — such that each Aᵢ is finite over R' and has exactly one prime r i lying over p', while R' → B is quasi-finite at no prime lying over p'.

public theorem Algebra.exists_etale_completeOrthogonalIdempotents_finite_not_quasiFiniteAt
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (p : Ideal R) [p.IsPrime] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R') (p' : Ideal R')
      (_ : p'.IsPrime) (_ : p'.LiesOver p) (n : ℕ) (e : Fin (n + 1) → R' ⊗[R] S)
      (_ : CompleteOrthogonalIdempotents e) (r : Fin n → Ideal (R' ⊗[R] S))
      (_ : ∀ i, (r i).IsPrime) (_ : ∀ i, (r i).LiesOver p'),
      Function.Bijective (Ideal.ResidueField.mapₐ p p' (Algebra.ofId _ _) (p'.over_def p)) ∧
      (∀ i : Fin n, Module.Finite R' (Localization.Away (e i.castSucc))) ∧
      (∀ i : Fin n, e i.castSucc ∉ r i) ∧
      (∀ (i : Fin n) (q : Ideal (R' ⊗[R] S)), q.IsPrime → q.LiesOver p' →
        e i.castSucc ∉ q → q = r i) ∧
      ∀ (q : Ideal (R' ⊗[R] S)) [q.IsPrime], q.LiesOver p' → e (Fin.last n) ∉ q →
        ¬ Algebra.QuasiFiniteAt R' q
Tag 00UL, a lemma

Tag 00UL in the Stacks Project.

Algebra.exists_etale_completeOrthogonalIdempotents_finite_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalStructure.lean, line 1115. The attribute's comment: “The product decomposition is given by complete orthogonal idempotents e : Fin (n + 1) → R' ⊗[R] S, the factors being (R' ⊗[R] S)[1/e i], and the primes of a factor are named by the primes of R' ⊗[R] S avoiding the corresponding idempotent. Unlike Tag 00UK this does not assert κ(p) = κ(p'), which the source's proof gives up in order to control the residue fields. See the module docstring.”.

Étale local structure of a finite type algebra along a fibre (Stacks 00UL). Let S be a finite type R-algebra and p a prime of R. There are an étale R-algebra R', a prime p' of R' lying over p, and a decomposition R' ⊗[R] S = A₁ × ⋯ × Aₙ × B — given by complete orthogonal idempotents e 0, …, e n, with Aᵢ = (R' ⊗[R] S)[1/e i] and B = (R' ⊗[R] S)[1/e n] — such that each Aᵢ is finite over R' and has exactly one prime r i lying over p', each residue field extension κ(r i)/κ(p') is finite purely inseparable, and R' → B is quasi-finite at no prime lying over p'.

public theorem Algebra.exists_etale_completeOrthogonalIdempotents_finite_isPurelyInseparable
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (p : Ideal R) [p.IsPrime] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R') (p' : Ideal R')
      (_ : p'.IsPrime) (_ : p'.LiesOver p) (n : ℕ) (e : Fin (n + 1) → R' ⊗[R] S)
      (_ : CompleteOrthogonalIdempotents e) (r : Fin n → Ideal (R' ⊗[R] S))
      (_ : ∀ i, (r i).IsPrime) (_ : ∀ i, (r i).LiesOver p'),
      (∀ i : Fin n, Module.Finite R' (Localization.Away (e i.castSucc))) ∧
      (∀ i : Fin n, e i.castSucc ∉ r i) ∧
      (∀ (i : Fin n) (q : Ideal (R' ⊗[R] S)), q.IsPrime → q.LiesOver p' →
        e i.castSucc ∉ q → q = r i) ∧
      (∀ i : Fin n, letI := Localization.AtPrime.algebraOfLiesOver p' (r i)
        Module.Finite p'.ResidueField (r i).ResidueField ∧
          IsPurelyInseparable p'.ResidueField (r i).ResidueField) ∧
      ∀ (q : Ideal (R' ⊗[R] S)) [q.IsPrime], q.LiesOver p' → e (Fin.last n) ∉ q →
        ¬ Algebra.QuasiFiniteAt R' q
Sources
LeanAlgebra.exists_etale_completeOrthogonalIdempotents_finite_not_quasiFiniteAt · Algebra.exists_etale_completeOrthogonalIdempotents_finite_isPurelyInseparable

Section10.146 Local homomorphisms#

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

Tag 0GSD, a lemma

Tag 0GSD in the Stacks Project.

IsLocalRing.exists_mem_maximalIdeal_bijective_algebraMap_quotient_span_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/ModuloPowers.lean, line 458. The attribute's comment: “The hypothesis t ∈ m_R and the conclusion are the source's; the map shown bijective is the canonical R/tⁿR → S/tⁿS. Stated for all n : ℕ (the case n = 0 is the zero ring), with κ(m_R) → κ(m_S) merely surjective (equivalent, as it is injective automatically), and with the étale algebra T and the prime q as hypotheses rather than an existential.”.

An étale local homomorphism is an isomorphism modulo powers of a principal ideal. Let (R, m_R) → (S, m_S) be a local homomorphism of local rings such that S is the localization of an étale R-algebra T at a prime q, and such that the residue field extension κ(m_R) → κ(m_S) is surjective, hence an isomorphism. Then there is t ∈ m_R such that R/tⁿR → S/tⁿS is an isomorphism for every n.

public theorem IsLocalRing.exists_mem_maximalIdeal_bijective_algebraMap_quotient_span_pow
    (R : Type u) [CommRing R] [IsLocalRing R] (S : Type v) [CommRing S] [IsLocalRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)] (T : Type w) [CommRing T] [Algebra R T]
    [Algebra.Etale R T] [Algebra T S] [IsScalarTower R T S] (q : Ideal T) [q.IsPrime]
    [IsLocalization.AtPrime S q]
    (hres : Function.Surjective (IsLocalRing.ResidueField.map (algebraMap R S))) :
    ∃ t ∈ IsLocalRing.maximalIdeal R, ∀ n : ℕ, Function.Bijective
      (algebraMap (R ⧸ Ideal.span {t ^ n}) (S ⧸ (Ideal.span {t ^ n}).map (algebraMap R S)))
Tag 053K, a lemma

Tag 053K in the Stacks Project.

IsLocalRing.exists_finite_faithfullyFlat_forall_isMaximal_isLocalHom_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/FiniteFlatCover.lean, line 992. The attribute's comment: “The étale algebra T and the prime q presenting S are hypotheses rather than an existential, as in Lemma 0GSD. R → S' is Module.Finite, Algebra.FinitePresentation and Module.FaithfullyFlat; S'_{m'} is an arbitrary localization of S' at m'; the factorization is pinned by an equation with the canonical map R → S'_{m'}, and the factoring map is required to be local, as in the source's proof. See the module docstring.”.

Stacks 053K. Let (R, m_R) → (S, m_S) be a local homomorphism of local rings such that S is the localization of an étale R-algebra T at a prime q. Then there is a finite, finitely presented, faithfully flat R-algebra S' such that for every maximal ideal m' of S' the canonical map R → S'_{m'} factors as R → S → S'_{m'}, with S → S'_{m'} a local homomorphism.

public theorem IsLocalRing.exists_finite_faithfullyFlat_forall_isMaximal_isLocalHom_comp_eq
    (R : Type u) [CommRing R] [IsLocalRing R] (S : Type v) [CommRing S] [IsLocalRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)] (T : Type w) [CommRing T] [Algebra R T]
    [Algebra.Etale R T] [Algebra T S] [IsScalarTower R T S] (q : Ideal T) [q.IsPrime]
    [IsLocalization.AtPrime S q] :
    ∃ (S' : Type u) (_ : CommRing S') (_ : Algebra R S') (_ : Module.Finite R S')
      (_ : Algebra.FinitePresentation R S') (_ : Module.FaithfullyFlat R S'),
      ∀ (m' : Ideal S') (_ : m'.IsMaximal) (A : Type x) (_ : CommRing A) (_ : Algebra S' A)
        (_ : IsLocalization.AtPrime A m'), ∃ (ψ : S →+* A) (_ : IsLocalHom ψ),
          ψ.comp (algebraMap R S) = (algebraMap S' A).comp (algebraMap R S')
Sources
LeanIsLocalRing.exists_mem_maximalIdeal_bijective_algebraMap_quotient_span_pow · IsLocalRing.exists_finite_faithfullyFlat_forall_isMaximal_isLocalHom_comp_eq

Section10.147 Integral closure and smooth base change#

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

Tag 03GF, an example

Tag 03GF in the Stacks Project.

vandermondeProd_isUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RootsOfUnity/VandermondeUnit.lean, line 250.

Stacks 03GF. For every d < p, the element Δ\_d = ∏\_\{0 ≤ i < j < d} (α\_i - α\_j) is a unit in R' = Z[1/p][x]/(Phi(x)).

Δ_d is a double product of the differences αᵢ - αⱼ; each such difference (for i < j < d ≤ p-1) is a unit by alpha_sub_isUnit, and a product of units is a unit (Finset.prod_induction with IsUnit.mul, isUnit_one).

theorem vandermondeProd_isUnit (d : ℕ) (hd : d < p) : IsUnit (vandermondeProd p d)
Tag 03GG, a lemma

Tag 03GG in the Stacks Project.

Algebra.Smooth.toIntegralClosure_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/BaseChange.lean, line 118. The attribute's comment: “The isomorphism of the tag is bijectivity of Mathlib's canonical map TensorProduct.toIntegralClosure, whose AlgEquiv form is AlgEquiv.ofBijective applied to it. This is Mathlib's TensorProduct.toIntegralClosure_bijective_of_smooth, which carries no @[stacks] tag upstream. See the module docstring.”. References: EGA IV (18.12.15), “more general”; EGA IV (6.14.5), “smooth base change”.

Let R → S be a smooth ring map, let R → B be any ring map, let A = integralClosure R B be the integral closure of R in B and let A' = integralClosure S (S ⊗[R] B) be the integral closure of S in S ⊗[R] B. Then the canonical map S ⊗[R] A → A', s ⊗ a ↦ s ⊗ a, is an isomorphism.

public theorem toIntegralClosure_bijective {R S B : Type*} [CommRing R] [CommRing S] [CommRing B]
    [Algebra R S] [Algebra R B] [Algebra.Smooth R S] :
    Function.Bijective (TensorProduct.toIntegralClosure R S B)
Tag 0CBF, a lemma

Tag 0CBF in the Stacks Project.

TensorProduct.toIntegralClosure_bijective_of_directLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/BaseChange.lean, line 371. The attribute's comment: “The colimit step of the tag, with the smoothness of the stages weakened to what the argument uses: bijectivity of the map at each stage. The tag's own hypothesis is recovered in TensorProduct.toIntegralClosure_bijective_of_directLimit_smooth below. The filtered colimit is spelled as a colimit over a directed nonempty preorder, presented by an R-algebra equivalence DirectLimit G F ≃ₐ[R] S so that the conclusion is about an abstract S; the isomorphism of the tag is bijectivity of Mathlib's canonical map TensorProduct.toIntegralClosure, as in the smooth case 03GG. See the module docstring.”.

Let R → S and R → B be ring maps, let A = integralClosure R B and let A' = integralClosure S (S ⊗[R] B). If S is R-algebra isomorphic to the colimit DirectLimit G F of a directed system G of R-algebras and the canonical map G i ⊗[R] A → integralClosure (G i) (G i ⊗[R] B) is bijective for every i, then the canonical map S ⊗[R] A → A' is bijective.

public theorem TensorProduct.toIntegralClosure_bijective_of_directLimit
    {R S B : Type*} [CommRing R] [CommRing S] [CommRing B] [Algebra R S] [Algebra R B]
    {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    {G : ι → Type*} [∀ i, CommRing (G i)] [∀ i, Algebra R (G i)]
    (F : ∀ i j, i ≤ j → (G i →ₐ[R] G j)) [DirectedSystem G fun i j h ↦ F i j h]
    (e : DirectLimit G F ≃ₐ[R] S)
    (H : ∀ i, Function.Bijective (TensorProduct.toIntegralClosure R (G i) B)) :
    Function.Bijective (TensorProduct.toIntegralClosure R S B)

TensorProduct.toIntegralClosure_bijective_of_directLimit_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/IntegralClosure/BaseChange.lean, line 390. The attribute's comment: “The literal form of the tag, as the colimit step TensorProduct.toIntegralClosure_bijective_of_directLimit applied to the smooth case 03GG (TensorProduct.toIntegralClosure_bijective_of_smooth).”. References: EGA IV (6.14.5), “colimit of smooth base”; EGA IV (18.12.15).

Let R → S and R → B be ring maps, let A = integralClosure R B and let A' = integralClosure S (S ⊗[R] B). If S is R-algebra isomorphic to the colimit DirectLimit G F of a directed system G of smooth R-algebras, then the canonical map S ⊗[R] A → A' is an isomorphism.

public theorem TensorProduct.toIntegralClosure_bijective_of_directLimit_smooth
    {R S B : Type*} [CommRing R] [CommRing S] [CommRing B] [Algebra R S] [Algebra R B]
    {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    {G : ι → Type*} [∀ i, CommRing (G i)] [∀ i, Algebra R (G i)] [∀ i, Algebra.Smooth R (G i)]
    (F : ∀ i j, i ≤ j → (G i →ₐ[R] G j)) [DirectedSystem G fun i j h ↦ F i j h]
    (e : DirectLimit G F ≃ₐ[R] S) :
    Function.Bijective (TensorProduct.toIntegralClosure R S B)
Sources
LeanvandermondeProd_isUnit · Algebra.Smooth.toIntegralClosure_bijective · TensorProduct.toIntegralClosure_bijective_of_directLimit · TensorProduct.toIntegralClosure_bijective_of_directLimit_smooth

Section10.148 Formally unramified maps#

Section 10.148 of the Stacks Project, Tag 00UM. 6 tags here are carried by 2 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00UN, a definition

Tag 00UN in the Stacks Project.

Declarations registered for the tag:

Tag 0H91, a lemma

Tag 0H91 in the Stacks Project.

Declarations registered for the tag:

Tag 00UO, a lemma

Tag 00UO in the Stacks Project.

Declarations registered for the tag:

  • Algebra.formallyUnramified_iff registered with add_to_stacks in StacksFrontier/RingTheory/Unramified/Basic.lean, line 58 (StacksFrontier): “formally unramified iff the module of differentials vanishes”. References: EGA IV (17.2.1), “affine case”; EGA 0 (21.7.4), “b) ⇔ d)”; EGA IV (17.4.1), “(c) <=> (e)”; EGA 0 (20.7.4), “discrete case”; EGA 0 (21.7.4), “b) <=> d)”; EGA IV (17.2.1), “affine/ring case”.
Tag 04E8, a lemma

Tag 04E8 in the Stacks Project.

formally_unramified_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Basic.lean, line 278. References: EGA IV (17.4.2), “Affine case of a ⇔ e”.

Formally unramified is a local property: for a ring map R → S, being formally unramified is equivalent to all the localized maps R → S_𝔮 being formally unramified, which in turn is equivalent to all the maps R_𝔭 → S_𝔮 (with 𝔭 = R ∩ 𝔮) being formally unramified.

theorem formally_unramified_local
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] :
    List.TFAE
      [ Algebra.FormallyUnramified R S,
        ∀ (𝔮 : Ideal S) [𝔮.IsPrime],
          Algebra.FormallyUnramified R (Localization.AtPrime 𝔮),
        ∀ (𝔮 : Ideal S) [𝔮.IsPrime],
          haveI : (𝔮.comap (algebraMap R S)).IsPrime := Ideal.IsPrime.comap _
          haveI : 𝔮.LiesOver (𝔮.comap (algebraMap R S)) := ⟨rfl⟩
          haveI : Algebra (Localization.AtPrime (𝔮.comap (algebraMap R S)))
              (Localization.AtPrime 𝔮) := Localization.AtPrime.algebraOfLiesOver _ 𝔮
          Algebra.FormallyUnramified
            (Localization.AtPrime (𝔮.comap (algebraMap R S)))
            (Localization.AtPrime 𝔮) ]
Tag 04E9, a lemma

Tag 04E9 in the Stacks Project.

Declarations registered for the tag:

Tag 07QE, a lemma

Tag 07QE in the Stacks Project.

Algebra.FormallyUnramified.directLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Basic.lean, line 424.

Concrete Ring.DirectLimit form. Equip the direct limit Ring.DirectLimit S φ of a directed system of R-algebras with its canonical R-algebra structure directLimitAlgebra φ. If every S i is formally unramified over R, then so is the direct limit. (No extra compatibility hypothesis is needed: the canonical maps Ring.DirectLimit.of … i are automatically R-algebra homomorphisms, cf. Ring.DirectLimit.of_commutes.)

theorem Algebra.FormallyUnramified.directLimit
    [DirectedSystem S (fun i j h => (φ i j h : S i → S j))]
    (hunram : ∀ i, Algebra.FormallyUnramified R (S i)) :
    letI := directLimitAlgebra φ
    Algebra.FormallyUnramified R (Ring.DirectLimit S (fun i j h => (φ i j h : S i → S j)))
Sources
LeanAlgebra.FormallyUnramified · Algebra.FormallyUnramified.iff_comp_injective · Algebra.FormallyUnramified.base_change · Algebra.formallyUnramified_iff · formally_unramified_local · Algebra.FormallyUnramified.localization_map · Algebra.FormallyUnramified.of_isLocalization · Algebra.FormallyUnramified.directLimit

Section10.149 Conormal modules and universal thickenings#

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

Tag 04EB, a lemma

Tag 04EB in the Stacks Project.

Algebra.FormallyUnramified.exists_extension_ker_sq_eq_bot_and_existsUnique_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Thickening.lean, line 289. The attribute's comment: “The surjection of R-algebras S' → S is an Algebra.Extension R S (the structure whose data is exactly a surjection onto S of R-algebras). The source's square is encoded by A being an R-algebra — its b : R → A is algebraMap R A — and a being an R-algebra map, so that commutativity of the square is a's R-linearity. The test algebra lives in a universe of its own; see the module docstring.”.

Stacks 04EB. Let R → S be a formally unramified ring map. There is a surjection of R-algebras S' → S whose kernel is an ideal of square zero and which is universal: for every R-algebra A, every ideal I ⊆ A with I ^ 2 = 0 and every R-algebra map a : S → A/I, there is a unique R-algebra map a' : S' → A such that S' → A → A/I equals S' → S → A/I. The surjection S' → S is algebraMap P.Ring S for the produced Algebra.Extension P.

theorem Algebra.FormallyUnramified.exists_extension_ker_sq_eq_bot_and_existsUnique_lift
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FormallyUnramified R S] :
    ∃ P : Algebra.Extension.{max u v} R S, P.ker ^ 2 = ⊥ ∧
      ∀ ⦃A : Type w⦄ [CommRing A] [Algebra R A] (I : Ideal A), I ^ 2 = ⊥ →
        ∀ a : S →ₐ[R] A ⧸ I, ∃! a' : P.Ring →ₐ[R] A,
          (Ideal.Quotient.mkₐ R I).comp a' = a.comp (IsScalarTower.toAlgHom R P.Ring S)
Tag 04EC, a definition

Tag 04EC in the Stacks Project.

Algebra.FormallyUnramified.universalFirstOrderThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Thickening.lean, line 368. The attribute's comment: “Part (1). The surjection S' → S is an Algebra.Extension R S, the structure whose data is exactly a surjection of R-algebras onto S; the surjection is algebraMap S'.Ring S. Only determined up to unique isomorphism, so defined by choosing one of the thickenings produced by Tag 04EB and used only through Algebra.FormallyUnramified.isUniversalFirstOrderThickening. See the module docstring.”.

The universal first order thickening S' → S of S over a formally unramified base R: the surjection of R-algebras onto S with square-zero kernel through which every square-zero situation over S lifts uniquely, provided by Tag 04EB. It is determined up to unique isomorphism by Algebra.FormallyUnramified.isUniversalFirstOrderThickening, which is all that is ever used about it.

noncomputable def universalFirstOrderThickening : Extension.{max u v} R S

Algebra.FormallyUnramified.conormal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Thickening.lean, line 385. The attribute's comment: “Part (2). The kernel of algebraMap S'.Ring S seen as an S-module is Algebra.Extension.Cotangent, the quotient of the kernel by its square — equal to the kernel because the square is zero, and the object on which S acts. See the module docstring.”.

The conormal module C_{S/R} of a formally unramified ring map R → S: the kernel of the universal first order thickening S' → S, as a module over S. Being an ideal of square zero in S', that kernel equals its own image in S' / (ker) ^ 2, which is where the S-action lives.

abbrev conormal : Type (max u v)
Tag 04ED, a lemma

Tag 04ED in the Stacks Project.

UniversalThickening.universal_property, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Thickening.lean, line 1174.

For any commutative ring A with a square-zero ideal J ⊆ A, and ring homomorphisms b : R → A, a : R/I → A/J such that the square a ∘ (R → R/I) = (A → A/J) ∘ b commutes (where R → A/J is b followed by A → A/J), there exists a unique R-algebra homomorphism a' : R/I² → A, encoded as a unique ring homomorphism with a' ∘ (R → R/I²) = b (the R-algebra condition), such that (A → A/J) ∘ a' = a ∘ π.

theorem universal_property
    {A : Type*} [CommRing A] (J : Ideal A) (hJ : IsSquareZero J)
    (b : R →+* A) (a : (R ⧸ I) →+* (A ⧸ J))
    (hcomm : a.comp (Ideal.Quotient.mk I) = (Ideal.Quotient.mk J).comp b) :
    ∃! a' : (R ⧸ I ^ 2) →+* A,
      a'.comp (Ideal.Quotient.mk (I ^ 2)) = b ∧
      (Ideal.Quotient.mk J).comp a' = a.comp (pi I : (R ⧸ I ^ 2) →+* (R ⧸ I))

UniversalThickening.conormal_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Thickening.lean, line 1222. References: EGA 0 (20.5.12), “kernel of E → C is R/R²”.

Consequently the universal first order thickening of R/I over R is the surjection π : R/I² → R/I, whose kernel — the conormal module C_{(R/I)/R} — is I/I². Concretely, the kernel of π is Ideal.cotangentIdeal I (Statement 1b), and the conormal module Ideal.Cotangent I (the R-module I/I²) is R-linearly isomorphic to this kernel via Ideal.cotangentEquivIdeal. We record both facts: the kernel description and the existence of such an R-linear equivalence.

theorem conormal_module :
    RingHom.ker (pi I : (R ⧸ I ^ 2) →+* (R ⧸ I)) = I.cotangentIdeal ∧
    Nonempty (I.Cotangent ≃ₗ[R] (RingHom.ker (pi I : (R ⧸ I ^ 2) →+* (R ⧸ I))))
Tag 04EE, a lemma

Tag 04EE in the Stacks Project.

Algebra.Extension.IsUniversalFirstOrderThickening.localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Thickening.lean, line 473. The attribute's comment: “Both parts at once: part (1) is N = Algebra.algebraMapSubmonoid B M, part (2) is M = ⊥, whose instance IsLocalization (⊥ : Submonoid A) A is not found by synthesis and is supplied as IsLocalization.of_le_isUnit bot_le. The localized thickening is an arbitrary Q : Algebra.Extension Aₘ Bₙ pinned by the IsLocalization and IsScalarTower hypotheses and by algebraMap_comp, because Mathlib's Algebra.Extension.localization does not localize the base. The In particular on conormal modules is the ideal equation, Algebra.idealMap_isLocalizedModule supplying the rest. That φ⁻¹(N) is multiplicative is Submonoid.comap. See the module docstring.”.

Stacks 04EE. Let A → B be a ring map, let φ : P.Ring → B be a universal first order thickening of B over A, let M ⊆ A and N ⊆ B be multiplicative subsets, and let Aₘ and Bₙ be localizations of A at M and of B at N, compatibly. Then the localization φ⁻¹(N)⁻¹P.Ring → N⁻¹B of φ is a universal first order thickening of N⁻¹B over Aₘ, and its kernel is the extension of ker φ, so that the conormal module localizes: N⁻¹C_{B/A} = C_{N⁻¹B/Aₘ}. Taking N to be the image of M gives the source's part (1), and taking M = ⊥, so that Aₘ = A, gives its part (2).

theorem Algebra.Extension.IsUniversalFirstOrderThickening.localization {A : Type u} {B : Type v}
    [CommRing A] [CommRing B] [Algebra A B]
    {P : Extension.{w} A B} (hP : P.IsUniversalFirstOrderThickening)
    (M : Submonoid A) (N : Submonoid B)
    {Aₘ : Type*} [CommRing Aₘ] [Algebra A Aₘ] [IsLocalization M Aₘ]
    {Bₙ : Type*} [CommRing Bₙ] [Algebra B Bₙ] [IsLocalization N Bₙ]
    [Algebra A Bₙ] [IsScalarTower A B Bₙ] [Algebra Aₘ Bₙ] [IsScalarTower A Aₘ Bₙ]
    (Q : Extension.{w} Aₘ Bₙ) [Algebra P.Ring Q.Ring] [IsScalarTower A P.Ring Q.Ring]
    [IsLocalization (N.comap (algebraMap P.Ring B)) Q.Ring]
    (algebraMap_comp : (algebraMap Q.Ring Bₙ).comp (algebraMap P.Ring Q.Ring)
      = (algebraMap B Bₙ).comp (algebraMap P.Ring B)) :
    Q.IsUniversalFirstOrderThickening ∧ Q.ker = P.ker.map (algebraMap P.Ring Q.Ring)
Tag 04EF, a lemma

Tag 04EF in the Stacks Project.

Algebra.Extension.IsUniversalFirstOrderThickening.formallyUnramified_ring_and_bijective_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Thickening.lean, line 1052. The attribute's comment: “The thickening B' → B is an Algebra.Extension A B satisfying Algebra.Extension.IsUniversalFirstOrderThickening (04EC); existence is 04EB. Tensor products carry the scalars on the left, as in KaehlerDifferential.mapBaseChange, and the source's canonical map is spelled as the B-linear extension of ω ↦ 1 ⊗ₜ KaehlerDifferential.map ω. Formal unramifiedness of A → B is not assumed: it follows from hP. See the module docstring.”.

Stacks 04EF. Let R → A → B be ring maps and let B' → B be the universal first order thickening of B over A. Then B' is formally unramified over A, and the canonical map Ω_{A/R} ⊗_A B → Ω_{B'/R} ⊗_{B'} B, which sends b ⊗ D a to b ⊗ D (algebraMap A B' a), is an isomorphism.

public theorem formallyUnramified_ring_and_bijective_map (R : Type u) {A : Type v} {B : Type*}
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B]
    [IsScalarTower R A B] {P : Extension.{w} A B} (hP : P.IsUniversalFirstOrderThickening) :
    FormallyUnramified A P.Ring ∧
      Function.Bijective
        ((((TensorProduct.mk P.Ring B Ω[P.Ring⁄R] 1).restrictScalars A).comp
          (KaehlerDifferential.map R R A P.Ring)).liftBaseChange B)
Sources
LeanAlgebra.FormallyUnramified.exists_extension_ker_sq_eq_bot_and_existsUnique_lift · Algebra.FormallyUnramified.universalFirstOrderThickening · Algebra.FormallyUnramified.conormal · UniversalThickening.universal_property · UniversalThickening.conormal_module · Algebra.Extension.IsUniversalFirstOrderThickening.localization · Algebra.Extension.IsUniversalFirstOrderThickening.formallyUnramified_ring_and_bijective_map

Section10.150 Formally étale maps#

Section 10.150 of the Stacks Project, Tag 00UP. 7 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0H92, a lemma

Tag 0H92 in the Stacks Project.

Declarations registered for the tag:

Tag 00UR, a lemma

Tag 00UR in the Stacks Project.

Algebra.formallyEtale_iff_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 119. References: EGA IV (17.3.2), “(ii), étale case”; EGA IV (17.3.1), “étale case, ring maps”.

A finitely presented algebra is étale if and only if it is formally étale.

theorem Algebra.formallyEtale_iff_etale
    (R : Type*) (S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (hfp : Algebra.FinitePresentation R S) :
    Algebra.FormallyEtale R S ↔ Algebra.Etale R S
Tag 031N, a lemma

Tag 031N in the Stacks Project.

Algebra.FormallyEtale.colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/FirstProperties.lean, line 148.

Let R be a commutative ring and let ι be a directed set, a nonempty preorder in which every pair has an upper bound. Let F : ι ⥤ CommAlgCat R be a directed system of R-algebras over ι, the family S_i = F.obj i with the transition maps encoded by functoriality. If every S_i is formally étale over R, then the colimit S = colim_i S_i is formally étale over R.

theorem Algebra.FormallyEtale.colimit
    (R : Type) [CommRing R]
    (ι : Type) [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
    (F : ι ⥤ CommAlgCat.{0} R)
    (h : ∀ i : ι, Algebra.FormallyEtale R (F.obj i)) :
    Algebra.FormallyEtale R (colimit F : CommAlgCat R)
Tag 04EG, a lemma

Tag 04EG in the Stacks Project.

Declarations registered for the tag:

Tag 0H1D, a lemma

Tag 0H1D in the Stacks Project.

FormallyEtaleH1D.quotMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/AssociatedGraded.lean, line 336. The attribute's comment: “(1)”.

If φ : R → S is formally étale and R → S/J is surjective, with I = ker(R → S/J), then for every n ≥ 1 the canonical map φ̄ₙ : R/I^n → S/J^n is bijective.

theorem quotMap_bijective
    (hφ : RingHom.FormallyEtale φ)
    (hsurj : Function.Surjective ((Ideal.Quotient.mk J).comp φ))
    (n : ℕ) (hn : 1 ≤ n) :
    Function.Bijective (quotMap φ J n)

FormallyEtaleH1D.grMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/AssociatedGraded.lean, line 349. The attribute's comment: “(2)”.

If φ : R → S is formally étale and R → S/J is surjective, with I = ker(R → S/J), then the induced map of associated graded rings gr(φ) : ⊕_n I^n/I^{n+1} → ⊕_n J^n/J^{n+1} is an isomorphism: for every n its degree-n component I^n/I^{n+1} → J^n/J^{n+1} is bijective.

theorem grMap_bijective
    (hφ : RingHom.FormallyEtale φ)
    (hsurj : Function.Surjective ((Ideal.Quotient.mk J).comp φ))
    (n : ℕ) :
    Function.Bijective (grMap φ J n)
Tag 0H93, a lemma

Tag 0H93 in the Stacks Project.

KaehlerDifferential.isBaseChange_quotient_ideal_pow_of_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/DiagonalIdeal.lean, line 380. The attribute's comment: “Stated for an arbitrary exponent n in place of the source's k + 1, and in Mathlib's IsBaseChange form; the map is the hypothesis hφ, which pins it. The source's final assertion, that S' ⊗_S Ω[S⁄R] → Ω[S'⁄R] is an isomorphism, is KaehlerDifferential.isBaseChange_of_formallyEtale. See the module docstring.”. References: EGA IV (17.2.4), “affine case”.

Let R → S → S' be ring maps and let J, resp. J', be the kernel of the multiplication map S ⊗[R] S → S, resp. S' ⊗[R] S' → S'. If S → S' is formally étale, then the canonical ring map (S ⊗[R] S) ⧸ J ^ n → (S' ⊗[R] S') ⧸ (J') ^ n, i.e. the unique one sending the class of a ⊗ₜ b to the class of a ⊗ₜ b, exhibits its target as the base change of its source along S → S': S' ⊗_S ((S ⊗[R] S) ⧸ J ^ n) = (S' ⊗[R] S') ⧸ (J') ^ n.

theorem isBaseChange_quotient_ideal_pow_of_formallyEtale [Algebra.FormallyEtale S S']
    (n : ℕ)
    (φ : ((S ⊗[R] S) ⧸ KaehlerDifferential.ideal R S ^ n) →ₐ[S]
      ((S' ⊗[R] S') ⧸ KaehlerDifferential.ideal R S' ^ n))
    (hφ : ∀ a b : S, φ (Ideal.Quotient.mk _ (a ⊗ₜ[R] b)) =
      Ideal.Quotient.mk _ (algebraMap S S' a ⊗ₜ[R] algebraMap S S' b)) :
    IsBaseChange S' φ.toLinearMap
Tag 0H94, a lemma

Tag 0H94 in the Stacks Project.

LinearMap.IsUniversalDifferentialOperatorOfOrderLE.isBaseChange_of_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/Basic/PrincipalParts.lean, line 700. The attribute's comment: “Stated in Mathlib's IsBaseChange form, for an arbitrary base change M' of M and arbitrary modules of principal parts on both sides (Definition 09CL); the map is pinned by hg, compatibility with the universal differential operators, and its existence is elementary. The source's second assertion, the unique extension of a finite order differential operator, follows formally, as the source's It follows that says. The source sets M' = S' ⊗_R M, a slip for S' ⊗_S M. See the module docstring.”.

Let R → S → S' be ring maps with S → S' formally étale (for example étale), let M be an S-module, let k : ℕ and set M' = S' ⊗[S] M, the base change of M along S → S' given by f. Let (P, D) be a module of principal parts of order k of M relative to R → S and let (P', D') be one of M' relative to R → S'. Then the unique S-linear map g : P → P' with g ∘ D = D' ∘ f exhibits P' as the base change of P along S → S': S' ⊗[S] Pᵏ_{S/R}(M) = Pᵏ_{S'/R}(M'). It follows that every differential operator M → N of order at most k has a unique extension to a differential operator M' → S' ⊗[S] N of order at most k.

theorem isBaseChange_of_formallyEtale [Algebra.FormallyEtale S S'] (k : ℕ)
    {D : M →ₗ[R] P} (hD : D.IsUniversalDifferentialOperatorOfOrderLE S k)
    {D' : M' →ₗ[R] P'} (hD' : D'.IsUniversalDifferentialOperatorOfOrderLE S' k)
    (f : M →ₗ[S] M') (hf : IsBaseChange S' f) (g : P →ₗ[S] P')
    (hg : ∀ m : M, g (D m) = D' (f m)) :
    IsBaseChange S' g
Sources
LeanAlgebra.FormallyEtale.instTensorProduct · Algebra.formallyEtale_iff_etale · Algebra.FormallyEtale.colimit · Algebra.FormallyEtale.of_isLocalization · FormallyEtaleH1D.quotMap_bijective · FormallyEtaleH1D.grMap_bijective · KaehlerDifferential.isBaseChange_quotient_ideal_pow_of_formallyEtale · LinearMap.IsUniversalDifferentialOperatorOfOrderLE.isBaseChange_of_formallyEtale

Section10.151 Unramified ring maps#

Section 10.151 of the Stacks Project, Tag 00US. 8 tags here are carried by 28 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00UT, a definition

Tag 00UT in the Stacks Project.

Algebra.GUnramified, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Defs.lean, line 122. The attribute's comment: “Item (2). Ω_{S/R} = 0 is Algebra.FormallyUnramified (Lemma 00UO, Algebra.formallyUnramified_iff), as in Mathlib's Algebra.Unramified, Algebra.Smooth and Algebra.Etale. Item (1) is Algebra.Unramified, item (3) is ∃ g ∉ q, Algebra.Unramified R (Localization.Away g) and item (4) is ∃ g ∉ q, Algebra.GUnramified R (Localization.Away g). See the module docstring.”.

A ring map R → S is G-unramified if it is of finite presentation and Ω_{S/R} = 0 (Stacks 00UT (2)); the vanishing of the differentials is recorded as formal unramifiedness, which is the same condition by Lemma 00UO. This is the notion of EGA; dropping finite presentation to finite type gives Algebra.Unramified, item (1) of the same definition.

public class Algebra.GUnramified (R : Type*) [CommRing R] (S : Type*) [CommRing S] [Algebra R S] :
    Prop
Tag 00UU, a lemma

Tag 00UU in the Stacks Project.

Algebra.unramified_iff_and_gUnramified_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 126. The attribute's comment: “Both equivalences, as one lemma. Ω_{S/R} = 0 is written out as Subsingleton Ω[S⁄R] on the right of each; on the left, Algebra.Unramified and Algebra.GUnramified (Definition 00UT) are formal unramifiedness together with finite type resp. finite presentation, so the literal reading of the lemma would be structure eta. See the module docstring.”. References: EGA IV (17.3.2), “(ii) unramified”; EGA IV (17.4.2), “affine case: a) ⇔ c)”.

Stacks 00UU. A ring map R → S is unramified if and only if it is of finite type and Ω_{S/R} = 0, and G-unramified if and only if it is of finite presentation and Ω_{S/R} = 0. Both equivalences come from the identification of the vanishing of Ω_{S/R} with formal unramifiedness (Lemma 00UO, Algebra.formallyUnramified_iff), which is the condition that Algebra.Unramified and Algebra.GUnramified pair with their finiteness conditions.

public theorem Algebra.unramified_iff_and_gUnramified_iff (R S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] :
    (Algebra.Unramified R S ↔ Algebra.FiniteType R S ∧ Subsingleton Ω[S⁄R]) ∧
      (Algebra.GUnramified R S ↔ Algebra.FinitePresentation R S ∧ Subsingleton Ω[S⁄R])
Tag 00UV, a lemma

Tag 00UV in the Stacks Project.

Algebra.unramified_and_gUnramified_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 926. The attribute's comment: “All thirteen items, both variants of each, as one conjunction in the source's order; item n is the n-th conjunct and its (resp. G-unramified) reading is that conjunct's second component. The conjuncts share the universe variables u, v, w, and each item is exported under its own name; a proof should cite those names. Items (8) and (9) quantify over a prime of the fibre κ(𝔭) ⊗_R S rather than over a prime of S lying over 𝔭. See the module docstring.”.

Stacks 00UV. Properties of unramified and G-unramified ring maps: (1) base change, (2) composition, (3) a principal localization, (4) a quotient, (5) an étale map, (6)–(9) four criteria at a prime in terms of the vanishing of the differentials, (10) descent along a principal open cover, (11) unramifiedness at every prime, (12)–(13) descent to a finite type ℤ-algebra. Each item has a version for Algebra.Unramified and one for Algebra.GUnramified, the source's "resp.", differing only in whether the finiteness condition is finite type or finite presentation. Cite the items by the names listed in the module docstring, not by projecting.

public theorem Algebra.unramified_and_gUnramified_properties :
    -- (1) base change
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (R' : Type w)
        [CommRing R'] [Algebra R R'], (Unramified R S → Unramified R' (R' ⊗[R] S)) ∧
          (GUnramified R S → GUnramified R' (R' ⊗[R] S))) ∧
    -- (2) composition
    (∀ {R : Type u} {S : Type v} {T : Type w} [CommRing R] [CommRing S] [CommRing T] [Algebra R S]
        [Algebra S T] [Algebra R T] [IsScalarTower R S T],
        (Unramified R S → Unramified S T → Unramified R T) ∧
          (GUnramified R S → GUnramified S T → GUnramified R T)) ∧
    -- (3) a principal localization
    (∀ {R : Type u} [CommRing R] (f : R) (Rf : Type v) [CommRing Rf] [Algebra R Rf]
        [IsLocalization.Away f Rf], GUnramified R Rf ∧ Unramified R Rf) ∧
    -- (4) a quotient
    (∀ {R : Type u} [CommRing R] (I : Ideal R),
        Unramified R (R ⧸ I) ∧ (I.FG → GUnramified R (R ⧸ I))) ∧
    -- (5) an étale map
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Etale R S],
        GUnramified R S ∧ Unramified R S) ∧
    -- (6) the stalk of the differentials at the prime vanishes
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) [q.IsPrime],
        Subsingleton (LocalizedModule q.primeCompl Ω[S⁄R]) →
          (FiniteType R S → ∃ g ∉ q, Unramified R (Localization.Away g)) ∧
            (FinitePresentation R S → ∃ g ∉ q, GUnramified R (Localization.Away g))) ∧
    -- (7) the fibre of the differentials at the prime vanishes
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) [q.IsPrime],
        Subsingleton (q.Fiber Ω[S⁄R]) →
          (FiniteType R S → ∃ g ∉ q, Unramified R (Localization.Away g)) ∧
            (FinitePresentation R S → ∃ g ∉ q, GUnramified R (Localization.Away g))) ∧
    -- (8) the stalk of the differentials of the fibre over `𝔭` vanishes
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime]
        (q : Ideal (p.Fiber S)) [q.IsPrime],
        Subsingleton (LocalizedModule q.primeCompl Ω[p.Fiber S⁄p.ResidueField]) →
          (FiniteType R S → ∃ g : S,
              Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
                Unramified R (Localization.Away g)) ∧
            (FinitePresentation R S → ∃ g : S,
              Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
                GUnramified R (Localization.Away g))) ∧
    -- (9) the fibre at `q` of the differentials of the fibre over `𝔭` vanishes
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime]
        (q : Ideal (p.Fiber S)) [q.IsPrime],
        Subsingleton (q.Fiber Ω[p.Fiber S⁄p.ResidueField]) →
          (FiniteType R S → ∃ g : S,
              Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
                Unramified R (Localization.Away g)) ∧
            (FinitePresentation R S → ∃ g : S,
              Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
                GUnramified R (Localization.Away g))) ∧
    -- (10) descent along a cover of `Spec S` by principal opens
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (s : Set S),
        Ideal.span s = ⊤ →
        ((∀ g ∈ s, Unramified R (Localization.Away g)) → Unramified R S) ∧
          ((∀ g ∈ s, GUnramified R (Localization.Away g)) → GUnramified R S)) ∧
    -- (11) unramified at every prime
    (∀ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S],
        ((∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, Unramified R (Localization.Away g)) →
            Unramified R S) ∧
          ((∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, GUnramified R (Localization.Away g)) →
            GUnramified R S)) ∧
    -- (12) a G-unramified map is a base change of one over a finite type `ℤ`-algebra
    (∀ {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S], GUnramified R S →
        ∃ (R₀ : Subring R) (S₀ : Type u) (_ : CommRing S₀) (_ : Algebra R₀ S₀),
          FiniteType ℤ R₀ ∧ GUnramified R₀ S₀ ∧ Nonempty (S ≃ₐ[R] R ⊗[R₀] S₀)) ∧
    -- (13) an unramified map is a quotient of a base change of one over a finite type `ℤ`-algebra
    (∀ {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S], Unramified R S →
        ∃ (R₀ : Subring R) (S₀ : Type u) (_ : CommRing S₀) (_ : Algebra R₀ S₀)
          (f : (R ⊗[R₀] S₀) →ₐ[R] S),
          FiniteType ℤ R₀ ∧ Unramified R₀ S₀ ∧ Function.Surjective f)

Algebra.GUnramified.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1005. The attribute's comment: “Item (1), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties; the unramified version is Mathlib's Algebra.Unramified.baseChange.”. References: EGA IV (17.3.3), “(iii) unramified, affine”; EGA IV (17.1.3), “(iii) unram., affine”; SGA 1 I (3.5), “(iii), affine case”.

The base change of a G-unramified ring map is G-unramified (Stacks 00UV (1)); item (1) of Algebra.unramified_and_gUnramified_properties. This is Algebra.Unramified.baseChange, whose statement is the other half of the item, with finite type replaced by finite presentation.

public theorem Algebra.GUnramified.baseChange (R : Type u) [CommRing R] (A : Type v) [CommRing A]
    [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [GUnramified R A] :
    GUnramified B (B ⊗[R] A)

Algebra.GUnramified.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1018. The attribute's comment: “Item (2), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties; the unramified version is Mathlib's Algebra.Unramified.comp.”. References: EGA IV (17.3.3), “(ii) unramified, affine”; EGA IV (17.1.3), “(ii) unram., affine”; SGA 1 I (3.5), “(ii), affine case”.

The composition of G-unramified ring maps is G-unramified (Stacks 00UV (2)); item (2) of Algebra.unramified_and_gUnramified_properties. This is Algebra.Unramified.comp, whose statement is the other half of the item, with finite type replaced by finite presentation.

public theorem Algebra.GUnramified.comp (R : Type u) [CommRing R] (A : Type v) [CommRing A]
    [Algebra R A] (B : Type w) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [GUnramified R A] [GUnramified A B] : GUnramified R B

Algebra.GUnramified.of_isLocalization_Away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1031. The attribute's comment: “Item (3), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties; the unramified version is Mathlib's Algebra.Unramified.of_isLocalization_Away.”.

A principal localization R → R_r is G-unramified (Stacks 00UV (3)), stated for an arbitrary model A of R_r; item (3) of Algebra.unramified_and_gUnramified_properties. This is Algebra.Unramified.of_isLocalization_Away, whose statement is the other half of the item, with finite type replaced by finite presentation.

public theorem Algebra.GUnramified.of_isLocalization_Away {R : Type u} [CommRing R] {A : Type v}
    [CommRing A] [Algebra R A] (r : R) [IsLocalization.Away r A] : GUnramified R A

Algebra.Unramified.quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1039. The attribute's comment: “Item (4), first sentence, exported from Algebra.unramified_and_gUnramified_properties.”.

A quotient R → R ⧸ I is unramified (Stacks 00UV (4), first sentence); item (4) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.Unramified.quotient {R : Type u} [CommRing R] (I : Ideal R) :
    Unramified R (R ⧸ I)

Algebra.GUnramified.quotient_of_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1047. The attribute's comment: “Item (4), second sentence, exported from Algebra.unramified_and_gUnramified_properties.”.

A quotient R → R ⧸ I by a finitely generated ideal is G-unramified (Stacks 00UV (4), second sentence); item (4) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.GUnramified.quotient_of_fg {R : Type u} [CommRing R] {I : Ideal R}
    (hI : I.FG) : GUnramified R (R ⧸ I)

Algebra.GUnramified.of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1057. The attribute's comment: “Item (5), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties; the unramified version is Mathlib's Algebra.Etale.instUnramified.”.

An étale ring map is G-unramified (Stacks 00UV (5)); item (5) of Algebra.unramified_and_gUnramified_properties. This is Algebra.Etale.instUnramified, whose statement is the other half of the item, with finite type replaced by finite presentation.

public theorem Algebra.GUnramified.of_etale {R : Type u} [CommRing R] {S : Type v} [CommRing S]
    [Algebra R S] [Etale R S] : GUnramified R S

Algebra.exists_unramified_away_of_subsingleton_localizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1066. The attribute's comment: “Item (6), the unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite type ring map whose differentials have vanishing stalk at a prime q is unramified at q (Stacks 00UV (6)): there is a g ∉ q with R → S_g unramified. Item (6) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_unramified_away_of_subsingleton_localizedModule {R : Type u}
    [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [FiniteType R S] (q : Ideal S)
    [q.IsPrime] (hq : Subsingleton (LocalizedModule q.primeCompl Ω[S⁄R])) :
    ∃ g ∉ q, Unramified R (Localization.Away g)

Algebra.exists_gUnramified_away_of_subsingleton_localizedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1077. The attribute's comment: “Item (6), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite presentation ring map whose differentials have vanishing stalk at a prime q is G-unramified at q (Stacks 00UV (6)): there is a g ∉ q with R → S_g G-unramified. Item (6) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_gUnramified_away_of_subsingleton_localizedModule {R : Type u}
    [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [FinitePresentation R S] (q : Ideal S)
    [q.IsPrime] (hq : Subsingleton (LocalizedModule q.primeCompl Ω[S⁄R])) :
    ∃ g ∉ q, GUnramified R (Localization.Away g)

Algebra.exists_unramified_away_of_subsingleton_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1088. The attribute's comment: “Item (7), the unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite type ring map whose differentials have vanishing fibre at a prime q is unramified at q (Stacks 00UV (7)): there is a g ∉ q with R → S_g unramified. Item (7) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_unramified_away_of_subsingleton_fiber {R : Type u} [CommRing R]
    {S : Type v} [CommRing S] [Algebra R S] [FiniteType R S] (q : Ideal S) [q.IsPrime]
    (hq : Subsingleton (q.Fiber Ω[S⁄R])) : ∃ g ∉ q, Unramified R (Localization.Away g)

Algebra.exists_gUnramified_away_of_subsingleton_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1098. The attribute's comment: “Item (7), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite presentation ring map whose differentials have vanishing fibre at a prime q is G-unramified at q (Stacks 00UV (7)): there is a g ∉ q with R → S_g G-unramified. Item (7) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_gUnramified_away_of_subsingleton_fiber {R : Type u} [CommRing R]
    {S : Type v} [CommRing S] [Algebra R S] [FinitePresentation R S] (q : Ideal S) [q.IsPrime]
    (hq : Subsingleton (q.Fiber Ω[S⁄R])) : ∃ g ∉ q, GUnramified R (Localization.Away g)

Algebra.exists_unramified_away_of_subsingleton_localizedModule_of_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1109. The attribute's comment: “Item (8), the unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite type ring map whose fibre over p has differentials with vanishing stalk at a prime q of that fibre is unramified at q (Stacks 00UV (8)): there is a g in S whose image in κ(p) ⊗_R S avoids q and with R → S_g unramified. Item (8) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_unramified_away_of_subsingleton_localizedModule_of_fiber
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [FiniteType R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal (p.Fiber S)) [q.IsPrime]
    (hq : Subsingleton (LocalizedModule q.primeCompl Ω[p.Fiber S⁄p.ResidueField])) :
    ∃ g : S, Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
      Unramified R (Localization.Away g)

Algebra.exists_gUnramified_away_of_subsingleton_localizedModule_of_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1123. The attribute's comment: “Item (8), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite presentation ring map whose fibre over p has differentials with vanishing stalk at a prime q of that fibre is G-unramified at q (Stacks 00UV (8)): there is a g in S whose image in κ(p) ⊗_R S avoids q and with R → S_g G-unramified. Item (8) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_gUnramified_away_of_subsingleton_localizedModule_of_fiber
    {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [FinitePresentation R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal (p.Fiber S)) [q.IsPrime]
    (hq : Subsingleton (LocalizedModule q.primeCompl Ω[p.Fiber S⁄p.ResidueField])) :
    ∃ g : S, Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
      GUnramified R (Localization.Away g)

Algebra.exists_unramified_away_of_subsingleton_fiber_of_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1137. The attribute's comment: “Item (9), the unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite type ring map whose fibre over p has differentials with vanishing fibre at a prime q of that fibre is unramified at q (Stacks 00UV (9)): there is a g in S whose image in κ(p) ⊗_R S avoids q and with R → S_g unramified. Item (9) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_unramified_away_of_subsingleton_fiber_of_fiber {R : Type u}
    [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [FiniteType R S] (p : Ideal R)
    [p.IsPrime] (q : Ideal (p.Fiber S)) [q.IsPrime]
    (hq : Subsingleton (q.Fiber Ω[p.Fiber S⁄p.ResidueField])) :
    ∃ g : S, Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
      Unramified R (Localization.Away g)

Algebra.exists_gUnramified_away_of_subsingleton_fiber_of_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1151. The attribute's comment: “Item (9), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A finite presentation ring map whose fibre over p has differentials with vanishing fibre at a prime q of that fibre is G-unramified at q (Stacks 00UV (9)): there is a g in S whose image in κ(p) ⊗_R S avoids q and with R → S_g G-unramified. Item (9) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.exists_gUnramified_away_of_subsingleton_fiber_of_fiber {R : Type u}
    [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [FinitePresentation R S] (p : Ideal R)
    [p.IsPrime] (q : Ideal (p.Fiber S)) [q.IsPrime]
    (hq : Subsingleton (q.Fiber Ω[p.Fiber S⁄p.ResidueField])) :
    ∃ g : S, Algebra.TensorProduct.includeRight (R := R) (A := p.ResidueField) g ∉ q ∧
      GUnramified R (Localization.Away g)

Algebra.Unramified.of_span_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1164. The attribute's comment: “Item (10), the unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

Being unramified is local on the target: if s ⊆ S generates the unit ideal and R → S_g is unramified for every g ∈ s, then R → S is unramified (Stacks 00UV (10)); item (10) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.Unramified.of_span_eq_top {R : Type u} [CommRing R] {S : Type v}
    [CommRing S] [Algebra R S] {s : Set S} (hs : Ideal.span s = ⊤)
    (H : ∀ g ∈ s, Unramified R (Localization.Away g)) : Unramified R S

Algebra.GUnramified.of_span_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1174. The attribute's comment: “Item (10), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

Being G-unramified is local on the target: if s ⊆ S generates the unit ideal and R → S_g is G-unramified for every g ∈ s, then R → S is G-unramified (Stacks 00UV (10)); item (10) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.GUnramified.of_span_eq_top {R : Type u} [CommRing R] {S : Type v}
    [CommRing S] [Algebra R S] {s : Set S} (hs : Ideal.span s = ⊤)
    (H : ∀ g ∈ s, GUnramified R (Localization.Away g)) : GUnramified R S

Algebra.Unramified.of_forall_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1183. The attribute's comment: “Item (11), the unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A ring map unramified at every prime of the target is unramified (Stacks 00UV (11)); item (11) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.Unramified.of_forall_prime {R : Type u} [CommRing R] {S : Type v}
    [CommRing S] [Algebra R S]
    (H : ∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, Unramified R (Localization.Away g)) :
    Unramified R S

Algebra.GUnramified.of_forall_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1193. The attribute's comment: “Item (11), the G-unramified version, exported from Algebra.unramified_and_gUnramified_properties.”.

A ring map G-unramified at every prime of the target is G-unramified (Stacks 00UV (11)); item (11) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.GUnramified.of_forall_prime {R : Type u} [CommRing R] {S : Type v}
    [CommRing S] [Algebra R S]
    (H : ∀ (q : Ideal S) [q.IsPrime], ∃ g ∉ q, GUnramified R (Localization.Away g)) :
    GUnramified R S

Algebra.GUnramified.exists_finiteType_int_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1204. The attribute's comment: “Item (12), exported from Algebra.unramified_and_gUnramified_properties.”.

A G-unramified ring map is a base change of a G-unramified map over a finite type ℤ-algebra (Stacks 00UV (12)): there are a subring R₀ ⊆ R of finite type over ℤ and a G-unramified R₀-algebra S₀ with S ≃ R ⊗_{R₀} S₀ as R-algebras. Item (12) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.GUnramified.exists_finiteType_int_baseChange {R : Type u} [CommRing R]
    {S : Type v} [CommRing S] [Algebra R S] [GUnramified R S] :
    ∃ (R₀ : Subring R) (S₀ : Type u) (_ : CommRing S₀) (_ : Algebra R₀ S₀),
      FiniteType ℤ R₀ ∧ GUnramified R₀ S₀ ∧ Nonempty (S ≃ₐ[R] R ⊗[R₀] S₀)

Algebra.Unramified.exists_finiteType_int_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Properties.lean, line 1215. The attribute's comment: “Item (13), exported from Algebra.unramified_and_gUnramified_properties.”.

An unramified ring map is a quotient of a base change of an unramified map over a finite type ℤ-algebra (Stacks 00UV (13)): there are a subring R₀ ⊆ R of finite type over ℤ and an unramified R₀-algebra S₀ with a surjection R ⊗_{R₀} S₀ → S of R-algebras. Item (13) of Algebra.unramified_and_gUnramified_properties.

public theorem Algebra.Unramified.exists_finiteType_int_surjective {R : Type u} [CommRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Unramified R S] :
    ∃ (R₀ : Subring R) (S₀ : Type u) (_ : CommRing S₀) (_ : Algebra R₀ S₀)
      (f : (R ⊗[R₀] S₀) →ₐ[R] S),
      FiniteType ℤ R₀ ∧ Unramified R₀ S₀ ∧ Function.Surjective f
Tag 02FL, a lemma

Tag 02FL in the Stacks Project.

exists_isIdempotentElem_isLocalization_away_of_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/LocalStructure.lean, line 850.

Stacks Tag 02FL. If R → S is unramified, then there is an idempotent e ∈ S ⊗[R] S such that the multiplication map μ : S ⊗[R] S → S exhibits S as the localization of A := S ⊗[R] S away from e. Equivalently (the standard reading of "isomorphic as objects under A"), the localization map A → A_e is isomorphic to μ under A.

Here the (S ⊗[R] S)-algebra structure on S is the one induced by the multiplication map μ = Algebra.TensorProduct.lmul' R.

theorem exists_isIdempotentElem_isLocalization_away_of_unramified (R S : Type*) [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.Unramified R S] :
    ∃ e : S ⊗[R] S, IsIdempotentElem e ∧
      letI : Algebra (S ⊗[R] S) S := (Algebra.TensorProduct.lmul' R).toRingHom.toAlgebra
      IsLocalization.Away e S
Tag 02UR, a lemma

Tag 02UR in the Stacks Project.

Algebra.isOpen_singleton_fiber_of_isUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/QuasiFinite.lean, line 195. The attribute's comment: “Unramified at q is Algebra.IsUnramifiedAt R q (Definition 00UT (3), via Algebra.exists_unramified_of_isUnramifiedAt). Quasi-finite at q is Definition 00PL, the equivalent conditions of Lemma 00PK, and the conclusion is condition (1), q isolated in its fibre; condition (2), Algebra.QuasiFiniteAt R q, is instead Mathlib's instance Algebra.IsUnramifiedAt.instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified, which holds under weaker hypotheses than the source's. The second sentence needs no declaration: Algebra.QuasiFinite R S for [Algebra.Unramified R S] is inferInstance. See the module docstring.”. References: EGA IV (17.4.3), “affine case”; EGA IV (17.4.1.2), “quasi-finite (ring case)”.

Stacks 02UR. Let S be an R-algebra of finite type and let q be a prime of S. If R → S is unramified at q then it is quasi-finite at q: the point q is isolated in the fibre of Spec S → Spec R through it. In particular an unramified ring map is quasi-finite: for [Algebra.Unramified R S], Algebra.QuasiFinite R S is found by instance resolution.

public theorem Algebra.isOpen_singleton_fiber_of_isUnramifiedAt {R S : Type*} [CommRing R]
    [CommRing S] [Algebra R S] [Algebra.FiniteType R S] (q : PrimeSpectrum S)
    [Algebra.IsUnramifiedAt R q.asIdeal] :
    IsOpen (X := PrimeSpectrum.comap (algebraMap R S) ⁻¹' {q.comap (algebraMap R S)}) {⟨q, rfl⟩}
Tag 02FM, a lemma

Tag 02FM in the Stacks Project.

Algebra.map_eq_maximalIdeal_localizationAtPrime_of_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/EtaleMapMaximalIdeal.lean, line 55. The attribute's comment: “The displayed equality m_{p'} = p R'_{p'}, for R → R' formally unramified and essentially of finite type rather than étale.”. References: EGA IV (18.6.1), “more general”.

The maximal ideal of a local ring of an unramified algebra is generated by the base. If R → R' is essentially of finite type and formally unramified and p' is a prime of R' lying over a prime p of R, then the ideal generated by p in R'_{p'} is the maximal ideal of R'_{p'}.

theorem Algebra.map_eq_maximalIdeal_localizationAtPrime_of_formallyUnramified
    {R R' : Type u} [CommRing R] [CommRing R'] [Algebra R R']
    [Algebra.EssFiniteType R R'] [Algebra.FormallyUnramified R R']
    (p : Ideal R) [p.IsPrime] (p' : Ideal R') [p'.IsPrime] [p'.LiesOver p] :
    Ideal.map (algebraMap R (Localization.AtPrime p')) p
      = IsLocalRing.maximalIdeal (Localization.AtPrime p')
Tag 08WD, a lemma

Tag 08WD in the Stacks Project.

Algebra.Etale.tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/Basic.lean, line 259. The attribute's comment: “The three items are the entries, in the source's order, of one List.TFAE. Étale is Mathlib's Algebra.Etale, formally étale plus finite presentation, which is the source's Definition 00U1 by its Lemma 00UR; flat is Module.Flat R S; G-unramified and unramified are Algebra.GUnramified and Algebra.Unramified (Definition 00UT). See the module docstring.”.

Stacks 08WD. Let R → S be a ring map. The following are equivalent:

  1. R → S is étale;
  2. R → S is flat and G-unramified;
  3. R → S is flat, unramified, and of finite presentation.
public theorem Algebra.Etale.tfae (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] :
    List.TFAE
      [Algebra.Etale R S,
       Module.Flat R S ∧ Algebra.GUnramified R S,
       Module.Flat R S ∧ Algebra.Unramified R S ∧ Algebra.FinitePresentation R S]
Tag 0G1C, a lemma

Tag 0G1C in the Stacks Project.

MvPolynomial.etale_aeval_iff_height_eq_and_span_range_D_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/MvPolynomialCriterion.lean, line 366. References: SGA 1 II (5.1), “(i) ⟺ (iii)”.

Stacks 0G1C. Let k be a field, let A be a k-algebra of finite type and let a₁, …, aₙ ∈ A. The k-algebra map φ : k[x₁, …, xₙ] → A, xᵢ ↦ aᵢ, is étale if and only if (a) every maximal ideal of A has height n, equivalently the local rings of A at maximal ideals have dimension n, and (b) the differentials d(a₁), …, d(aₙ) generate Ω[A⁄k] as an A-module.

public theorem MvPolynomial.etale_aeval_iff_height_eq_and_span_range_D_eq_top
    {n : ℕ} (k A : Type*) [Field k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A]
    (a : Fin n → A) :
    (aeval a : MvPolynomial (Fin n) k →ₐ[k] A).toRingHom.Etale ↔
      (∀ m : Ideal A, m.IsMaximal → Ideal.height m = n) ∧
      Submodule.span A (Set.range fun i ↦ KaehlerDifferential.D k A (a i)) = ⊤
Sources
LeanAlgebra.GUnramified · Algebra.unramified_iff_and_gUnramified_iff · Algebra.unramified_and_gUnramified_properties · Algebra.GUnramified.baseChange · Algebra.GUnramified.comp · Algebra.GUnramified.of_isLocalization_Away · Algebra.Unramified.quotient · Algebra.GUnramified.quotient_of_fg

Section10.152 Local structure of unramified ring maps#

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

Tag 0395, a proposition

Tag 0395 in the Stacks Project.

Algebra.exists_hasStandardEtaleSurjectionOn_of_exists_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/LocalStructure.lean, line 257. The attribute's comment: “The conclusion's three items are Mathlib's HasStandardEtaleSurjectionOn R g, namely ∃ (P : StandardEtalePair R) (φ : P.Ring →ₐ[R] Localization.Away g), Surjective φ. The hypothesis "unramified at q" is Definition 00UT (3) verbatim, ∃ g ∉ Q, Algebra.Unramified R (Localization.Away g), rather than Mathlib's hypothesis pair [Algebra.FiniteType R S] [Algebra.IsUnramifiedAt R Q], which implies it but is not implied by it; so this is strictly more general than Mathlib's Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn and implies it. See the module docstring.”.

Stacks 0395. Let R → S be a ring map and q ⊂ S a prime. If R → S is unramified at q — that is, if R → S_g is unramified for some g ∈ S, g ∉ q — then there are a g ∈ S, g ∉ q, a standard étale ring map R → S' and a surjective R-algebra map S' → S_g.

public theorem Algebra.exists_hasStandardEtaleSurjectionOn_of_exists_unramified {R : Type u}
    {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (Q : Ideal S) [Q.IsPrime]
    (hQ : ∃ g ∉ Q, Algebra.Unramified R (Localization.Away g)) :
    ∃ g ∉ Q, HasStandardEtaleSurjectionOn R g
Tag 00UX, a lemma

Tag 00UX in the Stacks Project.

Algebra.exists_etale_isIdempotentElem_surjective_of_isUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/EtaleLocalStructure.lean, line 264. The attribute's comment: “The product decomposition R' ⊗_R S = A × B is given by an idempotent e, with A = (R' ⊗[R] S)[1/e], as in Mathlib's Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq (Tag 00UJ); p'A lying over q is read along S → R' ⊗[R] S → A. See the module docstring.”.

Étale local structure of a ring map unramified at a prime. Let S be a finite type R-algebra and let q be a prime of S lying over the prime p of R at which S is unramified over R. There are an étale R-algebra R', a prime p' of R' lying over p and an idempotent e of R' ⊗[R] S — the product decomposition R' ⊗[R] S = A × B with A = (R' ⊗[R] S)[1/e] and B = (R' ⊗[R] S)[1/(1 - e)] — such that R' → A is surjective and p'A is a prime of A lying over p' and, along S → R' ⊗[R] S → A, over q.

public theorem Algebra.exists_etale_isIdempotentElem_surjective_of_isUnramifiedAt
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    [Algebra.IsUnramifiedAt R q] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R')
      (p' : Ideal R') (_ : p'.IsPrime) (_ : p'.LiesOver p) (e : R' ⊗[R] S)
      (_ : IsIdempotentElem e),
      Function.Surjective (algebraMap R' (Localization.Away e)) ∧
      (p'.map (algebraMap R' (Localization.Away e))).IsPrime ∧
      (p'.map (algebraMap R' (Localization.Away e))).LiesOver p' ∧
      (p'.map (algebraMap R' (Localization.Away e))).comap
        ((algebraMap (R' ⊗[R] S) (Localization.Away e)).comp
          (Algebra.TensorProduct.includeRight : S →ₐ[R] R' ⊗[R] S).toRingHom) = q
Tag 00UY, a lemma

Tag 00UY in the Stacks Project.

Algebra.exists_etale_completeOrthogonalIdempotents_surjective_not_liesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/LocalStructure.lean, line 771. The attribute's comment: “The product decomposition is given by complete orthogonal idempotents e : Fin (n + 1) → R' ⊗[R] S, the factors being (R' ⊗[R] S)[1/e i]. The prime of Aᵢ lying over p' is named as the source names it, namely p'Aᵢ. See the module docstring.”.

Separating the points of a fibre of an unramified ring map (Stacks 00UY). Let S be an unramified R-algebra and p a prime of R. There are an étale R-algebra R', a prime p' of R' lying over p, and a decomposition R' ⊗[R] S = A₁ × ⋯ × Aₙ × B — given by complete orthogonal idempotents e 0, …, e n, with Aᵢ = (R' ⊗[R] S)[1/e i] and B = (R' ⊗[R] S)[1/e n] — such that each R' → Aᵢ is surjective, each p'Aᵢ is a prime of Aᵢ lying over p', and no prime of B lies over p'.

public theorem Algebra.exists_etale_completeOrthogonalIdempotents_surjective_not_liesOver
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Algebra.Unramified R S]
    (p : Ideal R) [p.IsPrime] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R') (p' : Ideal R')
      (_ : p'.IsPrime) (_ : p'.LiesOver p) (n : ℕ) (e : Fin (n + 1) → R' ⊗[R] S)
      (_ : CompleteOrthogonalIdempotents e),
      (∀ i : Fin n, Function.Surjective (algebraMap R' (Localization.Away (e i.castSucc)))) ∧
      (∀ i : Fin n, (p'.map (algebraMap R' (Localization.Away (e i.castSucc)))).IsPrime) ∧
      (∀ i : Fin n, (p'.map (algebraMap R' (Localization.Away (e i.castSucc)))).LiesOver p') ∧
      ∀ q : Ideal (Localization.Away (e (Fin.last n))), q.IsPrime → ¬ q.LiesOver p'
Sources
LeanAlgebra.exists_hasStandardEtaleSurjectionOn_of_exists_unramified · Algebra.exists_etale_isIdempotentElem_surjective_of_isUnramifiedAt · Algebra.exists_etale_completeOrthogonalIdempotents_surjective_not_liesOver

Section10.153 Henselian local rings#

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

Tag 04GF, a definition

Tag 04GF in the Stacks Project.

normal_local_domain_sepClosed_fractionField_isStrictlyHenselian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Criteria.lean, line 326. References: SGA 7 I (0.0.3), “partial”.

Stacks Tag 04GF. Let R be a normal local domain (a local integral domain that is integrally closed in its fraction field K). If K is separably algebraically closed, then R is strictly henselian, i.e. R is a henselian local ring and its residue field is separably algebraically closed.

theorem normal_local_domain_sepClosed_fractionField_isStrictlyHenselian
    (R : Type*) [CommRing R] [IsLocalRing R] [IsDomain R] [IsIntegrallyClosed R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K] [IsSepClosed K] :
    HenselianLocalRing R ∧ IsSepClosed (IsLocalRing.ResidueField R)
Tag 06RR, a lemma

Tag 06RR in the Stacks Project.

hensel_uniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Criteria.lean, line 368. References: SGA 3 VIIB (1.6), “partial”.

Hensel uniqueness: in a local ring, two roots of a polynomial that are congruent modulo the maximal ideal must be equal, provided the formal derivative at one of them is not in the maximal ideal.

theorem hensel_uniqueness {R : Type*} [CommRing R] [IsLocalRing R]
    (f : Polynomial R) (a b : R)
    (hfa : f.eval a = 0) (hfb : f.eval b = 0)
    (hab : a - b ∈ IsLocalRing.maximalIdeal R)
    (hf' : (Polynomial.derivative f).eval a ∉ IsLocalRing.maximalIdeal R) :
    a = b
Tag 04GG, a lemma

Tag 04GG in the Stacks Project.

HenselianLocalRing.TFAE_factorization_etale_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/TFAE/Factorization.lean, line 664. The attribute's comment: “The thirteen items are the entries, in the source's order, of one List.TFAE. f̄ is Polynomial.map (IsLocalRing.residue R) f, gcd(g₀, h₀) = 1 is IsCoprime, degrees are Polynomial.degree and item (6) carries the source's tacit g₀ ≠ 0, without which it holds only for fields. A retraction is an element of S →ₐ[R] R, κ = κ(q) is bijectivity of the canonical Ideal.ResidueField.mapₐ. A product of local rings is a RingEquiv onto a Pi type; the two-factor decompositions of (11)–(13) are AlgEquivs. The source's quasi-finite of Definition 00PM is Algebra.FiniteType together with Mathlib's weaker Algebra.QuasiFinite. See the module docstring.”. References: EGA IV (18.5.13), “a'') existence half”; EGA IV (18.5.9), “(ii)”; EGA IV (18.5.11), “a), a'), b)”; SGA 4 VIII (4.1), “(i)–(iv)”.

Characterisations of henselian local rings (Stacks 04GG). For a local ring (R, 𝔪, κ) the following are equivalent: (1) R is henselian; (2) every f ∈ R[T] and every root a₀ ∈ κ of f̄ with f̄'(a₀) ≠ 0 come from a root a ∈ R of f with ā = a₀; (3) every coprime factorisation f̄ = g₀h₀ of the reduction of a monic f ∈ R[T] lifts to f = gh in R[T]; (4) the same with deg g = deg g₀; (5), (6) the same two statements for arbitrary f ∈ R[T], (6) under the source's tacit g₀ ≠ 0; (7) every étale R-algebra S with a prime q over 𝔪 such that κ = κ(q) admits a retraction S → R; (8) it admits a unique retraction τ with τ⁻¹(𝔪) = q; (9) every finite R-algebra is a product of local rings; (10) a finite product of local rings; (11) every finite type R-algebra is A × B with A finite over R and B quasi-finite over R at no prime over 𝔪; (12) the same with each irreducible component of Spec(κ ⊗_R B) of dimension ≥ 1; (13) every quasi-finite R-algebra is A × B with A finite over R and κ ⊗_R B = 0.

public theorem HenselianLocalRing.TFAE_factorization_etale_quasiFinite
    (R : Type u) [CommRing R] [IsLocalRing R] :
    List.TFAE
      [HenselianLocalRing R,
       ∀ f : R[X], ∀ a₀ : ResidueField R, aeval a₀ f = 0 → aeval a₀ (derivative f) ≠ 0 →
         ∃ a : R, f.IsRoot a ∧ residue R a = a₀,
       ∀ f : R[X], f.Monic → ∀ g₀ h₀ : (ResidueField R)[X], f.map (residue R) = g₀ * h₀ →
         IsCoprime g₀ h₀ →
         ∃ g h : R[X], f = g * h ∧ g.map (residue R) = g₀ ∧ h.map (residue R) = h₀,
       ∀ f : R[X], f.Monic → ∀ g₀ h₀ : (ResidueField R)[X], f.map (residue R) = g₀ * h₀ →
         IsCoprime g₀ h₀ →
         ∃ g h : R[X], f = g * h ∧ g.map (residue R) = g₀ ∧ h.map (residue R) = h₀ ∧
           g.degree = g₀.degree,
       ∀ f : R[X], ∀ g₀ h₀ : (ResidueField R)[X], f.map (residue R) = g₀ * h₀ →
         IsCoprime g₀ h₀ →
         ∃ g h : R[X], f = g * h ∧ g.map (residue R) = g₀ ∧ h.map (residue R) = h₀,
       ∀ f : R[X], ∀ g₀ h₀ : (ResidueField R)[X], g₀ ≠ 0 → f.map (residue R) = g₀ * h₀ →
         IsCoprime g₀ h₀ →
         ∃ g h : R[X], f = g * h ∧ g.map (residue R) = g₀ ∧ h.map (residue R) = h₀ ∧
           g.degree = g₀.degree,
       ∀ (S : Type u) [CommRing S] [Algebra R S], Algebra.Etale R S →
         ∀ q : Ideal S, ∀ [q.IsPrime] [q.LiesOver (maximalIdeal R)],
         Function.Bijective (Ideal.ResidueField.mapₐ (maximalIdeal R) q (Algebra.ofId R S)
           (q.over_def _)) → Nonempty (S →ₐ[R] R),
       ∀ (S : Type u) [CommRing S] [Algebra R S], Algebra.Etale R S →
         ∀ q : Ideal S, ∀ [q.IsPrime] [q.LiesOver (maximalIdeal R)],
         Function.Bijective (Ideal.ResidueField.mapₐ (maximalIdeal R) q (Algebra.ofId R S)
           (q.over_def _)) → ∃! τ : S →ₐ[R] R, (maximalIdeal R).comap (τ : S →+* R) = q,
       ∀ (S : Type u) [CommRing S] [Algebra R S], Module.Finite R S →
         ∃ (ι : Type u) (A : ι → Type u) (_ : ∀ i, CommRing (A i)) (_ : ∀ i, IsLocalRing (A i)),
           Nonempty (S ≃+* ∀ i, A i),
       ∀ (S : Type u) [CommRing S] [Algebra R S], Module.Finite R S →
         ∃ (ι : Type u) (_ : Finite ι) (A : ι → Type u) (_ : ∀ i, CommRing (A i))
           (_ : ∀ i, IsLocalRing (A i)), Nonempty (S ≃+* ∀ i, A i),
       ∀ (S : Type u) [CommRing S] [Algebra R S], Algebra.FiniteType R S →
         ∃ (A B : Type u) (_ : CommRing A) (_ : CommRing B) (_ : Algebra R A) (_ : Algebra R B)
           (_ : S ≃ₐ[R] A × B), Module.Finite R A ∧
           ∀ q : Ideal B, ∀ [q.IsPrime], q.LiesOver (maximalIdeal R) →
             ¬ Algebra.QuasiFiniteAt R q,
       ∀ (S : Type u) [CommRing S] [Algebra R S], Algebra.FiniteType R S →
         ∃ (A B : Type u) (_ : CommRing A) (_ : CommRing B) (_ : Algebra R A) (_ : Algebra R B)
           (_ : S ≃ₐ[R] A × B), Module.Finite R A ∧
           ∀ p ∈ minimalPrimes (ResidueField R ⊗[R] B),
             1 ≤ ringKrullDim ((ResidueField R ⊗[R] B) ⧸ p),
       ∀ (S : Type u) [CommRing S] [Algebra R S], Algebra.FiniteType R S →
         Algebra.QuasiFinite R S →
         ∃ (A B : Type u) (_ : CommRing A) (_ : CommRing B) (_ : Algebra R A) (_ : Algebra R B)
           (_ : S ≃ₐ[R] A × B), Module.Finite R A ∧
           Subsingleton (ResidueField R ⊗[R] B)]
Tag 04GH, a lemma

Tag 04GH in the Stacks Project.

HenselianLocalRing.henselianLocalRing_and_finite_of_finite_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/QuasiFinite.lean, line 783. The attribute's comment: “The four items are the four conjuncts, in the source's order. A finite product of local rings is an AlgEquiv onto a Pi type over a Finite index type (04GG (10)'s spelling, upgraded from RingEquiv because the factors are required finite over R); S_q is any IsLocalization.AtPrime Sq q in a scalar tower over R; the source's quasi-finiteness at q is Algebra.QuasiFiniteAt R q and its quasi-finite ring map is Algebra.FiniteType together with Mathlib's weaker Algebra.QuasiFinite. Item (4) is item (3) with q quantified. See the module docstring.”. References: EGA IV (18.5.9), “(ii) necessity”; EGA IV (18.5.10), “R henselian local”; SGA 4 VIII (4.1), “partial”.

Finite and quasi-finite algebras over a henselian local ring (Stacks 04GH). Let (R, 𝔪, κ) be a henselian local ring. (1) A finite R-algebra S is a finite product of henselian local rings each finite over R. (2) If moreover S is local, then S is henselian and R → S is a local homomorphism. (3) If S is of finite type over R and q is a prime of S lying over 𝔪 at which R → S is quasi-finite, then S_q is henselian and finite over R. (4) If R → S is quasi-finite, this holds at every prime q of S lying over 𝔪.

public theorem HenselianLocalRing.henselianLocalRing_and_finite_of_finite_of_quasiFiniteAt
    (R : Type u) [CommRing R] [HenselianLocalRing R] :
    (∀ (S : Type v) [CommRing S] [Algebra R S], Module.Finite R S →
        ∃ (ι : Type (max u v)) (_ : Finite ι) (A : ι → Type (max u v))
          (_ : ∀ i, CommRing (A i))
          (_ : ∀ i, Algebra R (A i)) (_ : ∀ i, HenselianLocalRing (A i)),
          (∀ i, Module.Finite R (A i)) ∧ Nonempty (S ≃ₐ[R] ∀ i, A i)) ∧
      (∀ (S : Type v) [CommRing S] [Algebra R S] [IsLocalRing S], Module.Finite R S →
        HenselianLocalRing S ∧ IsLocalHom (algebraMap R S)) ∧
      (∀ (S : Type v) [CommRing S] [Algebra R S], Algebra.FiniteType R S →
        ∀ q : Ideal S, ∀ [q.IsPrime] [q.LiesOver (maximalIdeal R)], Algebra.QuasiFiniteAt R q →
        ∀ (Sq : Type w) [CommRing Sq] [Algebra R Sq] [Algebra S Sq] [IsScalarTower R S Sq]
          [IsLocalization.AtPrime Sq q], HenselianLocalRing Sq ∧ Module.Finite R Sq) ∧
      (∀ (S : Type v) [CommRing S] [Algebra R S], Algebra.FiniteType R S →
        Algebra.QuasiFinite R S →
        ∀ q : Ideal S, ∀ [q.IsPrime] [q.LiesOver (maximalIdeal R)],
        ∀ (Sq : Type w) [CommRing Sq] [Algebra R Sq] [Algebra S Sq] [IsScalarTower R S Sq]
          [IsLocalization.AtPrime Sq q], HenselianLocalRing Sq ∧ Module.Finite R Sq)
Tag 04GJ, a lemma

Tag 04GJ in the Stacks Project.

exists_algEquiv_prod_of_henselianLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/FiniteType/Basic/ProductOfLocalRings.lean, line 611. References: EGA IV (18.5.9), “more general”; SGA 4 VIII (4.1), “(ii)”.

Stacks Tag 04GJ (Lemma 10.153.5). A finite type algebra over a henselian local ring decomposes, up to R-algebra isomorphism, as a finite product of local algebras finite over R, times an algebra B that is not quasi-finite at any prime lying over the maximal ideal of R.

theorem exists_algEquiv_prod_of_henselianLocalRing (R : Type u) [CommRing R] [HenselianLocalRing R]
    (S : Type v) [CommRing S] [Algebra R S] [Algebra.FiniteType R S] :
    ∃ (n : ℕ) (A : Fin n → Type (max u v)) (_ : ∀ i, CommRing (A i))
      (_ : ∀ i, Algebra R (A i)),
      (∀ i, IsLocalRing (A i)) ∧ (∀ i, Module.Finite R (A i)) ∧
      ∃ (B : Type (max u v)) (_ : CommRing B) (_ : Algebra R B),
        (∀ (𝔮 : Ideal B) [𝔮.IsPrime], 𝔮.LiesOver (IsLocalRing.maximalIdeal R) →
          ¬ Algebra.QuasiFiniteAt R 𝔮) ∧
        Nonempty (S ≃ₐ[R] (∀ i, A i) × B)
Tag 06DD, a lemma

Tag 06DD in the Stacks Project.

exists_prod_local_purelyInseparable_not_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/FiniteType/StrictlyHenselian/ProductDecomposition.lean, line 765.

Let (R, m, κ) be a strictly henselian local ring (a henselian local ring whose residue field is separably closed) and let S be a finite type R-algebra. Then S decomposes as an R-algebra isomorphism S ≃ₐ[R] (∏ i, A i) × B, where: * each A i is a local ring, finite over R, with R → A i a local homomorphism; * for each i, the induced residue field extension κ → κ(m_{A i}) is finite and purely inseparable; * R → B is not quasi-finite at any prime of B lying over m.

theorem exists_prod_local_purelyInseparable_not_quasiFiniteAt (R : Type) [CommRing R]
    [HenselianLocalRing R] [IsSepClosed (ResidueField R)]
    (S : Type) [CommRing S] [Algebra R S] [Algebra.FiniteType R S] :
    ∃ (n : ℕ) (A : Fin n → Type) (_ : ∀ i, CommRing (A i)) (_ : ∀ i, Algebra R (A i)) (_ :
      ∀ i, IsLocalRing (A i)) (_ : ∀ i, IsLocalHom (algebraMap R (A i))) (B : Type) (_ :
      CommRing B) (_ : Algebra R B),
      -- the `R`-algebra decomposition `S ≅ (∏ i, A i) × B`
      Nonempty (S ≃ₐ[R] ((Π i, A i) × B)) ∧
        -- (1) each `A i` is finite over `R` (locality and local-hom are recorded
        --     by the instance binders above)
        (∀ i, Module.Finite R (A i)) ∧
          -- (2) each residue extension `κ → κ(m_{A i})` is purely inseparable and
          --     finite, where the `κ`-algebra structure on `κ(m_{A i})` comes from
          --     the residue field map of the local homomorphism `R → A i`
          (∀ i,
              letI : Algebra (ResidueField R) (ResidueField (A i)) :=
                (ResidueField.map (algebraMap R (A i))).toAlgebra
              IsPurelyInseparable (ResidueField R) (ResidueField (A i)) ∧
                Module.Finite (ResidueField R) (ResidueField (A i))) ∧
            -- (3) `R → B` is not quasi-finite at any prime of `B` lying over `m`
            (∀ (q : Ideal B) (hq : q.IsPrime),
              q.LiesOver (maximalIdeal R) → ¬@Algebra.QuasiFiniteAt R B _ _ _ q hq)
Tag 04GK, a lemma

Tag 04GK in the Stacks Project.

CommAlgCat.FiniteEtale.isEquivalence_baseChange_residueField, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/FiniteEtale.lean, line 793. The attribute's comment: “The functor S ↦ S/𝔪S of the source is Mathlib's base change functor CommAlgCat.FiniteEtale.baseChange R (IsLocalRing.ResidueField R), S ↦ κ ⊗[R] S; the canonical identification of the two is Algebra.TensorProduct.quotIdealMapEquivQuotTensor. Equivalent via the functor is CategoryTheory.Functor.IsEquivalence of that functor, stated as an instance as Mathlib states the sibling FiniteEtale.fiber Ω Ω. The object universe is pinned to R's, as in Mathlib's CommAlgCat.FiniteEtale.equivOfIsSepClosed. See the module docstring.”. References: EGA IV (18.3.2), “local, I = maximal ideal”; EGA IV (18.5.15), “henselian local ring”; SGA 1 IX (1.8), “more general”; SGA 7 XIII (1.2.1), “the equivalence”; SGA 1 IX (1.8), “more general”; SGA 3 VIIB (1.6.E), “(b), special case”; SGA 7 IX (2.2.4), “more general”.

Stacks 04GK. Let (R, 𝔪, κ) be a henselian local ring. Base change along the residue map R → κ, which on objects is S ↦ κ ⊗[R] S ≅ S/𝔪S, is an equivalence from the category of finite étale R-algebras to the category of finite étale κ-algebras.

public instance CommAlgCat.FiniteEtale.isEquivalence_baseChange_residueField (R : Type u)
    [CommRing R] [HenselianLocalRing R] :
    (CommAlgCat.FiniteEtale.baseChange.{u, u, u} R (ResidueField R)).IsEquivalence
Tag 04GL, a lemma

Tag 04GL in the Stacks Project.

Algebra.IsUnramifiedIn.exists_algEquiv_prod_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Unramified.lean, line 359. The attribute's comment: “The source's factors Aᵢ with R → Aᵢ surjective are spelled as the quotients R ⧸ Iᵢ with their canonical maps (Ideal.quotientKerAlgEquivOfSurjective identifies the two forms), and Iᵢ ≠ ⊤ records that the factor is nonzero, the source's locality of Aᵢ then being automatic. Strictly henselian is HenselianLocalRing R with IsSepClosed (ResidueField R). The hypothesis is weakened from Algebra.Unramified R S to finite type together with Algebra.IsUnramifiedIn S 𝔪, which is what the proof uses; the source's hypothesis implies it by Algebra.unramified_iff_forall. See the module docstring.”.

Unramified algebras over a strictly henselian local ring (Stacks 04GL). Let (R, 𝔪, κ) be a strictly henselian local ring and let S be a finite type R-algebra which is unramified at every prime lying over 𝔪 — for instance an unramified R-algebra. Then there are finitely many proper ideals I₁, …, Iₙ of R and an R-algebra B no prime of which lies over 𝔪, together with an isomorphism of R-algebras S ≅ (R/I₁) × ⋯ × (R/Iₙ) × B.

public theorem Algebra.IsUnramifiedIn.exists_algEquiv_prod_quotient
    (R : Type u) [CommRing R] [HenselianLocalRing R] [IsSepClosed (ResidueField R)]
    (S : Type v) [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (hS : Algebra.IsUnramifiedIn S (maximalIdeal R)) :
    ∃ (n : ℕ) (I : Fin n → Ideal R) (B : Type (max u v)) (_ : CommRing B) (_ : Algebra R B),
      Nonempty (S ≃ₐ[R] (∀ i, R ⧸ I i) × B) ∧ (∀ i, I i ≠ ⊤) ∧
        ∀ q : Ideal B, q.IsPrime → ¬ q.LiesOver (maximalIdeal R)
Tag 04GM, a lemma

Tag 04GM in the Stacks Project.

henselianLocalRing_of_isAdicComplete_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Criteria.lean, line 342. References: EGA IV (18.5.14), “local case”; EGA IV (18.5.16), “special case”; SGA 3 X (4.0), “partial”.

A complete local ring is Henselian: IsAdicComplete.henselianRing provides the lifting property, and we transport the simple-root hypothesis along Ideal.Quotient.mk.

theorem henselianLocalRing_of_isAdicComplete_maximalIdeal
    (R : Type*) [CommRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R] :
    HenselianLocalRing R
Tag 06RS, a lemma

Tag 06RS in the Stacks Project.

henselianLocalRing_of_krullDimLE_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Criteria.lean, line 590.

Stacks Tag 06RS / Lemma 10.153.10. A local ring of Krull dimension 0 is henselian.

theorem henselianLocalRing_of_krullDimLE_zero (R : Type*) [CommRing R] [IsLocalRing R]
  [Ring.KrullDimLE 0 R] :
    HenselianLocalRing R
Tag 08HQ, a lemma

Tag 08HQ in the Stacks Project.

existsUnique_algHom_henselian_of_residue_datum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/EtaleLifting/HenselianRetraction.lean, line 761.

Stacks Tag 08HQ (map into henselian). Let R → S be a ring map with S henselian local, p = R ∩ m_S the contraction of the maximal ideal. Given an etale R-algebra A, a prime q of A lying over p, and a κ(p)-algebra map τ : κ(q) → κ(m_S), there is a unique R-algebra map f : A → S with q = f⁻¹(m_S) inducing τ on residue fields.

theorem existsUnique_algHom_henselian_of_residue_datum
    (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [HenselianLocalRing S]
    (A : Type*) [CommRing A] [Algebra R A] [Algebra.Etale R A]
    -- `q` is a prime of `A` lying over `p = R ∩ m_S`.
    (𝔮 : Ideal A) [𝔮.IsPrime]
    (hlo : 𝔮.comap (algebraMap R A) = (maximalIdeal S).comap (algebraMap R S))
    -- `τ : κ(q) → κ(m_S)` is a `κ(p)`-algebra map: the triangle over `κ(p)` commutes.
    (τ : 𝔮.ResidueField →+* (maximalIdeal S).ResidueField)
    (hτ : τ.comp (Ideal.ResidueField.map _ 𝔮 (algebraMap R A) hlo.symm)
        = Ideal.ResidueField.map _ (maximalIdeal S) (algebraMap R S) rfl) :
    -- There is a unique `R`-algebra map `f : A → S` with `q = f⁻¹(m_S)` inducing `τ`.
    ∃! f : A →ₐ[R] S,
      ∃ (h : (maximalIdeal S).comap f.toRingHom = 𝔮),
        Ideal.ResidueField.map 𝔮 (maximalIdeal S) f.toRingHom h.symm = τ
Tag 04GX, a lemma

Tag 04GX in the Stacks Project.

bijOn_solutions_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/EtaleLifting/SolutionsBijection.lean, line 478.

Stacks Tag 04GX. Let φ : R → S be a local homomorphism of strictly henselian local rings and let P_1, …, P_n ∈ R[x_1, …, x_n] be polynomials such that R[x_1, …, x_n]/(P_1, …, P_n) is étale over R. Then the coordinatewise map r ↦ (fun i => φ (r i)) induces a bijection between the solutions of the P_i over R and the solutions of their images P_i^φ over S.

theorem bijOn_solutions_of_etale
    {R S : Type*} [CommRing R] [CommRing S]
    [HenselianLocalRing R] [HenselianLocalRing S]
    [IsSepClosed (IsLocalRing.ResidueField R)] [IsSepClosed (IsLocalRing.ResidueField S)]
    (φ : R →+* S) (hφ : IsLocalHom φ)
    (n : ℕ) (P : Fin n → MvPolynomial (Fin n) R)
    [Algebra.Etale R (MvPolynomial (Fin n) R ⧸ Ideal.span (Set.range P))] :
    Set.BijOn (fun r : Fin n → R => (fun i => φ (r i) : Fin n → S))
      {r : Fin n → R | ∀ i, MvPolynomial.eval r (P i) = 0}
      {s : Fin n → S | ∀ i, MvPolynomial.eval s (MvPolynomial.map φ (P i)) = 0}
Tag 05D6, a lemma

Tag 05D6 in the Stacks Project.

Module.exists_sSupIndep_finitePresentation_of_countable_span_of_mittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/MittagLeffler/Henselian.lean, line 626. The attribute's comment: “Mittag-Leffler is spelled out inline as condition (1) of 059E, as in 059M, 059N, 059P, 059R, 05CQ and 0AS7; countable generation as a countable spanning set, as in 0590; and the direct sum decomposition internally, as an independent set of submodules of M with supremum ⊤, as in 058W. Test data in the universe of M, whence Small.{v} R. See the module docstring.”.

Stacks 05D6. Let R be a henselian local ring and let M be an R-module which is countably generated — it admits a countable spanning set — and Mittag-Leffler, the latter in the intrinsic form 059E (1): every map f : P → M from a finitely presented module dominates and is dominated by a map g : P → Q into a finitely presented module, domination meaning Ker(f ⊗ id_T) = Ker(g ⊗ id_T) for every R-module T. Then M is a direct sum of finitely presented R-modules, in the internal form: there is an independent set of finitely presented submodules of M whose supremum is ⊤.

public theorem Module.exists_sSupIndep_finitePresentation_of_countable_span_of_mittagLeffler
    (R : Type u) [CommRing R] [HenselianLocalRing R] [Small.{v} R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (hcg : ∃ s : Set M, s.Countable ∧ Submodule.span R s = ⊤)
    (hML : ∀ (P : Type v) [AddCommGroup P] [Module R P] [Module.FinitePresentation R P]
      (f : P →ₗ[R] M), ∃ (Q : Type v) (_ : AddCommGroup Q) (_ : Module R Q)
        (_ : Module.FinitePresentation R Q) (g : P →ₗ[R] Q), ∀ (T : Type v) [AddCommGroup T]
          [Module R T], LinearMap.ker (f.rTensor T) = LinearMap.ker (g.rTensor T)) :
    ∃ S : Set (Submodule R M), sSupIndep S ∧ sSup S = ⊤ ∧
      ∀ N ∈ S, Module.FinitePresentation R N
Sources
Leannormal_local_domain_sepClosed_fractionField_isStrictlyHenselian · hensel_uniqueness · HenselianLocalRing.TFAE_factorization_etale_quasiFinite · HenselianLocalRing.henselianLocalRing_and_finite_of_finite_of_quasiFiniteAt · exists_algEquiv_prod_of_henselianLocalRing · exists_prod_local_purelyInseparable_not_quasiFiniteAt · CommAlgCat.FiniteEtale.isEquivalence_baseChange_residueField · Algebra.IsUnramifiedIn.exists_algEquiv_prod_quotient

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.