16 Smoothing Ring Maps
Chapter 16 of the Stacks Project, Smoothing Ring Maps, Tag 07BW: the 13 sections of its 14 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 75 tags are carried by 117 declarations of the repository (all in StacksFrontier).
Section16.2 Singular ideals#
Section 16.2 of the Stacks Project, Tag 07C4. 8 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07C5, a definition
Tag 07C5 in the Stacks Project.
Stacks.Smoothing.singularIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdeals.lean, line 220. The attribute's comment: “the singular ideal”.
The singular ideal
H_{A/R}ofAoverR: the vanishing ideal of the set of primes ofAat whichR → Ais not smooth.
noncomputable def singularIdeal : Ideal A
Stacks.Smoothing.singularIdeal_isRadical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdeals.lean, line 225. The attribute's comment: “radicality”.
The singular ideal is radical.
theorem singularIdeal_isRadical : (singularIdeal R A).IsRadical
Stacks.Smoothing.zeroLocus_singularIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdeals.lean, line 231. The attribute's comment: “vanishing locus”.
The vanishing locus of the singular ideal is exactly the locus of primes at which
R → Ais not smooth.
theorem zeroLocus_singularIdeal :
PrimeSpectrum.zeroLocus (singularIdeal R A : Set A) =
{q : PrimeSpectrum A | ¬ Algebra.SmoothAt R A q.asIdeal}
Stacks.Smoothing.eq_singularIdeal_iff_of_isRadical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdeals.lean, line 240. The attribute's comment: “uniqueness”.
A radical ideal is the singular ideal exactly when its vanishing locus is the non-smooth locus; this is the uniqueness in the definition of the singular ideal.
theorem eq_singularIdeal_iff_of_isRadical {I : Ideal A} (hI : I.IsRadical) :
I = singularIdeal R A ↔
PrimeSpectrum.zeroLocus (I : Set A) =
{q : PrimeSpectrum A | ¬ Algebra.SmoothAt R A q.asIdeal}
Tag 07C6, a lemma
Tag 07C6 in the Stacks Project.
Stacks.Smoothing.exists_notMem_eq_mul_jacobianMinorOn_of_smoothAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardElementAtSmoothPrime.lean, line 79.
Stacks 07C6. If a finite polynomial presentation of
AoverRis smooth at a primeq(Definition 00TB), then some elementa ∈ Aoutsideqis a multiple of ac × cJacobian minordet(∂f_j/∂x_i)_{j ∈ V, i ∈ U}on setsU,Vofcvariables andcrelations, and, modulo the square of the full relation ideal, every lift ofacarries every relation into the ideal generated by the relations indexed byV.
theorem exists_notMem_eq_mul_jacobianMinorOn_of_smoothAt
{R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A]
(P : _root_.Presentation R A) (q : Ideal A) [q.IsPrime]
(hq : Algebra.SmoothAt R A q) :
∃ (a : A), a ∉ q ∧
∃ (c : ℕ) (U : Finset (Fin P.n)) (V : Finset (Fin P.m))
(_hcn : c ≤ P.n) (_hcm : c ≤ P.m) (hU : U.card = c) (hV : V.card = c),
∃ a' : A,
a = a' * P.lift (P.jacobianMinorOn c U V hU hV) ∧
(∀ (ℓ : Fin P.m) (ã : MvPolynomial (Fin P.n) R), P.IsLift a ã →
ã * P.f ℓ ∈ P.selectedRelIdeal V + P.relIdeal ^ 2)
Tag 07C7, a definition
Tag 07C7 in the Stacks Project.
IsElementaryStandard, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/BaseChangeOfPresentation.lean, line 214. The attribute's comment: “the first of the two notions the definition introduces: a is elementary standard in A over R, i.e. some presentation A = R[x_1,…,x_n]/(f_1,…,f_m) and some 0 ≤ c ≤ min(n, m) satisfy 16.2.3.1 and 16.2.3.2. The two conditions themselves are Presentation.IsElementaryStandardFor”.
An element
a ∈ Ais elementary standard inAoverRif there exists a presentation ofAoverRand an integercwith0 ≤ c ≤ min(n, m)realizingaas elementary standard.
def IsElementaryStandard (a : A) : Prop
IsStrictlyStandard, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/BaseChangeOfPresentation.lean, line 224. The attribute's comment: “the second of the two notions the definition introduces: a is strictly standard in A over R, i.e. some presentation A = R[x_1,…,x_n]/(f_1,…,f_m) and some 0 ≤ c ≤ min(n, m) satisfy 16.2.3.3 and 16.2.3.4. The two conditions themselves are Presentation.IsStrictlyStandardFor”.
An element
a ∈ Ais strictly standard inAoverRif there exists a presentation ofAoverRand an integercwith0 ≤ c ≤ min(n, m)realizingaas strictly standard.
def IsStrictlyStandard (a : A) : Prop
Tag 07ET, a lemma
Tag 07ET in the Stacks Project.
Stacks.Smoothing.exists_comp_eq_lsmul_of_eq_sum_jacobianMinor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdeals.lean, line 95. The attribute's comment: “the forward half: the equation of 07ER implies that there is an A-linear ψ : ⊕_{i = 1,…,n} A dx_i → A^{⊕c} whose composition with A^{⊕c} →^{(f_1,…,f_c)} I/I² →^{f ↦ df} ⊕_{i = 1,…,n} A dx_i is multiplication by a. The two-step composite is the Jacobian map jacobianMatrix, whose j-th column is d f_j. Only 07ER is hypothesised, as in the source; the condition of 07ES is not assumed”.
A strictly standard equation supplies a left inverse to its Jacobian map. Only the equation 16.2.3.3 is used; the relation-ideal condition 16.2.3.4 is not needed.
theorem exists_comp_eq_lsmul_of_eq_sum_jacobianMinor
(P : Presentation R A) (a : A) (c : ℕ) (hcm : c ≤ P.m)
(ha : ∃ aI : Finset (Fin P.n) → A,
a = ∑ s ∈ Finset.powersetCard c (Finset.univ : Finset (Fin P.n)),
aI s * P.lift (if h : s.card = c then P.jacobianMinor c hcm s h else 0)) :
∃ ψ : (Fin P.n → A) →ₗ[A] (Fin c → A),
ψ.comp (Matrix.toLin' (jacobianMatrix P c hcm)) =
LinearMap.lsmul A (Fin c → A) a
Stacks.Smoothing.exists_pow_eq_sum_jacobianMinor_of_comp_eq_lsmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdeals.lean, line 157. The attribute's comment: “the converse half: if such a ψ exists — that is, if some A-linear ψ : ⊕_{i = 1,…,n} A dx_i → A^{⊕c} composed with A^{⊕c} →^{(f_1,…,f_c)} I/I² →^{f ↦ df} ⊕_{i = 1,…,n} A dx_i is multiplication by a — then a ^ c satisfies the equation of 07ER. As in the source the conclusion is only that equation, not the condition of 07ES”.
A left inverse to the Jacobian expresses the corresponding power as a sum of Jacobian minors (the equation of Stacks 07ER). This also holds for
c = 0, when the empty minor is1; the relation-ideal condition of Stacks 07ES is a separate requirement.
theorem exists_pow_eq_sum_jacobianMinor_of_comp_eq_lsmul
(P : Presentation R A) (a : A) (c : ℕ) (hcm : c ≤ P.m)
(ψ : (Fin P.n → A) →ₗ[A] (Fin c → A))
(hψ : ψ.comp (Matrix.toLin' (jacobianMatrix P c hcm)) =
LinearMap.lsmul A (Fin c → A) a) :
∃ aI : Finset (Fin P.n) → A,
a ^ c = ∑ s ∈ Finset.powersetCard c (Finset.univ : Finset (Fin P.n)),
aI s * P.lift (if h : s.card = c then P.jacobianMinor c hcm s h else 0)
Tag 07CA, a lemma
Tag 07CA in the Stacks Project.
Stacks.Smoothing.singularIdeal_eq_radical_span_isElementaryStandard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdealGenerators.lean, line 390. The attribute's comment: “elementary standard elements”.
Stacks 07CA. The singular ideal is the radical of the ideal generated by the elementary standard elements of
AoverR.
theorem singularIdeal_eq_radical_span_isElementaryStandard (R : Type u) [CommRing R] (A : Type v)
[CommRing A] [Algebra R A] [Algebra.FinitePresentation R A] :
singularIdeal R A = (Ideal.span {a : A | IsElementaryStandard (R := R) a}).radical
Stacks.Smoothing.singularIdeal_eq_radical_span_isStrictlyStandard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdealGenerators.lean, line 398. The attribute's comment: “strictly standard elements”.
Stacks 07CA. The singular ideal is the radical of the ideal generated by the strictly standard elements of
AoverR.
theorem singularIdeal_eq_radical_span_isStrictlyStandard (R : Type u) [CommRing R] (A : Type v)
[CommRing A] [Algebra R A] [Algebra.FinitePresentation R A] :
singularIdeal R A = (Ideal.span {a : A | IsStrictlyStandard (R := R) a}).radical
Tag 07CB, an example
Tag 07CB in the Stacks Project.
Stacks.Smoothing.NotQuasiCompact.finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SmoothLocusNotQuasiCompact.lean, line 283.
The ring map
R → A = R/(x)is of finite presentation.
theorem finitePresentation : Algebra.FinitePresentation (baseRing k) (quotientRing k)
Stacks.Smoothing.NotQuasiCompact.smoothLocus_eq_iUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SmoothLocusNotQuasiCompact.lean, line 294.
The smooth locus of
R → Ais the union of the standard opensD(y_i).
theorem smoothLocus_eq_iUnion :
Algebra.smoothLocus (baseRing k) (quotientRing k) =
⋃ i : ℕ, (PrimeSpectrum.basicOpen (y k i) : Set (PrimeSpectrum (quotientRing k)))
Stacks.Smoothing.NotQuasiCompact.smoothLocus_not_compact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SmoothLocusNotQuasiCompact.lean, line 344.
The smooth locus of the finitely presented ring map
R → Ais not quasi-compact.
theorem smoothLocus_not_compact :
¬ IsCompact (Algebra.smoothLocus (baseRing k) (quotientRing k))
Tag 07CC, a lemma
Tag 07CC in the Stacks Project.
isElementaryStandard_basechange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/BaseChangeOfPresentation.lean, line 492. The attribute's comment: “(1)”.
Let
R → Abe a ring map of finite presentation andR → R'a ring map. Ifa ∈ Ais elementary standard inAoverR, thena ⊗ 1 ∈ A ⊗_R R'is elementary standard inA ⊗_R R'overR'. HereA ⊗_R R'is modelled asR' ⊗[R] Aanda ⊗ 1as1 ⊗ a.
theorem isElementaryStandard_basechange (a : A) (ha : IsElementaryStandard (R := R) a) :
IsElementaryStandard (R := R')
(Algebra.TensorProduct.includeRight a : R' ⊗[R] A)
isStrictlyStandard_basechange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/BaseChangeOfPresentation.lean, line 506. The attribute's comment: “(2)”.
Let
R → Abe a ring map of finite presentation andR → R'a ring map. Ifa ∈ Ais strictly standard inAoverR, thena ⊗ 1 ∈ A ⊗_R R'is strictly standard inA ⊗_R R'overR'.
theorem isStrictlyStandard_basechange (a : A) (ha : IsStrictlyStandard (R := R) a) :
IsStrictlyStandard (R := R')
(Algebra.TensorProduct.includeRight a : R' ⊗[R] A)
Tag 07EU, a lemma
Tag 07EU in the Stacks Project.
exists_smooth_factorization_of_singularIdeal_map_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SingularIdealFactorization.lean, line 400.
Given ring maps
R → A → ΛwithAof finite presentation overR, if the image of the singular idealH_{A/R}generates the unit ideal ofΛ, thenA → Λfactors asA → B → ΛwithBsmooth overR.
theorem exists_smooth_factorization_of_singularIdeal_map_eq_top
(R : Type u) (A : Type v) (Λ : Type w) [CommRing R] [CommRing A] [CommRing Λ]
[Algebra R A] [Algebra A Λ] [Algebra R Λ] [IsScalarTower R A Λ]
[Algebra.FinitePresentation R A]
(h : Ideal.map (algebraMap A Λ) (singularIdeal R A) = ⊤) :
∃ (B : Type (max v w)) (_ : CommRing B) (_ : Algebra R B) (_ : Algebra A B)
(_ : Algebra B Λ),
IsScalarTower R A B ∧ IsScalarTower A B Λ ∧ IsScalarTower R B Λ ∧ Algebra.Smooth R B
Sources
Section16.3 Presentations of algebras#
Section 16.3 of the Stacks Project, Tag 07CD. 8 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07CE, a lemma
Tag 07CE in the Stacks Project.
Stacks.Smoothing.exists_finiteType_retraction_improving_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ImprovingPresentations.lean, line 611.
A finitely presented algebra admits one finite-type retract satisfying both local improvements of its presentation. The retract is the symmetric algebra of the finite conormal module of a polynomial presentation, and the retraction is its augmentation. This conormal module is projective when the algebra is a local complete intersection over the base.
theorem exists_finiteType_retraction_improving_presentation
(R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A]
[Algebra.FinitePresentation R A] :
∃ (C : Type v) (_ : CommRing C) (_ : Algebra R C) (_ : Algebra A C)
(_ : IsScalarTower R A C) (_ : Algebra.FiniteType A C) (g : C →ₐ[R] A)
(n : ℕ) (P : Algebra.Generators R A (Fin n))
(e : C ≃ₐ[A] SymmetricAlgebra A P.toExtension.Cotangent),
Module.Finite A P.toExtension.Cotangent ∧
(RingHom.IsLocalCompleteIntersection (algebraMap R A) →
Module.Projective A P.toExtension.Cotangent) ∧
(∀ c : C, g c = SymmetricAlgebra.algebraMapInv (e c)) ∧
g.comp (IsScalarTower.toAlgHom R A C) = AlgHom.id R A ∧
(∀ a : A,
RingHom.IsLocalCompleteIntersection (algebraMap R (Localization.Away a)) →
(letI : Algebra (Localization.Away a)
(Localization.Away (algebraMap A C a)) :=
(Localization.awayMap (algebraMap A C) a).toAlgebra;
Algebra.Smooth (Localization.Away a)
(Localization.Away (algebraMap A C a)) ∧
HasFreeConormalPresentation R (Localization.Away (algebraMap A C a)))) ∧
(∀ a : A, Algebra.Smooth R (Localization.Away a) →
Module.Free (Localization.Away (algebraMap A C a))
(KaehlerDifferential R (Localization.Away (algebraMap A C a))))
Tag 07EX, an equation
Tag 07EX in the Stacks Project.
Stacks.Smoothing.localizedConormalEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LocalizedConormalSequence.lean, line 81. The attribute's comment: “the two localized conormal-module identifications”.
The canonical description of the conormal module of the genuine localization presentation. The first factor is generated by the newly adjoined relation
P.σ(a) X - 1; the second is the localized old conormal module.
noncomputable def localizedConormalEquiv
{S : Type*} [CommRing S] [Algebra R S] [Algebra A S] [IsScalarTower R A S]
{I : Type uι} (P : Algebra.Generators R A I) (a : A)
[IsLocalization.Away a S] :
((Algebra.Generators.localizationAway S a).comp P).toExtension.Cotangent ≃ₗ[S]
S × (S ⊗[A] P.toExtension.Cotangent)
Stacks.Smoothing.localizedConormalEquiv_freeGenerator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LocalizedConormalSequence.lean, line 107. The attribute's comment: “the free generator in the localized identifications”.
The direct-sum identification sends the class of the new relation
P.σ(a) X - 1to the free generator.
theorem localizedConormalEquiv_freeGenerator
{S : Type*} [CommRing S] [Algebra R S] [Algebra A S] [IsScalarTower R A S]
{I : Type uι} (P : Algebra.Generators R A I) (a : A)
[IsLocalization.Away a S] :
(localizedConormalEquiv (S := S) P a)
(localizationRelationCotangent (S := S) P a) = (1, 0)
Stacks.Smoothing.localizedConormalEquiv_symm_comp_inr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LocalizedConormalSequence.lean, line 131. The attribute's comment: “compatibility of the localized identifications”.
On the localized old conormal summand, the inverse direct-sum identification is the canonical base-changed conormal map.
theorem localizedConormalEquiv_symm_comp_inr
{S : Type*} [CommRing S] [Algebra R S] [Algebra A S] [IsScalarTower R A S]
{I : Type uι} (P : Algebra.Generators R A I) (a : A)
[IsLocalization.Away a S] :
(localizedConormalEquiv (S := S) P a).symm.toLinearMap ∘ₗ
LinearMap.inr S S (S ⊗[A] P.toExtension.Cotangent) =
(Algebra.Extension.Cotangent.map
((Algebra.Generators.localizationAway S a).toComp P).toExtensionHom).liftBaseChange S
Stacks.Smoothing.localizedConormalSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LocalizedConormalSequence.lean, line 170. The attribute's comment: “exactness at the middle term”.
Exactness at
C_a ⊕ (J/J²)_ain the localized conormal sequence.
theorem localizedConormalSequence_exact
(a : A) [IsLocalization.Away (algebraMap A C a) L]
{K : Type uK} [AddCommGroup K] [Module A K]
(eK : (L ⊗[C] Q.toExtension.Cotangent) ≃ₗ[L] (L ⊗[A] K)) :
Function.Exact (localizedConormalIncoming P Q)
(localizedConormalOutgoing P Q eK)
Stacks.Smoothing.localizedConormalSequence_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LocalizedConormalSequence.lean, line 195. The attribute's comment: “surjectivity onto the final term”.
The final arrow is surjective, so the localized conormal sequence ends in zero.
theorem localizedConormalSequence_surjective
(a : A) [IsLocalization.Away (algebraMap A C a) L]
{K : Type uK} [AddCommGroup K] [Module A K]
(eK : (L ⊗[C] Q.toExtension.Cotangent) ≃ₗ[L] (L ⊗[A] K)) :
Function.Surjective (localizedConormalOutgoing P Q eK)
Tag 07M8, a proposition
Tag 07M8 in the Stacks Project.
Stacks.Smoothing.exists_smooth_lift_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LiftingAlongSurjections/SmoothLift.lean, line 149. The attribute's comment: “smooth lift”.
A smooth algebra over a quotient of the base is the special fibre of a smooth algebra over the base: if
R → R₀is surjective with kernelIandR₀ → A₀is smooth, there is a smoothR-algebraAtogether with a ring equivalenceA₀ ≃ A/IAcompatible with the maps fromR.
theorem exists_smooth_lift_of_surjective
(R : Type u) (R₀ : Type v) (A₀ : Type w) [CommRing R] [CommRing R₀] [CommRing A₀]
[Algebra R R₀] [Algebra R₀ A₀]
(hR : Function.Surjective (algebraMap R R₀))
(hA₀ : Algebra.Smooth R₀ A₀) :
∃ (A : Type (max u w)) (_ : CommRing A) (a : Algebra R A),
letI := a
Algebra.Smooth R A ∧
∃ e : A₀ ≃+* A ⧸ Ideal.map (algebraMap R A)
(RingHom.ker (algebraMap R R₀)),
∀ r : R, e (algebraMap R₀ A₀ (algebraMap R R₀ r)) =
Ideal.Quotient.mk _ (algebraMap R A r)
Stacks.Smoothing.exists_syntomic_lift_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LiftingAlongSurjections/SyntomicLift.lean, line 535. The attribute's comment: “syntomic lift”.
A syntomic algebra over a quotient of the base is the special fibre of a syntomic algebra over the base: if
R → R₀is surjective with kernelIandR₀ → A₀is syntomic, there is a syntomicR-algebraAtogether with a ring equivalenceA₀ ≃ A/IAcompatible with the maps fromR.
theorem exists_syntomic_lift_of_surjective
(R : Type u) (R₀ : Type v) (A₀ : Type w) [CommRing R] [CommRing R₀] [CommRing A₀]
[Algebra R R₀] [Algebra R₀ A₀]
(hR : Function.Surjective (algebraMap R R₀))
(hA₀ : Algebra.Syntomic R₀ A₀) :
∃ (A : Type (max u w)) (_ : CommRing A) (a : Algebra R A),
letI := a
Algebra.Syntomic R A ∧
∃ e : A₀ ≃+* A ⧸ Ideal.map (algebraMap R A)
(RingHom.ker (algebraMap R R₀)),
∀ r : R, e (algebraMap R₀ A₀ (algebraMap R R₀ r)) =
Ideal.Quotient.mk _ (algebraMap R A r)
Tag 07CG, a lemma
Tag 07CG in the Stacks Project.
Stacks.Smoothing.exists_smooth_retract_isRelativeGlobalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SyntomicCompleteIntersectionExtension.lean, line 172.
Stacks 07CG. A syntomic
R-algebraAadmits a smoothA-algebraCwith a retractionC → A, flat overRand a relative global complete intersection overR: soCis cut out of a polynomial ring bycequations, flat overR, with all fibres of dimensionn - c.
theorem exists_smooth_retract_isRelativeGlobalCompleteIntersection
(R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A]
[Algebra.Syntomic R A] :
∃ (C : Type v) (hC : CommRing C) (hRC : Algebra R C) (hAC : Algebra A C)
(hTower : IsScalarTower R A C),
let : CommRing C := hC
let : Algebra R C := hRC
let : Algebra A C := hAC
let : IsScalarTower R A C := hTower
Algebra.Smooth A C ∧
Module.Flat R C ∧
∃ ρ : C →+* A,
ρ.comp (algebraMap A C) = RingHom.id A ∧
Algebra.IsRelativeGlobalCompleteIntersection R C
Tag 07CH, a lemma
Tag 07CH in the Stacks Project.
Stacks.Smoothing.exists_smooth_retract_isStandardSmooth_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/FilteredColimitStandardSmooth.lean, line 311. The attribute's comment: “B is produced as a type in the universe of A, carrying compatible Algebra A B and Algebra R B instances with IsScalarTower R A B; "B is standard smooth over R" is Mathlib's Algebra.IsStandardSmooth, whose submersive presentation is exactly the displayed presentation with invertible c × c Jacobian minor. The retraction is a RingHom, which is automatically an R-algebra map. See the module docstring.”.
A smooth algebra has a standard smooth retract. For a smooth ring map
R → Athere is a smoothR-algebra mapA → Bwith a retraction such thatBis standard smooth overR, that is,B ≅ R[x_1, …, x_n]/(f_1, …, f_c)withdet(∂f_j/∂x_i)_{i, j = 1, …, c}invertible inB.
theorem exists_smooth_retract_isStandardSmooth_of_smooth :
Algebra.Smooth R A →
∃ (B : Type v) (_ : CommRing B) (_ : Algebra A B) (_ : Algebra R B),
IsScalarTower R A B ∧ Algebra.Smooth A B ∧
Algebra.IsStandardSmooth R B ∧
∃ (r : B →+* A),
r.comp (algebraMap A B) = RingHom.id A
Stacks.Smoothing.exists_smooth_isStandardSmooth_retraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardSmoothRetract.lean, line 484.
Stacks 07CH. Let
R → Abe a smooth ring map. Then there is a smoothA-algebraBwhich is standard smooth overRand such thatA → Bhas anA-algebra retraction.
theorem exists_smooth_isStandardSmooth_retraction (R : Type u) (A : Type v) [CommRing R]
[CommRing A] [Algebra R A] [Algebra.Smooth R A] :
∃ (B : Type v) (_ : CommRing B) (_ : Algebra A B) (_ : Algebra R B)
(_ : IsScalarTower R A B),
Algebra.Smooth A B ∧ Algebra.IsStandardSmooth R B ∧
∃ r : B →+* A, r.comp (algebraMap A B) = RingHom.id A
Tag 07CI, a lemma
Tag 07CI in the Stacks Project.
Stacks.Smoothing.ind_isStandardSmooth_of_ind_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/FilteredColimitStandardSmooth.lean, line 367. The attribute's comment: “"Λ is a filtered colimit of smooth (resp. standard smooth) R-algebras" is ObjectProperty.ind.{u} of RingHom.Smooth (resp. RingHom.IsStandardSmooth) on the category Under (CommRingCat.of R) of R-algebras, as in Lemma 07C3. See the module docstring.”.
A filtered colimit of smooth algebras is a filtered colimit of standard smooth algebras. Let
R → Λbe a ring map. IfΛis a filtered colimit of smoothR-algebras, thenΛis a filtered colimit of standard smoothR-algebras.
theorem ind_isStandardSmooth_of_ind_smooth {R Λ : Type u} [CommRing R] [CommRing Λ]
(f : R →+* Λ)
(h : ObjectProperty.ind.{u}
(fun B : Under (CommRingCat.of R) ↦ B.hom.hom.Smooth)
(Under.mk (CommRingCat.ofHom f))) :
ObjectProperty.ind.{u}
(fun B : Under (CommRingCat.of R) ↦ B.hom.hom.IsStandardSmooth)
(Under.mk (CommRingCat.ofHom f))
Tag 07EY, a lemma
Tag 07EY in the Stacks Project.
standardSmooth_presentation_with_prescribed_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardSmoothPresentation.lean, line 135.
Let
R → Abe a standard smooth ring map and letE ⊆ Abe a finite subset with exactlynelements. Then there existm ≥ 0,c ≥ n, and polynomialsf_1, ..., f_cinR[x_1, ..., x_{n+m}]together with a surjectiveR-algebra mapπwith kernel(f_1, ..., f_c)such that: 1.πis surjective with kernel(f)(soA ≅ R[x]/(f)); 2. the image of the Jacobian determinant (using the firstcvariables) is invertible inA; 3. the images of the firstnvariablesx_1, ..., x_nare exactlyE.
theorem standardSmooth_presentation_with_prescribed_generators
(R A : Type*) [CommRing R] [CommRing A] [Algebra R A]
(hA : IsStandardSmoothRingMap R A) (E : Finset A) (n : ℕ) (hn : E.card = n) :
∃ (m c : ℕ) (_ : n ≤ c) (hcnm : c ≤ n + m)
(f : Fin c → MvPolynomial (Fin (n + m)) R)
(π : MvPolynomial (Fin (n + m)) R →ₐ[R] A),
-- (1) Presentation: `π` is surjective with kernel `(f_1, ..., f_c)`.
(Function.Surjective π ∧
RingHom.ker π.toRingHom = Ideal.span (Set.range f)) ∧
-- (2) Standard smooth Jacobian condition: the image of the Jacobian
-- determinant is invertible in `A`.
IsUnit (π (jacobianDet hcnm f)) ∧
-- (3) Generators include `E`: `E` equals the set of images of the first `n`
-- variables `x_1, ..., x_n`.
(E : Set A) = Set.range (fun i : Fin n => π (X (Fin.castAdd m i)))
Tag 07EZ, a lemma
Tag 07EZ in the Stacks Project.
Stacks.Smoothing.exists_eventually_isStrictlyStandard_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StablyFreeStrictlyStandardPowers.lean, line 687. The attribute's comment: “clause (e), the implication (2) ⇒ a ^ e is strictly standard in A over R for all e ≥ e_0: the conclusion is ∃ e₀, ∀ e, e₀ ≤ e → ..., the source's all sufficiently large powers, and not merely that some power is strictly standard”.
Stacks 16.3.7 (e). Let
R → Abe of finite presentation anda ∈ A. IfA_ais smooth overRandΩ_{A_a/R}is stably free, thena ^ eis strictly standard inAoverRfor every sufficiently largee.
theorem exists_eventually_isStrictlyStandard_pow (S : SixStandardnessConditions.{u, v})
(hS : Algebra.Smooth S.R (Localization.Away S.a) ∧
Module.IsStablyFree (Localization.Away S.a)
(KaehlerDifferential S.R (Localization.Away S.a))) :
∃ e₀ : ℕ, ∀ e : ℕ, e₀ ≤ e → IsStrictlyStandard (R := S.R) (S.a ^ e)
Stacks.Smoothing.standardSmooth_localization_isSmooth_and_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardnessConditions.lean, line 92. The attribute's comment: “clause (a), the implication (4) ⇒ (3): if A_a is standard smooth over R then A_a is smooth over R and Ω_{A_a/R} is free”.
Standard smoothness of
A_aimplies condition (3):A_ais smooth overRand its module of relative differentials is free.
theorem standardSmooth_localization_isSmooth_and_free
(S : SixStandardnessConditions)
(h : Algebra.IsStandardSmooth S.R (Localization.Away S.a)) :
Algebra.Smooth S.R (Localization.Away S.a) ∧
Module.Free (Localization.Away S.a)
(KaehlerDifferential S.R (Localization.Away S.a))
Stacks.Smoothing.free_of_differentials_implies_stably_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardnessConditions.lean, line 104. The attribute's comment: “clause (a), the implication (3) ⇒ (2): if A_a is smooth over R and Ω_{A_a/R} is free then it is stably free”.
Condition (3) implies condition (2): a free module of differentials is stably free.
theorem free_of_differentials_implies_stably_free
(S : SixStandardnessConditions)
(h : Algebra.Smooth S.R (Localization.Away S.a) ∧
Module.Free (Localization.Away S.a)
(KaehlerDifferential S.R (Localization.Away S.a))) :
Algebra.Smooth S.R (Localization.Away S.a) ∧
Module.IsStablyFree (Localization.Away S.a)
(KaehlerDifferential S.R (Localization.Away S.a))
Stacks.Smoothing.smooth_of_smooth_and_stablyFree_differentials, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardnessConditions.lean, line 118. The attribute's comment: “clause (a), the implication (2) ⇒ (1): if A_a is smooth over R and Ω_{A_a/R} is stably free then A_a is smooth over R”.
Condition (2) implies condition (1): smoothness of
A_aoverR.
lemma smooth_of_smooth_and_stablyFree_differentials (S : SixStandardnessConditions)
(h : Algebra.Smooth S.R (Localization.Away S.a) ∧
Module.IsStablyFree (Localization.Away S.a)
(KaehlerDifferential S.R (Localization.Away S.a))) :
Algebra.Smooth S.R (Localization.Away S.a)
Stacks.Smoothing.elementaryStandard_implies_strictlyStandard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardnessConditions.lean, line 129. The attribute's comment: “clause (b), the implication (6) ⇒ (5): an elementary standard element is strictly standard, the single principal minor being the one on the first c variables”.
Condition (6) implies condition (5): an elementary standard element is strictly standard. The single principal minor is the minor indexed by the first
cvariables.
theorem elementaryStandard_implies_strictlyStandard
(S : SixStandardnessConditions)
(h : IsElementaryStandard (R := S.R) (A := S.A) S.a) :
IsStrictlyStandard (R := S.R) (A := S.A) S.a
Stacks.Smoothing.isStandardSmooth_localizationAway_of_isElementaryStandard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StandardnessConditions.lean, line 255. The attribute's comment: “clause (c), the implication (6) ⇒ (4): if a is elementary standard in A over R then A_a is standard smooth over R — condition (4), not merely smooth after some further localization”.
Condition (6) implies condition (4): an elementary standard element has a standard smooth localization.
theorem isStandardSmooth_localizationAway_of_isElementaryStandard
(S : SixStandardnessConditions)
(ha : IsElementaryStandard (R := S.R) S.a) :
Algebra.IsStandardSmooth S.R (Localization.Away S.a)
Stacks.Smoothing.smooth_and_isStablyFree_kaehlerDifferential_of_isStrictlyStandard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StrictlyStandardStablyFree.lean, line 286. The attribute's comment: “clause (d), the implication (5) ⇒ (2): if a is strictly standard in A over R then A_a is smooth over R and Ω_{A_a/R} is stably free. Both conjuncts of (2) are concluded; the smoothness one is the implication (5) ⇒ (1) of 07CA”.
Stacks 16.3.7, (5) ⇒ (2). If the distinguished element is strictly standard, then its localization is smooth and its module of differentials is stably free.
theorem smooth_and_isStablyFree_kaehlerDifferential_of_isStrictlyStandard
(S : SixStandardnessConditions)
(h : IsStrictlyStandard (R := S.R) S.a) :
Algebra.Smooth S.R (Localization.Away S.a) ∧
Module.IsStablyFree (Localization.Away S.a)
(KaehlerDifferential S.R (Localization.Away S.a))
Sources
Section16.4 Intermezzo: Néron desingularization#
Section 16.4 of the Stacks Project, Tag 0BJ1. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BJ2, a situation
Tag 0BJ2 in the Stacks Project.
Stacks.Smoothing.NeronSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronDesingularization.lean, line 76.
The standing data and hypotheses of Stacks 0BJ2: an extension
R → Λof discrete valuation rings of ramification index one, factored asR → A → ΛwithAflat and of finite type overR.
structure NeronSituation
Tag 0BJ3, a lemma
Tag 0BJ3 in the Stacks Project.
Stacks.Smoothing.neron_affineBlowup_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronDesingularization.lean, line 181. The attribute's comment: “neron_localization”.
Stacks 0BJ3. The affine blowup at
𝔭commutes with localizing away from an element outside𝔭: ifA' = A[𝔭/π], then the affine blowup ofA_aisA'_a.
theorem neron_affineBlowup_localization
(S : NeronSituation) (π : S.R)
(_hπ : Irreducible π)
(a : S.A)
(_ha : a ∉ S.maximalIdealPreimage)
(hπA : algebraMap S.R S.A π ∈ S.maximalIdealPreimage) :
let A' : Type _ := affineBlowupAlgebra S.maximalIdealPreimage
(algebraMap S.R S.A π) (Localization.Away (algebraMap S.R S.A π))
let Aa := Localization.Away a
let L := Localization.Away (algebraMap S.A A' a)
let B : Type _ := affineBlowupAlgebra
(S.maximalIdealPreimage.map (algebraMap S.A Aa))
(algebraMap S.A Aa (algebraMap S.R S.A π))
(Localization.Away (algebraMap S.A Aa (algebraMap S.R S.A π)))
∃ e : L ≃+* B,
(∀ x : S.A, e (algebraMap A' L (algebraMap S.A A' x)) =
algebraMap Aa B (algebraMap S.A Aa x)) ∧
(∀ x : Aa, e (Localization.awayMap (algebraMap S.A A') a x) =
algebraMap Aa B x)
Stacks.Smoothing.blowup_quotient_by_surjection, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronDesingularization.lean, line 339. The attribute's comment: “neron_surjection”.
Stacks 0BJ3. A surjection
B → Aof flat finite-typeR-algebras presents the blowup ofAat𝔭: it is the blowup ofBat the preimage of𝔭, modulo the extended kernel and then modulo theπ-power torsion.
lemma blowup_quotient_by_surjection (S : NeronSituation) (π : S.R)
(hπ : Ideal.span ({π} : Set S.R) = IsLocalRing.maximalIdeal S.R)
(B : Type*) [CommRing B] [Algebra S.R B] [Module.Flat S.R B]
[Algebra.FiniteType S.R B]
(f : B →ₐ[S.R] S.A) (hf : Function.Surjective f) :
Nonempty <|
let pB : Ideal B := Ideal.comap f.toRingHom S.maximalIdealPreimage
let B' := affineBlowupAlgebra pB (algebraMap S.R B π)
(Localization.Away (algebraMap S.R B π))
let I : Ideal B := RingHom.ker f.toRingHom
let IB' : Ideal B' := Ideal.map (algebraMap B B') I
let T := B' ⧸ IB'
let A' := affineBlowupAlgebra S.maximalIdealPreimage
(algebraMap S.R S.A π) (Localization.Away (algebraMap S.R S.A π))
(T ⧸ torsionIdeal T (algebraMap S.R T π)) ≃ₐ[S.R] A'
Tag 0BJ4, a lemma
Tag 0BJ4 in the Stacks Project.
Stacks.Smoothing.affineBlowup_smoothAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronBlowupSmooth.lean, line 373. The attribute's comment: “blowup_smooth”.
Stacks 0BJ4, smoothness. In a Néron situation with uniformizer
π, ifAis smooth overRat𝔭and the residue-field extensionκ(R) → κ(Λ)is separable, then the affine blowupA' = A[𝔭/π]is smooth overRat the prime𝔭'induced by the canonical mapA' → Λ.
theorem affineBlowup_smoothAt
(S : NeronSituation) (π : S.R)
(hπ : IsLocalRing.maximalIdeal S.R = Ideal.span ({π} : Set S.R))
(hsep : @Algebra.IsSeparableExtension
(IsLocalRing.maximalIdeal S.R).ResidueField
(IsLocalRing.maximalIdeal S.Λ).ResidueField _ _ S.residueFieldExtension)
(hS : Algebra.SmoothAt S.R S.A S.maximalIdealPreimage) :
Algebra.SmoothAt S.R
(affineBlowupAlgebra S.maximalIdealPreimage (algebraMap S.R S.A π)
(Localization.Away (algebraMap S.R S.A π)))
(Ideal.comap (canonicalNeronBlowupMap S π hπ).1
(IsLocalRing.maximalIdeal S.Λ))
Stacks.Smoothing.affineBlowup_differentials_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronBlowupSmooth.lean, line 788. The attribute's comment: “differentials_sequence”.
Stacks 0BJ4, the differential sequence. In a Néron situation with uniformizer
π, ifAis smooth overRat𝔭and the residue-field extensionκ(R) → κ(Λ)is separable, then forc = dim (A/πA)_𝔭the relative differentials of the affine blowupA'at its prime𝔭'sit in a short exact sequence0 → Ω_{A/R} ⊗_A A'_{𝔭'} → Ω_{A'/R} ⊗_{A'} A'_{𝔭'} → ((A'/πA')_{𝔭'})^c → 0, whose first map is the base change ofΩ_{A/R} → Ω_{A'/R}.
theorem affineBlowup_differentials_shortExact
(S : NeronSituation) (π : S.R)
(hπ : IsLocalRing.maximalIdeal S.R = Ideal.span ({π} : Set S.R))
(hsep : @Algebra.IsSeparableExtension
(IsLocalRing.maximalIdeal S.R).ResidueField
(IsLocalRing.maximalIdeal S.Λ).ResidueField _ _ S.residueFieldExtension)
(hsm : Algebra.SmoothAt S.R S.A S.maximalIdealPreimage)
(c : ℕ)
(hc : ringKrullDim
((Localization.AtPrime S.maximalIdealPreimage) ⧸
Ideal.span ({algebraMap S.R (Localization.AtPrime S.maximalIdealPreimage) π} :
Set (Localization.AtPrime S.maximalIdealPreimage))) = c) :
let A' := affineBlowupAlgebra S.maximalIdealPreimage (algebraMap S.R S.A π)
(Localization.Away (algebraMap S.R S.A π))
∀ (p' : Ideal A') [p'.IsPrime],
p' = Ideal.comap (canonicalNeronBlowupMap S π hπ).1 (IsLocalRing.maximalIdeal S.Λ) →
∀ (B : Type w) [CommRing B] [Algebra A' B] [IsLocalization.AtPrime B p']
[Algebra S.A B] [IsScalarTower S.A A' B],
let Q := B ⧸ Ideal.span ({algebraMap A' B (algebraMap S.R A' π)} : Set B)
∃ (f : B ⊗[S.A] Ω[S.A⁄S.R] →ₗ[B] B ⊗[A'] Ω[A'⁄S.R])
(_ : ∀ (x : B) (y : Ω[S.A⁄S.R]),
f (x ⊗ₜ[S.A] y) = x ⊗ₜ[A'] KaehlerDifferential.map S.R S.R S.A A' y)
(g : B ⊗[A'] Ω[A'⁄S.R] →ₗ[B] (Fin c → Q))
(hzero : ModuleCat.ofHom f ≫ ModuleCat.ofHom g = 0),
(ShortComplex.mk (ModuleCat.ofHom f) (ModuleCat.ofHom g) hzero).ShortExact
Tag 0BJ5, a lemma
Tag 0BJ5 in the Stacks Project.
Stacks.Smoothing.smoothAt_of_conormal_cokernel_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronSmoothnessCriterion.lean, line 276.
Stacks 0BJ5. In a Néron situation, suppose
Ais smooth overRat the generic point𝔮 = Ker(A → Λ), supposeAis a quotient of anR-algebraBwhich is smooth overRat the preimage of𝔭, and suppose the cokernel of the conormal mapI/I² ⊗_A Λ → Ω_{B/R} ⊗_B Λis a freeΛ-module. ThenAis smooth overRat𝔭too.
theorem smoothAt_of_conormal_cokernel_free
(S : NeronSituation)
(B : Type*) [CommRing B] [Algebra S.R B] [Algebra B S.A]
[IsScalarTower S.R B S.A]
(hsurj : Function.Surjective (algebraMap B S.A))
(hA : Algebra.SmoothAt S.R S.A S.kernelIdeal)
(_hB : Algebra.SmoothAt S.R B (Ideal.comap (algebraMap B S.A) S.maximalIdealPreimage))
(hfree : let _ := ConormalSeq.cotangentModule hsurj
Module.Free S.Λ
((S.Λ ⊗[S.A] (S.A ⊗[B] Ω[B⁄S.R])) ⧸
LinearMap.range
(LinearMap.baseChange S.Λ (ConormalSeq.conormalMap S.R hsurj)))) :
Algebra.SmoothAt S.R S.A S.maximalIdealPreimage
Tag 0BJ6, a lemma
Tag 0BJ6 in the Stacks Project.
Stacks.Smoothing.exists_finite_affineNeronBlowup_smoothAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronBlowupSequence/Desingularization.lean, line 741.
Stacks 0BJ6. In a Néron situation, if
Ais smooth overRat the generic prime𝔮 = Ker(A → Λ)and the residue-field extensionκ(R) → κ(Λ)is separable, then finitely many affine Néron blowups produce a stage that is smooth overRat its distinguished prime𝔭 = (· → Λ)^{-1}(𝔪_Λ).
theorem exists_finite_affineNeronBlowup_smoothAt
(S : NeronSituation.{u, v, w})
(hsm : Algebra.SmoothAt S.R S.A S.kernelIdeal)
(hsep : @Algebra.IsSeparableExtension
(IsLocalRing.maximalIdeal S.R).ResidueField
(IsLocalRing.maximalIdeal S.Λ).ResidueField _ _ S.residueFieldExtension) :
∃ T : NeronStage S,
Relation.ReflTransGen (IsAffineNeronBlowup S) (NeronStage.initial S) T ∧
Algebra.SmoothAt S.R T.A T.maximalIdealPreimage
Tag 0BJ7, a lemma
Tag 0BJ7 in the Stacks Project.
Stacks.Smoothing.ind_underSmooth_of_ramificationIdx_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/NeronIndSmooth.lean, line 260. The attribute's comment: “"Λ is a filtered colimit of smooth R-algebras" is CategoryTheory.ObjectProperty.ind.{u} of UnderSmooth (CommRingCat.of R) on the category Under (CommRingCat.of R) of R-algebras, the same spelling as the left-hand side of the library's Lemma 07C3. The residue fields are Ideal.ResidueField at the maximal ideals, as in the library's Lemmas 0BJ4-0BJ6, and the fraction fields are abstract, pinned by IsFractionRing. See the module docstring.”. References: SGA 7 I (0.5.1), “ind-smooth colimit”; SGA 7 I (0.5), “Lemma 0.5.1”.
Stacks 0BJ7 (Néron desingularization for discrete valuation rings). Let
R ⊂ Λbe an extension of discrete valuation rings which has ramification index1and induces a separable extension of residue fields and of fraction fields. ThenΛis a filtered colimit of smoothR-algebras.
theorem ind_underSmooth_of_ramificationIdx_one
(hinj : Function.Injective (algebraMap R Λ))
(hram : Stacks.DiscreteValuationRing.Ramification.ramificationIdx R Λ = 1)
(hres : letI := Ideal.residueFieldAlgebra (IsLocalRing.maximalIdeal R)
(IsLocalRing.maximalIdeal Λ)
Algebra.IsSeparableExtension (IsLocalRing.maximalIdeal R).ResidueField
(IsLocalRing.maximalIdeal Λ).ResidueField)
[Algebra.IsSeparableExtension K L] :
ObjectProperty.ind.{u} (UnderSmooth (CommRingCat.of R))
(Under.mk (CommRingCat.ofHom (algebraMap R Λ)))
Sources
Section16.5 The lifting problem#
Section 16.5 of the Stacks Project, Tag 07CJ. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07CK, a lemma
Tag 07CK in the Stacks Project.
Stacks.Smoothing.exists_smooth_quotient_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LiftingProblem.lean, line 422.
The lifting problem. Let
R → Λbe a ring map andI ⊂ Ran ideal withI² = 0such thatΛ/IΛis a filtered colimit of smoothR/I-algebras. Then everyR-algebra mapφ : A → ΛwithAof finite presentation overRfactors asA → B/J → ΛwithBa smoothR-algebra andJ ⊂ IBa finitely generated ideal.
theorem exists_smooth_quotient_factorization
{R Λ A : Type u} [CommRing R] [CommRing Λ] [CommRing A]
[Algebra R Λ] [Algebra R A] [Algebra.FinitePresentation R A]
(I : Ideal R) (hI : I ^ 2 = ⊥)
(hΛ : ObjectProperty.ind.{u}
(fun B : Under (CommRingCat.of (R ⧸ I)) ↦ B.hom.hom.Smooth)
(Under.mk (CommRingCat.ofHom (algebraMap (R ⧸ I) (Λ ⧸ I.map (algebraMap R Λ))))))
(φ : A →ₐ[R] Λ) :
∃ (B : Type u) (_ : CommRing B) (alg : Algebra R B),
letI := alg
Algebra.Smooth R B ∧
∃ J : Ideal B, J ≤ I.map (algebraMap R B) ∧ J.FG ∧
∃ (α : A →ₐ[R] B ⧸ J) (β : (B ⧸ J) →ₐ[R] Λ), β.comp α = φ
Tag 07CL, a lemma
Tag 07CL in the Stacks Project.
Stacks.Smoothing.exists_smooth_factorization_of_fg_le_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LiftingProblem.lean, line 772.
Stacks Project, Tag 07CL. Let
I ⊂ Rbe an ideal withI² = 0such thatΛ/IΛis a filtered colimit of smoothR/I-algebras, and letΛbe flat overR. Then anR-algebra mapφ : B → ΛwithBsmooth overRfactors asB → B' → ΛwithB'smooth overRand withB → B'killing any prescribed finitely generated idealJ ⊆ IBthatφannihilates.
theorem exists_smooth_factorization_of_fg_le_map
(I : Ideal R) (hI : I ^ 2 = ⊥)
(hΛ : ObjectProperty.ind.{u}
(fun C : Under (CommRingCat.of (R ⧸ I)) ↦ C.hom.hom.Smooth)
(Under.mk (CommRingCat.ofHom (algebraMap (R ⧸ I) (Λ ⧸ I.map (algebraMap R Λ))))))
[Module.Flat R Λ] {B : Type u} [CommRing B] [Algebra R B] [Algebra.Smooth R B]
(φ : B →ₐ[R] Λ) (J : Ideal B) (hJI : J ≤ I.map (algebraMap R B)) (hJfg : J.FG)
(hφJ : ∀ x ∈ J, φ x = 0) :
∃ (B' : Type u) (_ : CommRing B') (alg : Algebra R B'),
letI := alg
Algebra.Smooth R B' ∧
∃ (α : B →ₐ[R] B') (β : B' →ₐ[R] Λ), (∀ x ∈ J, α x = 0) ∧ β.comp α = φ
Tag 07CM, a proposition
Tag 07CM in the Stacks Project.
Stacks.Smoothing.ind_smooth_of_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LiftingProblem.lean, line 939.
Stacks Project, Tag 07CM: ind-smoothness of an algebra is stable under infinitesimal deformations. Let
R → Λbe a ring map andI ⊂ Ra nilpotent ideal. IfΛ/IΛis a filtered colimit of smoothR/I-algebras andR → Λis flat, thenΛis a filtered colimit of smoothR-algebras.Here "filtered colimit of smooth algebras" is
CategoryTheory.ObjectProperty.indofRingHom.SmoothonUnder (CommRingCat.of R), the spelling of07C3,07CKand07CL; nilpotence isIsNilpotent I, that isI ^ n = ⊥for somen; and flatness isModule.Flat R Λ.
theorem ind_smooth_of_isNilpotent (I : Ideal R) (hI : IsNilpotent I)
(hΛ : ObjectProperty.ind.{u}
(fun C : Under (CommRingCat.of (R ⧸ I)) ↦ C.hom.hom.Smooth)
(Under.mk (CommRingCat.ofHom (algebraMap (R ⧸ I) (Λ ⧸ I.map (algebraMap R Λ))))))
[Module.Flat R Λ] :
ObjectProperty.ind.{u} (fun C : Under (CommRingCat.of R) ↦ C.hom.hom.Smooth)
(Under.mk (CommRingCat.ofHom (algebraMap R Λ)))
Sources
Section16.6 The lifting lemma#
Section 16.6 of the Stacks Project, Tag 07CN. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07CP, a lemma
Tag 07CP in the Stacks Project.
Stacks.Smoothing.exists_finitePresentation_lift_smoothAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LiftingLemma/ExistsLift.lean, line 39.
Stacks Project, Tag 07CP. A finitely presented algebra modulo
π²admits a lift moduloπwith the asserted smoothness properties.
public theorem exists_finitePresentation_lift_smoothAt
(R : Type u) (Λ : Type v) (C : Type w)
[CommRing R] [CommRing Λ] [CommRing C] [IsNoetherianRing R]
[Algebra R Λ] (π : R)
(hR : ∀ r : R, r * π = 0 ↔ r * π ^ 2 = 0)
(hΛ : ∀ x : Λ,
x * algebraMap R Λ π = 0 ↔ x * (algebraMap R Λ π) ^ 2 = 0)
[Algebra (R ⧸ Ideal.span {π ^ 2}) C]
[Algebra.FinitePresentation (R ⧸ Ideal.span {π ^ 2}) C]
[Algebra (R ⧸ Ideal.span {π ^ 2})
(Λ ⧸ Ideal.span {(algebraMap R Λ π) ^ 2})]
(hquot : ∀ x : R, algebraMap (R ⧸ Ideal.span {π ^ 2})
(Λ ⧸ Ideal.span {(algebraMap R Λ π) ^ 2})
(Ideal.Quotient.mk _ x) = Ideal.Quotient.mk _ (algebraMap R Λ x))
(f : C →ₐ[R ⧸ Ideal.span {π ^ 2}]
Λ ⧸ Ideal.span {(algebraMap R Λ π) ^ 2}) :
∃ (D : Type (max u v w)) (_ : CommRing D) (_ : Algebra R D)
(_ : Algebra.FinitePresentation R D) (g : D →ₐ[R] Λ)
(c : C →+* D ⧸ Ideal.span {algebraMap R D π})
(reduceΛ : (Λ ⧸ Ideal.span {(algebraMap R Λ π) ^ 2}) →+*
Λ ⧸ Ideal.span {algebraMap R Λ π})
(reduceD : (D ⧸ Ideal.span {algebraMap R D π}) →+*
Λ ⧸ Ideal.span {algebraMap R Λ π})
(_ : Algebra (C ⧸ Ideal.span {
algebraMap (R ⧸ Ideal.span {π ^ 2}) C
(Ideal.Quotient.mk (Ideal.span {π ^ 2}) π)})
(D ⧸ Ideal.span {algebraMap R D π})),
(∀ x : Λ, reduceΛ (Ideal.Quotient.mk _ x) = Ideal.Quotient.mk _ x) ∧
(∀ x : D, reduceD (Ideal.Quotient.mk _ x) =
Ideal.Quotient.mk _ (g x)) ∧
(∀ x : C, reduceD (c x) = reduceΛ (f x)) ∧
(∀ x : R, c (algebraMap (R ⧸ Ideal.span {π ^ 2}) C
(Ideal.Quotient.mk _ x)) = Ideal.Quotient.mk _ (algebraMap R D x)) ∧
(∀ x : C, algebraMap
(C ⧸ Ideal.span {
algebraMap (R ⧸ Ideal.span {π ^ 2}) C
(Ideal.Quotient.mk (Ideal.span {π ^ 2}) π)})
(D ⧸ Ideal.span {algebraMap R D π}) (Ideal.Quotient.mk _ x) = c x) ∧
(∀ (q : Ideal D) [q.IsPrime], algebraMap R D π ∉ q →
Algebra.IsSmoothAt R q) ∧
(∀ (q : Ideal D) [q.IsPrime], algebraMap R D π ∈ q →
(∃ (p : Ideal C) (_ : p.IsPrime),
Algebra.IsSmoothAt (R ⧸ Ideal.span {π ^ 2}) p ∧
p = Ideal.comap c (Ideal.map
(Ideal.Quotient.mk (Ideal.span {algebraMap R D π})) q)) →
Algebra.IsSmoothAt R q) ∧
∀ (q : Ideal (D ⧸ Ideal.span {algebraMap R D π})) [q.IsPrime],
(∃ (p : Ideal C) (_ : p.IsPrime),
Algebra.IsSmoothAt (R ⧸ Ideal.span {π ^ 2}) p ∧
p = Ideal.comap c q) →
Algebra.IsSmoothAt
(C ⧸ Ideal.span {
algebraMap (R ⧸ Ideal.span {π ^ 2}) C
(Ideal.Quotient.mk (Ideal.span {π ^ 2}) π)}) q
Sources
Section16.7 The desingularization lemma#
Section 16.7 of the Stacks Project, Tag 07CQ. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07CR, a lemma
Tag 07CR in the Stacks Project.
Stacks.Smoothing.exists_finitePresentation_factorization_singularIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/DesingularizationLemma.lean, line 956.
The desingularization lemma. Let
Rbe Noetherian, letΛbe anR-algebra in which the annihilators ofπand ofπ²agree, and letAbe anR-algebra of finite presentation with anR-algebra mapf : A → Λ. If the image ofπinAis strictly standard overR, and if there is a retractionρ : A/π⁴A → R/π⁴Rcompatible with the maps toΛ/π⁴Λ, thenffactors through anR-algebraBof finite presentation with𝔞 B ⊆ H_{B/R}, where𝔞 = Ann_R (Ann_R (π²) / Ann_R (π)).
theorem exists_finitePresentation_factorization_singularIdeal
(R : Type u) (A : Type v) (Λ : Type w) [CommRing R] [CommRing A] [CommRing Λ]
[Algebra R A] [Algebra R Λ] [IsNoetherianRing R] [Algebra.FinitePresentation R A]
(π : R) (f : A →ₐ[R] Λ)
(hAnn : (Submodule.span Λ {algebraMap R Λ π}).annihilator =
(Submodule.span Λ {(algebraMap R Λ π) ^ 2}).annihilator)
(hstandard : IsStrictlyStandard (R := R) (algebraMap R A π))
(ρ : (A ⧸ Ideal.span {(algebraMap R A π) ^ 4}) →ₐ[R] (R ⧸ Ideal.span {π ^ 4}))
(hρ : ∀ (x : A) (r : R),
ρ (Ideal.Quotient.mk (Ideal.span {(algebraMap R A π) ^ 4}) x) =
Ideal.Quotient.mk (Ideal.span {π ^ 4}) r →
Ideal.Quotient.mk (Ideal.span {(algebraMap R Λ π) ^ 4}) (f x) =
Ideal.Quotient.mk (Ideal.span {(algebraMap R Λ π) ^ 4}) (algebraMap R Λ r)) :
∃ (B : Type u) (_ : CommRing B) (_ : Algebra R B) (_ : Algebra.FinitePresentation R B)
(g : A →ₐ[R] B) (h : B →ₐ[R] Λ),
h.comp g = f ∧
Ideal.map (algebraMap R B) (annihilatorDefectIdeal R π) ≤ singularIdeal R B
Tag 07CT, a lemma
Tag 07CT in the Stacks Project.
Stacks.Smoothing.exists_finitePresentation_factorization_singularIdeal_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/CommonDesingularization.lean, line 200.
Stacks 07CT. A strictly standard element and a factorization modulo its fourth power yield a common finitely presented factorization
A → B ← DoverΛwithH_{D/R} B ⊆ H_{B/D}andH_{D/R} B ⊆ H_{B/R}.
theorem exists_finitePresentation_factorization_singularIdeal_le
(R : Type u) (A : Type v) (D : Type w) (Λ : Type x)
[CommRing R] [CommRing A] [CommRing D] [CommRing Λ] [IsNoetherianRing R]
[Algebra R A] [Algebra R D] [Algebra R Λ]
[Algebra.FinitePresentation R A] [Algebra.FinitePresentation R D] (π : R)
(hR : (Submodule.span R {π}).annihilator = (Submodule.span R {π ^ 2}).annihilator)
(hΛ : (Submodule.span Λ {algebraMap R Λ π}).annihilator =
(Submodule.span Λ {(algebraMap R Λ π) ^ 2}).annihilator)
(fA : A →ₐ[R] Λ) (fD : D →ₐ[R] Λ)
(hπ : IsStrictlyStandard (R := R) (A := A) (algebraMap R A π))
(bar : (A ⧸ Ideal.span {(algebraMap R A π) ^ 4}) →ₐ[R]
D ⧸ Ideal.span {(algebraMap R D π) ^ 4})
(hbar : ∀ (a : A) (y : D),
bar (Ideal.Quotient.mk (Ideal.span {(algebraMap R A π) ^ 4}) a) =
Ideal.Quotient.mk (Ideal.span {(algebraMap R D π) ^ 4}) y →
Ideal.Quotient.mk (Ideal.span {(algebraMap R Λ π) ^ 4}) (fA a) =
Ideal.Quotient.mk (Ideal.span {(algebraMap R Λ π) ^ 4}) (fD y)) :
∃ (B : Type w) (_ : CommRing B) (_ : Algebra D B) (_ : Algebra R B)
(_ : IsScalarTower R D B) (_ : Algebra.FinitePresentation R B)
(a : A →ₐ[R] B) (g : B →ₐ[R] Λ),
g.comp a = fA ∧ g.comp (IsScalarTower.toAlgHom R D B) = fD ∧
(singularIdeal R D).map (algebraMap D B) ≤ singularIdeal D B ∧
(singularIdeal R D).map (algebraMap D B) ≤ singularIdeal R B
Tag 07F0, a lemma
Tag 07F0 in the Stacks Project.
Stacks.Smoothing.exists_finitePresentation_factorization_smoothAway_singularIdeal_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/DesingularizationLifting.lean, line 146.
Stacks 07F0. Let
Rbe Noetherian, letΛbe anR-algebra and letπ ∈ Rbe an element withAnn_R(π) = Ann_R(π²)andAnn_Λ(π) = Ann_Λ(π²). LetA → Λbe anR-algebra map withAof finite presentation and with the image ofπstrictly standard inAoverR, and letA/π⁸A → C̄ → Λ/π⁸Λbe a factorization of the induced map withC̄of finite presentation overR/π⁸R. ThenA → Λfactors asA → B → ΛwithBof finite presentation such thatR_π → B_πis smooth andH_{C̄/(R/π⁸R)} · Λ/π⁸Λ ⊆ √(H_{B/R}Λ) mod π⁸Λ.
theorem exists_finitePresentation_factorization_smoothAway_singularIdeal_le
(R : Type u) (Λ : Type v) (A : Type w) (C : Type x)
[CommRing R] [CommRing Λ] [CommRing A] [CommRing C] [IsNoetherianRing R]
[Algebra R Λ] [Algebra R A] [Algebra.FinitePresentation R A] (π : R)
(hR : (Submodule.span R {π}).annihilator = (Submodule.span R {π ^ 2}).annihilator)
(hΛ : (Submodule.span Λ {algebraMap R Λ π}).annihilator =
(Submodule.span Λ {(algebraMap R Λ π) ^ 2}).annihilator)
(fA : A →ₐ[R] Λ) (hπ : IsStrictlyStandard (R := R) (A := A) (algebraMap R A π))
[Algebra (R ⧸ Ideal.span {π ^ 8}) C]
[Algebra.FinitePresentation (R ⧸ Ideal.span {π ^ 8}) C]
[Algebra (R ⧸ Ideal.span {π ^ 8}) (Λ ⧸ Ideal.span {(algebraMap R Λ π) ^ 8})]
(hquot : ∀ r : R, algebraMap (R ⧸ Ideal.span {π ^ 8})
(Λ ⧸ Ideal.span {(algebraMap R Λ π) ^ 8}) (Ideal.Quotient.mk _ r) =
Ideal.Quotient.mk _ (algebraMap R Λ r))
(toC : (A ⧸ Ideal.span {(algebraMap R A π) ^ 8}) →+* C)
(htoC : ∀ r : R, toC (Ideal.Quotient.mk _ (algebraMap R A r)) =
algebraMap (R ⧸ Ideal.span {π ^ 8}) C (Ideal.Quotient.mk _ r))
(fC : C →ₐ[R ⧸ Ideal.span {π ^ 8}] Λ ⧸ Ideal.span {(algebraMap R Λ π) ^ 8})
(hfC : ∀ a : A, fC (toC (Ideal.Quotient.mk _ a)) = Ideal.Quotient.mk _ (fA a)) :
∃ (B : Type (max u v x)) (_ : CommRing B) (_ : Algebra R B)
(_ : Algebra.FinitePresentation R B) (a : A →ₐ[R] B) (g : B →ₐ[R] Λ),
g.comp a = fA ∧
(letI : Algebra (Localization.Away π) (Localization.Away (algebraMap R B π)) :=
(Localization.awayMap (algebraMap R B) π).toAlgebra
Algebra.Smooth (Localization.Away π) (Localization.Away (algebraMap R B π))) ∧
Ideal.map fC.toRingHom (singularIdeal (R ⧸ Ideal.span {π ^ 8}) C) ≤
Ideal.map (Ideal.Quotient.mk (Ideal.span {(algebraMap R Λ π) ^ 8}))
(Ideal.map g.toRingHom (singularIdeal R B)).radical
Sources
Section16.8 Warmup: reduction to a base field#
Section 16.8 of the Stacks Project, Tag 07F1. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07F2, a situation
Tag 07F2 in the Stacks Project.
Stacks.Smoothing.RegularRingMapSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/RegularRingMap.lean, line 59.
The standing data of Stacks 16.8.1: a regular ring map between Noetherian rings.
structure RegularRingMapSituation
Tag 07F3, a lemma
Tag 07F3 in the Stacks Project.
pt_product, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ProductOfFilteredColimits.lean, line 555.
Let
R_i → Λ_i(i = 1, 2) be ring maps of Noetherian rings. If PT holds forR_1 → Λ_1and forR_2 → Λ_2, then PT holds for the product ring mapR_1 × R_2 → Λ_1 × Λ_2(with the componentwise algebra structure).
theorem pt_product
(R₁ R₂ Λ₁ Λ₂ : Type)
[CommRing R₁] [CommRing R₂] [CommRing Λ₁] [CommRing Λ₂]
[Algebra R₁ Λ₁] [Algebra R₂ Λ₂]
[IsNoetherianRing R₁] [IsNoetherianRing Λ₁]
[IsNoetherianRing R₂] [IsNoetherianRing Λ₂]
(hPT₁ : PT R₁ Λ₁) (hPT₂ : PT R₂ Λ₂) :
letI : Algebra (R₁ × R₂) (Λ₁ × Λ₂) :=
((algebraMap R₁ Λ₁).prodMap (algebraMap R₂ Λ₂)).toAlgebra
PT (R₁ × R₂) (Λ₁ × Λ₂)
Tag 07F4, a lemma
Tag 07F4 in the Stacks Project.
Stacks.Smoothing.exists_factorization_isElementaryStandard, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/DelocalizingSmoothFactorization/ElementaryStandard.lean, line 86.
Stacks 07F4. Let
R → A → Λbe ring maps withAof finite presentation overRand letS ⊆ Rbe a multiplicative set. Given a factorizationS⁻¹A → B' → S⁻¹ΛwithB'smooth overS⁻¹R, there is a factorizationA → B → ΛofA → ΛbyR-algebras in which somes ∈ Smaps to an elementary standard element ofBoverR.Step 1 of the source proof, the reduction to a standard smooth
B', is Stacks 07CH; it is supplied byStacks.Smoothing.exists_smooth_isStandardSmooth_retraction.
theorem exists_factorization_isElementaryStandard
(S : Submonoid R)
[Algebra (Localization S) (Localization (S.map (algebraMap R A)))]
[IsScalarTower R (Localization S) (Localization (S.map (algebraMap R A)))]
[Algebra (Localization S) (Localization (S.map (algebraMap R Λ)))]
[Algebra (Localization (S.map (algebraMap R A)))
(Localization (S.map (algebraMap R Λ)))]
[Algebra A (Localization (S.map (algebraMap R Λ)))]
[IsScalarTower A Λ (Localization (S.map (algebraMap R Λ)))]
(h : ∃ (B' : Type u') (_ : CommRing B')
(_ : Algebra (Localization (S.map (algebraMap R A))) B')
(_ : Algebra (Localization S) B')
(_ : Algebra B' (Localization (S.map (algebraMap R Λ))))
(_ : Algebra A B')
(_ : IsScalarTower A (Localization (S.map (algebraMap R A))) B')
(_ : IsScalarTower (Localization S)
(Localization (S.map (algebraMap R A))) B')
(_ : IsScalarTower (Localization (S.map (algebraMap R A))) B'
(Localization (S.map (algebraMap R Λ))))
(_ : IsScalarTower A B' (Localization (S.map (algebraMap R Λ)))),
Algebra.Smooth (Localization S) B') :
∃ (B : Type u) (_ : CommRing B) (_ : Algebra A B) (_ : Algebra B Λ)
(_ : Algebra R B),
IsScalarTower R A B ∧ IsScalarTower A B Λ ∧ IsScalarTower R B Λ ∧
∃ s : S, IsElementaryStandard (R := R) (algebraMap R B s)
Tag 07F5, a lemma
Tag 07F5 in the Stacks Project.
Stacks.Smoothing.indSmooth_of_indSmooth_of_field_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ReductionToBaseField.lean, line 876. The attribute's comment: “Situation 07F2 is IsRegularRingMap plus the Noetherian hypotheses, and PT is IndSmooth, the ObjectProperty.ind spelling of Lemma 07C3.”.
Stacks 07F5. If property PT — that
Λis a filtered colimit of smoothR-algebras — holds for every regular ring mapR → Λof Noetherian rings whose source is a field, then it holds for every regular ring map of Noetherian rings.
theorem indSmooth_of_indSmooth_of_field_base
(hfield : ∀ (k : Type u) [Field k] (Λ : Type u) [CommRing Λ] [Algebra k Λ]
[IsNoetherianRing Λ], IsRegularRingMap k Λ → IndSmooth k Λ)
(R : Type u) [CommRing R] (Λ : Type u) [CommRing Λ] [Algebra R Λ]
[IsNoetherianRing R] [IsNoetherianRing Λ] (hregular : IsRegularRingMap R Λ) :
IndSmooth R Λ
Sources
Section16.9 Local tricks#
Section 16.9 of the Stacks Project, Tag 07F6. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07F8, a lemma
Tag 07F8 in the Stacks Project.
Stacks.Smoothing.canBeResolved_of_quotient_eighthPowerIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/LiftingResolutionsFromEighthPowers.lean, line 1264.
Stacks 07F8. Let
R → A → Λ ⊃ qbe a local smoothing situation, letr ≥ 1and letπ₁, …, π_r ∈ Rmap intoq. Assume that fori = 1, …, rthe annihilator ofπ_iequals the annihilator ofπ_i²inR/(π₁⁸, …, π_{i-1}⁸)Rand likewise inΛ/(π₁⁸, …, π_{i-1}⁸)Λ, and thatπ_imaps to a strictly standard element ofAoverR. If the chainR/(π₁⁸, …, π_r⁸)R → A/(π₁⁸, …, π_r⁸)A → Λ/(π₁⁸, …, π_r⁸)Λcan be resolved atq/(π₁⁸, …, π_r⁸)Λ, thenR → A → Λ ⊃ qcan be resolved.
theorem canBeResolved_of_quotient_eighthPowerIdeal
(S : LocalSmoothingSituation.{u, v, w})
{r : ℕ} (hr : 1 ≤ r) (π : Fin r → S.R)
(hπq : ∀ i, algebraMap S.R S.Λ (π i) ∈ S.q)
(hannR : ∀ i,
let I := eighthPowerPrefixIdeal π i
(Submodule.span (S.R ⧸ I) {Ideal.Quotient.mk I (π i)}).annihilator =
(Submodule.span (S.R ⧸ I) {(Ideal.Quotient.mk I (π i)) ^ 2}).annihilator)
(hannΛ : ∀ i,
let I := Ideal.map (algebraMap S.R S.Λ) (eighthPowerPrefixIdeal π i)
(Submodule.span (S.Λ ⧸ I)
{Ideal.Quotient.mk I (algebraMap S.R S.Λ (π i))}).annihilator =
(Submodule.span (S.Λ ⧸ I)
{(Ideal.Quotient.mk I (algebraMap S.R S.Λ (π i))) ^ 2}).annihilator)
(hstandard : ∀ i,
IsStrictlyStandard (R := S.R) (A := S.A) (algebraMap S.R S.A (π i)))
(hresolve :
let I := eighthPowerIdeal π
let IA := Ideal.map (algebraMap S.R S.A) I
let IΛ := Ideal.map (algebraMap S.A S.Λ) IA
letI : Algebra (S.R ⧸ I) (S.Λ ⧸ IΛ) :=
((algebraMap (S.A ⧸ IA) (S.Λ ⧸ IΛ)).comp
(algebraMap (S.R ⧸ I) (S.A ⧸ IA))).toAlgebra
letI : IsScalarTower (S.R ⧸ I) (S.A ⧸ IA) (S.Λ ⧸ IΛ) :=
IsScalarTower.of_algebraMap_eq (fun _ => rfl)
CanBeResolved
(S.R ⧸ I) (S.A ⧸ IA) (S.Λ ⧸ IΛ)
(Ideal.map (Ideal.Quotient.mk IΛ) S.q)) :
S.CanBeResolved
Tag 07F9, a lemma
Tag 07F9 in the Stacks Project.
Stacks.Smoothing.exists_finitePresentation_factorization_singularIdeal_not_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SpreadingOutResolutions.lean, line 1306.
Stacks 07F9. Let
R → A → Λ ⊃ qbe a local smoothing situation,p = R ∩ q. Ifqis minimal over𝔥_Aand the localized chainR_p → A_p → Λ_q ⊃ q Λ_qcan be resolved, then there is a factorizationA → C → ΛwithCof finite presentation overRandH_{C/R} Λ ⊄ q.
theorem exists_finitePresentation_factorization_singularIdeal_not_le
(S : LocalSmoothingSituation.{u, v, w})
(_hq : S.q ∈ S.radicalSingularIdealExtension.minimalPrimes)
(hresolve : S.IsResolvableAfterLocalizing) :
∃ (Cr : Type (max u v w)) (_ : CommRing Cr) (_ : Algebra S.R Cr) (_ : Algebra S.A Cr)
(_ : Algebra Cr S.Λ),
IsScalarTower S.R S.A Cr ∧ IsScalarTower S.A Cr S.Λ ∧ IsScalarTower S.R Cr S.Λ ∧
Algebra.FinitePresentation S.R Cr ∧
¬ Ideal.map (algebraMap Cr S.Λ) (singularIdeal S.R Cr) ≤ S.q
Tag 07FA, a lemma
Tag 07FA in the Stacks Project.
Stacks.Smoothing.canBeResolved_of_localization_dim_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ZeroDimensionalResolution.lean, line 556.
Stacks 07FA. Let
R → A → Λ ⊃ qbe a local smoothing situation withqminimal over𝔥_A = √(H_{A/R} Λ). If the localized chainR_p → A_p → Λ_q ⊃ q Λ_qcan be resolved andΛ_qhas Krull dimension zero, thenR → A → Λ ⊃ qcan be resolved.
theorem canBeResolved_of_localization_dim_zero (S : LocalSmoothingSituation.{u, v, w})
(hq : S.q ∈ S.radicalSingularIdealExtension.minimalPrimes)
(hresolve : S.IsResolvableAfterLocalizing)
(hdim : ringKrullDim (Localization.AtPrime S.q) = 0) : S.CanBeResolved
Sources
Section16.10 Separable residue fields#
Section 16.10 of the Stacks Project, Tag 07FB. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07FC, a lemma
Tag 07FC in the Stacks Project.
ogoma_ker_eq_of_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/OgomaKernelStabilization.lean, line 66.
Stacks Tag 07FC (Ogoma's lemma). Over a Noetherian ring
A, for a finiteA-moduleM, a multiplicative subsetSandπ : A, if multiplication byπandπ²have the same kernel on the localizationS⁻¹M, then there is a singles ∈ Ssuch that for alln > 0, multiplication bysⁿπand(sⁿπ)²have the same kernel onM.
theorem ogoma_ker_eq_of_localization {A M : Type*} [CommRing A] [AddCommGroup M] [Module A M]
[IsNoetherianRing A] [Module.Finite A M] (S : Submonoid A) (π : A)
(h : LinearMap.ker (LinearMap.lsmul A (LocalizedModule S M) π)
= LinearMap.ker (LinearMap.lsmul A (LocalizedModule S M) (π ^ 2))) :
∃ s ∈ S, ∀ n : ℕ, 0 < n →
LinearMap.ker (LinearMap.lsmul A M (s ^ n * π))
= LinearMap.ker (LinearMap.lsmul A M ((s ^ n * π) ^ 2))
Tag 07FD, a lemma
Tag 07FD in the Stacks Project.
Stacks.Smoothing.exists_parameters_pow_mem_and_annihilator_sq_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ParametersWithPowersInIdeal.lean, line 214.
Stacks 07FD. Let
Λbe a Noetherian ring, letIandqbe ideals ofΛwithqprime, and letn,ebe positive integers. Assume that the extension ofq ^ ntoΛ_qis contained in the extension ofI, and thatΛ_qis a regular local ring of dimensiond. Then there areπ₁, …, π_d ∈ Λsuch that(π₁, …, π_d) Λ_q = q Λ_q, such thatπ_i ^ n ∈ Ifor everyi, and such that for everyithe annihilator ofπ_iinΛ ⧸ (π₁ ^ e, …, π_{i-1} ^ e)is the annihilator ofπ_i ^ 2.
theorem exists_parameters_pow_mem_and_annihilator_sq_eq
(Λ : Type*) [CommRing Λ] [IsNoetherianRing Λ] (I q : Ideal Λ) [q.IsPrime]
(n e d : ℕ) (hn : 0 < n) (he : 0 < e)
(hqI : Ideal.map (algebraMap Λ (Localization.AtPrime q)) (q ^ n) ≤
Ideal.map (algebraMap Λ (Localization.AtPrime q)) I)
[IsRegularLocalRing (Localization.AtPrime q)]
(hd : ringKrullDim (Localization.AtPrime q) = d) :
∃ π : Fin d → Λ,
Ideal.map (algebraMap Λ (Localization.AtPrime q)) (Ideal.span (Set.range π)) =
Ideal.map (algebraMap Λ (Localization.AtPrime q)) q ∧
(∀ i : Fin d, π i ^ n ∈ I) ∧
(∀ i : Fin d, ∀ x : Λ ⧸ Ideal.span
(Set.range fun j : Fin i.1 => π (j.castLE (Nat.le_of_lt i.2)) ^ e),
x * Ideal.Quotient.mk _ (π i) = 0 ↔ x * Ideal.Quotient.mk _ (π i ^ 2) = 0)
Tag 07FE, a lemma
Tag 07FE in the Stacks Project.
Stacks.Smoothing.canBeResolved_of_isRegularLocalRing_of_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/SeparableResidueFieldResolution/RegularSeparableResolution.lean, line 83.
Stacks 07FE. Let
k → A → Λ ⊃ qbe a local smoothing situation over a fieldkwithΛNoetherian,qminimal over𝔥_A = √(H_{A/k} Λ),Λ_qa regular local ring and the residue field extensionκ(q)/kseparable. Then the chain can be resolved atq.
theorem canBeResolved_of_isRegularLocalRing_of_isSeparableExtension
(k : Type u) (A : Type v) (Lambda : Type w)
[Field k] [CommRing A] [CommRing Lambda]
[Algebra k A] [Algebra k Lambda] [Algebra A Lambda]
[IsScalarTower k A Lambda] [Algebra.FinitePresentation k A]
[IsNoetherianRing Lambda] (q : Ideal Lambda) [q.IsPrime]
(hq : (Ideal.map (algebraMap A Lambda)
(Stacks.Smoothing.singularIdeal k A)).radical.IsMinimalPrime q)
[IsRegularLocalRing (Localization.AtPrime q)]
[Algebra.IsSeparableExtension k q.ResidueField] :
CanBeResolved k A Lambda q
Sources
Section16.11 Inseparable residue fields#
Section 16.11 of the Stacks Project, Tag 07FF. 30 tags here are carried by 42 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07FG, a lemma
Tag 07FG in the Stacks Project.
Stacks.Smoothing.nonempty_coefficientSectionData_of_finite_h1Cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/InseparableResidueField/CentralClaim.lean, line 634. The attribute's comment: “The central claim of the source's proof, the only place where char k = p and dim H₁(L_{K/k}) < ∞ are used: there exist a ring-theoretic section σ : K → Λ of the residue map, generators λ₁, …, λ_d of 𝔪, and a finitely generated k ⊆ F₀ ⊆ K with the image of k in Λ contained in Ψ_σ(F₀[λ₁, …, λ_d]). The source's induction on the nilpotency order of 𝔪 is followed, including the correction of σ by a derivation K → 𝔪^{n-1} read off the Jacobi-Zariski sequence. NOT covered: the conclusion of the lemma, which is proved from this claim in exists_directedOn_flat_essFiniteType.”.
Stacks 07FG, the central claim of its proof: the data of
CoefficientSectionDataexists for every Artinian local algebra over a field of characteristicp > 0whose residue field extension hasdim_K H₁(L_{K/k}) < ∞.No finiteness is assumed of the residue field extension itself; the transcendence degree of
Koverkmay be infinite.
theorem nonempty_coefficientSectionData_of_finite_h1Cotangent {k Λ : Type*} [Field k]
[CommRing Λ] [Algebra k Λ] [IsArtinianRing Λ] [IsLocalRing Λ] (p : ℕ) [Fact p.Prime]
[CharP k p] [Module.Finite (ResidueField Λ) (Algebra.H1Cotangent k (ResidueField Λ))] :
Nonempty (CoefficientSectionData k Λ)
Stacks.Smoothing.exists_directedOn_flat_essFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/InseparableResidueField/CentralClaim.lean, line 665. The attribute's comment: “The lemma, under the source's own hypotheses and nothing else: char k = p > 0, Λ an Artinian local k-algebra, and dim H₁(L_{K/k}) < ∞, with no finiteness assumed of K/k. The conclusion is read in the directed-union form in which the source itself reads it (flatness of A → Λ out of a local ring makes it injective, as the source's first line observes): the approximating subalgebras are the stages Ψ_σ(F[λ]) for finitely generated F₀ ≤ F ≤ K, and they are Artinian local k-subalgebras of Λ, essentially of finite type over k, with Λ flat (indeed free) over each and with 𝔪_A Λ = 𝔪, and they are directed and cover Λ. The section σ and the finitely generated F₀ are produced by the source's induction on the nilpotency order of 𝔪 in nonempty_coefficientSectionData_of_finite_h1Cotangent, the only place where char k = p and dim H₁(L_{K/k}) < ∞ are used; the properties of the stages are exists_directedOn_flat_essFiniteType_of_coefficientSectionData.”.
Stacks 07FG. Let
kbe a field of characteristicp > 0and let(Λ, 𝔪, K)be an Artinian localk-algebra withdim_K H₁(L_{K/k}) < ∞. Then there is a directed family𝒜ofk-subalgebras ofΛwhich coversΛ— so thatΛis the filtered colimit of𝒜— each memberAof which is Artinian local, is essentially of finite type overk, hasΛflat over it, and satisfies𝔪_A Λ = 𝔪.
theorem exists_directedOn_flat_essFiniteType {k Λ : Type*} [Field k] [CommRing Λ]
[Algebra k Λ] [IsArtinianRing Λ] [IsLocalRing Λ] (p : ℕ) [Fact p.Prime] [CharP k p]
[Module.Finite (ResidueField Λ) (Algebra.H1Cotangent k (ResidueField Λ))] :
∃ 𝒜 : Set (Subalgebra k Λ), DirectedOn (· ≤ ·) 𝒜 ∧ (∀ y : Λ, ∃ A ∈ 𝒜, y ∈ A) ∧
∀ A ∈ 𝒜, ∃ (_ : IsArtinianRing A) (_ : IsLocalRing A),
Module.Flat A Λ ∧ Algebra.EssFiniteType k A ∧
Ideal.map A.val.toRingHom (maximalIdeal A) = maximalIdeal Λ
Stacks.Smoothing.exists_directedOn_flat_essFiniteType_of_charP, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/InseparableResidueField/CentralClaim.lean, line 681. The attribute's comment: “The lemma, under the source's own hypotheses: the statement of exists_directedOn_flat_essFiniteType, to which this reduces, under the name used for it in the documentation of the Stacks 07FH material in the second half of this file.”.
Stacks 07FG, under the name used for it in the documentation of the Stacks 07FH material in the second half of this file. The statement is that of
exists_directedOn_flat_essFiniteType.
alias exists_directedOn_flat_essFiniteType_of_charP
Stacks.Smoothing.exists_coefficientStage_basis_kaehlerDifferential_primePowerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/InseparableResidueField/FlatLocalization.lean, line 85. The attribute's comment: “A strengthening of the central claim of the source's proof, needed by Stacks 07FH and not proved there. 07FH picks λ₁, …, λ_t ∈ Λ whose images lie in the approximating subalgebra A ⊆ Λ_𝔮/𝔮^nΛ_𝔮 of 07FG and whose differentials form a basis of Ω_{F/k} for F = A/𝔪_A; no argument is given, A is never enlarged afterwards, and for a general member of the directed family the residues of elements of Λ lying in F do not generate F. With Λ/𝔮 = k[x, y], so K = k(x, y), and F = k(x/y) one has F ∩ k[x, y] = k, because a nonconstant element of k(x/y) is homogeneous of degree 0, so the differentials of the residues of Λ lying in F span 0 ≠ Ω_{F/k}; and by exists_subalgebra_residueField_image_eq_of_charP every finitely generated subfield of K above a bound does occur as A/𝔪_A. What is added here is that the section σ and the generators λ of 𝔪 may be chosen so that the coefficient field is generated by residues of elements of Λ — it is k(Ȳ) for a finite Y ⊆ Λ containing any prescribed finite set, with the images of all elements of Y inside the stage — whence a basis of Ω_{k(Ȳ)/k} among the differentials of residues of elements of Λ whose images lie in the stage. NOT covered: flatness of Λ_𝔮/𝔮^nΛ_𝔮 over this particular stage, which exists_stage supplies only for coefficient fields large enough to contain the b-coordinates of the generators of 𝔪.”.
The λ-choice of Stacks 07FH, in the setting of that lemma. Let
kbe a field of characteristicp > 0, letΛbe a Noetheriank-algebra, let𝔮be a prime ofΛ, letn ≥ 1and assumedim_K H₁(L_{K/k}) < ∞for the residue fieldK = κ(𝔮)ofΛ̄ = Λ_𝔮/𝔮^nΛ_𝔮. Then for every finite subsetSofΛthere are a ring-theoretic sectionσ : K → Λ̄of the residue map, generatorsλ₁, …, λ_dof the maximal ideal ofΛ̄, a finiteS ⊆ Y ⊆ Λand elementsμ₁, …, μ_tofYsuch that the stageA = Ψ_σ(F[λ₁, …, λ_d])of the coefficient fieldF = k(ȳ : y ∈ Y)contains the image ofkand the images of all elements ofY, has residue image exactlyF, and hasdμ̄₁, …, dμ̄_ta basis ofΩ_{F/k}.The hypothesis of
exists_coefficientStage_basis_kaehlerDifferentialon the mapΛ → Λ̄is automatic here:κ(𝔮)is the fraction field ofΛ/𝔮.
theorem exists_coefficientStage_basis_kaehlerDifferential_primePowerQuotient {k Λ : Type*}
[Field k] [CommRing Λ] [Algebra k Λ] [IsNoetherianRing Λ] (𝔮 : Ideal Λ) [𝔮.IsPrime] {n : ℕ}
[IsLocalRing (primePowerQuotient 𝔮 n)] (p : ℕ) [Fact p.Prime] [CharP k p]
[Module.Finite (ResidueField (primePowerQuotient 𝔮 n))
(Algebra.H1Cotangent k (ResidueField (primePowerQuotient 𝔮 n)))] (S : Finset Λ) :
∃ (Y : Finset Λ) (σ : ResidueField (primePowerQuotient 𝔮 n) →+* primePowerQuotient 𝔮 n)
(d : ℕ) (x : Fin d → primePowerQuotient 𝔮 n)
(F : IntermediateField k (ResidueField (primePowerQuotient 𝔮 n))) (t : ℕ) (lam : Fin t → Λ)
(hlam : ∀ j, residue (primePowerQuotient 𝔮 n)
(algebraMap Λ (primePowerQuotient 𝔮 n) (lam j)) ∈ F),
S ⊆ Y ∧ (∀ j, lam j ∈ Y) ∧ (∀ c, residue (primePowerQuotient 𝔮 n) (σ c) = c) ∧
Ideal.span (Set.range x) = maximalIdeal (primePowerQuotient 𝔮 n) ∧
F = IntermediateField.adjoin k ((fun y => residue (primePowerQuotient 𝔮 n)
(algebraMap Λ (primePowerQuotient 𝔮 n) y)) '' (Y : Set Λ)) ∧ F.FG ∧
(∀ a : k, algebraMap k (primePowerQuotient 𝔮 n) a ∈ coefficientStage σ F x) ∧
(∀ y ∈ Y, algebraMap Λ (primePowerQuotient 𝔮 n) y ∈ coefficientStage σ F x) ∧
(∀ z ∈ coefficientStage σ F x, residue (primePowerQuotient 𝔮 n) z ∈ F) ∧
∃ b : Module.Basis (Fin t) F (Ω[F⁄k]), ∀ j, b j = KaehlerDifferential.D k F
⟨residue (primePowerQuotient 𝔮 n) (algebraMap Λ (primePowerQuotient 𝔮 n) (lam j)),
hlam j⟩
Tag 07FH, a lemma
Tag 07FH in the Stacks Project.
Stacks.Smoothing.exists_mvPolynomial_factorization_isEssentiallySmooth_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/InseparableResidueField/EssentiallySmoothFactorization.lean, line 257. The attribute's comment: “clause (2), UNCONDITIONALLY: no hypothesis on κ(𝔮) beyond the tag's own (Λ Noetherian and geometrically regular over k); the characteristic hypothesis is not needed either. essentially smooth is RingHom.IsEssentiallySmooth (essentially of finite presentation, Tag 00QM (2), plus formally smooth); the Stacks Project uses the term here and in the two following lemmas without ever defining it, and this repository supplies the definition those proofs need, in StacksFrontier.RingTheory.Smoothing.EssentiallySmooth. WHAT IS PROVED: m and φ : k[y_1, …, y_m] → Λ with 𝔭 = φ^{-1}(𝔮), the ideal identity 𝔭Λ_𝔮 = 𝔮Λ_𝔮, flatness of g : k[y]_𝔭 → Λ_𝔮, a local Artinian subring D of Λ̄ = Λ_𝔮/𝔮^nΛ_𝔮 and a factorization of the induced map u : k[y]_𝔭/𝔭^n → Λ̄ as an essentially smooth map into D followed by the inclusion D → Λ̄, which is flat. HOW: clause (2) on its own needs no approximating subring at either end. Clause (1), exists_mvPolynomial_flat_localization, is unconditional and supplies φ with 𝔭Λ_𝔮 = 𝔮Λ_𝔮 and k[y]_𝔭 → Λ_𝔮 flat; hence 𝔭^n Λ_𝔮 = 𝔮^n Λ_𝔮, so u is the base change of a flat map along k[y]_𝔭 → k[y]_𝔭/𝔭^n and is flat, and u is a local homomorphism of local rings, hence faithfully flat (Module.FaithfullyFlat.of_flat_of_isLocalHom), hence INJECTIVE. So D = range u is a local Artinian subring of Λ̄, u restricts to an isomorphism onto it — essentially smooth, a bijective ring map being so — and D → Λ̄ is flat because u is. The source instead draws D from the directed family of Stacks 07FG, because it proves clause (3) at the same time: the approximating subring is needed for E ⊆ D, and that is where the source's unjustified λ-choice sits. WHAT REMAINS: clause (2) alone places no element inside D, so it is Stacks 07FT's joint use of clauses (2) AND (3) that carries the difficulty; see exists_mvPolynomial_factorization_mem_isEssentiallySmooth_flat, which is still conditional.”.
Stacks 07FH, clause (2), in the generality of the tag. Let
kbe a field, letΛbe a Noetherian geometrically regulark-algebra, let𝔮be a prime ofΛand letn ≥ 1. Then there arem ≥ 0and ak-algebra mapφ : k[y_1, …, y_m] → Λsuch that, with𝔭 = φ^{-1}(𝔮), one has𝔭 Λ_𝔮 = 𝔮 Λ_𝔮withg : k[y_1, …, y_m]_𝔭 → Λ_𝔮flat, and the mapk[y_1, …, y_m]_𝔭/𝔭^n → Λ_𝔮/𝔮^nΛ_𝔮induced bygfactors through a local Artinian subringDofΛ_𝔮/𝔮^nΛ_𝔮by an essentially smooth map followed by the inclusion ofD, which is flat."Essentially smooth" is
RingHom.IsEssentiallySmooth: essentially of finite presentation (Tag 00QM (2)) and formally smooth. The Stacks Project never defines the term; seeStacksFrontier/RingTheory/Smoothing/EssentiallySmooth.lean.
theorem exists_mvPolynomial_factorization_isEssentiallySmooth_flat
{k Λ : Type u} [Field k] [CommRing Λ] [Algebra k Λ] [IsNoetherianRing Λ]
[Algebra.IsGeometricallyRegular k Λ] (𝔮 : Ideal Λ) [𝔮.IsPrime]
{n : ℕ} (hn : 1 ≤ n) :
∃ (m : ℕ) (φ : MvPolynomial (Fin m) k →ₐ[k] Λ)
(g : Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮) →+* Localization.AtPrime 𝔮)
(u : primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n →+* primePowerQuotient 𝔮 n)
(D : Subring (primePowerQuotient 𝔮 n))
(a : primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n →+* D),
Ideal.map ((algebraMap Λ (Localization.AtPrime 𝔮)).comp φ.toRingHom)
(Ideal.comap φ.toRingHom 𝔮)
= Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) 𝔮 ∧
(∀ f, g (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)) f)
= algebraMap Λ (Localization.AtPrime 𝔮) (φ f)) ∧
g.Flat ∧
(∀ y, u (Ideal.Quotient.mk (Ideal.map (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)))
(Ideal.comap φ.toRingHom 𝔮 ^ n)) y)
= Ideal.Quotient.mk (Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n))
(g y)) ∧
(∀ z, (a z : primePowerQuotient 𝔮 n) = u z) ∧
∃ (_ : IsLocalRing D) (_ : IsArtinianRing D),
a.IsEssentiallySmooth ∧ D.subtype.Flat
Stacks.Smoothing.exists_mvPolynomial_flat_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/InseparableResidueField/FlatLocalization.lean, line 231. The attribute's comment: “clause (1), unconditionally. The source's choice of λ_1, …, λ_t ∈ Λ whose differentials form a basis of Ω_{F/k} for the residue field F of an approximating subalgebra A ⊆ Λ_𝔮/𝔮^nΛ_𝔮 of Stacks 07FG is not justified by the source's TEXT, which fixes A by 07FG and only afterwards asks for the λ, never enlarging A again: for SOME members of the directed family no such λ exist, the residues of those elements of Λ which land in F need not generate F (see the module docstring for the counterexample Λ/𝔮 = k[x, y], F = k(x/y)). That is all the counterexample shows. It says nothing against the source's ROUTE, since A may be chosen for the purpose rather than taken as given, and exists_coefficientStage_basis_kaehlerDifferential chooses it so. The choice is not needed for clause (1) in any case: the clause is the source's own construction specialized to F = k, where t = 0, the fibre of Λ_𝔮 over k is Λ_𝔮 itself, and λ_1, …, λ_m is a regular system of parameters of Λ_𝔮 lifted to 𝔮. What the λ-choice is needed for is the essential smoothness in clause (2); only regularity of Λ_𝔮, not geometric regularity, is used here. 𝔭 Λ_𝔮 = 𝔮 Λ_𝔮 is the stated equality of extended ideals and the flat arrow is the unique g with g ∘ (k[y] → k[y]_𝔭) = (k[y] → Λ → Λ_𝔮), flatness being RingHom.Flat. The source proves this from Lemma 07E6 and More on Algebra 15.36.2; the route here is miracle flatness, Lemma 00R4.”.
Stacks 07FH, clause (1). Let
kbe a field, letΛbe a Noetheriank-algebra which is geometrically regular overkand let𝔮be a prime ofΛ. Then there arem ≥ 0and ak-algebra mapφ : k[y_1, …, y_m] → Λsuch that, with𝔭 = φ^{-1}(𝔮), one has𝔭 Λ_𝔮 = 𝔮 Λ_𝔮and the induced local mapk[y_1, …, y_m]_𝔭 → Λ_𝔮is flat.
theorem exists_mvPolynomial_flat_localization {k Λ : Type u} [Field k] [CommRing Λ] [Algebra k Λ]
[IsNoetherianRing Λ] [Algebra.IsGeometricallyRegular k Λ] (𝔮 : Ideal Λ) [𝔮.IsPrime] :
∃ (m : ℕ) (φ : MvPolynomial (Fin m) k →ₐ[k] Λ)
(g : Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮) →+* Localization.AtPrime 𝔮),
Ideal.map ((algebraMap Λ (Localization.AtPrime 𝔮)).comp φ.toRingHom)
(Ideal.comap φ.toRingHom 𝔮)
= Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) 𝔮 ∧
(∀ f, g (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)) f)
= algebraMap Λ (Localization.AtPrime 𝔮) (φ f)) ∧
g.Flat
Stacks.Smoothing.exists_mvPolynomial_factorization_mem_isEssentiallySmooth_flat_of_charP, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/InseparableResidueField/GlobalStage.lean, line 718. The attribute's comment: “All three clauses, in the generality of the tag: no hypothesis on κ(𝔮) beyond the tag's own (Λ Noetherian and geometrically regular over a field k of characteristic p, 𝔮 a prime, n ≥ 1, E a finite subset of Λ_𝔮/𝔮^nΛ_𝔮). Clause (1) is the ideal identity 𝔭Λ_𝔮 = 𝔮Λ_𝔮 together with flatness of k[y]_𝔭 → Λ_𝔮; clause (2) is the factorization of k[y]_𝔭/𝔭^n → Λ_𝔮/𝔮^nΛ_𝔮 through a local Artinian subring D by an essentially smooth map followed by a flat one; clause (3) is E ⊆ D. Essentially smooth' is RingHom.IsEssentiallySmooth: essentially of finite presentation (Tag 00QM (2)) and formally smooth; the Stacks Project never defines the term. The λ-choice of the source's proof is not justified by its text and is false for a general member of the directed family of 07FG; the repair implemented here is due to Brian Nugent and is described in the module docstring and inexists_global_stage_primePowerQuotient`.”.
Stacks 07FH, all three clauses, in the generality of the tag. Let
kbe a field of characteristicp > 0, letΛbe a Noetherian geometrically regulark-algebra, let𝔮be a prime ofΛ, letn ≥ 1and letEbe a finite subset ofΛ̄ = Λ_𝔮/𝔮^nΛ_𝔮. Then there arem ≥ 0and ak-algebra mapφ : k[y_1, …, y_m] → Λsuch that, with𝔭 = φ^{-1}(𝔮):
𝔭 Λ_𝔮 = 𝔮 Λ_𝔮and the induced local mapg : k[y_1, …, y_m]_𝔭 → Λ_𝔮is flat — clause (1);- the map
u : k[y_1, …, y_m]_𝔭/𝔭^n → Λ̄induced bygfactors through a local Artinian subringDofΛ̄as an essentially smooth mapafollowed by the inclusion ofD, which is flat — clause (2);E ⊆ D— clause (3).No hypothesis is placed on
κ(𝔮). The proof of clause (3) is Brian Nugent's: seeexists_global_stage_primePowerQuotientfor his repair of the λ-choice, which the source's text leaves unjustified and which is false for a general member of the directed family of Stacks 07FG (two counterexamples are recorded in the implementation notes, the second of them his). The two ingredients are that the generating family of𝔪_Λ̄used to build the approximating subalgebraDis kept GLOBAL — chosen in𝔮 ⊆ Λonce and for all, so thatexists_stagestill grants freeness and the fibre's regular parameters can be extracted from it as a subfamily by Nakayama — and that the coefficient field is pushed up to one generated by residues of global elementss^P,a·s^{P-1}whose images lie inσ(F), whereσ(f) = q(a)/q(s)is an exact relation inΛ̄andPis ap-power at leastn. The pairs^P,a·s^{P-1}generates what neither member does: their residues areα^Pandf·α^P, of ratiof.
theorem exists_mvPolynomial_factorization_mem_isEssentiallySmooth_flat_of_charP
{k Λ : Type u} [Field k] [CommRing Λ] [Algebra k Λ] [IsNoetherianRing Λ]
[Algebra.IsGeometricallyRegular k Λ] (𝔮 : Ideal Λ) [𝔮.IsPrime] (p : ℕ) [Fact p.Prime]
[CharP k p] {n : ℕ} (hn : 1 ≤ n) (E : Finset (primePowerQuotient 𝔮 n)) :
∃ (m : ℕ) (φ : MvPolynomial (Fin m) k →ₐ[k] Λ)
(g : Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮) →+* Localization.AtPrime 𝔮)
(u : primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n →+* primePowerQuotient 𝔮 n)
(D : Subring (primePowerQuotient 𝔮 n))
(a : primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n →+* D),
Ideal.map ((algebraMap Λ (Localization.AtPrime 𝔮)).comp φ.toRingHom)
(Ideal.comap φ.toRingHom 𝔮)
= Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) 𝔮 ∧
(∀ f, g (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)) f)
= algebraMap Λ (Localization.AtPrime 𝔮) (φ f)) ∧
g.Flat ∧
(∀ y, u (Ideal.Quotient.mk (Ideal.map (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)))
(Ideal.comap φ.toRingHom 𝔮 ^ n)) y)
= Ideal.Quotient.mk (Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n))
(g y)) ∧
(∀ z, (a z : primePowerQuotient 𝔮 n) = u z) ∧
(∀ x ∈ E, x ∈ D) ∧
∃ (_ : IsLocalRing D) (_ : IsArtinianRing D),
a.IsEssentiallySmooth ∧ D.subtype.Flat
Tag 07FI, a lemma
Tag 07FI in the Stacks Project.
Stacks.Smoothing.exists_essentiallySmooth_enlargement_containing_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/EssentiallySmoothEnlargement.lean, line 633. The attribute's comment: “the setup as in Lemma 07FH carried as the part of that lemma's data the conclusion speaks about; the left-hand map is omitted, which strengthens the statement, and the source's λ ∉ 𝔮 is not assumed — see the implementation notes”.
Stacks 07FI. Let
kbe a field of characteristicp > 0, letΛbe ak-algebra, let𝔮 ⊆ Λbe a prime andn : ℕ, and supposeΛ_𝔮/𝔮ⁿΛ_𝔮is Artinian local — as it is in the situation of Lemma 07FH. LetDbe an Artinian local ring with a flat local mapb : D → Λ_𝔮/𝔮ⁿΛ_𝔮, the right-hand half of the factorization produced by that lemma. Then for everyλ ∈ Λthere is an integere > 0and a factorizationD → D' → Λ_𝔮/𝔮ⁿΛ_𝔮ofbsuch thatD → D'is an essentially smooth local map of Artinian local rings,D' → Λ_𝔮/𝔮ⁿΛ_𝔮is flat and local, andλ ^ eis in the image ofD'. Composing with the source'sk[y₁,…,y_m]_𝔭/𝔭ⁿ → Dgives the displayed four-term factorization.
theorem exists_essentiallySmooth_enlargement_containing_pow
(k : Type u) [Field k] (p : ℕ) [CharP k p] (hp : 0 < p)
(Λ : Type u) [CommRing Λ] [Algebra k Λ] (𝔮 : Ideal Λ) [𝔮.IsPrime] (n : ℕ)
[IsLocalRing (Localization.AtPrime 𝔮 ⧸
Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n))]
[IsArtinianRing (Localization.AtPrime 𝔮 ⧸
Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n))]
{D : Type u} [CommRing D] [IsLocalRing D] [IsArtinianRing D]
(b : D →+* (Localization.AtPrime 𝔮 ⧸
Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n)))
[IsLocalHom b] (hb : RingHom.Flat b) (lam : Λ) :
∃ (e : ℕ) (D' : Type u) (_ : CommRing D') (_ : IsLocalRing D') (_ : IsArtinianRing D')
(c : D →+* D') (b' : D' →+* (Localization.AtPrime 𝔮 ⧸
Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n)))
(_ : IsLocalHom c) (_ : IsLocalHom b'),
0 < e ∧ RingHom.IsEssentiallySmooth c ∧ RingHom.Flat b' ∧ b'.comp c = b ∧
∃ w : D', b' w = algebraMap Λ (Localization.AtPrime 𝔮 ⧸
Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n)) (lam ^ e)
Tag 07FJ, a lemma
Tag 07FJ in the Stacks Project.
Stacks.Smoothing.canBeResolvedInPositiveCharacteristic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/TwistedQuotientClosure.lean, line 291. The attribute's comment: “the lemma in full generality, with NO carried hypotheses: the whole of Situation 07F7 over a field of characteristic p > 0, with 𝔮 minimal over 𝔥_A, and the conclusion CanBeResolved k A Λ 𝔮. Its two inputs are both proved in this library. The first is item (9), Stacks 07FT, hasArtinianApproximationData; the second is items (22)-(26), Stacks 07G6-07GA, twistedQuotientLocallyResolvable. The λ-choice in the source's proof of Stacks 07FH, on which 07FT turns, is not justified by the source's text and is false for a general member of the directed family of 07FG; the repair is due to BRIAN NUGENT, and is implemented in exists_global_stage_primePowerQuotient.”.
Stacks 07FJ. Let
k → A → Λ ⊃ 𝔮be as in Situation 07F7 withkof characteristicp > 0,Aof finite presentation overk,ΛNoetherian and geometrically regular overk, and𝔮minimal over𝔥_A. Then the chain can be resolved at𝔮.This is
Stacks.Smoothing.canBeResolvedInPositiveCharacteristic_of_locallyResolvablewith both of its hypotheses discharged: item (9), Stacks 07FT, byStacks.Smoothing.hasArtinianApproximationData, and items (22)–(26) byStacks.Smoothing.twistedQuotientLocallyResolvableabove. Every one of the twenty-six items of the source's proof is therefore proved.
theorem canBeResolvedInPositiveCharacteristic : CanBeResolvedInPositiveCharacteristic.{u}
Tag 07FK, an item
Tag 07FK in the Stacks Project.
Stacks.Smoothing.LocalSmoothingSituation.exists_pos_map_pow_le_map_singularIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/MinimalSingularPrime.lean, line 60.
Stacks 07FK. In a local smoothing situation with
ΛNoetherian andqminimal over𝔥_A = √(H_{A/R} Λ), some positive power ofqextends intoH_{A/R} Λ_q.
theorem exists_pos_map_pow_le_map_singularIdeal [IsNoetherianRing S.Λ]
(hq : S.q ∈ S.radicalSingularIdealExtension.minimalPrimes) :
∃ N : ℕ, 0 < N ∧
Ideal.map (algebraMap S.Λ (Localization.AtPrime S.q)) (S.q ^ N) ≤
Ideal.map (algebraMap S.Λ (Localization.AtPrime S.q))
(Ideal.map (algebraMap S.A S.Λ) (singularIdeal S.R S.A))
Tag 07FL, an item
Tag 07FL in the Stacks Project.
Stacks.Smoothing.LocalSmoothingSituation.exists_fin_span_range_eq_singularIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/MinimalSingularPrime.lean, line 88.
Stacks 07FL. The singular ideal
H_{A/R}of a local smoothing situation is generated by finitely many elements ofA.
theorem exists_fin_span_range_eq_singularIdeal :
∃ (t : ℕ) (a : Fin t → S.A), Ideal.span (Set.range a) = singularIdeal S.R S.A
Tag 07FM, an item
Tag 07FM in the Stacks Project.
Stacks.Smoothing.LocalSmoothingSituation.exists_nat_eq_ringKrullDim_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/MinimalSingularPrime.lean, line 97.
Stacks 07FM. The Krull dimension of the localization
Λ_qof a local smoothing situation withΛNoetherian is a natural number.
theorem exists_nat_eq_ringKrullDim_localization [IsNoetherianRing S.Λ] :
∃ d : ℕ, ringKrullDim (Localization.AtPrime S.q) = (d : WithBot ℕ∞)
Tag 07FN, an item
Tag 07FN in the Stacks Project.
Stacks.Smoothing.parameterPowerIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ParameterPowerAlgebra.lean, line 51.
The ideal
(x_i^{2N} - Σ_j z_{ij} a_j : i = 1, …, d)of the polynomial ringA[x_1, …, x_d, z_{ij}], whose variables are indexed byFin d ⊕ Fin d × Fin tso thatx_i = X (Sum.inl i)andz_{ij} = X (Sum.inr (i, j)).
noncomputable def parameterPowerIdeal {A : Type v} [CommRing A] (d : ℕ) {t : ℕ} (N : ℕ)
(a : Fin t → A) : Ideal (MvPolynomial (Fin d ⊕ Fin d × Fin t) A)
Stacks.Smoothing.parameterPowerAlgebra, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ParameterPowerAlgebra.lean, line 61.
The algebra
B = A[x_1, …, x_d, z_{ij}]/(x_i^{2N} - Σ_j z_{ij} a_j): the algebraAwithdgeneric elementsx_iadjoined whose2N-th powers lie in the ideal generated bya_1, …, a_t.
abbrev parameterPowerAlgebra (A : Type v) [CommRing A] (d : ℕ) {t : ℕ} (N : ℕ)
(a : Fin t → A) : Type v
Tag 07FP, an item
Tag 07FP in the Stacks Project.
Stacks.Smoothing.exists_retraction_parameterPowerAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ParameterPowerAlgebra.lean, line 129.
Let
B = A[x_i, z_{ij}]/(x_i^{2N} - Σ_j z_{ij} a_j), viewed as ak[x_1, …, x_d]-algebra. There is a finite-typeB-algebraC, of finite presentation overk[x_1, …, x_d], with ak[x_1, …, x_d]-algebra retractionC → B, such that for eachb ∈ B: ifB_bis a local complete intersection overk[x_1, …, x_d], thenC_bis smooth overB_band has a presentation overk[x_1, …, x_d]with free conormal module; and ifB_bis smooth overk[x_1, …, x_d], then the module of differentials ofC_boverk[x_1, …, x_d]is free.
theorem exists_retraction_parameterPowerAlgebra (k : Type u) (A : Type v) [Field k] [CommRing A]
[Algebra k A] [Algebra.FiniteType k A] (d : ℕ) {t : ℕ} (N : ℕ) (a : Fin t → A) :
∃ (C : Type v) (_ : CommRing C) (_ : Algebra (MvPolynomial (Fin d) k) C)
(_ : Algebra (parameterPowerAlgebra A d N a) C)
(_ : IsScalarTower (MvPolynomial (Fin d) k) (parameterPowerAlgebra A d N a) C)
(_ : Algebra.FiniteType (parameterPowerAlgebra A d N a) C)
(_ : Algebra.FinitePresentation (MvPolynomial (Fin d) k) C)
(g : C →ₐ[MvPolynomial (Fin d) k] parameterPowerAlgebra A d N a),
g.comp (IsScalarTower.toAlgHom (MvPolynomial (Fin d) k)
(parameterPowerAlgebra A d N a) C) =
AlgHom.id (MvPolynomial (Fin d) k) (parameterPowerAlgebra A d N a) ∧
(∀ b : parameterPowerAlgebra A d N a,
RingHom.IsLocalCompleteIntersection
(algebraMap (MvPolynomial (Fin d) k) (Localization.Away b)) →
(letI : Algebra (Localization.Away b)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b)) :=
(Localization.awayMap
(algebraMap (parameterPowerAlgebra A d N a) C) b).toAlgebra;
Algebra.Smooth (Localization.Away b)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b)) ∧
HasFreeConormalPresentation (MvPolynomial (Fin d) k)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b)))) ∧
(∀ b : parameterPowerAlgebra A d N a,
Algebra.Smooth (MvPolynomial (Fin d) k) (Localization.Away b) →
Module.Free (Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b))
(KaehlerDifferential (MvPolynomial (Fin d) k)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b))))
Tag 07FQ, an item
Tag 07FQ in the Stacks Project.
Stacks.Smoothing.exists_pos_isStrictlyStandard_X_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StrictlyStandardParameterPowers.lean, line 594.
Stacks 07FQ. Let
Abe of finite type over a fieldk, leta_1, …, a_tgenerate the singular idealH_{A/k}, and letCbe an algebra overB = A[x\_i, z\_\{ij}]/(x\_i^\{2N} - Σ\_j z\_\{ij} a\_j)with the two localization properties that Stacks 07FP supplies. Then some positive powerx_i^c, onecfor alli, is strictly standard inCoverk[x_1, …, x_d].
theorem exists_pos_isStrictlyStandard_X_pow (k : Type u) (A : Type v) [Field k] [CommRing A]
[Algebra k A] [Algebra.FiniteType k A] (d N : ℕ) {t : ℕ} (a : Fin t → A)
(ha : Ideal.span (Set.range a) = singularIdeal k A) (C : Type v) [CommRing C]
[Algebra (MvPolynomial (Fin d) k) C] [Algebra (parameterPowerAlgebra A d N a) C]
[IsScalarTower (MvPolynomial (Fin d) k) (parameterPowerAlgebra A d N a) C]
[Algebra.FinitePresentation (MvPolynomial (Fin d) k) C]
(hC₁ : ∀ b : parameterPowerAlgebra A d N a,
RingHom.IsLocalCompleteIntersection
(algebraMap (MvPolynomial (Fin d) k) (Localization.Away b)) →
(letI : Algebra (Localization.Away b)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b)) :=
(Localization.awayMap (algebraMap (parameterPowerAlgebra A d N a) C) b).toAlgebra
Algebra.Smooth (Localization.Away b)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b)) ∧
HasFreeConormalPresentation (MvPolynomial (Fin d) k)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b))))
(hC₂ : ∀ b : parameterPowerAlgebra A d N a,
Algebra.Smooth (MvPolynomial (Fin d) k) (Localization.Away b) →
Module.Free (Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b))
(KaehlerDifferential (MvPolynomial (Fin d) k)
(Localization.Away (algebraMap (parameterPowerAlgebra A d N a) C b)))) :
∃ c : ℕ, 0 < c ∧ ∀ i : Fin d, IsStrictlyStandard (R := MvPolynomial (Fin d) k)
(algebraMap (MvPolynomial (Fin d) k) C (MvPolynomial.X i) ^ c)
Tag 07FR, an item
Tag 07FR in the Stacks Project.
Stacks.Smoothing.resolutionTruncationOrder, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StrictlyStandardParameterPowers.lean, line 657.
Stacks 07FR. The order
n = N + dcto which the local ringΛ_qis truncated in the proof of Stacks 07FJ.
def resolutionTruncationOrder (N d c : ℕ) : ℕ
Stacks.Smoothing.resolutionPowerExponent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/StrictlyStandardParameterPowers.lean, line 663.
Stacks 07FR. The exponent
e = 8cused in the proof of Stacks 07FJ: it is eight times the exponentcmakingx_i^cstrictly standard, so thatγ_i^e = (γ_i^c)^8is the eighth power required by Stacks 07F8.
def resolutionPowerExponent (c : ℕ) : ℕ
Tag 07FS, an item
Tag 07FS in the Stacks Project.
Stacks.Smoothing.exists_finset_primePowerQuotient_eq_image_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianApproximationData.lean, line 75. The attribute's comment: “Item 8 of the proof of Stacks 07FJ. E is produced as a Finset of Λ_𝔮/𝔮^nΛ_𝔮, which is the shape in which clause (3) of Stacks 07FH consumes it; the generating family of A is a Finset because A is of finite type over k.”.
Stacks 07FS. Let
Abe ak-algebra of finite type mapping to a ringΛwith a prime𝔮, and letnbe an exponent. ThenAhas a finitek-algebra generating family whose image inΛ_𝔮/𝔮^nΛ_𝔮is a finite subset of that ring.
theorem exists_finset_primePowerQuotient_eq_image_generators (k : Type u) (A : Type v)
(Λ : Type w) [CommRing k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [CommRing Λ]
[Algebra A Λ] (𝔮 : Ideal Λ) [𝔮.IsPrime] (n : ℕ) :
∃ (s : Finset A) (E : Finset (primePowerQuotient 𝔮 n)),
Algebra.adjoin k (s : Set A) = ⊤ ∧
(E : Set (primePowerQuotient 𝔮 n)) =
toPrimePowerQuotient 𝔮 n '' (algebraMap A Λ '' (s : Set A))
Tag 07FT, an item
Tag 07FT in the Stacks Project.
Stacks.Smoothing.exists_mvPolynomial_localArtinianFactorization_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianApproximationData.lean, line 144. The attribute's comment: “Item 9 of the proof of Stacks 07FJ, stated for the class of objects on which clauses (2) and (3) of Stacks 07FH are available in this repository: Λ Noetherian and geometrically regular over the field k of characteristic p > 0, with the residue field κ(𝔮) of Λ_𝔮 essentially of finite type over k, equivalently a finitely generated field extension of k. That restriction on the objects is the one recorded by exists_mvPolynomial_factorization_mem_isEssentiallySmooth_flat, which this theorem repackages; outside it clause (2) is open in this repository, the source's choice of λ_1, …, λ_t being unjustified as written and the natural repair provably destroying the flatness the argument needs — for the counterexample k = 𝐅_p, Λ̄ = k(v)[ε]/ε² see StacksFrontier.RingTheory.Smoothing.InseparableResidueField. Clause (1), the flat g with 𝔭Λ_𝔮 = 𝔮Λ_𝔮, needs no such restriction and is repeated here because the item states it. WHAT IS PROVED: the source's m, φ : k[y_1, …, y_m] → Λ, 𝔭 = φ^{-1}(𝔮), the flat g : k[y]_𝔭 → Λ_𝔮 compatible with φ, the ideal identity 𝔭Λ_𝔮 = 𝔮Λ_𝔮, and the factorization of the induced u : k[y]_𝔭/𝔭^n → Λ̄ as the equation D.subtype ∘ a = u of ring maps, with a essentially smooth, D.subtype flat and each of k[y]_𝔭/𝔭^n, D and Λ̄ local Artinian, which is the source's factorization by local Artinian rings. The source's E ⊆ D mod 𝔮^nΛ_𝔮 is ∀ e ∈ E, e ∈ D, E being a finite subset of Λ_𝔮/𝔮^nΛ_𝔮 already.”.
Stacks 07FT. Let
kbe a field of characteristicp > 0, letΛbe a Noetherian geometrically regulark-algebra, let𝔮be a prime ofΛ, letn ≥ 1and letEbe a finite subset ofΛ̄ = Λ_𝔮/𝔮^nΛ_𝔮. Then there aremand ak-algebra mapφ : k[y_1, …, y_m] → Λsuch that, with𝔭 = φ^{-1}(𝔮), the induced local mapg : k[y_1, …, y_m]_𝔭 → Λ_𝔮is flat with𝔭Λ_𝔮 = 𝔮Λ_𝔮, and the mapu : k[y_1, …, y_m]_𝔭/𝔭^n → Λ̄induced bygfactors asD.subtype ∘ athrough a subringDofΛ̄containingE, withaessentially smooth andD.subtypeflat. All three rings of the factorization are local Artinian."Essentially smooth" is
RingHom.IsEssentiallySmooth: essentially of finite presentation (Tag 00QM (2)) and formally smooth; seeStacksFrontier/RingTheory/Smoothing/EssentiallySmooth.lean.
theorem exists_mvPolynomial_localArtinianFactorization_mem {k Λ : Type u} [Field k] [CommRing Λ]
[Algebra k Λ] [IsNoetherianRing Λ] [Algebra.IsGeometricallyRegular k Λ] (𝔮 : Ideal Λ)
[𝔮.IsPrime] (p : ℕ) [Fact p.Prime] [CharP k p]
[Algebra.EssFiniteType k (ResidueField (Localization.AtPrime 𝔮))] {n : ℕ} (hn : 1 ≤ n)
(E : Finset (primePowerQuotient 𝔮 n)) :
∃ (m : ℕ) (φ : MvPolynomial (Fin m) k →ₐ[k] Λ)
(g : Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮) →+* Localization.AtPrime 𝔮)
(u : primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n →+* primePowerQuotient 𝔮 n)
(D : Subring (primePowerQuotient 𝔮 n))
(a : primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n →+* D),
Ideal.map ((algebraMap Λ (Localization.AtPrime 𝔮)).comp φ.toRingHom)
(Ideal.comap φ.toRingHom 𝔮)
= Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) 𝔮 ∧
(∀ f, g (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)) f)
= algebraMap Λ (Localization.AtPrime 𝔮) (φ f)) ∧
g.Flat ∧
(∀ y, u (Ideal.Quotient.mk (Ideal.map (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)))
(Ideal.comap φ.toRingHom 𝔮 ^ n)) y)
= Ideal.Quotient.mk (Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) (𝔮 ^ n))
(g y)) ∧
D.subtype.comp a = u ∧
(∀ e ∈ E, e ∈ D) ∧
∃ (_ : IsLocalRing (primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n))
(_ : IsArtinianRing (primePowerQuotient (Ideal.comap φ.toRingHom 𝔮) n))
(_ : IsLocalRing (primePowerQuotient 𝔮 n))
(_ : IsArtinianRing (primePowerQuotient 𝔮 n))
(_ : IsLocalRing D) (_ : IsArtinianRing D),
a.IsEssentiallySmooth ∧ D.subtype.Flat
Stacks.Smoothing.hasArtinianApproximationData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianApproximationGeneral.lean, line 81. The attribute's comment: “The lemma in full generality: for every field k of characteristic p > 0, every Noetherian geometrically regular k-algebra Λ, every prime 𝔮 of Λ, every n ≥ 1 and every finite subset E of Λ_𝔮/𝔮^nΛ_𝔮, there are m and a k-algebra map φ : k[y_1, …, y_m] → Λ such that, with 𝔭 = φ⁻¹(𝔮), the induced local map k[y]_𝔭 → Λ_𝔮 is flat with 𝔭Λ_𝔮 = 𝔮Λ_𝔮, and the induced map k[y]_𝔭/𝔭^n → Λ_𝔮/𝔮^nΛ_𝔮 factors through a local Artinian subring D containing E by an essentially smooth map followed by a flat one. The three clauses of Stacks 07FH that this consumes are proved in Stacks.Smoothing.exists_mvPolynomial_factorization_mem_isEssentiallySmooth_flat_of_charP; the λ-choice of the source's proof of 07FH is not justified by its text and is false for a general member of the directed family of 07FG, and the repair is due to Brian Nugent.”.
Stacks 07FT in full generality, the predicate
Stacks.Smoothing.HasArtinianApproximationDataproved: for every fieldkof characteristicp > 0, every Noetherian geometrically regulark-algebraΛ, every prime𝔮ofΛ, everyn ≥ 1and every finite subsetEofΛ_𝔮/𝔮^nΛ_𝔮, the Artinian approximation data exist.This was item (9) of the proof of Stacks 07FJ, carried as a hypothesis there and in
Stacks.Smoothing.TwistedQuotientResolution. The λ-choice of Stacks 07FH, on which it turns, is not justified by the source's text; the repair implemented here is due to Brian Nugent.
theorem hasArtinianApproximationData : HasArtinianApproximationData.{u}
Tag 07FU, an item
Tag 07FU in the Stacks Project.
Stacks.Smoothing.exists_fin_mem_span_eq_maximalIdeal_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianApproximationData.lean, line 261. The attribute's comment: “Item 10 of the proof of Stacks 07FJ. d is dim Λ_𝔮 of item 07FM, and the first thing proved is that it is also dim k[y_1, …, y_m]_𝔭: 𝔭Λ_𝔮 = 𝔮Λ_𝔮 makes the fibre of g over the closed point a field, and g is flat, hence satisfies going down, so Stacks 00ON gives height 𝔮Λ_𝔮 = height 𝔭k[y]_𝔭 + 0. A polynomial ring over a field is regular, so k[y]_𝔭 is a regular local ring and its maximal ideal is generated by dim k[y]_𝔭 elements; each may be taken to be the image of an element of 𝔭, because an element of the maximal ideal of a localization is a unit multiple of such an image. d elements of 𝔭 whose images generate the maximal ideal of the d-dimensional regular local ring k[y]_𝔭 is exactly a regular system of parameters of k[y]_𝔭, and the dimension equality is part of the conclusion so that this reading is pinned down. The hypotheses are the part of item 07FT that the step uses: φ, the flat g compatible with φ, and the ideal identity.”.
Stacks 07FU. Let
𝔮be a prime of a Noetherian ringΛ, let𝔭be the contraction of𝔮along ak-algebra mapφ : k[y_1, …, y_m] → Λand suppose the induced mapg : k[y_1, …, y_m]_𝔭 → Λ_𝔮is flat with𝔭Λ_𝔮 = 𝔮Λ_𝔮. Ifd = dim Λ_𝔮, thendim k[y_1, …, y_m]_𝔭 = dand there areπ_1, …, π_d ∈ 𝔭whose images generate the maximal ideal ofk[y_1, …, y_m]_𝔭, that is, form a regular system of parameters of it.
theorem exists_fin_mem_span_eq_maximalIdeal_of_flat {k : Type u} [Field k] {Λ : Type v}
[CommRing Λ] [Algebra k Λ] [IsNoetherianRing Λ] (𝔮 : Ideal Λ) [𝔮.IsPrime] {m : ℕ}
(φ : MvPolynomial (Fin m) k →ₐ[k] Λ)
(g : Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮) →+* Localization.AtPrime 𝔮)
(hmap : Ideal.map ((algebraMap Λ (Localization.AtPrime 𝔮)).comp φ.toRingHom)
(Ideal.comap φ.toRingHom 𝔮)
= Ideal.map (algebraMap Λ (Localization.AtPrime 𝔮)) 𝔮)
(hg : ∀ f, g (algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)) f)
= algebraMap Λ (Localization.AtPrime 𝔮) (φ f))
(hgflat : g.Flat) {d : ℕ}
(hd : ringKrullDim (Localization.AtPrime 𝔮) = (d : WithBot ℕ∞)) :
ringKrullDim (Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)) = (d : WithBot ℕ∞) ∧
∃ π : Fin d → MvPolynomial (Fin m) k, (∀ i, π i ∈ Ideal.comap φ.toRingHom 𝔮) ∧
Ideal.span (Set.range fun i => algebraMap (MvPolynomial (Fin m) k)
(Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮)) (π i))
= maximalIdeal (Localization.AtPrime (Ideal.comap φ.toRingHom 𝔮))
Tag 07FV, an item
Tag 07FV in the Stacks Project.
Stacks.Smoothing.parameterScalingRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianApproximationData.lean, line 331. The attribute's comment: “Item 11 of the proof of Stacks 07FJ, with one correction: the source writes R = k[y_1, …, y_m, t_1, …, t_m], but the t-block has d members, not m. Every later use of R in the proof writes k[y_1, …, y_m, t_1, …, t_d] — items 07FZ, 07G3 and 07G9, and repeatedly in the justifications — and γ_i = π_i t_i is defined only for i = 1, …, d, the π_i being the d elements supplied by item 07FU, with I = (γ_1^e, …, γ_d^e) in item 07G1. R is MvPolynomial (Fin m ⊕ Fin d) k with y_j = X (Sum.inl j) and t_i = X (Sum.inr i); the k-algebra map k[y_1, …, y_m] → R of the source is MvPolynomial.rename Sum.inl.”.
The polynomial ring
R = k[y_1, …, y_m, t_1, …, t_d], withy_j = X (Sum.inl j)the variables of the polynomial ring of Stacks 07FT andt_i = X (Sum.inr i)one new variable for each member of the regular system of parameters of Stacks 07FU.
abbrev parameterScalingRing (k : Type u) [CommRing k] (m d : ℕ) : Type u
Stacks.Smoothing.parameterScalingGen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianApproximationData.lean, line 339. The attribute's comment: “Item 11 of the proof of Stacks 07FJ; see parameterScalingRing for the correction to the source's R. γ_i is defined for i = 1, …, d, matching the d elements π_i of item 07FU.”.
The element
γ_i = π_i t_iofR = k[y_1, …, y_m, t_1, …, t_d]: thei-th member of a familyπ_1, …, π_dink[y_1, …, y_m], scaled by the new variablet_i.
noncomputable def parameterScalingGen {k : Type u} [CommRing k] {m d : ℕ}
(π : Fin d → MvPolynomial (Fin m) k) (i : Fin d) : parameterScalingRing k m d
Tag 07FW, an item
Tag 07FW in the Stacks Project.
Stacks.Smoothing.exists_annihilator_scaledVariable_sq_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/AnnihilatorStabilizedParameters.lean, line 244. The attribute's comment: “the source's R = k[y_1, …, y_m] is an arbitrary Noetherian ring P, and the data of (07FU) — the lifts of a regular system of parameters of P_p — are the hypotheses on π; γ_i = π_i t_i is scaledVariable π i”.
Stacks 07FW. Let
Pbe a Noetherian ring, letp ⊂ Pbe a prime such thatP_pis a regular local ring of dimensiond, and letπ₁, …, π_d ∈ Pmap to a regular system of parameters ofP_p. For everye > 0theπ_imay be rescaled by elements ofP \ p, which leaves them a regular system of parameters, so that inR ⧸ (γ₁ ^ e, …, γ_{i-1} ^ e)the annihilator ofγ_iis the annihilator ofγ_i ^ 2, whereR = P[t₁, …, t_d]andγ_i = π_i t_i.
theorem exists_annihilator_scaledVariable_sq_eq {P : Type u} [CommRing P] [IsNoetherianRing P]
(p : Ideal P) [p.IsPrime] [IsRegularLocalRing (Localization.AtPrime p)] {d : ℕ}
(hd : ringKrullDim (Localization.AtPrime p) = d) (π : Fin d → P)
(hspan : Ideal.span (Set.range fun i => algebraMap P (Localization.AtPrime p) (π i)) =
IsLocalRing.maximalIdeal (Localization.AtPrime p))
{e : ℕ} (he : 0 < e) :
∃ π' : Fin d → P, (∀ i, ∃ s ∈ p.primeCompl, π' i = s * π i) ∧
Ideal.span (Set.range fun i => algebraMap P (Localization.AtPrime p) (π' i)) =
IsLocalRing.maximalIdeal (Localization.AtPrime p) ∧
∀ i : Fin d, ∀ x : MvPolynomial (Fin d) P ⧸ Ideal.span (Set.range fun j : Fin i.1 =>
scaledVariable π' (j.castLE (Nat.le_of_lt i.2)) ^ e),
x * Ideal.Quotient.mk _ (scaledVariable π' i) = 0 ↔
x * Ideal.Quotient.mk _ (scaledVariable π' i ^ 2) = 0
Tag 07FX, an item
Tag 07FX in the Stacks Project.
Stacks.Smoothing.exists_essentiallySmooth_enlargement_annihilator_sq_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/AnnihilatorStabilizedParameters.lean, line 602. The attribute's comment: “the data of (07FT) — the Artinian local D, the flat local D → Λ_q/q^nΛ_q, and the memberships of the generators of A — are hypotheses, as are the lifts of (07FU); H_{A/k}Λ is the ideal generated by the images a_1, …, a_r and (a) is stated as the relation in Λ together with the reduction of each λ_{ij} into the image of D'”.
Stacks 07FX. In the situation of Stacks 07FJ, with
N ≤ n,q ^ N Λ_q ⊆ (a_1, …, a_r)Λ_qandπ_1, …, π_d ∈ qlifting a regular system of parameters ofΛ_q, suppose thea_jand theπ_ireduce inΛ_q/q^nΛ_qinto the image of an Artinian local ringDmapping toΛ_q/q^nΛ_qby a flat local homomorphism. Then there areδ_1, …, δ_d ∈ Λ \ qand a factorizationD → D' → Λ_q/q^nΛ_qwithD'Artinian local,D → D'essentially smooth andD' → Λ_q/q^nΛ_qflat and local, such that, writingπ'_i = δ_i π_i:(π'_i)^{2N} = Σ_j a_j λ_{ij}inΛwith everyλ_{ij}reducing into the image ofD'; the annihilator ofπ'_iinΛ ⧸ ((π'_1)^e, …, (π'_{i-1})^e)is the annihilator of(π'_i)^2; and everyδ_ireduces into the image ofD'.
theorem exists_essentiallySmooth_enlargement_annihilator_sq_eq
(k : Type u) [Field k] (p : ℕ) [CharP k p] (hp : 0 < p)
(Λ : Type u) [CommRing Λ] [IsNoetherianRing Λ] [Algebra k Λ]
(q : Ideal Λ) [q.IsPrime] [IsRegularLocalRing (Localization.AtPrime q)]
{d r N n e : ℕ} (hd : ringKrullDim (Localization.AtPrime q) = d)
(hN : 0 < N) (hn : N ≤ n) (he : 0 < e)
[IsLocalRing (truncatedLocalization Λ q n)] [IsArtinianRing (truncatedLocalization Λ q n)]
(a : Fin r → Λ)
(hqN : Ideal.map (algebraMap Λ (Localization.AtPrime q)) (q ^ N) ≤
Ideal.map (algebraMap Λ (Localization.AtPrime q)) (Ideal.span (Set.range a)))
(π : Fin d → Λ) (hπq : ∀ i, π i ∈ q)
(hπspan : Ideal.span (Set.range fun i => algebraMap Λ (Localization.AtPrime q) (π i)) =
IsLocalRing.maximalIdeal (Localization.AtPrime q))
{D : Type u} [CommRing D] [IsLocalRing D] [IsArtinianRing D]
(b : D →+* truncatedLocalization Λ q n) [IsLocalHom b] (hb : RingHom.Flat b)
(haD : ∀ j, ∃ w : D, b w = algebraMap Λ (truncatedLocalization Λ q n) (a j))
(hπD : ∀ i, ∃ w : D, b w = algebraMap Λ (truncatedLocalization Λ q n) (π i)) :
∃ (δ : Fin d → Λ) (lam : Fin d → Fin r → Λ) (D' : Type u) (_ : CommRing D')
(_ : IsLocalRing D') (_ : IsArtinianRing D') (c : D →+* D')
(b' : D' →+* truncatedLocalization Λ q n) (_ : IsLocalHom c) (_ : IsLocalHom b'),
c.IsEssentiallySmooth ∧ RingHom.Flat b' ∧ b'.comp c = b ∧
(∀ i, δ i ∈ q.primeCompl) ∧
(∀ i, (δ i * π i) ^ (2 * N) = ∑ j, a j * lam i j) ∧
(∀ i j, ∃ w : D', b' w = algebraMap Λ (truncatedLocalization Λ q n) (lam i j)) ∧
(∀ i, ∃ w : D', b' w = algebraMap Λ (truncatedLocalization Λ q n) (δ i)) ∧
(∀ i : Fin d, ∀ x : Λ ⧸ Ideal.span (Set.range fun j : Fin i.1 =>
(δ (j.castLE (Nat.le_of_lt i.2)) * π (j.castLE (Nat.le_of_lt i.2))) ^ e),
x * Ideal.Quotient.mk _ (δ i * π i) = 0 ↔
x * Ideal.Quotient.mk _ ((δ i * π i) ^ 2) = 0)
Tag 07FY, an item
Tag 07FY in the Stacks Project.
Stacks.Smoothing.parameterPowerAlgebraToTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 97.
The
A-algebra mapB = A[x_i, z_{ij}]/(x_i^{2N} - Σ_j z_{ij} a_j) → Λsendingx_itoπ'_iandz_{ij}toλ_{ij}, where(π'_i)^{2N} = Σ_j a_j λ_{ij}inΛ.
noncomputable def parameterPowerAlgebraToTarget {A : Type v} {Λ : Type w} [CommRing A]
[CommRing Λ] [Algebra A Λ] {d t : ℕ} (N : ℕ) (a : Fin t → A) (π' : Fin d → Λ)
(lam : Fin d → Fin t → Λ)
(hπ' : ∀ i, π' i ^ (2 * N) = ∑ j, algebraMap A Λ (a j) * lam i j) :
parameterPowerAlgebra A d N a →ₐ[A] Λ
Stacks.Smoothing.improvedAlgebraToTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 141.
The ring map
C → Λobtained by composing thek[x_1, …, x_d]-algebra retractiong : C → Bof Stacks 07FP with the mapB → ΛofStacks.Smoothing.parameterPowerAlgebraToTarget.
noncomputable def improvedAlgebraToTarget {k : Type u} {A : Type v} {Λ : Type w} {C : Type v}
[CommRing k] [CommRing A] [CommRing Λ] [CommRing C] [Algebra k A] [Algebra A Λ] {d t : ℕ}
[Algebra (MvPolynomial (Fin d) k) C] (N : ℕ) (a : Fin t → A) (π' : Fin d → Λ)
(lam : Fin d → Fin t → Λ)
(hπ' : ∀ i, π' i ^ (2 * N) = ∑ j, algebraMap A Λ (a j) * lam i j)
(g : C →ₐ[MvPolynomial (Fin d) k] parameterPowerAlgebra A d N a) : C →+* Λ
Tag 07FZ, an item
Tag 07FZ in the Stacks Project.
Stacks.Smoothing.twistedBaseToTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 172.
The
k-algebra mapR = k[y_1, …, y_m, t_1, …, t_d] → Λwhich is a givenφ : k[y_1, …, y_m] → Λon the variablesy_jand sendst_itoδ_i ∈ Λ.
noncomputable def twistedBaseToTarget {k : Type u} {Λ : Type w} [CommRing k] [CommRing Λ]
[Algebra k Λ] {m d : ℕ} (φ : MvPolynomial (Fin m) k →ₐ[k] Λ) (δ : Fin d → Λ) :
MvPolynomial (Fin m ⊕ Fin d) k →ₐ[k] Λ
Stacks.Smoothing.twistedBaseHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 196.
The
k-algebra mapk[x_1, …, x_d] → R = k[y_1, …, y_m, t_1, …, t_d]sendingx_ito the twisted parameterγ_i = π_i t_i.
noncomputable def twistedBaseHom {k : Type u} [CommRing k] {m d : ℕ}
(π : Fin d → MvPolynomial (Fin m) k) :
MvPolynomial (Fin d) k →ₐ[k] MvPolynomial (Fin m ⊕ Fin d) k
Tag 07G0, an item
Tag 07G0 in the Stacks Project.
Stacks.Smoothing.canBeResolved_of_canBeResolved_of_smooth_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 253. The attribute's comment: “for an arbitrary R-algebra D in place of C ⊗_{k[x_1, …, x_d]} R”.
Let
k → A → Λ ⊃ qbe a chain withH_{A/k} = (a_1, …, a_t), and letR → D → Λbe a chain through the sameΛwithRsmooth overk, whereA → Dis an intermediatek-algebra map. If everya_jmaps intoH_{D/R}, then resolvingR → D → Λ ⊃ qresolvesk → A → Λ ⊃ q. Applied toD = C ⊗_{k[x_1, …, x_d]} R, this is the reduction of step (16) of Stacks 07FJ.
theorem canBeResolved_of_canBeResolved_of_smooth_base {k : Type u} {R : Type u} {A : Type v}
{D : Type v} {Λ : Type w} [CommRing k] [CommRing R] [CommRing A] [CommRing D] [CommRing Λ]
[Algebra k R] [Algebra k A] [Algebra k D] [Algebra k Λ] [Algebra A Λ] [Algebra R D]
[Algebra R Λ] [Algebra D Λ] [Algebra A D] [IsScalarTower k A Λ] [IsScalarTower k R Λ]
[IsScalarTower k R D] [IsScalarTower k A D] [IsScalarTower R D Λ] [IsScalarTower A D Λ]
[Algebra.Smooth k R] {t : ℕ} (a : Fin t → A) (q : Ideal Λ)
(ha : Ideal.span (Set.range a) = singularIdeal k A)
(haD : ∀ j, algebraMap A D (a j) ∈ singularIdeal R D)
(h : CanBeResolved R D Λ q) : CanBeResolved k A Λ q
Tag 07G1, an item
Tag 07G1 in the Stacks Project.
Stacks.Smoothing.twistedParameterPowerIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 211.
The ideal
I = (γ_1^e, …, γ_d^e)ofR = k[y_1, …, y_m, t_1, …, t_d]generated by thee-th powers of the twisted parameters.
noncomputable def twistedParameterPowerIdeal {k : Type u} [CommRing k] {m d : ℕ}
(π : Fin d → MvPolynomial (Fin m) k) (e : ℕ) : Ideal (MvPolynomial (Fin m ⊕ Fin d) k)
Tag 07G2, an item
Tag 07G2 in the Stacks Project.
Stacks.Smoothing.canBeResolved_of_quotient_span_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 476. The attribute's comment: “for arbitrary γ_1, …, γ_d ∈ R, d ≥ 1”.
Let
R → D → Λ ⊃ qbe a chain withRNoetherian andDof finite presentation overR, letγ_1, …, γ_d ∈ Rwithd ≥ 1, and letI = (γ_1^{8c}, …, γ_d^{8c}). Assume eachγ_i^cmaps intoq, is strictly standard inDoverR, and has the annihilator condition of Stacks 07FW and 07FX inRand inΛmodulo the eighth powers ofγ_1^c, …, γ_{i-1}^c. Then resolvingR/I → D/ID → Λ/IΛresolvesR → D → Λ ⊃ q.
theorem canBeResolved_of_quotient_span_pow {R : Type u} {D : Type v} {Λ : Type w} [CommRing R]
[CommRing D] [CommRing Λ] [Algebra R D] [Algebra D Λ] [Algebra R Λ] [IsScalarTower R D Λ]
[IsNoetherianRing R] [Algebra.FinitePresentation R D] (q : Ideal Λ) [q.IsPrime] {d : ℕ}
(hd : 1 ≤ d) (γ : Fin d → R) (c : ℕ) (I : Ideal R)
(hI : I = Ideal.span (Set.range fun i => γ i ^ (8 * c)))
(hγq : ∀ i, algebraMap R Λ (γ i ^ c) ∈ q)
(hannR : ∀ i,
let K := eighthPowerPrefixIdeal (fun i => γ i ^ c) i
(Submodule.span (R ⧸ K) {Ideal.Quotient.mk K (γ i ^ c)}).annihilator =
(Submodule.span (R ⧸ K) {(Ideal.Quotient.mk K (γ i ^ c)) ^ 2}).annihilator)
(hannΛ : ∀ i,
let K := Ideal.map (algebraMap R Λ) (eighthPowerPrefixIdeal (fun i => γ i ^ c) i)
(Submodule.span (Λ ⧸ K)
{Ideal.Quotient.mk K (algebraMap R Λ (γ i ^ c))}).annihilator =
(Submodule.span (Λ ⧸ K)
{(Ideal.Quotient.mk K (algebraMap R Λ (γ i ^ c))) ^ 2}).annihilator)
(hstd : ∀ i, IsStrictlyStandard (R := R) (A := D) (algebraMap R D (γ i ^ c)))
(hresolve :
let ID := Ideal.map (algebraMap R D) I
let IΛ := Ideal.map (algebraMap D Λ) ID
letI : Algebra (R ⧸ I) (Λ ⧸ IΛ) :=
((algebraMap (D ⧸ ID) (Λ ⧸ IΛ)).comp (algebraMap (R ⧸ I) (D ⧸ ID))).toAlgebra
letI : IsScalarTower (R ⧸ I) (D ⧸ ID) (Λ ⧸ IΛ) :=
IsScalarTower.of_algebraMap_eq (fun _ => rfl)
CanBeResolved (R ⧸ I) (D ⧸ ID) (Λ ⧸ IΛ) (Ideal.map (Ideal.Quotient.mk IΛ) q)) :
CanBeResolved R D Λ q
Tag 07G3, an item
Tag 07G3 in the Stacks Project.
Stacks.Smoothing.twistedBasePrime, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 218.
The prime
r ⊂ R = k[y_1, …, y_m, t_1, …, t_d]which is the inverse image ofq ⊂ Λunder the map ofStacks.Smoothing.twistedBaseToTarget.
noncomputable def twistedBasePrime {k : Type u} {Λ : Type w} [CommRing k] [CommRing Λ]
[Algebra k Λ] {m d : ℕ} (φ : MvPolynomial (Fin m) k →ₐ[k] Λ) (δ : Fin d → Λ) (q : Ideal Λ) :
Ideal (MvPolynomial (Fin m ⊕ Fin d) k)
Tag 07G4, an item
Tag 07G4 in the Stacks Project.
Stacks.Smoothing.LocalSmoothingSituation.canBeResolved_of_nilpotent_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianFactorizationDescent.lean, line 346. The attribute's comment: “for a chain whose localized target has maximal ideal generated by finitely many nilpotents, which is the form taken by the quotient by (γ_1^e, …, γ_d^e)”.
Stacks 07FJ, step 20 (tag 07G4). It suffices to resolve the localized chain
(R/I)_𝔯 → C ⊗ (R/I)_𝔯 → Λ_𝔮/IΛ_𝔮: a chainR → A → Λ ⊃ 𝔮whose prime is minimal over𝔥_A, whose localized chain can be resolved, and in whose localizationΛ_𝔮the maximal ideal is generated by finitely many nilpotent elements, can be resolved. The last condition is the one supplied by the step: the images of the parametersπ_1, …, π_dgenerate the maximal ideal and theire-th powers already lie in the idealIdivided out.
theorem LocalSmoothingSituation.canBeResolved_of_nilpotent_generators
(S : LocalSmoothingSituation.{u, v, w}) {d : ℕ} (π : Fin d → Localization.AtPrime S.q)
(hgen : IsLocalRing.maximalIdeal (Localization.AtPrime S.q) = Ideal.span (Set.range π))
(hnil : ∀ i, IsNilpotent (π i))
(hq : S.q ∈ S.radicalSingularIdealExtension.minimalPrimes)
(hres : S.IsResolvableAfterLocalizing) : S.CanBeResolved
Tag 07G5, an item
Tag 07G5 in the Stacks Project.
Stacks.Smoothing.baseParameterPowerIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ResolutionReductions.lean, line 231.
The ideal
J = (π_1^e, …, π_d^e)ofk[y_1, …, y_m].
noncomputable def baseParameterPowerIdeal {k : Type u} [CommRing k] {m d : ℕ}
(π : Fin d → MvPolynomial (Fin m) k) (e : ℕ) : Ideal (MvPolynomial (Fin m) k)
Tag 07G6, an item
Tag 07G6 in the Stacks Project.
Stacks.Smoothing.canBeResolved_of_canBeResolved_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianFactorizationDescent.lean, line 437. The attribute's comment: “for an arbitrary base change R₁ → R₂ of the chain in place of the passage from (R/JR)_𝔭 to its localization (R/I)_𝔯, the base-changed target receiving the original target”.
Stacks 07FJ, step 22 (tag 07G6). It suffices to resolve the chain over
(R/JR)_𝔭: a solution there, localized at𝔯, solves the chain of step (20) over(R/I)_𝔯. Over a local Artinian target resolvability is the existence of a smooth factorization, and a smooth factorization is carried along any base change of the chain.
theorem canBeResolved_of_canBeResolved_baseChange [IsLocalRing L₁]
[Algebra.IsPushout R₁ A₁ R₂ A₂] {q : Ideal L₂} (hq : q ≠ ⊤)
(h : CanBeResolved R₁ A₁ L₁ (IsLocalRing.maximalIdeal L₁)) : CanBeResolved R₂ A₂ L₂ q
Tag 07G7, an item
Tag 07G7 in the Stacks Project.
Stacks.Smoothing.span_range_pow_le_span_range_pow_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianFactorizationDescent.lean, line 494. The attribute's comment: “with the hypothesis d(e-1)+1 ≤ n in place of the source's n = N + dc, which does not give 𝔭^n ⊆ J: a degree-n monomial in the regular system of parameters π_1, …, π_d lies in (π_1^e, …, π_d^e) only if some exponent reaches e, so the containment needs d(e-1) < n, whereas N is fixed in step (1) before c and hence before e = 8c”.
The bound of Stacks 07FJ, step 23, corrected. If
𝔭 = (π_1, …, π_d)andJ = (π_1^e, …, π_d^e)then𝔭^n ⊆ Jas soon asd(e - 1) < n, and this is sharp: a monomial of degreenin theπ_iis forced intoJonly when one of its exponents reachese. The boundd·e < nofStacks.AlgebraicGeometry.IdealPowerSections.span_range_pow_le_span_range_powis the same statement with a weaker hypothesis.
theorem span_range_pow_le_span_range_pow_of_le {d : ℕ} (π : Fin d → Y) {e n : ℕ} (he : 1 ≤ e)
(hn : d * (e - 1) + 1 ≤ n) :
Ideal.span (Set.range π) ^ n ≤ Ideal.span (Set.range fun i => π i ^ e)
Stacks.Smoothing.canBeResolved_quotient_of_canBeResolved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianFactorizationDescent.lean, line 543. The attribute's comment: “the reduction half of the step: the solution of the chain over (R/p^nR)_p is divided by J, which is a base change of the chain; the numeric input p^n ⊆ J is span_range_pow_le_span_range_pow_of_le, stated with the corrected bound”.
Stacks 07FJ, step 23 (tag 07G7). It suffices to resolve the chain before dividing by the ideal: dividing a solution of
R → A → Λby an idealIof the base gives a solution ofR/I → A/IA → Λ/IΛ, becauseA/IAis the base change ofAalongR → R/I. In step (23) the base is(R/𝔭^nR)_𝔭, the ideal isJ = (π_1^e, …, π_d^e), andspan_range_pow_le_span_range_pow_of_leis what makes(R/JR)_𝔭that quotient.
theorem canBeResolved_quotient_of_canBeResolved [IsLocalRing L] (I : Ideal R)
(h : CanBeResolved R A L (IsLocalRing.maximalIdeal L)) :
let IA := Ideal.map (algebraMap R A) I
let IL := Ideal.map (algebraMap A L) IA
letI : Algebra (R ⧸ I) (L ⧸ IL) :=
((algebraMap (A ⧸ IA) (L ⧸ IL)).comp (algebraMap (R ⧸ I) (A ⧸ IA))).toAlgebra
letI : IsScalarTower (R ⧸ I) (A ⧸ IA) (L ⧸ IL) := IsScalarTower.of_algebraMap_eq fun _ => rfl
∀ q : Ideal (L ⧸ IL), q ≠ ⊤ → CanBeResolved (R ⧸ I) (A ⧸ IA) (L ⧸ IL) q
Tag 07G8, an item
Tag 07G8 in the Stacks Project.
Stacks.Smoothing.hasSmoothFactorization_of_algHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianFactorizationDescent.lean, line 375.
Stacks 07FJ, step 24 (tag 07G8). It suffices to resolve the chain with
Bin place ofC: anR-algebra sectionC → Bcompatible with the maps to the target carries a smooth factorization ofB → Λto one ofC → Λ.
theorem hasSmoothFactorization_of_algHom {C₀ : Type u} [CommRing C₀] [Algebra R₀ C₀]
[Algebra C₀ L] [IsScalarTower R₀ C₀ L] (σ : C₀ →ₐ[R₀] A₀)
(hσ : ∀ c, algebraMap A₀ L (σ c) = algebraMap C₀ L c)
(h : HasSmoothFactorization R₀ A₀ L) : HasSmoothFactorization R₀ C₀ L
Tag 07G9, an item
Tag 07G9 in the Stacks Project.
Stacks.Smoothing.canBeResolved_of_factorization_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianFactorizationDescent.lean, line 616. The attribute's comment: “for a chain whose middle term is an arbitrary algebra of finite presentation over Λ₀[t_1, …, t_d] in place of B ⊗_{k[x_1, …, x_d]} (R/p^nR)_p, with essential smoothness of Λ₀ → D' spelled out as: D' is a localization of a Λ₀-algebra of finite presentation and is formally smooth over Λ₀”.
Stacks 07FJ, step 25 (tag 07G9). It suffices to find a factorization
B ⊗_{k[x_1, …, x_d]} (R/𝔭^nR)_𝔭 → D'[t_1, …, t_d] → Λ_𝔮/𝔮^nΛ_𝔮: the ringR_𝔭/𝔭^nR_𝔭is the polynomial ringΛ₀[t_1, …, t_d]overΛ₀ = k[y_1, …, y_m]_𝔭/𝔭^nk[y_1, …, y_m]_𝔭, the algebraD'is essentially smooth overΛ₀, henceD'[t_1, …, t_d]is a filtered colimit of smoothΛ₀[t_1, …, t_d]-algebras and the finitely presented middle term factors through one of them.
theorem canBeResolved_of_factorization_mvPolynomial {Λ₀ B₀ D A L : Type u} [CommRing Λ₀]
[CommRing B₀] [CommRing D] [CommRing A] [CommRing L] [Algebra Λ₀ B₀] [Algebra B₀ D]
[Algebra Λ₀ D] [IsScalarTower Λ₀ B₀ D] [Algebra.FinitePresentation Λ₀ B₀] (M : Submonoid B₀)
[IsLocalization M D] (hD : Algebra.FormallySmooth Λ₀ D) {d : ℕ}
[Algebra (MvPolynomial (Fin d) Λ₀) A] [Algebra A L] [Algebra (MvPolynomial (Fin d) Λ₀) L]
[IsScalarTower (MvPolynomial (Fin d) Λ₀) A L]
[Algebra.FinitePresentation (MvPolynomial (Fin d) Λ₀) A]
(g : A →ₐ[MvPolynomial (Fin d) Λ₀] MvPolynomial (Fin d) D)
(k : MvPolynomial (Fin d) D →ₐ[MvPolynomial (Fin d) Λ₀] L)
(hgk : k.comp g = IsScalarTower.toAlgHom (MvPolynomial (Fin d) Λ₀) A L)
{q : Ideal L} (hq : q ≠ ⊤) :
CanBeResolved (MvPolynomial (Fin d) Λ₀) A L q
Tag 07GA, an item
Tag 07GA in the Stacks Project.
Stacks.Smoothing.exists_algHom_parameterPowerAlgebra_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ArtinianFactorizationDescent.lean, line 651. The attribute's comment: “the choices of (07FT), (07FU) and (07FX) are hypotheses: the map A → D' whose existence is the condition E ⊆ D of (07FT), the images π_i, δ_i, λ_{ij} in D' of (07FU) and (07FX), the invertibility of δ_i in the local ring D', and clause (a) of (07FX) read in D'. The target D'[t_1, …, t_d] is MvPolynomial (Fin d) D'”.
Stacks 07FJ, step 26 (tag 07GA). The factorization required by step (25) exists. Its twist is that
B = A[x_i, z_{ij}]/(x_i^{2N} - Σ_j z_{ij}a_j)must sendx_itoπ_i t_i, not toπ'_i = δ_i π_i, for the square overk[x_1, …, x_d] → R_𝔭/𝔭^nR_𝔭to commute; the defining relation then forcesz_{ij} ↦ λ_{ij} t_i^{2N}/δ_i^{2N}, which lies inD'[t_1, …, t_d]becauseδ_iis a unit of the local ringD'. The map is produced as ak[x_1, …, x_d]-algebra map for the structurex_i ↦ π_i t_ionD'[t_1, …, t_d], which is exactly the commutation of the square in the source.
theorem exists_algHom_parameterPowerAlgebra_mvPolynomial (k : Type u) {A D : Type u} [CommRing k]
[CommRing A] [CommRing D] [Algebra k A] [Algebra k D] {d r N : ℕ} (a : Fin r → A)
(φ : A →ₐ[k] D) (π δ : Fin d → D) (lam : Fin d → Fin r → D) (hδ : ∀ i, IsUnit (δ i))
(hrel : ∀ i, (δ i * π i) ^ (2 * N) = ∑ j, φ (a j) * lam i j) :
letI : Algebra (MvPolynomial (Fin d) k) (MvPolynomial (Fin d) D) :=
(MvPolynomial.aeval (R := k) fun i => C (π i) * X i).toRingHom.toAlgebra
∃ ψ : parameterPowerAlgebra A d N a →ₐ[MvPolynomial (Fin d) k] MvPolynomial (Fin d) D,
(∀ x : A, ψ (algebraMap A (parameterPowerAlgebra A d N a) x) = C (φ x)) ∧
(∀ i, ψ (Ideal.Quotient.mk (parameterPowerIdeal d N a) (X (Sum.inl i))) = C (π i) * X i) ∧
∀ i j, ψ (Ideal.Quotient.mk (parameterPowerIdeal d N a) (X (Sum.inr (i, j)))) =
C (lam i j * (↑(hδ i).unit⁻¹ : D) ^ (2 * N)) * X i ^ (2 * N)
Sources
Section16.12 The main theorem#
Section 16.12 of the Stacks Project, Tag 07GB. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07GC, a theorem
Tag 07GC in the Stacks Project.
Stacks.Smoothing.indSmooth_of_isRegularRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/PopescuTheorem.lean, line 204. The attribute's comment: “Popescu's theorem with NO carried hypotheses: every regular ring map of Noetherian rings is a filtered colimit of smooth ring maps. Regularity is IsRegularRingMap (Situation 07F2) and the conclusion is IndSmooth, the ObjectProperty.ind spelling of Lemma 07C3. Every step of the source's argument is proved: the reduction to a field base (07F5), the Noetherian induction on 𝔥_A, the case 𝔥_A = Λ (07EU), the characteristic-zero resolution (07FE), and the characteristic-p resolution (07FJ, canBeResolvedInPositiveCharacteristic), whose own λ-choice repair is due to Brian Nugent. Nothing is assumed.”.
Popescu's theorem. A regular ring map of Noetherian rings makes its target a filtered colimit of smooth algebras.
theorem indSmooth_of_isRegularRingMap
(R : Type u) [CommRing R] (Λ : Type u) [CommRing Λ] [Algebra R Λ]
[IsNoetherianRing R] [IsNoetherianRing Λ] (hregular : IsRegularRingMap R Λ) :
IndSmooth R Λ
Sources
Section16.13 The approximation property for G-rings#
Section 16.13 of the Stacks Project, Tag 07QX. 4 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07QY, a theorem
Tag 07QY in the Stacks Project.
Stacks.Smoothing.exists_approximate_solution_of_henselian_isGRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ApproximationHenselianGRing.lean, line 239. The attribute's comment: “the full conclusion for a henselian local G-ring -- general m, n and every N, including N = 0 -- with 𝔪^N R^∧ as the extension of 𝔪^N to AdicCompletion (maximalIdeal R) R, and with NO carried hypotheses. All three of the source's cited inputs are formalized and used: Popescu's Theorem 07GC, reached from the G-ring hypothesis through Lemma 0AH2; and 07M7 and 04GG, which are consumed inside Lemma 0AH5 applied to the henselian pair (R, 𝔪). Nothing else is assumed.”.
Stacks 07QY (the approximation property for G-rings). Let
(R, 𝔪)be a henselian local G-ring. A system of polynomial equations overRwith a solution in the𝔪-adic completionR^∧has, for everyN, a solution inRcongruent to the given one modulo𝔪 ^ N R^∧.
theorem exists_approximate_solution_of_henselian_isGRing
{R : Type u} [CommRing R] [HenselianLocalRing R] (hG : IsGRing R)
{m n : ℕ} (f : Fin m → MvPolynomial (Fin n) R)
(a : Fin n → AdicCompletion (maximalIdeal R) R)
(ha : ∀ j, MvPolynomial.aeval a (f j) = 0) (N : ℕ) :
∃ b : Fin n → R,
(∀ i, a i - algebraMap R (AdicCompletion (maximalIdeal R) R) (b i) ∈
((maximalIdeal R) ^ N).map (algebraMap R (AdicCompletion (maximalIdeal R) R))) ∧
∀ j, MvPolynomial.aeval b (f j) = 0
Tag 07QZ, a theorem
Tag 07QZ in the Stacks Project.
Stacks.Smoothing.exists_localEtaleSolution_of_isGRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ApproximationGRing.lean, line 754. The attribute's comment: “the conclusion for a Noetherian local G-ring, with NO hypothesis beyond the source's own: the appeal to Popescu's Theorem 07GC that the source makes here runs through Lemma 0AH2 and indSmooth_of_isRegularRingMap, which is proved. The instance IsNoetherianRing R is redundant, being the first component of IsGRing (Tag 07GH); it is present because the statement names the maximal ideal of R^∧, which is only known to be local once R is known to be Noetherian. Every part of the source's conclusion is here: the étale R → R', the ideal 𝔪' lying over 𝔪, its MAXIMALITY, the residue field equality κ(𝔪) = κ(𝔪'), the solution b in R', and the congruence a_i - b_i ∈ (𝔪')^N R^∧ read along the embedding R' ⊂ R^∧ — which is local at 𝔪', as in the source's R ⊂ R'_{𝔪'} ⊂ R^h ⊂ R^∧. Two further conclusions are added: the same congruence modulo the smaller 𝔪^N R^∧, and the congruence of Lemma 0CAR in (R'_{𝔪'})^∧, which is the approx field of LocalEtaleSolution. See the module docstring.”.
Stacks 07QZ (the approximation property for G-rings). Let
(R, 𝔪)be a Noetherian local G-ring. A system of polynomial equations overRwith a solution in the𝔪-adic completionR^∧has, for everyN, a solution in an étale extensionR → R'at a maximal ideal𝔪'over𝔪withκ(𝔪) = κ(𝔪'), congruent to the given solution modulo(𝔪')^N R^∧.The G-ring hypothesis is the source's, and it enters where the source puts it: through Popescu's Theorem 07GC and Lemma 0AH2, which is
Stacks.Smoothing.isIndSmoothAdicCompletion_of_isGRing.
theorem exists_localEtaleSolution_of_isGRing
{R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hG : IsGRing R)
{m n : ℕ} (f : Fin m → MvPolynomial (Fin n) R) (N : ℕ)
(a : Fin n → AdicCompletion (maximalIdeal R) R)
(ha : ∀ j, MvPolynomial.aeval a (f j) = 0) :
∃ s : StacksDraft.ArtinApproximation.LocalEtaleSolution R f N a,
s.prime.IsMaximal ∧
∃ ι : s.carrier →ₐ[R] AdicCompletion (maximalIdeal R) R,
(∀ x : s.carrier,
x ∈ s.prime ↔ ι x ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R)) ∧
(∀ i, a i - ι (s.sol i) ∈
(s.prime ^ N).map (ι : s.carrier →+* AdicCompletion (maximalIdeal R) R)) ∧
∀ i, a i - ι (s.sol i) ∈
(maximalIdeal R ^ N).map (algebraMap R (AdicCompletion (maximalIdeal R) R))
Tag 0A1W, an example
Tag 0A1W in the Stacks Project.
IsLocalRing.isNoetherianRing_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/AlgebraicInCompletion.lean, line 102. The attribute's comment: “the henselization is Noetherian; this is Stacks 06LJ, proved in the library as isNoetherianRing_of_isHenselization”. References: EGA IV (18.6.6), “(v)”; SGA 4 VIII (4.1).
A henselization of a Noetherian local ring is Noetherian (Stacks 06LJ, recalled in the discussion of Stacks 0A1W).
theorem isNoetherianRing_henselization (R : Type u) (Rh : Type v) [CommRing R] [IsLocalRing R]
[IsNoetherianRing R] [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
[IsHenselization R (ResidueField R) Rh] : IsNoetherianRing Rh
IsLocalRing.exists_ringEquiv_adicCompletion_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/AlgebraicInCompletion.lean, line 111. The attribute's comment: “the map on completions R^∧ → (Rʰ)^∧ is an isomorphism; this is Stacks 06LJ, proved in the library as exists_ringEquiv_adicCompletion_of_isHenselization”.
The completion of a henselization is the completion of the base (Stacks 06LJ, recalled in the discussion of Stacks 0A1W):
R^∧ → (Rʰ)^∧is an isomorphism.
theorem exists_ringEquiv_adicCompletion_henselization (R Rh : Type u) [CommRing R] [IsLocalRing R]
[IsNoetherianRing R] [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
[IsHenselization R (ResidueField R) Rh] :
∃ e : AdicCompletion (maximalIdeal R) R ≃+* AdicCompletion (maximalIdeal Rh) Rh,
∀ x : R, e (algebraMap R (AdicCompletion (maximalIdeal R) R) x) =
algebraMap Rh (AdicCompletion (maximalIdeal Rh) Rh) (algebraMap R Rh x)
IsLocalRing.injective_henselizationToAdicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/AlgebraicInCompletion.lean, line 181. The attribute's comment: “the henselization is a subring of the completion: the canonical map is injective”.
A henselization of a Noetherian local ring is a subring of the completion (Stacks 0A1W). The canonical map
Rʰ → R^∧is faithfully flat, because it is flat — the completion is flat overRand the henselization is ind-étale overR— and local; hence it is injective.
theorem injective_henselizationToAdicCompletion :
Function.Injective (henselizationToAdicCompletion R Rh)
IsLocalRing.isAlgebraic_of_isHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/AlgebraicInCompletion.lean, line 241. The attribute's comment: “every element of the henselization is algebraic over R, equivalently over its fraction field”.
Every element of a henselization of a local domain is algebraic over it (Stacks 0A1W). A henselization is a filtered colimit of étale algebras, so the element comes from an étale stage, where
isAlgebraic_of_etaleapplies.
theorem isAlgebraic_of_isHenselization (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R]
(Rh : Type v) [CommRing Rh] [IsLocalRing Rh] [Algebra R Rh]
[IsHenselization R (ResidueField R) Rh] (g : Rh) : IsAlgebraic R g
IsLocalRing.finite_setOf_aeval_eq_zero_of_isHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/AlgebraicInCompletion.lean, line 261. The attribute's comment: “Rʰ ⊆ Rʰ ⊗_R K and Rʰ ⊗_R K is a finite product of field extensions of K; hence a nonzero polynomial over R has only finitely many roots in Rʰ”.
A nonzero polynomial has only finitely many roots in a henselization of a Noetherian local domain (Stacks 0A1W). The henselization is flat over the base, so it injects into its fibre over the generic point, and that fibre is a finite product of field extensions of the fraction field by Stacks 0AH1; a nonzero polynomial has finitely many roots in each factor.
theorem finite_setOf_aeval_eq_zero_of_isHenselization (R : Type u) [CommRing R] [IsDomain R]
[IsLocalRing R] [IsNoetherianRing R] (Rh : Type u) [CommRing Rh] [IsLocalRing Rh]
[Algebra R Rh] [IsHenselization R (ResidueField R) Rh]
(p : Polynomial R) (hp : p ≠ 0) :
{g : Rh | Polynomial.aeval g p = 0}.Finite
IsLocalRing.range_henselizationToAdicCompletion_eq_setOf_isAlgebraic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Henselian/Henselization/AlgebraicInCompletion.lean, line 420. The attribute's comment: “the conclusion of the example, with NO carried hypotheses: for a Noetherian local domain R which is a G-ring, the image of the henselization in R^∧ is exactly the set of elements of R^∧ algebraic over R. Algebraicity over the fraction field K is IsAlgebraic R, the source's own form a_n f^n + ⋯ + a_0 = 0 with a_i ∈ R and a_n ≠ 0, which over a domain is equivalent to algebraicity over K. Both inclusions are proved: ⊆ is isAlgebraic_of_isHenselization, and ⊇ uses Theorem 07QZ (Stacks.Smoothing.exists_localEtaleSolution_of_isGRing, unconditional), the factorization of its étale solution through Rʰ (exists_algHom_eq_of_etale, proved here rather than taken from the source's remark that the embedding factors as R' ⊂ R'_{𝔪'} ⊂ Rʰ ⊂ R^∧), the finiteness of the root set in Rʰ (finite_setOf_aeval_eq_zero_of_isHenselization) and Krull's intersection theorem in R^∧. The other clauses of this tag -- that Rʰ is Noetherian, that R^∧ → (Rʰ)^∧ is an isomorphism, that Rʰ → R^∧ is injective, and the two statements about Rʰ ⊗_R K -- are registered separately above.”.
Stacks 0A1W, the conclusion of the example. Let
Rbe a Noetherian local domain with fraction fieldKwhich is a G-ring. Then the henselizationRʰ, viewed as a subring of the completionR^∧, is exactly the set of elements ofR^∧that are algebraic overK.The inclusion
⊆isisAlgebraic_of_isHenselization. For⊇, Theorem 07QZ produces, for eachN, a rootgof the same polynomial in an étale extension ofR; that root is pushed intoRʰbyexists_algHom_eq_of_etaleand satisfiesf - g ∈ (𝔪 R^∧)^N. Since the polynomial has only finitely many roots inRʰand⋂_N (𝔪 R^∧)^N = 0, one of them must equalf.
theorem range_henselizationToAdicCompletion_eq_setOf_isAlgebraic [IsDomain R]
(hG : IsGRing R) :
Set.range (henselizationToAdicCompletion R Rh) =
{x : AdicCompletion (maximalIdeal R) R | IsAlgebraic R x}
Tag 0CAR, a lemma
Tag 0CAR in the Stacks Project.
StacksDraft.ArtinApproximation.artinApproximationGRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ApproximationGRingEtale.lean, line 614. The attribute's comment: “the full conclusion — étaleness of A → A', 𝔭' lying over 𝔭, the solution in A', the residue field equality κ(𝔭) = κ(𝔭') and the congruence a_i - b_i ∈ (𝔭')^N (A'_{𝔭'})^∧ for every i and every N — in the spelling of StacksDraft.ArtinApproximation.ArtinApproximationGRing, with NO carried hypotheses. The source's proof has two inputs and both are proved. The second, Algebra Lemma 00U2 (9), is etaleDescentAlongLocalization, from the public AlgebraicGeometry.exists_etale_pushout_of_localization. The first is Theorem 07QZ, Stacks.Smoothing.exists_localEtaleSolution_of_isGRing, itself unconditional because Popescu's Theorem 07GC is (indSmooth_of_isRegularRingMap, resting on Lemma 07FJ canBeResolvedInPositiveCharacteristic, whose λ-choice repair is due to Brian Nugent); the shape 0CAR's proof consumes it in is localApproximationProperty. The reduction of 0CAR to 07QZ — the base change of the system to A_𝔭, the descent of the solution and its equations to a principal localization, the identification of 𝔭' and of A'_{𝔭'} with S_q, the residue field equality and the transport of the congruence — is artinApproximationGRing_of_local.”.
Stacks 0CAR (Smoothing Ring Maps, Lemma 16.13.4). Let
Abe a Noetherian ring, let𝔭be a prime ofAsuch thatA_𝔭is a G-ring, and letf₁, …, f_mbe polynomials overAinnvariables. If the systemf = 0has a solution(a₁, …, a_n)in the completion ofA_𝔭, then for everyNthere are an étale ring mapA → A', a prime𝔭' ⊂ A'lying over𝔭withκ(𝔭) = κ(𝔭'), and a solution(b₁, …, b_n)of the system inA'witha_i - b_i ∈ (𝔭')^N (A'_{𝔭'})^∧.Both inputs of the source's proof are proved: Theorem 07QZ is
localApproximationPropertyand Algebra, Lemma 00U2 (9) isetaleDescentAlongLocalization.
theorem artinApproximationGRing : ArtinApproximationGRing.{u}
Sources
Section16.14 Approximation for henselian pairs#
Section 16.14 of the Stacks Project, Tag 0AH4. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AH5, a lemma
Tag 0AH5 in the Stacks Project.
Stacks.Smoothing.exists_solution_of_henselianPair_of_isRegularRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ApproximationHenselianGRing.lean, line 165. The attribute's comment: “the conclusion under the source's FIRST alternative hypothesis, that A → A^∧ is a regular ring map, with no other hypothesis: the appeal to Popescu's Theorem 07GC that the source makes here is indSmooth_of_isRegularRingMap, which is proved. Regularity is the Situation 07F2 spelling IsRegularRingMap, reached from the general IsRegularRingHom of 07BJ by the public isRegularRingMap_of_regularRingHom. The conclusion is the full one: a solution in A of the same system, congruent to the given one modulo the extension of I ^ N to A^∧, for every N ≥ 1. See also the two sibling wrappers for the source's other two alternatives.”.
Stacks 0AH5 under the source's first hypothesis. Let
(A, I)be a henselian pair withANoetherian such thatA → A^∧is a regular ring map. A system of polynomial equations overAwith a solution in the completion has, for everyN ≥ 1, a solution inAcongruent to it moduloI ^ N.
theorem exists_solution_of_henselianPair_of_isRegularRingMap
{A : Type u} [CommRing A] {I : Ideal A} [IsNoetherianRing A]
(hAI : HenselianPair A I) (hreg : IsRegularRingMap A (AdicCompletion I A))
{m n : ℕ} (f : Fin m → MvPolynomial (Fin n) A)
(â : Fin n → AdicCompletion I A) (hâ : ∀ j, MvPolynomial.aeval â (f j) = 0)
{N : ℕ} (hN : N ≠ 0) :
∃ a : Fin n → A,
(∀ i, â i - algebraMap A (AdicCompletion I A) (a i) ∈
(I ^ N).map (algebraMap A (AdicCompletion I A))) ∧
∀ j, MvPolynomial.aeval a (f j) = 0
Stacks.Smoothing.exists_solution_of_henselianPair_of_isGRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ApproximationHenselianGRing.lean, line 187. The attribute's comment: “the conclusion under the source's SECOND alternative hypothesis, that A is a Noetherian G-ring (IsGRing, Tag 07GH, whose first component is Noetherianness), with no other hypothesis. The source's reduction (2) ⟹ (1) is Lemma 0AH2 (isRegularRingHom_algebraMap_adicCompletion), and the appeal to Popescu's Theorem 07GC is indSmooth_of_isRegularRingMap, which is proved. The conclusion is the full one, as in the sibling wrapper for alternative (1).”.
Stacks 0AH5 under the source's second hypothesis. Let
(A, I)be a henselian pair withAa Noetherian G-ring. A system of polynomial equations overAwith a solution in the completion has, for everyN ≥ 1, a solution inAcongruent to it moduloI ^ N.
theorem exists_solution_of_henselianPair_of_isGRing
{A : Type u} [CommRing A] {I : Ideal A} (hG : IsGRing A) (hAI : HenselianPair A I)
{m n : ℕ} (f : Fin m → MvPolynomial (Fin n) A)
(â : Fin n → AdicCompletion I A) (hâ : ∀ j, MvPolynomial.aeval â (f j) = 0)
{N : ℕ} (hN : N ≠ 0) :
∃ a : Fin n → A,
(∀ i, â i - algebraMap A (AdicCompletion I A) (a i) ∈
(I ^ N).map (algebraMap A (AdicCompletion I A))) ∧
∀ j, MvPolynomial.aeval a (f j) = 0
Stacks.Smoothing.exists_solution_of_henselianPair_of_isGRing_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ApproximationHenselianGRing.lean, line 211. The attribute's comment: “the conclusion under the source's THIRD alternative hypothesis, that (A, I) is the henselization of a pair (C, J) with C a Noetherian G-ring, with no other hypothesis. The henselization is described exactly as in Lemma 0AH3 (isGRing_henselization): the pair (A, J A) is henselian and A has the universal property of the henselization of (C, J), which is the datum exists_henselization (Tag 0A02) produces. The source's reduction (3) ⟹ (2) is that lemma, (2) ⟹ (1) is Lemma 0AH2, and the appeal to Popescu's Theorem 07GC is indSmooth_of_isRegularRingMap, which is proved. The conclusion is the full one, as in the sibling wrappers for alternatives (1) and (2).”.
Stacks 0AH5 under the source's third hypothesis. Let
Cbe a Noetherian G-ring, letJ ⊂ Cbe an ideal and letAbe a henselization of the pair(C, J). A system of polynomial equations overAwith a solution in theJ A-adic completion ofAhas, for everyN ≥ 1, a solution inAcongruent to it modulo(J A) ^ N.
theorem exists_solution_of_henselianPair_of_isGRing_henselization
{C : Type u} [CommRing C] (hC : IsGRing C) (J : Ideal C)
(A : Type u) [CommRing A] [Algebra C A]
(hh : HenselianPair A (J.map (algebraMap C A)))
(hι : ∀ (B : Type u) (_ : CommRing B) (K : Ideal B), HenselianPair B K →
∀ g : C →+* B, J ≤ K.comap g →
∃! t : A →+* B, t.comp (algebraMap C A) = g ∧ J.map (algebraMap C A) ≤ K.comap t)
{m n : ℕ} (f : Fin m → MvPolynomial (Fin n) A)
(â : Fin n → AdicCompletion (J.map (algebraMap C A)) A)
(hâ : ∀ j, MvPolynomial.aeval â (f j) = 0) {N : ℕ} (hN : N ≠ 0) :
∃ a : Fin n → A,
(∀ i, â i - algebraMap A (AdicCompletion (J.map (algebraMap C A)) A) (a i) ∈
((J.map (algebraMap C A)) ^ N).map
(algebraMap A (AdicCompletion (J.map (algebraMap C A)) A))) ∧
∀ j, MvPolynomial.aeval a (f j) = 0
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.