88.2 Two categories to 88.17 Rig-smooth homomorphisms
Section88.2 Two categories#
Section 88.2 of the Stacks Project, Tag 0AL2. 8 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AL3, an equation
Tag 0AL3 in the Stacks Project.
Rig.AdicAlgebraSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/AdicAlgebraSystem.lean, line 54.
The category of inverse systems
… → B₃ → B₂ → B₁in whichBₙis a finite typeA ⧸ I ^ n-algebra and each transition identifies its target with reduction of its source moduloI ^ n. The Lean indexnrepresents the mathematical indexn + 1.
structure AdicAlgebraSystem (A : Type u) [CommRing A] (I : Ideal A)
Tag 0AL4, an equation
Tag 0AL4 in the Stacks Project.
Rig.AdicFiniteTypeAlgebra, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/CompletedBaseChange.lean, line 46.
The category of
I-adically completeA-algebras whose reduction moduloIis of finite type overA ⧸ I.
public abbrev AdicFiniteTypeAlgebra (A : Type u) [CommRing A] (I : Ideal A)
Tag 0AJN, an equation
Tag 0AJN in the Stacks Project.
Rig.adicQuotientFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/AdicAlgebraSystem.lean, line 461.
The functor which associates to an adically complete algebra
Bits inverse system of quotientsB ⧸ (I.map (algebraMap A B)) ^ (n + 1).Its transition maps are the canonical quotient maps, and its action on morphisms is induced by the underlying
A-algebra maps.
public noncomputable def adicQuotientFunctor (A : Type u) [CommRing A]
(I : Ideal A) :
AdicFiniteTypeAlgebra.{u, v} A I ⥤
AdicAlgebraSystem.{u, v} A I
Tag 0AJP, a lemma
Tag 0AJP in the Stacks Project.
Rig.exists_adicCompletion_mvPolynomial_quotient_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/PolynomialPresentation.lean, line 77. The attribute's comment: “completed_polynomial_presentation”.
Stacks Project, Tag 0AJP. An adically complete algebra of finite type modulo a finitely generated ideal is a quotient of a completed polynomial algebra in finitely many variables.
public theorem exists_adicCompletion_mvPolynomial_quotient_equiv
{A : Type u} [CommRing A] (I : Ideal A) (hI : I.FG)
(B : AdicFiniteTypeAlgebra.{u, v} A I) :
∃ r : ℕ,
let P := AdicCompletion
(I.map (MvPolynomial.C : A →+* MvPolynomial (Fin r) A))
(MvPolynomial (Fin r) A)
∃ J : Ideal P, Nonempty ((P ⧸ J) ≃ₐ[A] B.carrier)
Rig.iAdicallyCompleteRing_adicCompletion_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/PolynomialPresentation.lean, line 275. The attribute's comment: “polynomial_completions”.
The completion of a polynomial algebra is complete for the ideal extended from the coefficient ring.
public theorem iAdicallyCompleteRing_adicCompletion_mvPolynomial (hI : I.FG) :
IsAdicComplete (I.map (algebraMap A
(AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A))))
(AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A))
Rig.finiteType_quotient_adicCompletion_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/PolynomialPresentation.lean, line 292. The attribute's comment: “polynomial_completions”.
The reduction modulo
Iof a completed polynomial algebra is of finite type overA ⧸ I.
public theorem finiteType_quotient_adicCompletion_mvPolynomial (hI : I.FG) :
Algebra.FiniteType (A ⧸ I)
((AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A)) ⧸
I.map (algebraMap A
(AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A))))
Rig.adicQuotientEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/CategoryLimit.lean, line 570. The attribute's comment: “the functor (Bₙ) ↦ lim Bₙ is a quasi-inverse of the functor of 0AJN, so the two categories are equivalent”.
Stacks Project, Tag 0AJP. The functor
(Bₙ) ↦ lim Bₙfrom systems of finite type algebras over the quotientsA ⧸ Iⁿto adically complete algebras of finite type moduloIis quasi-inverse to the functorB ↦ (B ⧸ Iⁿ⁺¹B)of [StacksProject 0AJN]: the two categories are equivalent.
public noncomputable def adicQuotientEquivalence (hI : I.FG) :
AdicFiniteTypeAlgebra.{u, v} A I ≌ AdicAlgebraSystem.{u, v} A I
Tag 0AJQ, a lemma
Tag 0AJQ in the Stacks Project.
Rig.isNoetherianRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/PolynomialPresentation.lean, line 190. The attribute's comment: “noetherian_objects”.
Every adically complete algebra of finite type modulo an ideal over a Noetherian commutative ring has a Noetherian underlying ring.
public instance isNoetherianRing {A : Type u} [CommRing A] [IsNoetherianRing A]
{I : Ideal A} (B : AdicFiniteTypeAlgebra.{u, v} A I) :
IsNoetherianRing B.carrier
Rig.quotient_isAdicFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/PolynomialPresentation.lean, line 229. The attribute's comment: “quotients_remain_objects”.
Every quotient of an adically complete algebra of finite type modulo an ideal over a Noetherian ring is again an adically complete algebra of finite type modulo that ideal.
public theorem quotient_isAdicFiniteType {A : Type u} [CommRing A] [IsNoetherianRing A]
{I : Ideal A} (B : AdicFiniteTypeAlgebra.{u, v} A I)
(J : Ideal B.carrier) :
IsAdicComplete (I.map (algebraMap A (B.carrier ⧸ J))) (B.carrier ⧸ J) ∧
Algebra.FiniteType (A ⧸ I)
((B.carrier ⧸ J) ⧸ I.map (algebraMap A (B.carrier ⧸ J)))
Rig.iAdicallyCompleteRing_adicCompletion_mvPolynomial_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/PolynomialPresentation.lean, line 322. The attribute's comment: “polynomial_completions”.
The completion of the polynomial ring in
rvariables over a Noetherian ring is complete for the ideal extended from the coefficient ring.
public theorem iAdicallyCompleteRing_adicCompletion_mvPolynomial_of_isNoetherianRing :
IsAdicComplete
(I.map (algebraMap A
(AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A))))
(AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A))
Rig.finiteType_quotient_adicCompletion_mvPolynomial_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/PolynomialPresentation.lean, line 334. The attribute's comment: “polynomial_completions”.
The reduction modulo
Iof the completed polynomial ring inrvariables is of finite type overA ⧸ I.
public theorem finiteType_quotient_adicCompletion_mvPolynomial_of_isNoetherianRing :
Algebra.FiniteType (A ⧸ I)
((AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A)) ⧸
I.map (algebraMap A
(AdicCompletion (I.map (algebraMap A (MvPolynomial (Fin r) A)))
(MvPolynomial (Fin r) A))))
Rig.adicCompletion_isAdicallyComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FiniteTypeCompletions.lean, line 37. The attribute's comment: “finite_type_completions”.
The completion of a finite type algebra over a Noetherian ring is complete for the ideal extended directly from the base ring.
public theorem adicCompletion_isAdicallyComplete
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(C : Type v) [CommRing C] [Algebra A C] [Algebra.FiniteType A C] :
IsAdicComplete
(I.map (algebraMap A (AdicCompletion (I.map (algebraMap A C)) C)))
(AdicCompletion (I.map (algebraMap A C)) C)
Rig.adicCompletion_finiteType_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FiniteTypeCompletions.lean, line 54. The attribute's comment: “finite_type_completions”.
The quotient modulo the ideal from the base ring of the completion of a finite type algebra is of finite type over the quotient of the base ring.
public theorem adicCompletion_finiteType_quotient
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(C : Type v) [CommRing C] [Algebra A C] [Algebra.FiniteType A C] :
Algebra.FiniteType (A ⧸ I)
((AdicCompletion (I.map (algebraMap A C)) C) ⧸
I.map (algebraMap A (AdicCompletion (I.map (algebraMap A C)) C)))
Tag 0AL5, a remark
Tag 0AL5 in the Stacks Project.
Rig.adicBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/BaseChange.lean, line 632.
Stacks Project, Tag 0AL5. Let
A₁ → A₂be a ring map andI₁ ⊆ A₁,I₂ ⊆ A₂ideals withI₁ ^ cmapping intoI₂for somec ≥ 1. This induces ring mapsA₁ ⧸ I₁ ^ (cn) → A₂ ⧸ I₂ ^ n, and there is a base change functor(Bₙ) ↦ (B_{cn} ⊗ A₂ ⧸ I₂ ^ n)between the categories of systems. IfI₂is finitely generated there is a base change functorB ↦ (B ⊗[A₁] A₂)^between the categories of complete algebras, and if both ideals are finitely generated the two base change functors agree via the equivalencesB ↦ (B ⧸ IⁿB)ₙ.
public noncomputable def adicBaseChange :
AdicBaseChange.{v, u₁, u₂} A₁ A₂ I₁ I₂ hc hmap
Tag 0AK0, an equation
Tag 0AK0 in the Stacks Project.
Rig.completedBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/CompletedBaseChange.lean, line 759.
Stacks Project, Tag 0AK0. If a positive power of
I₁maps into the finitely generated idealI₂, thenB ↦ (B ⊗[A₁] A₂)⁁is a functor between the categories of adically complete algebras of finite type moduloI₁andI₂.
public noncomputable def completedBaseChange (I₁ : Ideal A₁) (I₂ : Ideal A₂) (c : ℕ)
(hc : 0 < c) (hmap : (I₁ ^ c).map (algebraMap A₁ A₂) ≤ I₂) (hI₂ : I₂.FG) :
CompletedBaseChange (A₁ := A₁) (A₂ := A₂) (I₁ := I₁) (I₂ := I₂)
Tag 0AL6, a remark
Tag 0AL6 in the Stacks Project.
Rig.quotient_isAdicallyComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/AdicAlgebraSystem.lean, line 174. The attribute's comment: “the quotient is complete”.
The quotient of an adically finite type algebra by an ideal from the base is complete for every ideal defining the induced adic topology.
public theorem quotient_isAdicallyComplete
(hc : 0 < c) (hd : 0 < d)
(hI : (I ^ c).map (Ideal.Quotient.mk a) ≤ barI)
(hbarI : barI ^ d ≤ I.map (Ideal.Quotient.mk a))
(B : AdicFiniteTypeAlgebra.{u, v} A I) :
IsAdicComplete (barI.map (algebraMap (A ⧸ a)
(B.carrier ⧸ a.map (algebraMap A B.carrier))))
(B.carrier ⧸ a.map (algebraMap A B.carrier))
Rig.tensor_quotient_completion_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/AdicAlgebraSystem.lean, line 205. The attribute's comment: “completed base change is the quotient”.
The canonical map from the tensor-product presentation of the quotient algebra to its
barI-adic completion is an isomorphism.
public theorem tensor_quotient_completion_bijective
(hc : 0 < c) (hd : 0 < d)
(hI : (I ^ c).map (Ideal.Quotient.mk a) ≤ barI)
(hbarI : barI ^ d ≤ I.map (Ideal.Quotient.mk a))
(B : AdicFiniteTypeAlgebra.{u, v} A I) :
Function.Bijective
(AdicCompletion.of
(baseChangedIdeal (A₂ := A ⧸ a) (I₂ := barI) B)
(baseChangedAlgebra (A₂ := A ⧸ a) B))
Rig.quotientBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Category/AdicAlgebraSystem.lean, line 242. The attribute's comment: “the quotient functor and its natural comparison”.
Base change to a closed subscheme is the quotient functor. The isomorphism to completed base change is the canonical completion map, and quotienting a morphism acts by quotienting its underlying algebra homomorphism.
public theorem quotientBaseChange
(hc : 0 < c) (hd : 0 < d)
(hI : (I ^ c).map (Ideal.Quotient.mk a) ≤ barI)
(hbarI : barI ^ d ≤ I.map (Ideal.Quotient.mk a)) :
∃ (Q : AdicFiniteTypeAlgebra.{u, v} A I ⥤
AdicFiniteTypeAlgebra.{u, max v u} (A ⧸ a) barI),
∃ (η : Q ≅
(completedBaseChange (A₁ := A) (A₂ := A ⧸ a)
I barI c hc hI (Ideal.fg_of_isNoetherianRing barI)).functor),
∃ (e : ∀ B : AdicFiniteTypeAlgebra.{u, v} A I,
(Q.obj B).carrier ≃+* (B.carrier ⧸ a.map (algebraMap A B.carrier))),
(∀ (B : AdicFiniteTypeAlgebra.{u, v} A I) (x : B.carrier),
((completedBaseChange (A₁ := A) (A₂ := A ⧸ a)
I barI c hc hI (Ideal.fg_of_isNoetherianRing barI)).completedTensorProductEquiv B)
(AdicFiniteTypeAlgebra.hom (η.hom.app B)
((e B).symm (Ideal.Quotient.mk (a.map (algebraMap A B.carrier)) x))) =
AdicCompletion.of
(baseChangedIdeal (A₂ := A ⧸ a) (I₂ := barI) B)
(baseChangedAlgebra (A₂ := A ⧸ a) B)
((Algebra.TensorProduct.quotIdealMapEquivTensorQuot B.carrier a)
(Ideal.Quotient.mk (a.map (algebraMap A B.carrier)) x))) ∧
(∀ {B C : AdicFiniteTypeAlgebra.{u, v} A I} (f : B ⟶ C) (x : B.carrier),
e C (AdicFiniteTypeAlgebra.hom (Q.map f)
((e B).symm (Ideal.Quotient.mk (a.map (algebraMap A B.carrier)) x))) =
Ideal.Quotient.mk (a.map (algebraMap A C.carrier))
(AdicFiniteTypeAlgebra.hom f x))
Sources
Section88.3 A naive cotangent complex#
Section 88.3 of the Stacks Project, Tag 0AJL. 7 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AJR, an equation
Tag 0AJR in the Stacks Project.
Rig.completedNaiveCotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent.lean, line 478.
For a supplied presentation
B = A[x₁, …, xᵣ]̂ / J, construct its completed naive cotangent complexJ / J² → ⨁ i, B dxᵢ. Its differential sends the class of a power seriesg ∈ Jto the tuple of its formal partial derivatives.
public noncomputable def completedNaiveCotangentComplex
[IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) : CompletedNaiveCotangentComplex P
Tag 0GAE, a lemma
Tag 0GAE in the Stacks Project.
Rig.completedNaiveCotangentComplex_homotopyEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/NaiveCotangentHomotopy.lean, line 1704.
The completed naive cotangent complexes associated to two completed polynomial presentations of the same
I-adically complete algebra are homotopy equivalent.
public theorem completedNaiveCotangentComplex_homotopyEquiv
{A : Type u} [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(B : AdicFiniteTypeAlgebra.{u, v} A I)
(P Q : CompletedPolynomialPresentation I B) :
Nonempty (HomotopyEquiv
(Rig.completedNaiveCotangentComplex B P).cochainComplex
(Rig.completedNaiveCotangentComplex B Q).cochainComplex)
Tag 0GAF, a lemma
Tag 0GAF in the Stacks Project.
Rig.surjective_completedPresentationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Completion.lean, line 397. The attribute's comment: “B^ = A[x₁, …, xₙ]^ / J^: the completed presentation is surjective”.
The completion
α^ : A[x₁, …, xₙ]^ → B^of a presentationα : A[x₁, …, xₙ] → Bof a finite type algebra over a Noetherian ring is surjective.
public theorem surjective_completedPresentationMap (α : MvPolynomial (Fin n) A →ₐ[A] B)
(hα : Function.Surjective α) : Function.Surjective (completedPresentationMap I α)
Rig.ker_completedPresentationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Completion.lean, line 404. The attribute's comment: “B^ = A[x₁, …, xₙ]^ / J^: the kernel of the completed presentation is J^”.
The kernel of the completion
α^of a presentationαwith kernelJis the idealJ^ = J · A[x₁, …, xₙ]^generated byJin the completed polynomial ring.
public theorem ker_completedPresentationMap (α : MvPolynomial (Fin n) A →ₐ[A] B)
(hα : Function.Surjective α) :
RingHom.ker (completedPresentationMap I α).toRingHom =
(RingHom.ker α.toRingHom).map
(algebraMap (MvPolynomial (Fin n) A) (adicCompletionMvPolynomial I n))
Rig.differential_conormalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Completion.lean, line 522. The attribute's comment: “the comparison commutes with the differentials”.
The square of differentials commutes: both ways round, the class of
g ∈ Jgoes to the tuple of the images inB^of the partial derivatives∂g/∂xᵢ.
public theorem differential_conormalComparison (x : G.toExtension.Cotangent) :
(completedComplex I G).differential (conormalComparison I G x) =
fun i ↦ algebraMap B (adicCompletionObj I (B := B)).carrier
(presentationDifferential G x i)
Rig.completionComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Completion.lean, line 544. The attribute's comment: “the comparison of complexes NL(α) ⊗_B B^ → NL^∧_{B^/A}”.
The canonical comparison of complexes
NL(α) ⊗_B B^ → NL^∧_{B^/A}: in degree-1it is theB^-linear extension of the mapJ / J² → J^ / (J^)²and in degree0it isdxᵢ ↦ dxᵢ.
public def completionComparison :
NaiveCotangent.ChainMap
(baseChangedTwoTerm (adicCompletionObj I (B := B)).carrier (presentationDifferential G))
(completedComplex I G).twoTerm
Rig.bijective_completionComparison_f₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Completion.lean, line 565. The attribute's comment: “the comparison is bijective in degree 0”.
The comparison
NL(α) ⊗_B B^ → NL^∧_{B^/A}is bijective in degree0.
public theorem bijective_completionComparison_f₀ :
Function.Bijective (completionComparison I G).f₀
Rig.bijective_completionComparison_f₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Completion.lean, line 572. The attribute's comment: “the comparison is bijective in degree 1”.
The comparison
NL(α) ⊗_B B^ → NL^∧_{B^/A}is bijective in degree1, that isB^ ⊗_B (J / J²) = J^ / (J^)².
public theorem bijective_completionComparison_f₁ :
Function.Bijective (completionComparison I G).f₁
Rig.bijective_completionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Completion.lean, line 637. The attribute's comment: “NL^∧_{B^/A} = NL(α) ⊗_B B^ as complexes”.
NL^∧_{B^/A} = NL(α) ⊗_B B^as complexes: the comparison of two-term complexes is bijective in both degrees and commutes with the two differentials.
public theorem bijective_completionComparison :
Function.Bijective (completionComparison I G).f₁ ∧
Function.Bijective (completionComparison I G).f₀ ∧
(completedComplex I G).twoTerm.d ∘ₗ (completionComparison I G).f₁ =
(completionComparison I G).f₀ ∘ₗ
(baseChangedTwoTerm (adicCompletionObj I (B := B)).carrier
(presentationDifferential G)).d
Rig.completedNaiveCotangentDerivedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/CompletionDerived.lean, line 236. The attribute's comment: “NL^∧_{B^/A} = NL_{B/A} ⊗^L_B B^ in D(B^)”.
Stacks 0GAF, second clause.
NL^∧_{B^/A} = NL_{B/A} ⊗^L_B B^inD(B^), for the canonical derived tensor product alongB → B^with the unit complexB^in degree0.
public def completedNaiveCotangentDerivedTensorIso :
(CochainComplex.DerivedTensor.canonicalDerivedTensorChangeOfRings
(algebraMap B (adicCompletionObj I (B := B)).carrier)
((CochainComplex.singleFunctor
(ModuleCat.{max u v} (adicCompletionObj I (B := B)).carrier) 0).obj
(ModuleCat.of (adicCompletionObj I (B := B)).carrier
(ULift.{u} (adicCompletionObj I (B := B)).carrier)))).F.obj
(DerivedCategory.Q.obj (naiveCotangentCochain A B)) ≅
DerivedCategory.Q.obj (completedComplex I G).cochainComplex
Rig.bijective_limitComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/CompletionLimit.lean, line 185. The attribute's comment: “lim NL(α) = NL(α) ⊗_B B^ as complexes”.
Stacks 0GAF, the
limform of the first clause.lim NL(α) = NL(α) ⊗_B B^as complexes: the comparison is bijective in both degrees and commutes with the differentials.
public theorem bijective_limitComparison :
Function.Bijective (limitComparison I G).f₁ ∧
Function.Bijective (limitComparison I G).f₀ ∧
(adicLimitTwoTerm I G).d ∘ₗ (limitComparison I G).f₁ =
(limitComparison I G).f₀ ∘ₗ
(baseChangedTwoTerm (adicCompletionObj I (B := B)).carrier
(presentationDifferential G)).d
Rig.bijective_limitCompletionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/CompletionLimit.lean, line 209. The attribute's comment: “NL^∧_{B^/A} = lim NL(α) ⊗_B B^ as complexes”.
Stacks 0GAF, first clause in its
limform.NL^∧_{B^/A} = lim NL(α) ⊗_B B^as complexes: the comparison from the degreewiseI-adic completion ofNL(α)to the completed naive cotangent complex of the completed presentation is bijective in both degrees and commutes with the differentials.
public theorem bijective_limitCompletionComparison :
Function.Bijective (limitCompletionComparison I G).f₁ ∧
Function.Bijective (limitCompletionComparison I G).f₀ ∧
(completedComplex I G).twoTerm.d ∘ₗ (limitCompletionComparison I G).f₁ =
(limitCompletionComparison I G).f₀ ∘ₗ (adicLimitTwoTerm I G).d
Tag 0AJS, a lemma
Tag 0AJS in the Stacks Project.
Rig.CompletedNaiveCotangentComplex.isDerivedLimit_reductionTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/DerivedProLimit.lean, line 657. The attribute's comment: “part (2)”.
Stacks 0AJS (2). Let
Abe a Noetherian ring,I ⊆ Aan ideal andBan object of the category of Stacks 0AL4, presented asB = A⟨x₁, …, x_r⟩ / J. Then the completed naive cotangent complex is the derived inverse limit of the naive cotangent complexes of the reductions,NL^∧_{B/A} = R lim NL_{Bₙ/Aₙ}inD(B): the inverse system{NL_{Bₙ/Aₙ}}has surjective transition maps andNL^∧_{B/A}is its ordinary inverse limit.
public theorem isDerivedLimit_reductionTower [IsNoetherianRing A]
(K : CompletedNaiveCotangentComplex P) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{max u v} B.carrier)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
IsDerivedLimit ((K.reductionTower ⋙ cochainComplexFunctor B.carrier) ⋙
DerivedCategory.Q) (DerivedCategory.Q.obj K.cochainComplex)
Rig.CompletedNaiveCotangentComplex.nonempty_iso_reductionTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/StrictProLimit.lean, line 336. The attribute's comment: “part (1)”.
Stacks 0AJS (1). Let
Abe a Noetherian ring,I ⊆ Aan ideal andBan object of the category of Stacks 0AL4, presented asB = A⟨x₁, …, x_r⟩ / J. Then the pro-objects{NL^∧_{B/A} ⊗_B Bₙ}and{NL_{Bₙ/Aₙ}}are strictly isomorphic: there is one shift making the two systems isomorphic in the strict pro-category, and at every level the second system is the naive cotangent complex of the induced presentationBₙ = Aₙ[x₁, …, x_r] / Jₙ— the conormal modules and the degree-0terms agree and the two differentials correspond.
public theorem nonempty_iso_reductionTower [IsNoetherianRing A]
(K : CompletedNaiveCotangentComplex P) :
Nonempty (proObj K.completedReductionTower ≅ proObj K.reductionTower) ∧
∀ n : ℕ, ∃ (e₁ : (K.reductionTower.obj (op n)).X₁ ≃ₗ[B.carrier]
(P.reductionGenerators n).toExtension.Cotangent)
(e₀ : (K.reductionTower.obj (op n)).X₀ ≃ₗ[B.carrier]
(P.reductionGenerators n).toExtension.CotangentSpace),
∀ x, e₀ ((K.reductionTower.obj (op n)).d x) =
(P.reductionGenerators n).toExtension.cotangentComplex (e₁ x)
Tag 0GAG, a lemma
Tag 0GAG in the Stacks Project.
Rig.baseChangeComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/BaseChangeComparison.lean, line 251. The attribute's comment: “the comparison map”.
The canonical comparison map
NL^∧_{B₁/A₁} ⊗_{B₁} B₂ → NL^∧_{B₂/A₂}, for the presentation ofB₁cut out by a generating familygofB₁moduloI₁and the compatible presentation of the base changeB₂in the same variables.In degree
-1it is theB₂-linear extension of the mapJ₁ / J₁² → J₂ / J₂²induced by the base-change map of completed polynomial algebras, and in degree0it isdxᵢ ↦ dxᵢ.
public def baseChangeComparison :
NaiveCotangent.ChainMap
(baseChangedTwoTerm B₂.carrier
(completedNaiveCotangentComplex B₁ (ofGenerators B₁ r g hI₁ hgen)).differential)
(completedNaiveCotangentComplex B₂
(baseChangePresentation (B₁ := B₁) hI₂ hc hmap hspan r g hgen)).twoTerm
Rig.bijective_onH₀_baseChangeComparison_of_completedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/BaseChangeComparison.lean, line 369. The attribute's comment: “isomorphism on H⁰”.
Let
(A₁, I₁) → (A₂, I₂)be as in Stacks Remark 0AL5 — a map of Noetherian pairs carrying a positive power ofI₁intoI₂— letB₁be adically of finite type over(A₁, I₁), and letB₂be its completed base change(B₁ ⊗_{A₁} A₂)^∧_{I₂}. Then the canonical comparison mapNL^∧_{B₁/A₁} ⊗_{B₁} B₂ → NL^∧_{B₂/A₂}ofRig.baseChangeComparisoninduces an isomorphism onH⁰. The identification ofB₂with(B₁ ⊗_{A₁} A₂)^∧_{I₂}is the datae,heA,heB.
public theorem bijective_onH₀_baseChangeComparison_of_completedBaseChange :
Function.Bijective (baseChangeComparison hI₁ hI₂ hc hmap
(le_span_range_sup_adicIdeal_of_completedBaseChange hI₂ e heA heB) r g hgen).onH₀
Rig.surjective_onH₁_baseChangeComparison_of_completedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/BaseChangeComparison.lean, line 381. The attribute's comment: “surjection on H⁻¹”.
In the situation of
Rig.bijective_onH₀_baseChangeComparison_of_completedBaseChange—(A₁, I₁) → (A₂, I₂)as in Stacks Remark 0AL5 with both rings Noetherian, andB₂the completed base change ofB₁— the canonical comparison mapNL^∧_{B₁/A₁} ⊗_{B₁} B₂ → NL^∧_{B₂/A₂}induces a surjection onH⁻¹.
public theorem surjective_onH₁_baseChangeComparison_of_completedBaseChange :
Function.Surjective (baseChangeComparison hI₁ hI₂ hc hmap
(le_span_range_sup_adicIdeal_of_completedBaseChange hI₂ e heA heB) r g hgen).onH₁
Tag 0ALM, a lemma
Tag 0ALM in the Stacks Project.
Rig.CompletedPolynomialPresentation.exists_sixTerm_exact_combined, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/CombinedPresentation.lean, line 1196.
The six-term exact sequence of Stacks 0ALM.
Let
Abe a Noetherian ring,I ⊆ Aan ideal,Ban object of (Stacks 0AL4) with a completed polynomial presentationB = A⟨x₁, …, x_r⟩/J, andCan object of (0AL4) overBpresented overBbyψ : B⟨y₁, …, y_s⟩ ↠ C, so thatC = A⟨x, y⟩/Kby the combined presentation. Then there is an exact sequenceH⁻¹(NL^∧_{B/A} ⊗_B C) → H⁻¹(NL^∧_{C/A}) → H⁻¹(NL^∧_{C/B}) --δ--> H⁰(NL^∧_{B/A} ⊗_B C) → H⁰(NL^∧_{C/A}) → H⁰(NL^∧_{C/B}) → 0.Every input of
NaiveCotangent.exists_sixTerm_exact_of_finAppendis now discharged: the degree-0row is the split row⨁_{i<r} C → ⨁_{i<r+s} C → ⨁_{j<s} Cof that file, the degree-1row isRig.CompletedPolynomialPresentation.exact_cotangentMap_combinedtogether with..._surjective_cotangentMap_combined, and the two squares are the two lemmas above.This theorem alone is the content of the tag: the combined presentation, the two commuting squares and the right exactness of the degree-
1row are steps of the source's proof, not part of its statement.
public theorem exists_sixTerm_exact_combined
(hFc : ∀ j, @Continuous _ _
(RestrictedPowerSeries.polynomialCompletionLimitTopology B.adicIdeal (Fin s))
(RestrictedPowerSeries.polynomialCompletionLimitTopology B.adicIdeal (Fin s)) (F j))
(hFp : ∀ (j : Fin s) (q : MvPolynomial (Fin s) B.carrier),
F j (algebraMap (MvPolynomial (Fin s) B.carrier)
(AdicCompletion.completedMvPolynomial B.adicIdeal (Fin s)) q) =
algebraMap (MvPolynomial (Fin s) B.carrier)
(AdicCompletion.completedMvPolynomial B.adicIdeal (Fin s))
(MvPolynomial.pderiv j q)) :
∃ δ : NaiveCotangent.H₁
(NaiveCotangent.TwoTerm.ofFree (outerDifferential s ψ hψ F)) →ₗ[C.carrier]
NaiveCotangent.H₀
(NaiveCotangent.TwoTerm.ofFree (P.innerBaseChangeDifferential (C := C) KB)),
Function.Exact
(NaiveCotangent.chainMapInl _
(P.combinedDifferential_comp_innerCotangentMap s ψ hψ KB KC)).onH₁
(NaiveCotangent.chainMapProj _
(P.outerDifferential_comp_outerCotangentMap s ψ hψ KC F hFc hFp)).onH₁ ∧
Function.Exact
(NaiveCotangent.chainMapProj _
(P.outerDifferential_comp_outerCotangentMap s ψ hψ KC F hFc hFp)).onH₁ δ ∧
Function.Exact δ
(NaiveCotangent.chainMapInl _
(P.combinedDifferential_comp_innerCotangentMap s ψ hψ KB KC)).onH₀ ∧
Function.Exact
(NaiveCotangent.chainMapInl _
(P.combinedDifferential_comp_innerCotangentMap s ψ hψ KB KC)).onH₀
(NaiveCotangent.chainMapProj _
(P.outerDifferential_comp_outerCotangentMap s ψ hψ KC F hFc hFp)).onH₀ ∧
Function.Surjective
(NaiveCotangent.chainMapProj _
(P.outerDifferential_comp_outerCotangentMap s ψ hψ KC F hFc hFp)).onH₀
Tag 0AQJ, a lemma
Tag 0AQJ in the Stacks Project.
Rig.CompletedPolynomialPresentation.injective_onH₁_chainMapInl_of_lci, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/CombinedLci.lean, line 1014.
Stacks 0AQJ. Let
Abe Noetherian,I ⊆ Aan ideal,B → Ca morphism of the category (Stacks 0AL4),B = A⟨x₁, …, x_r⟩ / Ja completed polynomial presentation andψ : B⟨y₁, …, y_s⟩ ↠ Ca presentation ofCoverB. Assume thatB / IⁿB → C / IⁿCis a local complete intersection homomorphism for everyn ≥ 1. Then the first map
H⁻¹(NL^∧_{B/A} ⊗_B C) ⟶ H⁻¹(NL^∧_{C/A})of the six-term sequence of Stacks 0ALM is injective. The map is the one induced on
H⁻¹by the left-hand chain map of that sequence, namely the chain map ofRig.CompletedPolynomialPresentation.combinedDifferential_comp_innerCotangentMap.
public theorem injective_onH₁_chainMapInl_of_lci
(KB : CompletedNaiveCotangentComplex P)
(KC : CompletedNaiveCotangentComplex
(P.combinedPresentation s (ψ.restrictScalars A) hψ))
(h : ∀ n : ℕ, RingHom.IsLocalCompleteIntersection (reductionMap B C (n + 1))) :
Function.Injective (NaiveCotangent.chainMapInl _
(P.combinedDifferential_comp_innerCotangentMap s ψ hψ KB KC)).onH₁
Sources
Section88.4 Rig-smooth algebras#
Section 88.4 of the Stacks Project, Tag 0GAH. 5 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GAI, a definition
Tag 0GAI in the Stacks Project.
Rig.IsRigSmooth, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothDefs.lean, line 60.
Stacks Project, Tag 0GAI. Rig-smoothness of an adically finite type
A-algebra over(A, I): some uniform power ofIannihilatesExt¹from its completed naive cotangent complex to everyB-module.
public def IsRigSmooth (B : AdicFiniteTypeAlgebra.{u, v} A I) : Prop
Tag 0GAJ, a lemma
Tag 0GAJ in the Stacks Project.
Rig.isRigSmooth_iff_cotangentCohomologyCondition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigSmoothCriteria/Equivalences.lean, line 377. The attribute's comment: “conditions (1) and (2)”.
Rig-smoothness is equivalent to the cohomological criterion for the completed naive cotangent complex.
public theorem isRigSmooth_iff_cotangentCohomologyCondition
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B) :
Rig.IsRigSmooth B ↔ HasCotangentCohomologyCondition B P
Rig.isRigSmooth_iff_cotangentFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigSmoothCriteria/Equivalences.lean, line 403. The attribute's comment: “conditions (1) and (3)”.
Rig-smoothness is equivalent to uniform factorization of powers of the ideal of definition through the differential of a chosen completed naive cotangent complex.
public theorem isRigSmooth_iff_cotangentFactorization
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B) :
Rig.IsRigSmooth B ↔ HasCotangentFactorization B P
Rig.isRigSmooth_iff_hasJacobianCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigSmoothCriteria/Equivalences.lean, line 459. The attribute's comment: “conditions (1) and (4)”.
Rig-smoothness is equivalent to a finite Jacobian cover away from the ideal of definition.
public theorem isRigSmooth_iff_hasJacobianCover
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B) :
Rig.IsRigSmooth B ↔ HasJacobianCover B P
Rig.isElementPowerTorsion_hneg_of_jacobianChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigSmoothCriteria/Equivalences.lean, line 527. The attribute's comment: “the proof of (4) ⟹ (2): H⁻¹(NL^∧) is b_l-power torsion”.
Stacks 0GAJ, inside the proof of (4) ⟹ (2). Let
bcarry a Jacobian chart: a subsetTofmof the variables andmelementsf₁, …, fₘof the presentation idealJwhose Jacobian minor alongTdividesb, withb J ⊆ (f₁, …, fₘ) + J². ThenH⁻¹(NL^∧_{B/A})isb-power torsion; in factb²already annihilates it.
public theorem isElementPowerTorsion_hneg_of_jacobianChart
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) (b : P.completedPolynomialRing)
{m : ℕ} (T : Fin m ↪ Fin P.variableCount) (f : Fin m → P.ker)
(hdet : P.toAlgHom
(Matrix.det fun i j : Fin m ↦
(completedNaiveCotangentComplex B P).partialDeriv (T i) (f j : P.completedPolynomialRing)) ∣
P.toAlgHom b)
(hrelations : ∀ x : P.completedPolynomialRing, x ∈ P.ker →
b * x ∈ Ideal.span (Set.range fun j : Fin m ↦ (f j : P.completedPolynomialRing)) +
P.ker ^ 2) :
IsElementPowerTorsion B.carrier (completedNaiveCotangentComplex B P).Hneg
(P.toAlgHom b)
Rig.free_localized_hzero_of_jacobianChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigSmoothCriteria/JacobianChartPointwise.lean, line 411. The attribute's comment: “the proof of (4) ⟹ (2): H⁰(NL^∧) is finite free after inverting b_l”.
Stacks 0GAJ, inside the proof of (4) ⟹ (2). Let
bcarry a Jacobian chart: a subsetTofmof the variables andmelementsf₁, …, fₘof the presentation idealJwhose Jacobian minor alongTdividesb, withb J ⊆ (f₁, …, fₘ) + J². ThenH⁰(NL^∧_{B/A})becomes finite free after invertingb.
public theorem free_localized_hzero_of_jacobianChart
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) (b : P.completedPolynomialRing)
{m : ℕ} (T : Fin m ↪ Fin P.variableCount) (f : Fin m → P.ker)
(hdet : P.toAlgHom
(Matrix.det fun i j : Fin m ↦
(completedNaiveCotangentComplex B P).partialDeriv (T i) (f j : P.completedPolynomialRing)) ∣
P.toAlgHom b)
(hrelations : ∀ x : P.completedPolynomialRing, x ∈ P.ker →
b * x ∈ Ideal.span (Set.range fun j : Fin m ↦ (f j : P.completedPolynomialRing)) +
P.ker ^ 2) :
Module.Free (Localization.Away (P.toAlgHom b))
(LocalizedModule (Submonoid.powers (P.toAlgHom b))
(completedNaiveCotangentComplex B P).Hzero) ∧
Module.Finite (Localization.Away (P.toAlgHom b))
(LocalizedModule (Submonoid.powers (P.toAlgHom b))
(completedNaiveCotangentComplex B P).Hzero)
Tag 0GAK, a lemma
Tag 0GAK in the Stacks Project.
Rig.isRigSmooth_adicCompletionObj_of_smoothAwayFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigSmoothSmoothLocus.lean, line 705. The attribute's comment: “part (1)”.
Stacks 0GAK (1). If
Spec(B) → Spec(A)is smooth overSpec(A) ∖ V(I), then theI-adic completionB^is rig-smooth over(A, I).
public theorem isRigSmooth_adicCompletionObj_of_smoothAwayFrom (h : SmoothAwayFrom A I B) :
IsRigSmooth (adicCompletionObj I (B := B))
Rig.exists_sub_one_mem_and_smoothAwayFrom_of_isRigSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigSmoothSmoothLocus.lean, line 747. The attribute's comment: “part (2)”.
Stacks 0GAK (2). If the
I-adic completionB^is rig-smooth over(A, I), then there isg ∈ 1 + IBsuch thatSpec(B_g) → Spec(A)is smooth overSpec(A) ∖ V(I).
public theorem exists_sub_one_mem_and_smoothAwayFrom_of_isRigSmooth
(h : IsRigSmooth (adicCompletionObj I (B := B))) :
∃ g : B, g - 1 ∈ I.map (algebraMap A B) ∧ SmoothAwayFrom A I (Localization.Away g)
Tag 0GAL, a lemma
Tag 0GAL in the Stacks Project.
Rig.smul_ext_one_completedBaseChangeOfIsNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/BaseChangeExt.lean, line 556.
Stacks Project, Tag 0GAL. Let
(A₁, I₁) → (A₂, I₂)be as in Stacks Remark 0AL5 — a ring mapA₁ → A₂of Noetherian rings with idealsI₁ ⊆ A₁,I₂ ⊆ A₂such thatI₁ ^ cmaps intoI₂for somec ≥ 1— letB₁be adically of finite type over(A₁, I₁)(Stacks 0AL4), letB₂ = (B₁ ⊗_{A₁} A₂)^∧be its base change, the value atB₁of the completed base-change functorRig.completedBaseChangeOfIsNoetherianRingof Remark 0AL5, and letf₂ ∈ B₂be the image off₁ ∈ B₁, that is off₁ ⊗ 1(Rig.CompletedBaseChange.scalar). Iff₁annihilatesExt¹_{B₁}(NL^∧_{B₁/A₁}, N₁)for everyB₁-moduleN₁, thenf₂annihilatesExt¹_{B₂}(NL^∧_{B₂/A₂}, N₂)for everyB₂-moduleN₂.The completed cotangent complexes are computed from arbitrary completed polynomial presentations
P₁andP₂, on which they do not depend (Stacks 0GAE).
public theorem smul_ext_one_completedBaseChangeOfIsNoetherianRing
(hpow : ∃ c : ℕ, 0 < c ∧ (I₁ ^ c).map (algebraMap A₁ A₂) ≤ I₂)
(B₁ : AdicFiniteTypeAlgebra.{u₁, v} A₁ I₁)
(P₁ : CompletedPolynomialPresentation I₁ B₁)
(P₂ : CompletedPolynomialPresentation I₂
((completedBaseChangeOfIsNoetherianRing hpow).functor.obj B₁))
(f₁ : B₁.carrier)
(h : ∀ (N : ModuleCat.{max u₁ v} B₁.carrier)
(ξ : DerivedCategory.Ext (derivedCompletedNaiveCotangentComplex B₁ P₁)
((DerivedCategory.singleFunctor (ModuleCat.{max u₁ v} B₁.carrier) 0).obj N) 1),
f₁ • ξ = 0) :
∀ (N : ModuleCat.{max u₂ v}
((completedBaseChangeOfIsNoetherianRing hpow).functor.obj B₁).carrier)
(ξ : DerivedCategory.Ext
(derivedCompletedNaiveCotangentComplex
((completedBaseChangeOfIsNoetherianRing hpow).functor.obj B₁) P₂)
((DerivedCategory.singleFunctor (ModuleCat.{max u₂ v}
((completedBaseChangeOfIsNoetherianRing hpow).functor.obj B₁).carrier) 0).obj N) 1),
(completedBaseChangeOfIsNoetherianRing hpow).scalar B₁ f₁ • ξ = 0
Tag 0GAM, a lemma
Tag 0GAM in the Stacks Project.
Rig.isRigSmooth_completedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothBaseChange.lean, line 135.
Stacks Project, Tag 0GAM. Rig-smoothness is preserved by completed base change along a map of Noetherian rings whose source and target ideals define the same closed subset of the target spectrum.
public theorem isRigSmooth_completedBaseChange
(hV : (I₁.map (algebraMap A₁ A₂)).radical = I₂.radical)
(C : CompletedBaseChange (A₁ := A₁) (A₂ := A₂) (I₁ := I₁) (I₂ := I₂))
(B₁ : AdicFiniteTypeAlgebra.{u₁, v} A₁ I₁) (hB₁ : IsRigSmooth B₁) :
IsRigSmooth (C.functor.obj B₁)
Rig.isRigSmooth_completedBaseChangedAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothCompletedBaseChange.lean, line 86.
Stacks Project, Tag 0GAM. Let
A₁ → A₂be a map of Noetherian rings and letI₁ ⊆ A₁,I₂ ⊆ A₂be ideals withV(I₁ A₂) = V(I₂). IfB₁is rig-smooth over(A₁, I₁), then its base changeB₂ = (B₁ ⊗_{A₁} A₂)^, theI₂-adic completion of Remark 0AL5, is rig-smooth over(A₂, I₂).
public theorem isRigSmooth_completedBaseChangedAlgebra
(hV : (I₁.map (algebraMap A₁ A₂)).radical = I₂.radical)
(B₁ : AdicFiniteTypeAlgebra.{u₁, v} A₁ I₁) (hB₁ : IsRigSmooth B₁) :
IsRigSmooth (I := I₂)
(⟨CommAlgCat.of A₂ (completedBaseChangedAlgebra (I₂ := I₂) B₁),
isAdicComplete_and_finiteType_completedBaseChangedAlgebra hV B₁⟩ :
AdicFiniteTypeAlgebra.{u₂, max v u₂} A₂ I₂)
Sources
Section88.5 Deformations of ring homomorphisms#
Section 88.5 of the Stacks Project, Tag 0GAN. 5 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AK3, a remark
Tag 0AK3 in the Stacks Project.
Rig.exists_continuousAlgHom_add_variables, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Deformation.lean, line 294. The attribute's comment: “existence of the perturbed map”.
A continuous algebra map on restricted series can be perturbed by arbitrary increments in the images of its finitely many variables.
public theorem exists_continuousAlgHom_add_variables
{A : Type u} [CommRing A] (I : Ideal A) (hI : I.FG)
{C : Type w} [CommRing C] [Algebra A C]
[IsAdicComplete (I.map (algebraMap A C)) C]
{σ : Type v}
(ψ : RestrictedPowerSeries I σ →ₐ[A] C)
(hψ : @Continuous _ _ (limitTopology I σ)
((I.map (algebraMap A C)).adicTopology) ψ)
(δ : σ → C) :
∃! ψ' : RestrictedPowerSeries I σ →ₐ[A] C,
@Continuous _ _ (limitTopology I σ)
((I.map (algebraMap A C)).adicTopology) ψ' ∧
∀ i, ψ' (polynomialAlgHom I σ (MvPolynomial.X i)) =
ψ (polynomialAlgHom I σ (MvPolynomial.X i)) + δ i
Rig.eval_add_variables_eq_linear_add_error, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Deformation.lean, line 347. The attribute's comment: “linear approximation and quadratic error”.
The evaluation of a perturbed restricted series is its original evaluation plus the formal linear term, up to the ideal generated by pairwise products of increments.
public theorem eval_add_variables_eq_linear_add_error
{A : Type u} [CommRing A] (I : Ideal A) (hI : I.FG)
{C : Type w} [CommRing C] [Algebra A C]
[IsAdicComplete (I.map (algebraMap A C)) C]
{σ : Type v} [Fintype σ]
(ψ ψ' : RestrictedPowerSeries I σ →ₐ[A] C)
(hψ : @Continuous _ _ (limitTopology I σ)
((I.map (algebraMap A C)).adicTopology) ψ)
(hψ' : @Continuous _ _ (limitTopology I σ)
((I.map (algebraMap A C)).adicTopology) ψ')
(δ : σ → C)
(hδ : ∀ i, ψ' (polynomialAlgHom I σ (MvPolynomial.X i)) =
ψ (polynomialAlgHom I σ (MvPolynomial.X i)) + δ i)
(g : RestrictedPowerSeries I σ) :
∃ ξ : C,
ξ ∈ Ideal.span (Set.range (fun ij : σ × σ ↦ δ ij.1 * δ ij.2)) ∧
ψ' g = ψ g + (∑ i, ψ (partialDerivative I i g) * δ i) + ξ
Tag 0GAP, a remark
Tag 0GAP in the Stacks Project.
Rig.exists_perturbed_continuousAlgHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Lifting.lean, line 412. The attribute's comment: “the lifting claim”.
Stacks 0GAP, the lifting claim, in the principal case.
Let
I = (a), letCbe anI-adically completeA-algebra on whichais a nonzerodivisor, and letJbe an ideal ofA⟨x₁, …, x_r⟩satisfying the obstruction relationa ^ c · g ≡ ∑ i (∂g/∂xᵢ) γᵢmoduloJ²for a fixed familyγ₁, …, γ_r ∈ J. Then a continuousA-algebra mapψ : A⟨x₁, …, x_r⟩ → Cwithψ(J) ⊆ aⁿCcan be perturbed to a continuousψ'withψ'(J) ⊆ a^{2(n-c)}C, the perturbation taking values ina^{n-c}C.The perturbation is
xᵢ ↦ ψ(xᵢ) - δᵢwherea ^ c δᵢ = ψ(γᵢ); the two conclusions are the first-order expansion of Stacks 0AK3 applied to it.
public theorem exists_perturbed_continuousAlgHom (a : A) (I : Ideal A) (hI : I = Ideal.span {a})
{C : Type w} [CommRing C] [Algebra A C] [IsAdicComplete (I.map (algebraMap A C)) C]
(ha : IsRegular (algebraMap A C a))
{r : ℕ} (Jid : Ideal (RestrictedPowerSeries I (Fin r))) (c n : ℕ) (hc : c ≤ n)
(γ : Fin r → RestrictedPowerSeries I (Fin r)) (hγ : ∀ i, γ i ∈ Jid)
(hcramer : ∀ g ∈ Jid, algebraMap A (RestrictedPowerSeries I (Fin r)) (a ^ c) * g
- ∑ i, partialDerivative I i g * γ i ∈ Jid ^ 2)
(ψ : RestrictedPowerSeries I (Fin r) →ₐ[A] C)
(hψc : @Continuous _ _ (limitTopology I (Fin r))
((I.map (algebraMap A C)).adicTopology) ψ)
(hψJ : ∀ g ∈ Jid, ψ g ∈ (I.map (algebraMap A C)) ^ n) :
∃ ψ' : RestrictedPowerSeries I (Fin r) →ₐ[A] C,
(@Continuous _ _ (limitTopology I (Fin r))
((I.map (algebraMap A C)).adicTopology) ψ') ∧
(∀ g ∈ Jid, ψ' g ∈ (I.map (algebraMap A C)) ^ (2 * (n - c))) ∧
(∀ g, ψ' g - ψ g ∈ (I.map (algebraMap A C)) ^ (n - c))
Rig.sub_mem_pow_two_mul_of_sub_mem_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingGeneral.lean, line 119. The attribute's comment: “the obstruction map o(ψ) is well defined”.
Stacks 0GAP, the well-definedness of the obstruction map. Representatives of one class in
J / J²have the same image inIⁿC / I²ⁿC, soo(ψ) : J/J² → IⁿC/I²ⁿC,g ↦ ψ(g), is well defined.
public theorem sub_mem_pow_two_mul_of_sub_mem_sq (JC : Ideal C) (Jid : Ideal Rs) (n : ℕ)
(ψ : Rs →ₐ[A] C) (hψJ : ∀ g ∈ Jid, ψ g ∈ JC ^ n) (g g' : Rs) (h : g - g' ∈ Jid ^ 2) :
ψ g - ψ g' ∈ JC ^ (2 * n)
Rig.exists_obstruction_difference_of_lifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingGeneral.lean, line 169. The attribute's comment: “o(ψₙ) does not depend on the chosen lift”.
Stacks 0GAP, the independence of the obstruction class of the chosen lift. Two continuous
A-algebra mapsψ, ψ' : A⟨x₁, …, x_r⟩ → Cthat reduce to the same map moduloIⁿCsatisfy
ψ'(g) - ψ(g) - ∑ i, ψ(∂g/∂xᵢ) εᵢ ∈ I²ⁿCfor everyg,with
εᵢ = ψ'(xᵢ) - ψ(xᵢ) ∈ IⁿC. So the obstruction mapso(ψ')ando(ψ)differ by the composite of the differential ofNL^∧_{B/A}withdxᵢ ↦ εᵢ, and therefore define the same class inExt¹_B(NL^∧_{B/A}, IⁿC/I²ⁿC).
public theorem exists_obstruction_difference_of_lifts (I : Ideal A) (hI : I.FG)
{C : Type w} [CommRing C] [Algebra A C] [IsAdicComplete (I.map (algebraMap A C)) C]
{r : ℕ} (n : ℕ)
(ψ ψ' : RestrictedPowerSeries I (Fin r) →ₐ[A] C)
(hψc : @Continuous _ _ (limitTopology I (Fin r))
((I.map (algebraMap A C)).adicTopology) ψ)
(hψ'c : @Continuous _ _ (limitTopology I (Fin r))
((I.map (algebraMap A C)).adicTopology) ψ')
(hsame : ∀ g, ψ' g - ψ g ∈ (I.map (algebraMap A C)) ^ n) :
∃ ε : Fin r → C, (∀ i, ε i ∈ (I.map (algebraMap A C)) ^ n) ∧
∀ g, ψ' g - ψ g - ∑ i, ψ (partialDerivative I i g) * ε i
∈ (I.map (algebraMap A C)) ^ (2 * n)
Rig.exists_perturbed_algHom_of_obstruction_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingGeneral.lean, line 257. The attribute's comment: “the lifting claim, arbitrary ideal”.
Stacks 0GAP, the power-series computation, for an arbitrary ideal
I.Let
Cbe anI-adically completeA-algebra,Jan ideal ofA⟨x₁, …, x_r⟩, andψ : A⟨x₁, …, x_r⟩ → Ca continuousA-algebra map. Suppose there areδ₁, …, δ_r ∈ I^{n'}Cwith
ψ(g) - ∑ i, ψ(∂g/∂xᵢ) δᵢ ∈ I^{2n'}Cfor everyg ∈ J,which is the statement that the obstruction map of
ψagrees withh ∘ dintoI^{n'}C / I^{2n'}C, forh : ⨁ i, B dxᵢ → I^{n'}C / I^{2n'}Cthe map sendingdxᵢto the class ofδᵢ. Thenψ' : xᵢ ↦ ψ(xᵢ) - δᵢis a continuousA-algebra map withψ'(J) ⊆ I^{2n'}C, andψ' - ψtakes values inI^{n'}C.No principality of
I, no regularity onCand no relation betweenn'and the precision ofψare used; the two conclusions are the first-order expansion of Stacks 0AK3 applied to the perturbation.
public theorem exists_perturbed_algHom_of_obstruction_factors (I : Ideal A) (hI : I.FG)
{C : Type w} [CommRing C] [Algebra A C] [IsAdicComplete (I.map (algebraMap A C)) C]
{r : ℕ} (Jid : Ideal (RestrictedPowerSeries I (Fin r))) (n' : ℕ)
(ψ : RestrictedPowerSeries I (Fin r) →ₐ[A] C)
(hψc : @Continuous _ _ (limitTopology I (Fin r))
((I.map (algebraMap A C)).adicTopology) ψ)
(δ : Fin r → C) (hδ : ∀ i, δ i ∈ (I.map (algebraMap A C)) ^ n')
(hfac : ∀ g ∈ Jid, ψ g - ∑ i, ψ (partialDerivative I i g) * δ i
∈ (I.map (algebraMap A C)) ^ (2 * n')) :
∃ ψ' : RestrictedPowerSeries I (Fin r) →ₐ[A] C,
(@Continuous _ _ (limitTopology I (Fin r))
((I.map (algebraMap A C)).adicTopology) ψ') ∧
(∀ g ∈ Jid, ψ' g ∈ (I.map (algebraMap A C)) ^ (2 * n')) ∧
(∀ g, ψ' g - ψ g ∈ (I.map (algebraMap A C)) ^ n')
Rig.exists_algHom_quotient_of_obstruction_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingGeneral.lean, line 319. The attribute's comment: “the claim”.
Stacks 0GAP, the claim of the remark, for an arbitrary ideal
I.Let
Abe a ring with a finitely generated idealI, letBbe anI-adically completeA-algebra of finite type moduloIwith a completed polynomial presentationB = A⟨x₁, …, x_r⟩ / J, and letCbe anI-adically completeA-algebra. Letψₙ : B → C / IⁿCbe anA-algebra map andψ : A⟨x₁, …, x_r⟩ → Ca continuous lift of it.If the obstruction map of
ψmaps to zero inExt¹_B(NL^∧_{B/A}, I^{n'}C / I^{2n'}C)for somen' ≤ n— that is, if there areδ₁, …, δ_r ∈ I^{n'}Cwithψ(g) - ∑ i, ψ(∂g/∂xᵢ) δᵢ ∈ I^{2n'}Cfor everyg ∈ J— then there is anA-algebra homomorphismψ'_{2n'} : B → C / I^{2n'}Cwhich agrees withψₙas maps intoC / I^{n'}C.Neither principality of
Inor regularity of anything onCis assumed, and no Cramer relation onJis hypothesised: the only input is the vanishing of the obstruction class.
public theorem exists_algHom_quotient_of_obstruction_factors
{I : Ideal A} (hI : I.FG) {B : AdicFiniteTypeAlgebra.{u, v} A I}
(P : CompletedPolynomialPresentation I B)
{C : Type w} [CommRing C] [Algebra A C] [IsAdicComplete (I.map (algebraMap A C)) C]
(n n' : ℕ) (hn' : n' ≤ n)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n)
(ψ : RestrictedPowerSeries I (Fin P.variableCount) →ₐ[A] C)
(hψc : @Continuous _ _ (limitTopology I (Fin P.variableCount))
((I.map (algebraMap A C)).adicTopology) ψ)
(hψred : ∀ g, Ideal.Quotient.mk ((I.map (algebraMap A C)) ^ n) (ψ g)
= ψn (P.restrictedToAlgHom g))
(δ : Fin P.variableCount → C) (hδ : ∀ i, δ i ∈ (I.map (algebraMap A C)) ^ n')
(hfac : ∀ g ∈ P.restrictedKer, ψ g - ∑ i, ψ (partialDerivative I i g) * δ i
∈ (I.map (algebraMap A C)) ^ (2 * n')) :
∃ ψ₂ : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ (2 * n'),
(Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (by omega : n' ≤ 2 * n'))).comp ψ₂
= (Ideal.Quotient.factorₐ A (Ideal.pow_le_pow_right hn')).comp ψn
Rig.exists_algHom_quotient_of_obstruction_vanishes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingGeneral.lean, line 374. The attribute's comment: “the claim, with the lift chosen internally”.
Stacks 0GAP, the claim of the remark with the lift of
ψₙproduced internally.For a Noetherian
A, anA-algebra mapψₙ : B → C/IⁿCwhose obstruction class vanishes inExt¹_B(NL^∧_{B/A}, I^{n'}C/I^{2n'}C)— the vanishing being witnessed, as in the source, on some continuous liftψofψₙ, which byRig.obstruction_factors_of_lift_changeis the same as on every one — lifts toψ'_{2n'} : B → C/I^{2n'}Cagreeing withψₙintoC/I^{n'}C.
public theorem exists_algHom_quotient_of_obstruction_vanishes
{I : Ideal A} (hI : I.FG) {B : AdicFiniteTypeAlgebra.{u, v} A I}
(P : CompletedPolynomialPresentation I B)
{C : Type w} [CommRing C] [Algebra A C] [IsAdicComplete (I.map (algebraMap A C)) C]
(n n' : ℕ) (hn' : n' ≤ n)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n)
(hvanish : ∀ ψ : RestrictedPowerSeries I (Fin P.variableCount) →ₐ[A] C,
@Continuous _ _ (limitTopology I (Fin P.variableCount))
((I.map (algebraMap A C)).adicTopology) ψ →
(∀ g, Ideal.Quotient.mk ((I.map (algebraMap A C)) ^ n) (ψ g)
= ψn (P.restrictedToAlgHom g)) →
∃ δ : Fin P.variableCount → C, (∀ i, δ i ∈ (I.map (algebraMap A C)) ^ n') ∧
∀ g ∈ P.restrictedKer, ψ g - ∑ i, ψ (partialDerivative I i g) * δ i
∈ (I.map (algebraMap A C)) ^ (2 * n')) :
∃ ψ₂ : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ (2 * n'),
(Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (by omega : n' ≤ 2 * n'))).comp ψ₂
= (Ideal.Quotient.factorₐ A (Ideal.pow_le_pow_right hn')).comp ψn
Rig.exists_obstruction_factors_of_exists_algHom_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingGeneral.lean, line 405. The attribute's comment: “o(ψₙ) is the obstruction: the converse”.
Stacks 0GAP, the converse of the claim:
o(ψₙ)is the obstruction, not merely an obstruction. Ifψₙ : B → C/IⁿCdoes lift to anA-algebra mapψ₂ : B → C/I²ⁿC, then the obstruction map of any continuous liftψofψₙalready factors through the differential ofNL^∧_{B/A}, i.e.o(ψₙ) = 0inExt¹_B(NL^∧_{B/A}, IⁿC/I²ⁿC).The proof is the independence of the obstruction class of the chosen lift: a continuous lift
χofψ₂is in particular a lift ofψₙwithχ(J) ⊆ I²ⁿC, soo(χ) = 0, ando(ψ) = o(χ) - h ∘ dforh : dxᵢ ↦ χ(xᵢ) - ψ(xᵢ).
public theorem exists_obstruction_factors_of_exists_algHom_quotient
{I : Ideal A} (hI : I.FG) {B : AdicFiniteTypeAlgebra.{u, v} A I}
(P : CompletedPolynomialPresentation I B)
{C : Type w} [CommRing C] [Algebra A C] [IsAdicComplete (I.map (algebraMap A C)) C]
(n : ℕ)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n)
(ψ : RestrictedPowerSeries I (Fin P.variableCount) →ₐ[A] C)
(hψc : @Continuous _ _ (limitTopology I (Fin P.variableCount))
((I.map (algebraMap A C)).adicTopology) ψ)
(hψred : ∀ g, Ideal.Quotient.mk ((I.map (algebraMap A C)) ^ n) (ψ g)
= ψn (P.restrictedToAlgHom g))
(ψ₂ : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ (2 * n))
(hψ₂ : (Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (show n ≤ 2 * n by omega))).comp ψ₂ = ψn) :
∃ δ : Fin P.variableCount → C, (∀ i, δ i ∈ (I.map (algebraMap A C)) ^ n) ∧
∀ g ∈ P.restrictedKer, ψ g - ∑ i, ψ (partialDerivative I i g) * δ i
∈ (I.map (algebraMap A C)) ^ (2 * n)
Rig.obstruction_factors_iff_exists_algHom_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingGeneral.lean, line 457. The attribute's comment: “o(ψₙ) is the obstruction to lifting ψₙ to C/I²ⁿC”.
Stacks 0GAP, the headline sentence of the remark: the obstruction to lifting
ψₙ : B → C/IⁿCtoC/I²ⁿCis the classo(ψₙ). Reading the class through the cokernel description ofExt¹_B(NL^∧_{B/A}, IⁿC/I²ⁿC)of Stacks 0ALN part (1), its vanishing says that the obstruction map of a continuous liftψofψₙish ∘ dfor someh : ⨁ i, B dxᵢ → IⁿC/I²ⁿC, i.e. that there areδ₁, …, δ_r ∈ IⁿCwithψ(g) - ∑ i, ψ(∂g/∂xᵢ) δᵢ ∈ I²ⁿCfor everyg ∈ J.
public theorem obstruction_factors_iff_exists_algHom_quotient
{I : Ideal A} (hI : I.FG) {B : AdicFiniteTypeAlgebra.{u, v} A I}
(P : CompletedPolynomialPresentation I B)
{C : Type w} [CommRing C] [Algebra A C] [IsAdicComplete (I.map (algebraMap A C)) C]
(n : ℕ)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n)
(ψ : RestrictedPowerSeries I (Fin P.variableCount) →ₐ[A] C)
(hψc : @Continuous _ _ (limitTopology I (Fin P.variableCount))
((I.map (algebraMap A C)).adicTopology) ψ)
(hψred : ∀ g, Ideal.Quotient.mk ((I.map (algebraMap A C)) ^ n) (ψ g)
= ψn (P.restrictedToAlgHom g)) :
(∃ δ : Fin P.variableCount → C, (∀ i, δ i ∈ (I.map (algebraMap A C)) ^ n) ∧
∀ g ∈ P.restrictedKer, ψ g - ∑ i, ψ (partialDerivative I i g) * δ i
∈ (I.map (algebraMap A C)) ^ (2 * n))
↔ ∃ ψ₂ : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ (2 * n),
(Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (show n ≤ 2 * n by omega))).comp ψ₂ = ψn
Rig.exists_conormal_cramer_relation_of_ext_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Obstruction.lean, line 245. The attribute's comment: “the obstruction class”.
Stacks 0GAP. The obstruction relation in the form the lifting arguments use: if
bannihilates every first Ext group of the completed naive cotangent complex, andβliftsbtoA⟨x₁, …, x_r⟩, then there areγ₁, …, γ_r ∈ Jwith
β · g - ∑ i, (∂g/∂xᵢ) · γᵢ ∈ J²for everyg ∈ J.Applying an
A-algebra mapψ : A⟨x₁, …, x_r⟩ → Cwithψ(J) ⊆ IⁿCturns this into the statement thatb · o(ψ)is the composite of the differential with the mapdxᵢ ↦ ψ(γᵢ) mod I²ⁿC, i.e. that the obstruction class is killed byb.
public theorem exists_conormal_cramer_relation_of_ext_annihilated
(K : CompletedNaiveCotangentComplex P) (b : B.carrier)
(β : P.completedPolynomialRing) (hβ : P.toAlgHom β = b)
(hExt : ∀ (N : ModuleCat.{max u v} B.carrier)
(ξ : DerivedCategory.Ext (DerivedCategory.Q.obj K.cochainComplex)
((DerivedCategory.singleFunctor (ModuleCat.{max u v} B.carrier) 0).obj N) 1),
b • ξ = 0) :
∃ γ : Fin P.variableCount → P.completedPolynomialRing,
(∀ i, γ i ∈ P.ker) ∧
∀ g ∈ P.ker, β * g - ∑ i, K.partialDeriv i g * γ i ∈ P.ker ^ 2
Rig.ObstructionLift.obstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ObstructionClass.lean, line 295. The attribute's comment: “the obstruction map o(ψ) : J/J² → IᵐC/I²ᵐC”.
Stacks 0GAP, the obstruction map. The
B-linear map
o(ψ) : J/J² → IᵐC/I²ᵐC,g ↦ ψ(g),well defined because
ψ(J) ⊆ IᵐCforcesψ(J²) ⊆ I²ᵐC. TheB-action on the target is throughresidue, i.e. through the reduction ofψmoduloIᵐC.
public def obstruction : P.extension.Cotangent →ₗ[B.carrier] D.target
Rig.ObstructionLift.obstructionBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ObstructionClass.lean, line 313. The attribute's comment: “the C-linear extension of o(ψ) over J/J² ⊗_B C”.
Stacks 0GAP, the
C-linear extension of the obstruction map. Since theB-action onIᵐC/I²ᵐCfactors throughC/IᵐC, theB-linear mapo(ψ)extends to aC/IᵐC-linear map
(C/IᵐC) ⊗_B J/J² → IᵐC/I²ᵐC.This is the extension the remark records after constructing
o(ψ).
public def obstructionBaseChange :
D.base ⊗[B.carrier] P.extension.Cotangent →ₗ[D.base] D.target
Rig.ObstructionLift.extClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ObstructionClass.lean, line 383. The attribute's comment: “the obstruction class o(ψₘ) in Ext¹_B(NL^∧_{B/A}, IᵐC/I²ᵐC)”.
Stacks 0GAP, the obstruction class
o(ψₘ) ∈ Ext¹_B(NL^∧_{B/A}, IᵐC/I²ᵐC),the image of
o(ψ)under the identification ofExt¹withCoker (Hom_B(⨁ B dxᵢ, -) → Hom_B(J/J², -))of Stacks 0ALN part (1).
public def extClass :
DerivedCategory.Ext (DerivedCategory.Q.obj K.cochainComplex)
((DerivedCategory.singleFunctor (ModuleCat.{max u v} B.carrier) 0).obj
(ModuleCat.of B.carrier D.target)) 1
Rig.ObstructionLift.extClass_eq_zero_iff_exists_linearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ObstructionClass.lean, line 395. The attribute's comment: “the vanishing of o(ψₘ) as a factorization through d”.
Stacks 0GAP: the obstruction class vanishes exactly when
o(ψ)factors through the differential ofNL^∧_{B/A}, i.e. exactly when there is aB-linearh : ⨁ i, B dxᵢ → IᵐC/I²ᵐCwithh ∘ d = o(ψ). This is the cokernel description of Stacks 0ALN part (1), read on the completed naive cotangent complex.
public theorem extClass_eq_zero_iff_exists_linearMap :
D.extClass K = 0 ↔
∃ h : (Fin P.variableCount → B.carrier) →ₗ[B.carrier] D.target,
∀ z, h (K.differential z) = D.obstruction z
Rig.ObstructionLift.extClass_eq_zero_iff_exists_delta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ObstructionClass.lean, line 454. The attribute's comment: “the vanishing of o(ψₘ) on representatives”.
Stacks 0GAP: the obstruction class vanishes exactly when there are
δ₁, …, δ_r ∈ IᵐCwith
ψ(g) - ∑ i, ψ(∂g/∂xᵢ) δᵢ ∈ I²ᵐCfor everyg ∈ J.The
δᵢare representatives of the valuesh(dxᵢ)of the factorisationhof the previous theorem; this is the form in which the lifting argument consumes the vanishing.
public theorem extClass_eq_zero_iff_exists_delta :
D.extClass K = 0 ↔
∃ δ : Fin P.variableCount → C, (∀ i, δ i ∈ (I.map (algebraMap A C)) ^ m) ∧
∀ g ∈ P.ker, D.lift g - ∑ i, D.lift (K.partialDeriv i g) * δ i
∈ (I.map (algebraMap A C)) ^ (2 * m)
Rig.exists_algHom_quotient_of_extClass_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ObstructionClass.lean, line 503. The attribute's comment: “the claim, with the hypothesis as the vanishing of the Ext class”.
Stacks 0GAP, the claim of the remark with its hypothesis in the form the remark states it: the vanishing of the obstruction class in
Ext¹_B(NL^∧_{B/A}, I^{n'}C/I^{2n'}C).Let
Abe a Noetherian ring,Ia finitely generated ideal,BanI-adically completeA-algebra of finite type moduloIwith a completed polynomial presentationB = A⟨x₁, …, x_r⟩ / J, andCanI-adically completeA-algebra. Letψₙ : B → C/IⁿCbe anA-algebra map andDa continuous lift of it toA⟨x₁, …, x_r⟩withD.lift(J) ⊆ I^{n'}C, for somen' ≤ n. Ifo(ψ_{n'}) = 0inExt¹_B(NL^∧_{B/A}, I^{n'}C/I^{2n'}C), then there is anA-algebra homomorphismψ'_{2n'} : B → C/I^{2n'}Cagreeing withψₙas maps intoC/I^{n'}C.Arbitrary
I, no regularity hypothesis, and no Cramer relation assumed.
public theorem exists_algHom_quotient_of_extClass_eq_zero [IsNoetherianRing A] (hI : I.FG)
[IsAdicComplete (I.map (algebraMap A C)) C] (n n' : ℕ) (hn' : n' ≤ n)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n)
(D : ObstructionLift P C n')
(hcont : @Continuous _ _ (limitTopology I (Fin P.variableCount))
((I.map (algebraMap A C)).adicTopology)
(D.lift.comp (adicCompletionAlgEquiv I (Fin P.variableCount)).toAlgHom))
(hred : ∀ g, Ideal.Quotient.mk ((I.map (algebraMap A C)) ^ n)
(D.lift (adicCompletionAlgEquiv I (Fin P.variableCount) g))
= ψn (P.restrictedToAlgHom g))
(hvanish : D.extClass (completedNaiveCotangentComplex B P) = 0) :
∃ ψ₂ : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ (2 * n'),
(Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (show n' ≤ 2 * n' by omega))).comp ψ₂
= (Ideal.Quotient.factorₐ A (Ideal.pow_le_pow_right hn')).comp ψn
Tag 0GAQ, a lemma
Tag 0GAQ in the Stacks Project.
Rig.exists_algHom_lift_of_dualSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingUniformity.lean, line 809. The attribute's comment: “with the conclusion at precision I^{n-(2+D)c}, D = max(d,1) -- the level the library's Tag 0GAD reaches -- in place of the source's I^{n-(1+d)c}, and with n > 2(2+D)c for the source's n > 2(1+d)c; the Ext hypothesis is used through Tag 0GAP's cokernel form and Tag 0GAC, so Tags 0E1W, 0G9G and 0GAD are not invoked; carries 0GAC's open duality input as hdual, and d, q₀ as a family S of DualSituations with m-independent invariants”.
Stacks 0GAQ, with the precision of the conclusion corrected as in the library's Tag 0GAD.
Let
Abe a Noetherian ring,I ⊆ Aan ideal,Ban object of the category of Stacks 0AL4 for(A, I)with a completed polynomial presentationP, and supposeI ^ cannihilatesExt¹_B(NL^∧_{B/A}, N)for everyB-moduleN. LetCbe a NoetherianI-adically completeA-algebra whose invariants of Local Cohomology, Section 0GA6 aredandq₀, writeD = k + 1 = max(d, 1), and letn ≥ q₀ + (1+D)cwithn > 2(2+D)c. Then everyA-algebra mapψₙ : B → C / IⁿCagrees moduloI^{n-(2+D)c}with the reduction of anA-algebra mapφ : B → C.Deviation from the source. The source concludes agreement modulo
I^{n-(1+d)c}undern ≥ max(q₀ + (1+d)c, 2(1+d)c + 1). The level reached here isn - (2+D)c, which is the level the source's argument for Tag 0GAD reaches withDin place ofd(Stacks.LocalCohomology.UniformityIII.CanDualSituation.ext_one_powQuot_map_eq_zeroatd), and the bound onnis adjusted ton > 2(2+D)caccordingly;D = max(d, 1)in place ofdis inherited from the library's Tag 0GAC. The discrepancy is the one that Tag 0GAD's docstring records: the source's own argument produces maps at leveln - (2+d)c, and ford ≥ 1the module it asserts the obstruction dies in admits no canonical map to or from the one its argument reaches. Twisting down is harmless for the iteration, so the only effect is on the numbers.The route. The source passes from
Ext¹_B(NL^∧_{B/A}, N)toExt¹_{C/IⁿC}of the derived base change (Tags 0E1W and 0G9G) in order to apply Tag 0GAD. Here the Ext-annihilation hypothesis is used through Tag 0GAP in its cokernel form — the obstruction relationa · g ≡ ∑ i (∂g/∂xᵢ) γᵢmoduloJ²ofRig.exists_restricted_cramer_relation— which base changes toC / IᵐCby elementary means, so that Tag 0GAC applies directly to the explicit two-term complex and Tags 0E1W, 0G9G and 0GAD itself are not needed. The level reached is the one of Tag 0GAD, as it must be: the argument is the same.The carried hypotheses.
Sis the family ofDualSituations of Tag 0GA6, one for each thicknessm, with the invariantsdandq₀independent ofm(hd,hq₀); the structure carries the blowup cohomology of Tag 0GAA, which the library does not build from the blowup.hdualis the open duality input of the library's Tag 0GAC, carried for every levelm ≥ n: it is the section ofp^*(M^∨)at levelm - 2cobtained by factoring throughcan : p^*(M^∨) → (p^*M)^∨, whose kernel and cokernel being scheme theoretically supported onY_cis not available. Nothing else is assumed.
public theorem exists_algHom_lift_of_dualSituation
{I : Ideal A} (B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) (c : ℕ)
(hExt : ∀ a ∈ I ^ c, ∀ (N : ModuleCat.{max u v} B.carrier)
(ξ : DerivedCategory.Ext
(DerivedCategory.Q.obj (completedNaiveCotangentComplex B P).cochainComplex)
((DerivedCategory.singleFunctor (ModuleCat.{max u v} B.carrier) 0).obj N) 1),
(algebraMap A B.carrier a) • ξ = 0)
{C : Type u} [CommRing C] [IsNoetherianRing C] [Algebra A C]
[IsAdicComplete (I.map (algebraMap A C)) C]
(S : ∀ m : ℕ, DualSituation C (I.map (algebraMap A C)) m c)
(d q₀ k : ℕ) (hd : ∀ m, (S m).d = d) (hq₀ : ∀ m, (S m).q₀ = q₀)
(hk : max d 1 = k + 1)
(n : ℕ) (hn₁ : q₀ + (k + 2) * c ≤ n) (hn₂ : 2 * ((k + 3) * c) < n)
(hdual : ∀ (m e : ℕ) (_ : n ≤ m) (hem : e + 2 * c = m) (hq : (S m).q₀ ≤ e)
(M : ANCModule (I.map (algebraMap A C)) m c)
(φ : resModule (I.map (algebraMap A C)) m M.1 →ₗ[C]
powQuot (I.map (algebraMap A C)) m m),
∃ σ' : (S m).H M.dual 0 (e : ℤ),
(S m).ev M e hq σ'
= (powQuotLe (I.map (algebraMap A C)) (Nat.le.intro hem)).comp φ)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n) :
∃ φ : B.carrier →ₐ[A] C,
(Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (Nat.sub_le n ((k + 3) * c)))).comp ψn =
(Ideal.Quotient.mkₐ A ((I.map (algebraMap A C)) ^ (n - (k + 3) * c))).comp φ
Rig.exists_algHom_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/LiftingUniformitySource.lean, line 124. The attribute's comment: “with d = d(Gr_I(C)) and q₀ = q(Gr_I(C)) the defining quantities of Section 0GA6 computed on the blowup of Spec(C) in IC (maximal fibre dimension and the threshold qS), and NL^∧_{B/A} computed from a completed polynomial presentation P of B”.
Stacks Project, Tag 0GAQ. Let
c ≥ 0, letIbe an ideal of a Noetherian ringA, letBbe in the category of Stacks 0AL4 for(A, I), with a completed polynomial presentationP, such thatI ^ cannihilatesExt¹_B(NL^∧_{B/A}, N)for everyB-moduleN, and letCbe a NoetherianI-adically completeA-algebra. Denoted = d(Gr_I(C))andq₀ = q(Gr_I(C))the integers of Local Cohomology, Section 0GA6. Then forn ≥ max(q₀ + (d + 1)c, 2(d + 1)c + 1)everyA-algebra mapψₙ : B → C/IⁿCagrees moduloI^{n-(d+1)c}with the reduction of anA-algebra mapφ : B → C.The two integers are the defining quantities of Section 0GA6, computed on the blowup
XofSpec(C)inIC:dis the maximal dimension of the fibres ofX ⟶ Spec(C)(Stacks.LocalCohomology.UniformityIII.fibreDim, a maximum byStacks.LocalCohomology.UniformityIII.topologicalKrullDim_fiber_le_fibreDimandStacks.LocalCohomology.UniformityIII.fibreDim_le), andq₀is the least integer past which the twists𝒪_Y(q)of the exceptional divisor have no higher cohomology and global sectionsI^q C/I^{q+1} C(Stacks.LocalCohomology.UniformityIII.qS), which is the source'sq(S)becauseHⁱ(Y, 𝒪_Y(q))vanishes fori > danyway (Stacks 02V7;Stacks.LocalCohomology.UniformityIII.qS_isLeast_isBaseThresholdUpTo_fibreDim).The proof. The obstruction relation of Stacks 0GAP makes the obstruction complex
[(C/IᵐC) ⊗ J → (C/IᵐC)ʳ]of a lift a two-term complex whose differential splits multiplication byI^c; the obstruction then dies at levelm - (d+1)cby the corrected Tag 0GAD (Stacks.LocalCohomology.UniformityIII.exists_extension_of_split), and the iteration of the source (Rig.exists_algHom_lift_of_extension) passes to the limit in the complete ringC. The source's own argument for Tag 0GAD reaches onlym - (2+d)cford > 0; the argument used is the one the source gives ford = 0(a local lift and the vanishing of a global obstruction), carried out for everyd, which reaches the source's level.
public theorem exists_algHom_lift
{I : Ideal A} (B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) (c : ℕ)
(hExt : ∀ a ∈ I ^ c, ∀ (N : ModuleCat.{max u v} B.carrier)
(ξ : DerivedCategory.Ext
(DerivedCategory.Q.obj (completedNaiveCotangentComplex B P).cochainComplex)
((DerivedCategory.singleFunctor (ModuleCat.{max u v} B.carrier) 0).obj N) 1),
(algebraMap A B.carrier a) • ξ = 0)
{C : Type u} [CommRing C] [IsNoetherianRing C] [Algebra A C]
[IsAdicComplete (I.map (algebraMap A C)) C]
(n : ℕ)
(hn : max (qS (I.map (algebraMap A C)) +
(fibreDim (I.map (algebraMap A C)) + 1) * c)
(2 * ((fibreDim (I.map (algebraMap A C)) + 1) * c) + 1) ≤ n)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n) :
∃ φ : B.carrier →ₐ[A] C,
(Ideal.Quotient.factorₐ A (Ideal.pow_le_pow_right
(Nat.sub_le n ((fibreDim (I.map (algebraMap A C)) + 1) * c)))).comp ψn =
(Ideal.Quotient.mkₐ A ((I.map (algebraMap A C)) ^
(n - (fibreDim (I.map (algebraMap A C)) + 1) * c))).comp φ
Tag 0AK6, a lemma
Tag 0AK6 in the Stacks Project.
Rig.exists_algHom_lift_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Lifting.lean, line 683.
Stacks 0AK6. Let
I = (a)be a principal ideal of a Noetherian ringA, letBbe anI-adically completeA-algebra of finite type moduloI, and supposea ^ cannihilatesExt¹_B(NL^∧_{B/A}, N)for everyB-moduleN. LetCbe anI-adically completeA-algebra on whichais a nonzerodivisor and letn > 2c. Then everyA-algebra mapB → C / aⁿCagrees moduloa ^ (n - c)with the reduction of anA-algebra mapB → C.
public theorem exists_algHom_lift_of_isRegular
(a : A) (I : Ideal A) (hI : I = Ideal.span {a})
(B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B)
(c : ℕ)
(hExt : ∀ (N : ModuleCat.{max u v} B.carrier)
(ξ : DerivedCategory.Ext
(DerivedCategory.Q.obj (completedNaiveCotangentComplex B P).cochainComplex)
((DerivedCategory.singleFunctor (ModuleCat.{max u v} B.carrier) 0).obj N) 1),
(algebraMap A B.carrier a) ^ c • ξ = 0)
{C : Type w} [CommRing C] [Algebra A C]
[IsAdicComplete (I.map (algebraMap A C)) C]
(ha : IsRegular (algebraMap A C a))
(n : ℕ) (hn : 2 * c < n)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n) :
∃ φ : B.carrier →ₐ[A] C,
(Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (Nat.sub_le n c))).comp ψn =
(Ideal.Quotient.mkₐ A ((I.map (algebraMap A C)) ^ (n - c))).comp φ
Tag 0AK7, a lemma
Tag 0AK7 in the Stacks Project.
Rig.exists_algHom_lift_of_torsion_disjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/DeformationPrincipal.lean, line 240.
Stacks 0AK7. Let
I = (a)be a principal ideal of a Noetherian ringA, letBbe anI-adically completeA-algebra of finite type moduloI, and supposea ^ cannihilatesExt¹_B(NL^∧_{B/A}, N)for everyB-moduleN. LetCbe anI-adically completeA-algebra whosea-power torsionC[a^∞]meetsa^d Cin0, and letn > max (2c) (c + d). Then everyA-algebra mapB → C / aⁿCagrees moduloa ^ (n - c)with the reduction of anA-algebra mapB → C.This drops the regularity hypothesis of Stacks 0AK6: the torsion is killed, 0AK6 is applied to
C / C[a^∞], and the resulting map is glued with the reduction ofψₙalong the cartesian square of quotients ofCbyC[a^∞]anda^{n-c}C.
public theorem exists_algHom_lift_of_torsion_disjoint
(a : A) (I : Ideal A) (hI : I = Ideal.span {a})
(B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B)
(c : ℕ)
(hExt : ∀ (N : ModuleCat.{max u v} B.carrier)
(ξ : DerivedCategory.Ext
(DerivedCategory.Q.obj (completedNaiveCotangentComplex B P).cochainComplex)
((DerivedCategory.singleFunctor (ModuleCat.{max u v} B.carrier) 0).obj N) 1),
(algebraMap A B.carrier a) ^ c • ξ = 0)
{C : Type w} [CommRing C] [Algebra A C]
[IsAdicComplete (I.map (algebraMap A C)) C]
(d : ℕ)
(htorsion : Disjoint (torsionIdeal C (algebraMap A C a))
((I.map (algebraMap A C)) ^ d))
(n : ℕ) (hn : max (2 * c) (c + d) < n)
(ψn : B.carrier →ₐ[A] C ⧸ (I.map (algebraMap A C)) ^ n) :
∃ φ : B.carrier →ₐ[A] C,
(Ideal.Quotient.factorₐ A
(Ideal.pow_le_pow_right (Nat.sub_le n c))).comp ψn =
(Ideal.Quotient.mkₐ A ((I.map (algebraMap A C)) ^ (n - c))).comp φ
Sources
Section88.6 Algebraization of rig-smooth algebras over G-rings#
Section 88.6 of the Stacks Project, Tag 0ALU. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GAR, a lemma
Tag 0GAR in the Stacks Project.
Rig.PerturbedPresentation.exists_algEquiv_of_perturbation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RigSmooth/PerturbationAlgEquiv.lean, line 147.
Stacks 0GAR. Let
Ibe an ideal of a Noetherian ringA,r ≥ 0andP = A[x₁, …, x_r]^∧theI-adic completion. LetP^⊕t --K--> P^⊕m --(g₁, …, g_m)--> P → B → 0be a resolution of the quotientB = P/(g₁, …, g_m), and assumeBis rig-smooth over(A, I). Then there is an integern₀such that for everyn ≥ n₀and every complexP^⊕t --K'--> P^⊕m --(g'₁, …, g'_m)--> Pwithgᵢ - g'ᵢ ∈ IⁿPandK - K' ∈ Iⁿ Mat(m × t, P)there is an isomorphism ofA-algebrasB ≅ B' = P/(g'₁, …, g'_m); moreover the perturbed complex is again a resolution.The proof is the source's. * (A)
I^cannihilatesExt¹_B(NL^∧_{B/A}, -)for somec, by rig-smoothness (exists_extAnnihilated_of_isRigSmooth). * (B) Fornbeyond an Artin-Rees constant of the resolution the perturbed complex is a resolution (Stacks 07VE) andGr_I(B) ≅ Gr_I(B')— as the equality of initial forms of the two ideals (Stacks 07VF,exists_perturbationBound_sameInitialForms). * (C) The invariants of Local Cohomology, Section 0GA6 are those ofB:q₀ = q(Gr_I(B))serves forB'becauseqonly depends onGr_I(isBaseThreshold_quotIdeal_of_sameInitialForms), and the vanishing degreedis read off a generating family ofI, so it serves for every quotient ofP(subsingleton_blowupHmod_of_span). * Lemma 0GAQ (Rig.exists_algHom_lift_of_dualSituation', viaexists_comparison_algHom_of_liftingInputsAboveExponent) lifts the canonicalB → B'/IⁿB'to anA-algebra mapφ : B → B'congruent to it modulo a fixed power ofI; its inputs are the blowup's dual situations and the duality input of Tag 0GAC (liftingInputsOfIsBaseThreshold). * The final paragraph: such aφis an isomorphism (exists_perturbationBound_algEquiv_of_algHom, by Artin-Rees and Nakayama).The integer
n₀absorbs the precision loss of the lifting lemma, so its exact value is immaterial; the source's choice ismax(c₁ + 1, q₀ + (d₀ + 1)c, 2(d₀ + 1)c + 1).
public theorem exists_algEquiv_of_perturbation {t m : ℕ}
(K : (Fin t → completedPolynomialAlgebra I r) →ₗ[completedPolynomialAlgebra I r]
(Fin m → completedPolynomialAlgebra I r))
(g : (Fin m → completedPolynomialAlgebra I r) →ₗ[completedPolynomialAlgebra I r]
completedPolynomialAlgebra I r)
(hexact : LinearMap.ker g = LinearMap.range K)
(hB : IsRigSmooth (quotientObj A I r (LinearMap.range g))) :
∃ n₀ : ℕ, ∀ n ≥ n₀,
∀ (K' : (Fin t → completedPolynomialAlgebra I r) →ₗ[completedPolynomialAlgebra I r]
(Fin m → completedPolynomialAlgebra I r))
(g' : (Fin m → completedPolynomialAlgebra I r) →ₗ[completedPolynomialAlgebra I r]
completedPolynomialAlgebra I r),
g'.comp K' = 0 →
CongruentModPow (I.map (algebraMap A (completedPolynomialAlgebra I r))) K K' n →
CongruentModPow (I.map (algebraMap A (completedPolynomialAlgebra I r))) g g' n →
LinearMap.ker g' = LinearMap.range K' ∧
Nonempty
((completedPolynomialAlgebra I r ⧸
(LinearMap.range g : Ideal (completedPolynomialAlgebra I r))) ≃ₐ[A]
(completedPolynomialAlgebra I r ⧸
(LinearMap.range g' : Ideal (completedPolynomialAlgebra I r))))
Tag 0GAS, a lemma
Tag 0GAS in the Stacks Project.
Rig.exists_finiteType_adicCompletion_algEquiv_henselization_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/GRing.lean, line 414.
A quotient of the henselization of a finite type
A-algebra has a completion algebraizable by a finite typeA-algebra.
public theorem exists_finiteType_adicCompletion_algEquiv_henselization_quotient
(A : Type u) (C : Type v) [CommRing A] [IsNoetherianRing A]
[CommRing C] [Algebra A C] [Algebra.FiniteType A C]
(I : Ideal A)
(J : Ideal (henselization C (I.map (algebraMap A C)) : Type v)) :
let H := (henselization C (I.map (algebraMap A C)) : Type v)
letI : Algebra A H :=
((algebraMap C H).comp (algebraMap A C)).toAlgebra
∃ (B : Type (max u v)) (_ : CommRing B) (_ : Algebra A B)
(_ : Algebra.FiniteType A B),
Nonempty (AdicCompletion (I.map (algebraMap A B)) B ≃ₐ[A]
AdicCompletion (I.map (algebraMap A (H ⧸ J))) (H ⧸ J))
Tag 0GAT, a proposition
Tag 0GAT in the Stacks Project.
Rig.exists_finiteType_adicCompletion_algEquiv_of_isGRing_of_isRigSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/PerturbationStableQuotients.lean, line 110.
Stacks Project, Proposition 0GAT. Let
Ibe an ideal of a Noetherian G-ringAand letBbe an object of the category of Tag 0AL4. IfBis rig-smooth over(A, I), then there is a finite typeA-algebraCand an isomorphismB ≅ C^∧ofA-algebras.Every step of the source's proof is carried out:
Rig.exists_finiteType_adicCompletion_algEquiv_of_isRigSmooth'runs the presentation (Tag 0AJP), its finite free resolution, the henselizationHof(A[x], I A[x])with its G-ring property (Tags 07PV, 0AH3) and completionP(Tag 0AGV), the approximation of the resolution's relations overH(Tag 0AH5, with Popescu's Theorem 07GC and Tag 0AH2), and the final algebraization (Tag 0GAS); Lemma 0GAR isRig.perturbationStableQuotients.
public theorem exists_finiteType_adicCompletion_algEquiv_of_isGRing_of_isRigSmooth
(A : Type u) [CommRing A] [IsNoetherianRing A] (hA : IsGRing A) (I : Ideal A)
(B : AdicFiniteTypeAlgebra.{u, v} A I) (hB : IsRigSmooth B) :
∃ (C : Type (max u v)) (_ : CommRing C) (_ : Algebra A C),
Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)
Tag 0AK4, a lemma
Tag 0AK4 in the Stacks Project.
Stacks.Smoothing.exists_etale_neighbourhood_algHom_approximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smoothing/ApproximationOfCompletionMaps.lean, line 188. The attribute's comment: “the full conclusion with NO carried hypotheses, for every N ≥ 1: an étale C-algebra C' inducing an isomorphism C / IC ≅ C' / IC' (indeed C / (IC)^n ≅ C' / (IC)^n C' for every n), and an A-algebra map B → C' agreeing modulo I ^ N with the given map of I-adic completions. Stacks 0AH5 is used, not assumed, and the IsIndSmoothAdicCompletion hypothesis it carries in place of the source's G-ring is discharged by Popescu's Theorem 07GC (indSmooth_of_isRegularRingMap) through isIndSmoothAdicCompletion_of_isGRing, applied once to the henselization of (C, IC), which is a G-ring by 0AH3 and whose completion map is regular by 0AH2. Stacks 0AKJ supplies the single étale stage.”.
Stacks 0AK4. Let
Abe a Noetherian G-ring,I ⊆ Aan ideal andB,Cfinite typeA-algebras. EveryA-algebra mapψbetween theI-adic completions ofBandCis approximated, to every positive orderN, by anA-algebra mapφ : B → C'into an étaleC-algebraC'whose closed fibre agrees with that ofC.
public theorem exists_etale_neighbourhood_algHom_approximation
(A : Type u) (B : Type v) (C : Type w)
[CommRing A] (hA : IsGRing A)
[CommRing B] [Algebra A B] [Algebra.FiniteType A B]
[CommRing C] [Algebra A C] [Algebra.FiniteType A C]
(I : Ideal A)
(ψ : AdicCompletion (I.map (algebraMap A B)) B →ₐ[A]
AdicCompletion (I.map (algebraMap A C)) C)
(N : ℕ) (hN : 1 ≤ N) :
∃ (C' : Type (max u v w)) (_ : CommRing C') (_ : Algebra C C')
(_ : Algebra A C') (_ : IsScalarTower A C C') (_ : Algebra.Etale C C')
(φ : B →ₐ[A] C'),
(∀ n : ℕ, Function.Bijective
(Ideal.quotientMap (((I.map (algebraMap A C)) ^ n).map (algebraMap C C'))
(algebraMap C C') Ideal.le_comap_map)) ∧
Function.Bijective
(Ideal.quotientMap ((I.map (algebraMap A C)).map (algebraMap C C'))
(algebraMap C C') Ideal.le_comap_map) ∧
∀ b : B,
Ideal.quotientMap (((I.map (algebraMap A C)) ^ N).map (algebraMap C C'))
(algebraMap C C') Ideal.le_comap_map
(AdicCompletion.evalₐ (I.map (algebraMap A C)) N
(ψ (algebraMap B (AdicCompletion (I.map (algebraMap A B)) B) b))) =
Ideal.Quotient.mk (((I.map (algebraMap A C)) ^ N).map (algebraMap C C')) (φ b)
Sources
Section88.7 Algebraization of rig-smooth algebras#
Section 88.7 of the Stacks Project, Tag 0GAU. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GAV, a lemma
Tag 0GAV in the Stacks Project.
Rig.jacobianDet_smul_naiveCotangentComplex_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization.lean, line 183. The attribute's comment: “square_null_action”.
For a square presentation
B = A[x₁, …, xₙ]/(f₁, …, fₙ), the image of the Jacobian determinant annihilatesNL_{B/A}in the derived category ofB-modules.
public theorem jacobianDet_smul_naiveCotangentComplex_eq_zero
(A : Type u) [CommRing A] (n : ℕ)
(f : Fin n → MvPolynomial (Fin n) A) :
(Ideal.Quotient.mk (Ideal.span (Set.range f))
(Matrix.det (fun i j : Fin n ↦ MvPolynomial.pderiv i (f j)))) •
𝟙 (Deformation.Artin.derivedNaiveCotangentComplex A
(MvPolynomial (Fin n) A ⧸ Ideal.span (Set.range f))) = 0
Rig.jacobianDet_smul_ext_one_naiveCotangentComplex_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization.lean, line 525. The attribute's comment: “ext_annihilation”.
Let
B = A[x₁, …, xₙ]/(f₁, …, fₘ), wherem ≤ n. The image inBof the Jacobian determinant formed with the firstmvariables annihilatesExt¹_B(NL_{B/A}, N)for everyB-moduleN.
public theorem jacobianDet_smul_ext_one_naiveCotangentComplex_eq_zero
(A : Type u) [CommRing A] (m n : ℕ) (f : Fin m → MvPolynomial (Fin n) A)
(h : m ≤ n)
(N : ModuleCat.{max u v}
(MvPolynomial (Fin n) A ⧸ Ideal.span (Set.range f)))
(x : DerivedCategory.Ext
(derivedNaiveCotangentComplex A
(MvPolynomial (Fin n) A ⧸ Ideal.span (Set.range f)))
((DerivedCategory.singleFunctor
(ModuleCat.{max u v} (MvPolynomial (Fin n) A ⧸ Ideal.span (Set.range f))) 0).obj N) 1) :
Ideal.Quotient.mk (Ideal.span (Set.range f))
(Matrix.det (fun i j : Fin m => MvPolynomial.pderiv (Fin.castLE h i) (f j))) • x = 0
Tag 0GAW, a lemma
Tag 0GAW in the Stacks Project.
Rig.exists_finiteType_adicCompletion_algEquiv_of_jacobianChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/JacobianChartAlgebraization.lean, line 972.
Stacks Project, Tag 0GAW: the Jacobian criterion for algebraization.
Let
Abe a Noetherian ring,I ⊆ Aan ideal andBanI-adically completeA-algebra withB/IBof finite type overA/I(an object of Stacks 0AL4), presented asB = A⟨x₁, …, x_r⟩/J. Assume there areb ∈ B,0 ≤ m ≤ randf₁, …, f_m ∈ Jsuch that
V(b) ⊆ V(IB)inSpec(B),- the image of
Δ = det(∂fⱼ/∂xᵢ)_{1 ≤ i, j ≤ m}inBdividesb, andbJ ⊆ (f₁, …, f_m) + J².Then there exist a finite type
A-algebraCand anA-algebra isomorphismB ≅ C^∧.Here
bis given by a lift toA⟨x⟩; condition (1) isIB ⊆ √(b).The proof. As in the source,
Cis the algebraA[z₁, …, z_t, x₁, …, x_r]/(z₁Δ' - a₁^{c₁}, …, z_tΔ' - a_t^{c₁}, f'₁, …, f'_m)of Stacks 0GAV built from polynomial approximationsf'ⱼof thefⱼand generatorsa₁, …, a_tofI, and it maps ontoB/IⁿB. The lift of that map toφ : C^∧ → Bis produced by Newton's method (exists_algHom_newton): in this algebra the Jacobian determinant of the relations with respect toz₁, …, z_t, x₁, …, x_misΔ'^{t+1}, and the relations themselves force a fixed power ofIintoΔ'B, so the linearized equations can be solved exactly at each step and the source's uniform lifting result Stacks 0GAQ is not needed.φis surjective because it is surjective moduloI, a power ofIkillsKer(φ)/Ker(φ)²(exists_pow_smul_cotangent_eq_bot_of_jacobianChart, the source's application of Stacks 0ALM and of the comparison of free modules of rankr - m), and Stacks 0ALR concludes.
public theorem exists_finiteType_adicCompletion_algEquiv_of_jacobianChart
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B)
(m : ℕ) (hm : m ≤ P.variableCount) (b : P.completedPolynomialRing)
(f : Fin m → P.ker)
(hvanish : B.adicIdeal ≤ (Ideal.span {P.toAlgHom b}).radical)
(hjacobian :
P.toAlgHom (Matrix.det fun i j : Fin m ↦
(completedNaiveCotangentComplex B P).partialDeriv (Fin.castLE hm i)
(f j : P.completedPolynomialRing)) ∣ P.toAlgHom b)
(hrelations : ∀ x : P.completedPolynomialRing, x ∈ P.ker →
b * x ∈ Ideal.span (Set.range fun j : Fin m ↦ (f j : P.completedPolynomialRing)) +
P.ker ^ 2) :
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C),
Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)
Rig.exists_finiteType_algEquiv_adicCompletion_of_jacobianChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/JacobianCriterion.lean, line 535. The attribute's comment: “carrying, beyond the source's hypotheses: S, a family of Stacks 0GA6 DualSituations for B, one per thickness and per Ext-exponent, as the library's Stacks 0GAQ carries one per thickness; d, q₀, k, hd, hq₀, hk, the Stacks 0GA6 invariants of B, independent of thickness and exponent, with k+1 = D = max(d,1); hdual, the open duality input of Stacks 0GAC that Stacks 0GAQ carries, here for every level and exponent because n is chosen in the proof; and hconormal, that a power of I kills Ker(φ)/Ker(φ)² for every surjection φ from the completion of a finite type A-algebra onto B with both sides rig-smooth (both rig-smoothness inputs are discharged here), which is the source's last step by the Stacks 0ALM six-term sequence and the localized comparison H⁰(NL^∧_{C^∧/A}) ⊗ B[1/b] = H⁰(NL^∧_{B/A}) ⊗ B[1/b], absent from the library. Inherited, not assumed: the Stacks 0GAQ used lifts to precision I^{n-(2+D)c} under n > 2(2+D)c for the source's I^{n-(1+d)c}; and B is taken in A's own universe, the only case that Stacks 0GAQ's target admits”.
Stacks 0GAW, carrying the hypotheses that the library's Stacks 0GAQ carries.
Let
Abe a Noetherian ring,I ⊆ Aan ideal,BanI-adically completeA-algebra of finite type moduloI, presented asB = A⟨x₁, …, x_r⟩/J, and suppose givenb, an integerm ≤ randf₁, …, f_m ∈ JwithV(b) ⊆ V(IB), with the Jacobian determinantΔ = det(∂fⱼ/∂xᵢ)_{i, j ≤ m}dividing the image ofb, and withbJ ⊆ (f₁, …, f_m) + J². ThenBis theI-adic completion of a finite typeA-algebra.The route. The hypotheses make
Brig-smooth over(A, I), so a powerI^{c}annihilatesExt¹_B(NL^∧_{B/A}, N), andV(b) ⊆ V(IB)givesc₁withI^{c₁}B ⊆ bB. WritingI = (a₁, …, a_t)and approximating thefⱼby polynomialsf'ⱼto accuracyn, the algebra
C = A[z₁, …, z_t, x₁, …, x_r]/(z₁Δ' - a₁^{c₁}, …, z_tΔ' - a_t^{c₁}, f'₁, …, f'_m)of Stacks 0GAV has
I^{1 + t((t+1)c₁ - 1)}annihilatingExt¹of its completed naive cotangent complex — an exponent independent ofn, which is what letsnbe chosen in terms of it — and maps ontoB/IⁿBbyx_i ↦ x_i,z_k ↦ b_k b'. Stacks 0GAQ lifts that surjection toφ : C^∧ → B, which is surjective because it is surjective moduloI, and Stacks 0ALR algebraizesBfromφ.The carried hypotheses, one line each.
S— a family of Stacks 0GA6DualSituations forB, one for each thickness and each Ext-exponent, exactly as the library's Stacks 0GAQ carries one for each thickness.d,q₀,k,hd,hq₀,hk— the invariants of Stacks 0GA6 ofB, independent of the thickness and of the exponent, withk + 1 = D = max(d, 1).hdual— the open duality input of Stacks 0GAC, which Stacks 0GAQ carries for every levelm ≥ n, here carried for every level and every exponent sincenis chosen inside the proof.hconormal— that for every finite typeA-algebraCand every surjectionφ : C^∧ → BofA-algebras with bothBandC^∧rig-smooth over(A, I)a power ofIannihilatesKer(φ)/Ker(φ)²; this is the step the source makes with the six-term sequence of Stacks 0ALM and the comparisonH⁰(NL^∧_{C^∧/A}) ⊗ B[1/b] = H⁰(NL^∧_{B/A}) ⊗ B[1/b]of free modules of rankr - m, which the library does not have. Both rig-smoothness inputs are discharged here:B's from the Jacobian chart of the statement,C^∧'s from the smoothness ofCaway fromV(I).Two further deviations, both inherited rather than assumed: the Stacks 0GAQ used here lifts only to precision
I^{n-(2+D)c}undern > 2(2+D)c, in place of the source'sI^{n-(1+d)c}undern > 2(1+d)c; andBis taken in the universe ofA, which is the only case Stacks 0GAQ's target admits.
public theorem exists_finiteType_algEquiv_adicCompletion_of_jacobianChart
(B : AdicFiniteTypeAlgebra.{u, u} A I) (P : CompletedPolynomialPresentation I B)
(m : ℕ) (hm : m ≤ P.variableCount) (b : P.completedPolynomialRing)
(f : Fin m → P.ker)
(hvanish : B.adicIdeal ≤ (Ideal.span {P.toAlgHom b}).radical)
(hjacobian :
P.toAlgHom (Matrix.det fun i j : Fin m ↦
(completedNaiveCotangentComplex B P).partialDeriv (Fin.castLE hm i)
(f j : P.completedPolynomialRing)) ∣ P.toAlgHom b)
(hrelations : ∀ x : P.completedPolynomialRing, x ∈ P.ker →
b * x ∈ Ideal.span (Set.range fun j : Fin m ↦ (f j : P.completedPolynomialRing)) +
P.ker ^ 2)
(S : ∀ c l : ℕ, DualSituation B.carrier (I.map (algebraMap A B.carrier)) l c)
(d q₀ k : ℕ) (hd : ∀ c l, (S c l).d = d) (hq₀ : ∀ c l, (S c l).q₀ = q₀)
(hk : max d 1 = k + 1)
(hdual : ∀ (c l e : ℕ) (hel : e + 2 * c = l) (hq : (S c l).q₀ ≤ e)
(M : ANCModule (I.map (algebraMap A B.carrier)) l c)
(ϕ : resModule (I.map (algebraMap A B.carrier)) l M.1 →ₗ[B.carrier]
powQuot (I.map (algebraMap A B.carrier)) l l),
∃ s : (S c l).H M.dual 0 (e : ℤ),
(S c l).ev M e hq s =
(powQuotLe (I.map (algebraMap A B.carrier)) (Nat.le.intro hel)).comp ϕ)
(hconormal : ∀ (C : Type u) [CommRing C] [Algebra A C] [Algebra.FiniteType A C]
(ϕ : AdicCompletion (I.map (algebraMap A C)) C →ₐ[A] B.carrier),
Function.Surjective ϕ → IsRigSmooth B → IsRigSmooth (adicCompletionObj I (B := C)) →
∃ c : ℕ, I ^ c • (⊤ : Submodule A (RingHom.ker ϕ.toRingHom).Cotangent) = ⊥) :
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C),
Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)
Tag 0GAX, a remark
Tag 0GAX in the Stacks Project.
Rig.isRigSmooth_algebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/RigSmoothAlgebraizationGZ.lean, line 109.
Stacks 0GAX. Let
Ibe an ideal of a Noetherian ringAand letBbe an object of the category of Stacks 0AL4 which is rig-smooth over(A, I). ThenBis isomorphic to theI-adic completion of a finite typeA-algebra (Gabber–Zavyalov [Theorem 1.2]). This supersedes the partial results:
- if
Ais a G-ring, the result follows from Proposition 0GAT;- if
Bis rig-étale over(A, I), the result follows from Lemma 0AKA;- if
Iis principal, the result follows from Elkik [III, Theorem 7].The four conjuncts are, in order, the theorem (
Rig.exists_finiteType_algEquiv_adicCompletion_of_isRigSmooth) and the three partial results, each proved by the route the remark names: Proposition 0GAT and Lemma 0AKA throughRig.exists_finiteType_adicCompletion_algEquiv_of_isRigSmooth_of_isGRing_or_isRigEtale, and Elkik's theorem throughRig.exists_finiteType_adicCompletion_algEquiv_of_isRigSmooth_principal. In the theorem the finite type algebra lies in the universe ofA; the partial results produce it in the universemax u v, as the lemmas they follow from do.
public theorem isRigSmooth_algebraization :
(∀ {A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I), IsRigSmooth B →
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C), Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)) ∧
(∀ {A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I), IsRigSmooth B → IsGRing A →
∃ (C : Type (max u v)) (_ : CommRing C) (_ : Algebra A C), Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)) ∧
(∀ {A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I), IsRigSmooth B → IsRigEtale B →
∃ (C : Type (max u v)) (_ : CommRing C) (_ : Algebra A C), Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)) ∧
(∀ {A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I), IsRigSmooth B → I.IsPrincipal →
∃ (C : Type (max u v)) (_ : CommRing C) (_ : Algebra A C), Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C))
Sources
Section88.8 Rig-étale algebras#
Section 88.8 of the Stacks Project, Tag 0ALP. 8 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GAY, a definition
Tag 0GAY in the Stacks Project.
Rig.IsRigEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothDefs.lean, line 73.
Stacks Project, Tag 0GAY. An adically complete algebra of finite type modulo
Iis rig-étale over(A, I)if some power ofIacts by zero on its completed naive cotangent complex inD(B). The condition is imposed for each completed polynomial presentation ofB.
public abbrev IsRigEtale (B : AdicFiniteTypeAlgebra.{u, v} A I) : Prop
Tag 0AJU, a lemma
Tag 0AJU in the Stacks Project.
Rig.CompletedNaiveCotangentComplex.exists_annihilator_twoTerm_iff_forall_reducedComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/Annihilation.lean, line 399. The attribute's comment: “(3) iff (4) for the reduced complexes”.
Stacks 0AJU, the equivalence of (0AJW) and (0AJX). For a completed polynomial presentation
B = A⟨x₁, …, x_r⟩ / Jof an objectBof the category (Stacks 0AL4) over a Noetherian ringA, the following are equivalent:
- some power of
IannihilatesH^i(NL^∧_{B/A})fori = -1, 0;- some power of
IannihilatesH^i(NL_{Bₙ/Aₙ})fori = -1, 0and alln ≥ 1.Here
NL_{Bₙ/Aₙ}isRig.CompletedNaiveCotangentComplex.reducedComplex, the object the strict pro-isomorphism of Stacks 0AJS (1) produces: the quotient ofNL^∧_{B/A}by the image ofJ ∩ Iⁿ A⟨x⟩in degree-1and byIⁿB · (⨁ B dxᵢ)in degree0. The forward implication doubles the exponent and the backward one preserves it; seeannihilatesCohomology_reducedComplexandannihilatesCohomology_twoTerm. Annihilation by the idealIᶜBis the source's elementwise condition byannihilatesCohomology_adicIdeal_pow_iff, and the left-hand side is condition (3) on the nose:H⁻¹isLinearMap.ker K.differentialandH⁰is(Fin r → B) ⧸ LinearMap.range K.differential.The sublabel records that
NL_{Bₙ/Aₙ}is taken in the shape Stacks 0AJS (1) produces; see the implementation notes for the identifications that would be needed to read condition (4) throughAlgebra.naiveCotangentComplex Aₙ Bₙinstead.
public theorem exists_annihilator_twoTerm_iff_forall_reducedComplex [IsNoetherianRing A]
(K : CompletedNaiveCotangentComplex P) :
(∃ c : ℕ, NaiveCotangent.AnnihilatesCohomology (B.adicIdeal ^ c) K.twoTerm) ↔
∃ c : ℕ, ∀ n ≥ 1, NaiveCotangent.AnnihilatesCohomology (B.adicIdeal ^ c)
(K.reducedComplex n)
Rig.isCohomologyAnnihilated_iff_isReductionCohomologyAnnihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/ReductionIdentification.lean, line 418. The attribute's comment: “(3) iff (4)”.
Stacks 0AJU, the equivalence of conditions (3) and (4). For a completed polynomial presentation
B = A⟨x₁, …, x_r⟩ / Jof an objectBof the category (Stacks 0AL4) over a Noetherian ringA, the following are equivalent:
- (3) some power
I^cofIannihilatesH^{-1}andH^0ofNL^∧_{B/A}, that is, the kernel and the cokernel of the differential ofRig.completedNaiveCotangentComplex B P;- (4) some power
I^cofIannihilates, for everyn ≥ 1, the degree-1and degree-0homology ofAlgebra.naiveCotangentComplex Aₙ Bₙ, whereAₙ = A / IⁿandBₙ = B / IⁿB.Condition (4) is the source's, and is presentation-free:
NL_{Bₙ/Aₙ}is the naive cotangent complex of the tautological presentationAₙ[Bₙ] → Bₙand its cohomology is the categorical homology of aHomologicalComplex.double. Three identifications turn it into a statement about the presentationBₙ = Aₙ[x₁, …, x_r] / Jₙof Stacks 0AJS, through which the source's argument runs: the homology of adoubleis the kernel and the cokernel of its differential; those are independent of the presentation; andreducedComplex n, the quotient ofNL^∧_{B/A}by the image ofJ ∩ Iⁿ A⟨x⟩and byIⁿB · (⨁ B dxᵢ), isNL(Bₙ = Aₙ[x] / Jₙ). The transport of the annihilation statement across those is thenRig.CompletedNaiveCotangentComplex.exists_annihilator_twoTerm_iff_forall_reducedComplex, whose forward direction doubles the exponent and whose backward direction spends the shift of Stacks 0AJS (1) and preserves it.
public theorem isCohomologyAnnihilated_iff_isReductionCohomologyAnnihilated
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B) :
(∃ c : ℕ,
(I ^ c).map (algebraMap A B.carrier) ≤
Module.annihilator B.carrier
(LinearMap.ker (completedNaiveCotangentComplex B P).differential) ∧
(I ^ c).map (algebraMap A B.carrier) ≤
Module.annihilator B.carrier
((Fin P.variableCount → B.carrier) ⧸
LinearMap.range (completedNaiveCotangentComplex B P).differential)) ↔
∃ c : ℕ, ∀ n : ℕ, 1 ≤ n →
∀ a : A, a ∈ I ^ c →
((Ideal.Quotient.mk ((I ^ n).map (algebraMap A B.carrier))
(algebraMap A B.carrier a)) ∈
Module.annihilator (B.carrier ⧸ (I ^ n).map (algebraMap A B.carrier))
((Algebra.naiveCotangentComplex (A ⧸ I ^ n)
(B.carrier ⧸ (I ^ n).map (algebraMap A B.carrier))).homology 1) ∧
(Ideal.Quotient.mk ((I ^ n).map (algebraMap A B.carrier))
(algebraMap A B.carrier a)) ∈
Module.annihilator (B.carrier ⧸ (I ^ n).map (algebraMap A B.carrier))
((Algebra.naiveCotangentComplex (A ⧸ I ^ n)
(B.carrier ⧸ (I ^ n).map (algebraMap A B.carrier))).homology 0))
Rig.isRigEtale_iff_exists_annihilator_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleCriterion.lean, line 191. The attribute's comment: “(1) iff (3)”.
Stacks 0AJU, (1) ⇔ (3). For an
I-adically completeA-algebraBof finite type moduloIover a Noetherian ringA, and any completed polynomial presentationB = A⟨x₁, …, x_r⟩ / J, rig-étaleness ofBover(A, I)is equivalent to the existence of acwithIᶜBannihilating both cohomology modulesH⁻¹(NL^∧_{B/A}) = ker dandH⁰(NL^∧_{B/A}) = coker d.Condition (1) is annihilation of the complex in the derived category and condition (3) is annihilation of its cohomology, which is weaker for a general complex; the two agree here because
NL^∧_{B/A}has two terms and its degree-0term is free, so the annihilating scalar is realised by an honest two-sided splitting of the differential. Passing from (3) to (1) costs a squaring of the ideal and passing back costs nothing, which is why the statement is an equivalence of the existence of an exponent rather than of a fixed one.
public theorem isRigEtale_iff_exists_annihilator_cohomology
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B) :
IsRigEtale B ↔
∃ c : ℕ,
(I ^ c).map (algebraMap A B.carrier) ≤
Module.annihilator B.carrier
(LinearMap.ker (completedNaiveCotangentComplex B P).differential) ∧
(I ^ c).map (algebraMap A B.carrier) ≤
Module.annihilator B.carrier
((Fin P.variableCount → B.carrier) ⧸
LinearMap.range (completedNaiveCotangentComplex B P).differential)
Rig.isArtinJacobian_of_isRigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleLifting.lean, line 309. The attribute's comment: “(1) implies (6)”.
Stacks 0AJU, (1) implies (6). A rig-étale adic algebra satisfies the elementwise Jacobian criterion: for every
a ∈ Ithere are an exponentcand elementsf₁, …, f_rof the kernelJof a completed polynomial presentation such that the Jacobian determinantdet(∂fⱼ/∂xᵢ)dividesa ^ cinBanda ^ c · J ⊆ (f₁, …, f_r) + J².The proof is the one in the source. Rig-étaleness gives an exponent
c₀witha ^ c₀ · 𝟙 NL^∧_{B/A} = 0inD(B), hence by Stacks 0ALN(1) a two-sided retractionH : ⨁ i, B dxᵢ → J / J²of the differential up toa ^ c₀(Rig.exists_linearMap_twoSided_of_smul_id_eq_zero). Takingfᵢ ∈ JrepresentingH(dxᵢ), the identityd ∘ H = a ^ c₀says that the Jacobian matrix(∂fⱼ/∂xᵢ)is exactlya ^ c₀times the identity, so its determinant isa ^ (c₀ r); andH ∘ d = a ^ c₀is the conormal Cramer relation. The exponent is taken to bec₀ (r + 1), which dominates bothc₀ randc₀, the latter being needed whenr = 0.
public theorem isArtinJacobian_of_isRigEtale (B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) (hB : IsRigEtale B) :
∀ a : A, a ∈ I →
∃ (c : ℕ) (f : Fin P.variableCount → P.ker),
Matrix.det (fun i j : Fin P.variableCount =>
P.toAlgHom ((completedNaiveCotangentComplex B P).partialDeriv i
(f j : P.completedPolynomialRing))) ∣ (algebraMap A B.carrier a) ^ c ∧
∀ g : P.ker,
algebraMap A P.completedPolynomialRing (a ^ c) * (g : P.completedPolynomialRing) ∈
Ideal.span (Set.range fun i => (f i : P.completedPolynomialRing)) + P.ker ^ 2
Rig.isArtinPreliminary_of_isArtinJacobian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleTFAE.lean, line 244. The attribute's comment: “(6) implies (5)”.
Stacks 0AJU, (6) ⇒ (5). If the Jacobian determinant of
f₁, …, f_r ∈ Jdividesa ^ c, thena ^ cannihilatesH⁰(NL^∧_{B/A}).Cramer's rule
M · adj(M) = det(M) · 1putsdet(M) · eᵢin the image of the Jacobian matrix, whose columns are images of the differential; sodet(M), and with it every multiple of it, carries⨁ i, B dxᵢinto the image of the differential. The second half of the two conditions is literally the same sentence, so the exponent and the family carry over.
public theorem isArtinPreliminary_of_isArtinJacobian (B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) (h : IsArtinJacobian B P) :
IsArtinPreliminary B P
Rig.isCohomologyAnnihilated_of_isArtinPreliminary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleTFAE.lean, line 374. The attribute's comment: “(5) implies (3)”.
Stacks 0AJU, (5) ⇒ (3). Condition (5) gives, for each
a ∈ I, a power ofaannihilating both cohomology modules ofNL^∧_{B/A}: forH⁰this is its first half and forH⁻¹it isRig.pow_mem_annihilator_ker_differential_of_artinPreliminary. The scalars annihilating both form an ideal of the Noetherian ringB, and every element ofIBhas a power in it, so a single power ofIBlies in it.
public theorem isCohomologyAnnihilated_of_isArtinPreliminary
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B)
(h : IsArtinPreliminary B P) : IsCohomologyAnnihilated B P
Rig.isRigEtale_iff_isJacobianCramerBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleTFAE.lean, line 410. The attribute's comment: “(1) iff (7)”.
Stacks 0AJU, (1) ⇔ (7). Rig-étaleness of
Bover(A, I)is equivalent to the Jacobian ideal and the Cramer ideal of every finite generating family ofJeach containing a power ofIB.For a single family this is Stacks 0AJY,
Rig.isRigEtale_iff_exists_pow_le_completedJacobianIdeal_and_completedCramerIdeal; the quantified form follows becauseJis a finitely generated ideal of the Noetherian ringA⟨x₁, …, x_r⟩, so at least one such family exists.
public theorem isRigEtale_iff_isJacobianCramerBounded (B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) :
IsRigEtale B ↔ IsJacobianCramerBounded B P
Rig.tfae_isRigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleTFAE.lean, line 443.
Stacks 0AJU. Let
Abe a Noetherian ring,I ⊆ Aan ideal,BanI-adically completeA-algebra of finite type moduloIandB = A⟨x₁, …, x_r⟩ / Ja completed polynomial presentation. The seven Artin criteria are equivalent:
Bis rig-étale over(A, I);- some power of
Iannihilates the identity ofNL^∧_{B/A}inD(B);- some power of
IBannihilatesH⁻¹(NL^∧_{B/A})andH⁰(NL^∧_{B/A});- some power of
IannihilatesH^i(NL_{Bₙ/Aₙ})fori = -1, 0and everyn ≥ 1;- for every
a ∈ Isomea ^ cannihilatesH⁰(NL^∧_{B/A})and there aref₁, …, f_r ∈ Jwitha ^ c · J ⊆ (f₁, …, f_r) + J²;- for every
a ∈ Ithere aref₁, …, f_r ∈ Jwhose Jacobian determinant dividesa ^ cand witha ^ c · J ⊆ (f₁, …, f_r) + J²;- the Jacobian ideal and the Cramer ideal of every finite generating family of
Jeach contain a power ofIB.The cycle is closed as
(1) ⇒ (6) ⇒ (5) ⇒ (3) ⇒ (1), with(1) ⇔ (2),(3) ⇔ (4)and(1) ⇔ (7)hung off it.
public theorem tfae_isRigEtale (B : AdicFiniteTypeAlgebra.{u, v} A I)
(P : CompletedPolynomialPresentation I B) :
List.TFAE [IsRigEtale B, IsDerivedAnnihilated B P, IsCohomologyAnnihilated B P,
IsReductionCohomologyAnnihilated B, IsArtinPreliminary B P, IsArtinJacobian B P,
IsJacobianCramerBounded B P]
Tag 0AJY, an item
Tag 0AJY in the Stacks Project.
Rig.isRigEtale_iff_exists_pow_le_completedJacobianIdeal_and_completedCramerIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/JacobianCramerCriterion.lean, line 180. The attribute's comment: “(7) of 0AJU, as an equivalence with rig-étaleness”.
Stacks 0AJY, part (7) of Stacks 0AJU. For an
I-adically completeA-algebraBof finite type moduloIover a Noetherian ringA, a completed polynomial presentationB = A⟨x₁, …, x_r⟩ / Jand generatorsf₁, …, f_tofJ, rig-étaleness ofBover(A, I)is equivalent to the Jacobian ideal and the Cramer ideal ofBoverAeach containing a power ofIB.
public theorem isRigEtale_iff_exists_pow_le_completedJacobianIdeal_and_completedCramerIdeal
(B : AdicFiniteTypeAlgebra.{u, v} A I) (P : CompletedPolynomialPresentation I B) {t : ℕ}
(f : Fin t → P.completedPolynomialRing) (hf : P.ker = Ideal.span (Set.range f)) :
IsRigEtale B ↔
((∃ c : ℕ, (I ^ c).map (algebraMap A B.carrier) ≤ completedJacobianIdeal B P f) ∧
∃ c : ℕ, (I ^ c).map (algebraMap A B.carrier) ≤ completedCramerIdeal B P)
Tag 0GB1, a lemma
Tag 0GB1 in the Stacks Project.
Rig.isRigSmooth_of_isRigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Restricted/RigEtale.lean, line 95.
Stacks 0GB1. A rig-étale adically finite type algebra over
(A, I)is rig-smooth.
theorem isRigSmooth_of_isRigEtale {A : Type u} [CommRing A] [IsNoetherianRing A]
{I : Ideal A} (B : AdicFiniteTypeAlgebra.{u, v} A I)
(hB : IsRigEtale B) : IsRigSmooth B
Tag 0ALQ, a lemma
Tag 0ALQ in the Stacks Project.
Rig.isRigEtale_adicCompletionObj_of_isEtaleOutside, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleLocus.lean, line 434. The attribute's comment: “part (1)”.
Stacks 0ALQ, part (1). Let
Abe a Noetherian ring,I ⊆ Aan ideal andBa finite typeA-algebra. IfSpec(B) → Spec(A)is étale overSpec(A) ∖ V(I), then theI-adic completionB^satisfies the equivalent conditions of Stacks 0AJU, that is,B^is rig-étale over(A, I).Étaleness off
V(I)says thatH¹(L_{B/A})andΩ_{B/A}are supported inV(IB), so — both being finite modules over the Noetherian ringB— a power ofIBannihilates them, hence also their base changes toB^. The pivotRig.isRigEtale_adicCompletionObj_iffturns that into rig-étaleness.
public theorem isRigEtale_adicCompletionObj_of_isEtaleOutside (h : IsEtaleOutside I B) :
IsRigEtale (adicCompletionObj I (B := B))
Rig.exists_isEtaleOutside_localization_of_isRigEtale_adicCompletionObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleLocus.lean, line 471. The attribute's comment: “part (2)”.
Stacks 0ALQ, part (2). Let
Abe a Noetherian ring,I ⊆ Aan ideal andBa finite typeA-algebra. If theI-adic completionB^satisfies the equivalent conditions of Stacks 0AJU — that is, ifB^is rig-étale over(A, I)— then there isg ∈ 1 + IBsuch thatSpec(B_g) → Spec(A)is étale overSpec(A) ∖ V(I).The element
gis produced by Nakayama's lemma: rig-étaleness gives acwithIᶜ B^annihilatingB^ ⊗_B H¹(L_{B/A})andB^ ⊗_B Ω_{B/A}, soIᶜ Bannihilates both finiteB-modules only modulo⋂ₙ (IB)ⁿ, and one element of1 + IBkills that intersection. After inverting it, every prime ofBoffV(IB)contains no element ofIᶜ Band so lies outside the supports of the two modules, which is étaleness there.
public theorem exists_isEtaleOutside_localization_of_isRigEtale_adicCompletionObj
(h : IsRigEtale (adicCompletionObj I (B := B))) :
∃ g : B, g - 1 ∈ I.map (algebraMap A B) ∧ IsEtaleOutside I (Localization.Away g)
Rig.isEtaleOutside_and_isRigEtale_adicCompletionObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleLocus.lean, line 529.
Stacks 0ALQ. Let
Abe a Noetherian ring,I ⊆ Aan ideal andBa finite typeA-algebra, and writeB^for theI-adic completion ofB.
- If
Spec(B) → Spec(A)is étale overSpec(A) ∖ V(I), thenB^satisfies the equivalent conditions of Stacks 0AJU, in the form of their first conditionRig.IsRigEtale.- If
B^satisfies those conditions, then there existsg ∈ 1 + IBsuch thatSpec(B_g) → Spec(A)is étale overSpec(A) ∖ V(I).The two implications are
Rig.isRigEtale_adicCompletionObj_of_isEtaleOutsideandRig.exists_isEtaleOutside_localization_of_isRigEtale_adicCompletionObj.
public theorem isEtaleOutside_and_isRigEtale_adicCompletionObj :
(IsEtaleOutside I B → IsRigEtale (adicCompletionObj I (B := B))) ∧
(IsRigEtale (adicCompletionObj I (B := B)) →
∃ g : B, g - 1 ∈ I.map (algebraMap A B) ∧ IsEtaleOutside I (Localization.Away g))
Tag 0AK2, a lemma
Tag 0AK2 in the Stacks Project.
Rig.smul_id_of_completedBaseChangeFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/BaseChangeSmulId.lean, line 102.
With
(A₁, I₁) → (A₂, I₂)as in Stacks Remark 0AL5, witnessed byhcandhmap, a scalarf₁ ∈ B₁acting by zero onNL^∧_{B₁/A₁}inD(B₁)has its imageRig.CompletedBaseChange.scalarin the base changeB₂ = C.functor.obj B₁acting by zero onNL^∧_{B₂/A₂}inD(B₂), for any completed polynomial presentations of the two algebras.
public theorem smul_id_of_completedBaseChangeFunctor
(C : CompletedBaseChange (A₁ := A₁) (A₂ := A₂) (I₁ := I₁) (I₂ := I₂))
(hc : 0 < c) (hmap : (I₁ ^ c).map (algebraMap A₁ A₂) ≤ I₂)
(B₁ : AdicFiniteTypeAlgebra.{u₁, v} A₁ I₁)
(P₁ : CompletedPolynomialPresentation I₁ B₁)
(P₂ : CompletedPolynomialPresentation I₂ (C.functor.obj B₁)) (f₁ : B₁.carrier)
(h : f₁ • 𝟙 (derivedCompletedNaiveCotangentComplex B₁ P₁) = 0) :
C.scalar B₁ f₁ •
𝟙 (derivedCompletedNaiveCotangentComplex (C.functor.obj B₁) P₂) = 0
Tag 0GB2, a lemma
Tag 0GB2 in the Stacks Project.
Rig.isRigEtale_completedBaseChangeOfIsNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleBaseChange.lean, line 227. The attribute's comment: “preservation of rig-étaleness”.
Let
A₁ → A₂be a map of Noetherian rings and letIᵢ ⊆ Aᵢbe ideals withV(I₁ A₂) = V(I₂). LetB₁be adically of finite type over(A₁, I₁)and letB₂ = (B₁ ⊗_{A₁} A₂)^∧_{I₂}be its base change as in Stacks Remark 0AL5, the functorRig.completedBaseChangeOfIsNoetherianRing. IfB₁is rig-étale over(A₁, I₁), thenB₂is rig-étale over(A₂, I₂).
public theorem isRigEtale_completedBaseChangeOfIsNoetherianRing
(hV : PrimeSpectrum.zeroLocus ((I₁.map (algebraMap A₁ A₂) : Ideal A₂) : Set A₂) =
PrimeSpectrum.zeroLocus (I₂ : Set A₂))
(B₁ : AdicFiniteTypeAlgebra.{u₁, v} A₁ I₁) (hB₁ : IsRigEtale B₁) :
IsRigEtale ((completedBaseChangeOfIsNoetherianRing
(exists_pos_pow_map_le_of_zeroLocus_eq hV)).functor.obj B₁)
Tag 0AKJ, a lemma
Tag 0AKJ in the Stacks Project.
Rig.exists_etale_factorization_algHom_henselization, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Henselization.lean, line 322. The attribute's comment: “étale factorization”.
Stacks Project, Tag 0AKJ (étale factorization). Every map from a finite type algebra to the henselization of
(C, IC)factors through an étaleC-algebra whose closed fibre is canonically isomorphic to that ofC.
public lemma exists_etale_factorization_algHom_henselization
(A : Type u) (B : Type v) (C : Type w)
[CommRing A] [IsNoetherianRing A]
[CommRing B] [Algebra A B] [Algebra.FiniteType A B]
(I : Ideal A)
[CommRing C] [Algebra A C] :
let H := (henselization C (I.map (algebraMap A C)) : Type w)
letI : Algebra A H :=
((algebraMap C H).comp (algebraMap A C)).toAlgebra
letI : IsScalarTower A C H :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
∀ f : B →ₐ[A] H,
∃ (Cp : Type (max u v w)) (_ : CommRing Cp) (_ : Algebra C Cp)
(_ : Algebra A Cp) (_ : IsScalarTower A C Cp) (_ : Algebra.Etale C Cp)
(g : B →ₐ[A] Cp)
(k : Cp →ₐ[C] H),
Function.Bijective
(Ideal.quotientMap ((I.map (algebraMap A C)).map (algebraMap C Cp))
(algebraMap C Cp) Ideal.le_comap_map) ∧
(k.restrictScalars A).comp g = f
Rig.exists_unique_algHom_henselization_of_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/HenselizationDescent.lean, line 963. The attribute's comment: “descent and uniqueness”.
Stacks Project, Tag 0AKJ (descent and uniqueness). Let
Abe a Noetherian ring,I ⊆ Aan ideal andBa finite typeA-algebra such thatSpec(B) → Spec(A)is étale overSpec(A) ∖ V(I), and letCbe a NoetherianA-algebra. Then everyA-algebra mapB^∧ → C^∧ofI-adic completions comes from a uniqueA-algebra mapB → Cʰinto the henselization of the pair(C, IC).Uniqueness is
Rig.eq_of_henselizationToAdicCompletion_comp_eq, which rests on the fact thatCʰis a subring ofC^∧. For existence, follow the source and replace(A, I, B, C)by(C, IC, C ⊗_A B, C): the given map makesD = C ⊗_A BaC-algebra overC^∧, and the étaleness hypothesis, which annihilatesΩ_{B/A}by a power ofI, annihilatesΩ_{D/C}by the same power after base change.exists_algHom_henselization_of_annihilator_kaehlerDifferentialthen liftsD → C^∧toD → Cʰ, and restricting alongB → Dgives the map sought.
public theorem exists_unique_algHom_henselization_of_adicCompletion
(A : Type u) (B : Type v) (C : Type w)
[CommRing A] [IsNoetherianRing A]
[CommRing B] [Algebra A B] [Algebra.FiniteType A B]
(I : Ideal A) (hEtale : IsEtaleOutside I B)
[CommRing C] [Algebra A C] [IsNoetherianRing C] :
let H := (henselization C (I.map (algebraMap A C)) : Type w)
letI : Algebra A H :=
((algebraMap C H).comp (algebraMap A C)).toAlgebra
letI : IsScalarTower A C H :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
∀ φ : AdicCompletion (I.map (algebraMap A B)) B →ₐ[A]
AdicCompletion (I.map (algebraMap A C)) C,
∃! ψ : B →ₐ[A] H,
((henselizationToAdicCompletion C
(I.map (algebraMap A C))).val.restrictScalars A).comp ψ =
φ.comp (IsScalarTower.toAlgHom A B
(AdicCompletion (I.map (algebraMap A B)) B))
Sources
Section88.9 A pushout argument#
Section 88.9 of the Stacks Project, Tag 0AK8. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0ALT, a lemma
Tag 0ALT in the Stacks Project.
Stacks.Etale.exists_finiteType_etale_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PushoutLift/Main.lean, line 381.
Stacks 0ALT. Let
Abe a Noetherian ring,I ⊆ Aan ideal andJ ⊆ Aa nilpotent ideal, and consider a commutative diagram of finite type ring mapsC ---> C ⧸ JC ^ B₀ ^ A ---> A ⧸ Jsuch that
Spec C → Spec Ais étale overSpec A \ V(I), such thatSpec B₀ → Spec (A ⧸ J)is étale overSpec (A ⧸ J) \ V(I (A ⧸ J)), and such thatB₀ → C ⧸ JCis étale and induces an isomorphismB₀ ⧸ I B₀ = (C ⧸ JC) ⧸ I (C ⧸ JC). Then the diagram can be filled in: there are a finite typeA-algebraB, anA-algebra mapB → Cwhich is étale, and an isomorphismB ⧸ JB ≅ B₀compatible with the maps toC ⧸ JC, such thatSpec B → Spec Ais étale overSpec A \ V(I).
theorem exists_finiteType_etale_lift
(A C B₀ : Type u) [CommRing A] [CommRing C] [CommRing B₀]
[IsNoetherianRing A] [Algebra A C] [Algebra.FiniteType A C]
(I J : Ideal A) (hJ : IsNilpotent J)
[Algebra A B₀] [Algebra (A ⧸ J) B₀] [IsScalarTower A (A ⧸ J) B₀]
[Algebra.FiniteType (A ⧸ J) B₀]
[Algebra (A ⧸ J) (C ⧸ J.map (algebraMap A C))]
[IsScalarTower A (A ⧸ J) (C ⧸ J.map (algebraMap A C))]
[Algebra B₀ (C ⧸ J.map (algebraMap A C))]
[IsScalarTower (A ⧸ J) B₀ (C ⧸ J.map (algebraMap A C))]
[Algebra.Etale B₀ (C ⧸ J.map (algebraMap A C))]
(hC : ∀ q : Ideal C, ∀ _ : q.IsPrime, ¬ I ≤ q.comap (algebraMap A C) →
Algebra.IsEtaleAt A q)
(hB₀ : ∀ q : Ideal B₀, ∀ _ : q.IsPrime,
¬ I.map (Ideal.Quotient.mk J) ≤ q.comap (algebraMap (A ⧸ J) B₀) →
Algebra.IsEtaleAt (A ⧸ J) q)
(hmod : Function.Bijective (Ideal.quotientMap
(((I.map (Ideal.Quotient.mk J)).map (algebraMap (A ⧸ J) B₀)).map
(algebraMap B₀ (C ⧸ J.map (algebraMap A C))))
(algebraMap B₀ (C ⧸ J.map (algebraMap A C))) Ideal.le_comap_map)) :
∃ (B : Type u) (_ : CommRing B) (_ : Algebra A B) (_ : Algebra.FiniteType A B)
(_ : Algebra B C) (_ : IsScalarTower A B C) (_ : Algebra.Etale B C)
(e : (B ⧸ J.map (algebraMap A B)) ≃ₐ[A] B₀),
(∀ q : Ideal B, ∀ _ : q.IsPrime, ¬ I ≤ q.comap (algebraMap A B) →
Algebra.IsEtaleAt A q) ∧
∀ b : B, algebraMap B₀ (C ⧸ J.map (algebraMap A C))
(e (Ideal.Quotient.mk (J.map (algebraMap A B)) b)) =
Ideal.Quotient.mk (J.map (algebraMap A C)) (algebraMap B C b)
Stacks.Etale.exists_finiteType_etale_lift_of_isNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PushoutLiftAcrossNilpotent.lean, line 182. The attribute's comment: “extra hypothesis: the ideal I·B₀ is nilpotent, equivalently the open set Spec(B₀) minus V(I·B₀) along which the source glues is empty; the conclusion is delivered in full”.
Let
Abe a Noetherian ring,I ⊆ Aan ideal andJ ⊆ Aa nilpotent ideal, and consider a commutative diagram of finite type ring mapsC ---> C ⧸ JC ^ B₀ ^ A ---> A ⧸ Jsuch that
Spec C → Spec Ais étale overSpec A \ V(I), such thatSpec B₀ → Spec (A ⧸ J)is étale overSpec (A ⧸ J) \ V(I (A ⧸ J)), and such thatB₀ → C ⧸ JCis étale and induces an isomorphismB₀ ⧸ I B₀ = (C ⧸ JC) ⧸ I (C ⧸ JC). Then the diagram can be filled in: there are a finite typeA-algebraB, anA-algebra mapB → Cwhich is étale, and an isomorphismB ⧸ JB ≅ B₀compatible with the maps toC ⧸ JC, such thatSpec B → Spec Ais étale overSpec A \ V(I).This takes the extra hypothesis
hnilthatI B₀is nilpotent, equivalently that the open setSpec B₀ \ V(I B₀)is empty.
theorem exists_finiteType_etale_lift_of_isNilpotent
(A C B₀ : Type u) [CommRing A] [CommRing C] [CommRing B₀]
[IsNoetherianRing A] [Algebra A C] [Algebra.FiniteType A C]
(I J : Ideal A) (_hJ : IsNilpotent J)
[Algebra A B₀] [Algebra (A ⧸ J) B₀] [IsScalarTower A (A ⧸ J) B₀]
[Algebra.FiniteType (A ⧸ J) B₀]
[Algebra (A ⧸ J) (C ⧸ J.map (algebraMap A C))]
[IsScalarTower A (A ⧸ J) (C ⧸ J.map (algebraMap A C))]
[Algebra B₀ (C ⧸ J.map (algebraMap A C))]
[IsScalarTower (A ⧸ J) B₀ (C ⧸ J.map (algebraMap A C))]
[Algebra.Etale B₀ (C ⧸ J.map (algebraMap A C))]
(hC : ∀ q : Ideal C, ∀ _ : q.IsPrime, ¬ I ≤ q.comap (algebraMap A C) →
Algebra.IsEtaleAt A q)
(_hB₀ : ∀ q : Ideal B₀, ∀ _ : q.IsPrime,
¬ I.map (Ideal.Quotient.mk J) ≤ q.comap (algebraMap (A ⧸ J) B₀) →
Algebra.IsEtaleAt (A ⧸ J) q)
(hmod : Function.Bijective (Ideal.quotientMap
(((I.map (Ideal.Quotient.mk J)).map (algebraMap (A ⧸ J) B₀)).map
(algebraMap B₀ (C ⧸ J.map (algebraMap A C))))
(algebraMap B₀ (C ⧸ J.map (algebraMap A C))) Ideal.le_comap_map))
(hnil : IsNilpotent ((I.map (Ideal.Quotient.mk J)).map (algebraMap (A ⧸ J) B₀))) :
∃ (B : Type u) (_ : CommRing B) (_ : Algebra A B) (_ : Algebra.FiniteType A B)
(_ : Algebra B C) (_ : IsScalarTower A B C) (_ : Algebra.Etale B C)
(e : (B ⧸ J.map (algebraMap A B)) ≃ₐ[A] B₀),
(∀ q : Ideal B, ∀ _ : q.IsPrime, ¬ I ≤ q.comap (algebraMap A B) →
Algebra.IsEtaleAt A q) ∧
∀ b : B, algebraMap B₀ (C ⧸ J.map (algebraMap A C))
(e (Ideal.Quotient.mk (J.map (algebraMap A B)) b)) =
Ideal.Quotient.mk (J.map (algebraMap A C)) (algebraMap B C b)
Stacks.Etale.exists_finiteType_etale_lift_of_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/PushoutLiftAcrossNilpotent.lean, line 233. The attribute's comment: “extra hypothesis: I·B₀ is the unit ideal of B₀, equivalently the closed set V(I·B₀) in Spec(B₀) along which the source glues is empty; the conclusion is delivered in full”.
The data and the conclusion are those of
exists_finiteType_etale_lift_of_isNilpotent, with the extra hypothesishtopthatI B₀is the unit ideal, equivalently that the closed setV(I B₀) ⊆ Spec B₀is empty, in place ofhnil.
theorem exists_finiteType_etale_lift_of_eq_top
(A C B₀ : Type u) [CommRing A] [CommRing C] [CommRing B₀]
[IsNoetherianRing A] [Algebra A C] [Algebra.FiniteType A C]
(I J : Ideal A) (hJ : IsNilpotent J)
[Algebra A B₀] [Algebra (A ⧸ J) B₀] [IsScalarTower A (A ⧸ J) B₀]
[Algebra.FiniteType (A ⧸ J) B₀]
[Algebra (A ⧸ J) (C ⧸ J.map (algebraMap A C))]
[IsScalarTower A (A ⧸ J) (C ⧸ J.map (algebraMap A C))]
[Algebra B₀ (C ⧸ J.map (algebraMap A C))]
[IsScalarTower (A ⧸ J) B₀ (C ⧸ J.map (algebraMap A C))]
[Algebra.Etale B₀ (C ⧸ J.map (algebraMap A C))]
(hC : ∀ q : Ideal C, ∀ _ : q.IsPrime, ¬ I ≤ q.comap (algebraMap A C) →
Algebra.IsEtaleAt A q)
(hB₀ : ∀ q : Ideal B₀, ∀ _ : q.IsPrime,
¬ I.map (Ideal.Quotient.mk J) ≤ q.comap (algebraMap (A ⧸ J) B₀) →
Algebra.IsEtaleAt (A ⧸ J) q)
(_hmod : Function.Bijective (Ideal.quotientMap
(((I.map (Ideal.Quotient.mk J)).map (algebraMap (A ⧸ J) B₀)).map
(algebraMap B₀ (C ⧸ J.map (algebraMap A C))))
(algebraMap B₀ (C ⧸ J.map (algebraMap A C))) Ideal.le_comap_map))
(htop : (I.map (Ideal.Quotient.mk J)).map (algebraMap (A ⧸ J) B₀) = ⊤) :
∃ (B : Type u) (_ : CommRing B) (_ : Algebra A B) (_ : Algebra.FiniteType A B)
(_ : Algebra B C) (_ : IsScalarTower A B C) (_ : Algebra.Etale B C)
(e : (B ⧸ J.map (algebraMap A B)) ≃ₐ[A] B₀),
(∀ q : Ideal B, ∀ _ : q.IsPrime, ¬ I ≤ q.comap (algebraMap A B) →
Algebra.IsEtaleAt A q) ∧
∀ b : B, algebraMap B₀ (C ⧸ J.map (algebraMap A C))
(e (Ideal.Quotient.mk (J.map (algebraMap A B)) b)) =
Ideal.Quotient.mk (J.map (algebraMap A C)) (algebraMap B C b)
Sources
Section88.10 Algebraization of rig-étale algebras#
Section 88.10 of the Stacks Project, Tag 0AK5. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0ALS, a lemma
Tag 0ALS in the Stacks Project.
Rig.exists_finiteType_algEquiv_of_isRigEtale_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/PrincipalIsomorphism.lean, line 221. The attribute's comment: “the rig-étale case of Elkik III Theorem 7, over a principal ideal”.
Stacks 0ALS, the rig-étale case of [Elkik, III Theorem 7], with no restriction on the universe of
B. LetAbe a Noetherian ring andI = (a)a principal ideal. LetBbe an object of the category ofI-adically completeA-algebras of finite type moduloI(Stacks 0AL4) which is rig-étale over(A, I). Then there is a finite typeA-algebraCand an isomorphismB ≅ C^∧.The carrier of
Bis replaced by the quotientA⟨x₁, …, x_r⟩/Jof a presentation ofB(Rig.quotientObj), which lives in the universe ofAand isA-algebra isomorphic toB.carrierbyRig.CompletedPolynomialPresentation.quotientEquiv; rig-étaleness transports across that isomorphism byRig.isRigEtale_of_algEquiv(Stacks 0GB2), andRig.exists_finiteType_algEquiv_of_isRigEtale_principal_sameUniverseapplies to it.
public theorem exists_finiteType_algEquiv_of_isRigEtale_principal
(hI : I.IsPrincipal) (B : AdicFiniteTypeAlgebra.{u, v} A I) (hB : IsRigEtale B) :
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C),
Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)
Tag 0AKA, a lemma
Tag 0AKA in the Stacks Project.
Rig.exists_finiteType_algEquiv_adicCompletion_of_isRigEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/RigEtaleAlgebraization.lean, line 82.
Let
Abe a Noetherian ring andI ⊆ Aan ideal. IfBis an object ofRig.AdicFiniteTypeAlgebra A Iwhich is rig-étale over(A, I), then there is a finite typeA-algebraCand an isomorphismB ≅ C^∧with itsI-adic completion.
public theorem exists_finiteType_algEquiv_adicCompletion_of_isRigEtale
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I) (hB : IsRigEtale B) :
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C),
Algebra.FiniteType A C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)
Tag 0AKG, a lemma
Tag 0AKG in the Stacks Project.
Rig.exists_isEtaleOutside_finiteType_algEquiv_of_isRigEtale_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/EtaleOutside.lean, line 270. The attribute's comment: “the converse implication, over a PRINCIPAL ideal: the equivalent conditions of Stacks 0AJU imply condition (8). Stacks 0ALS algebraizes a rig-étale object over a principal ideal and the improvement step above makes the algebraization étale over the complement of V(I); that improvement step, Rig.exists_isEtaleOutside_finiteType_algEquiv_of_algEquiv_adicCompletion, is proved for an arbitrary ideal”.
Stacks 0AKG, the equivalent conditions of Stacks 0AJU imply condition (8), over a principal ideal. Let
Abe a Noetherian ring andI = (a)a principal ideal. LetBbe an object of the category ofI-adically completeA-algebras of finite type moduloI(Stacks 0AL4) which is rig-étale over(A, I). Then there is a finite typeA-algebraCwithSpec(C) → Spec(A)étale overSpec(A) ∖ V(I)and an isomorphismB ≅ C^∧.Stacks 0ALS (
Rig.exists_finiteType_algEquiv_of_isRigEtale_principal) algebraizesBover a principal ideal, andRig.exists_isEtaleOutside_finiteType_algEquiv_of_algEquiv_adicCompletionimproves the algebraization to one étale offV(I).
public theorem exists_isEtaleOutside_finiteType_algEquiv_of_isRigEtale_principal
(hI : I.IsPrincipal) (B : AdicFiniteTypeAlgebra.{u, v} A I) (hB : IsRigEtale B) :
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C),
Algebra.FiniteType A C ∧ IsEtaleOutside I C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)
Rig.isRigEtale_iff_exists_isEtaleOutside_algEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Algebraization/RigEtaleAlgebraization.lean, line 102.
Let
Abe a Noetherian ring,I ⊆ Aan ideal andBanI-adically completeA-algebra withA ⧸ I → B ⧸ IBof finite type. ThenBis rig-étale if and only if there is a finite typeA-algebraCwithSpec(C) → Spec(A)étale overSpec(A) ∖ V(I)and an isomorphismB ≅ C^∧ofA-algebras.
public theorem isRigEtale_iff_exists_isEtaleOutside_algEquiv
{A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A}
(B : AdicFiniteTypeAlgebra.{u, v} A I) :
IsRigEtale B ↔
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C),
Algebra.FiniteType A C ∧ IsEtaleOutside I C ∧
Nonempty (B.carrier ≃ₐ[A] AdicCompletion (I.map (algebraMap A C)) C)
Rig.isRigEtale_of_isEtaleOutside_of_algEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigEtaleLocus.lean, line 590. The attribute's comment: “condition (8) implies the equivalent conditions of Stacks 0AJU; the converse implication is not covered, since it rests on the algebraization lemma — that a rig-étale object of this category is the completion of a finite type algebra — which this library does not carry”.
Stacks 0AKG, condition (8) implies the equivalent conditions of Stacks 0AJU. Let
Abe a Noetherian ring,I ⊆ Aan ideal andBanI-adically completeA-algebra of finite type moduloI. IfBis isomorphic as anA-algebra to theI-adic completionC^∧of a finite typeA-algebraCwithSpec(C) → Spec(A)étale overSpec(A) ∖ V(I), thenBis rig-étale over(A, I).This is Stacks 0ALQ, part (1) applied to
C, followed by the invariance of rig-étaleness under isomorphism.
public theorem isRigEtale_of_isEtaleOutside_of_algEquiv
{B : AdicFiniteTypeAlgebra.{u, w} A I} {C : Type v} [CommRing C] [Algebra A C]
[Algebra.FiniteType A C] (hC : IsEtaleOutside I C)
(e : B.carrier ≃ₐ[A] (adicCompletionObj I (B := C)).carrier) :
IsRigEtale B
Sources
Section88.11 Finite type morphisms#
Section 88.11 of the Stacks Project, Tag 0GBV. 5 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GBW, a lemma
Tag 0GBW in the Stacks Project.
AlgebraicGeometry.FormalSpace.hasPropertyOnAffineChartMap_adicStar_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicFiniteTypeCharacterization.lean, line 223. The attribute's comment: “the equivalence of conditions (1) and (2), read on a map of affine formal algebraic spaces whose presenting rings are all adic*”.
The equivalence of conditions (1) and (2) of Stacks 0GBW, read on charts. Let
t : U ⟶ Vbe a map of affine formal algebraic spaces overSall of whose presenting topological rings are adic*. Thentcorresponds to an adic, topologically of finite type arrow ofWAdm^{adic*}exactly when it corresponds to a taut, topologically of finite type arrow ofWAdm^{count}.The two conditions quantify over different classes of presentations, so neither inclusion is formal: the condition for countably indexed weakly admissible rings quantifies over strictly more presentations, since an adic* ring is countably indexed weakly admissible, and the hypotheses
hUandhVare what make the two ranges of quantification agree. On a single presentation the two properties of the arrow are identified by Stacks 0GBW.
theorem hasPropertyOnAffineChartMap_adicStar_iff {U V : FppfSheaf B S hS} (t : U ⟶ V)
(hU : ∀ (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[IsLinearTopology R R] (E : QuotientSystem B S hS R), (U ≅ formalSpectrum E) →
TopologicalRing.IsAdicStar R)
(hV : ∀ (A : Type u) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsLinearTopology A A] (D : QuotientSystem B S hS A), (V ≅ formalSpectrum D) →
TopologicalRing.IsAdicStar A) :
HasPropertyOnAffineChartMap B S hS TopologicalRing.IsAdicStar
TopologicalRing.IsAdicTopologicallyOfFiniteTypeHom t ↔
HasPropertyOnAffineChartMap B S hS TopologicalRing.IsCountablyWeaklyAdmissible
TopologicalRing.IsTautTopologicallyOfFiniteTypeHom t
Rig.adicFiniteType_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FiniteType.lean, line 719. The attribute's comment: “equivalent_conditions”. References: EGA I (10.13.4); EGA I (10.13.1), “affine case”; EGA 0 (7.5.5), “(a) <=> (c)”.
The eight characterizations of an adic morphism of topologically finite type.
public theorem adicFiniteType_tfae (φ : A →+* B) (hφ : Continuous φ)
(hA : TopologicalRing.IsAdic A) (hB : TopologicalRing.IsAdic B)
(hAfg : ∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧ I.FG)
(hBfg : ∃ J : Ideal B, TopologicalRing.IsIdealOfDefinition J ∧ J.FG) :
List.TFAE [
RingHom.IsAdic φ ∧ TopologicalRing.IsTopologicallyOfFiniteType φ,
RingHom.IsTaut φ ∧ TopologicalRing.IsTopologicallyOfFiniteType φ,
FiniteTypeModuloSomeIdealOfDefinition φ,
FiniteTypeModuloEveryIdealOfDefinition φ,
FiniteTypeAdicAlgebraForSomeIdeal φ,
FiniteTypeAdicAlgebraForEveryIdeal φ,
TopologicalRing.HasRestrictedPowerSeriesPresentation φ,
HasCompletedPolynomialPresentation φ]
TopologicalRing.adicTopologicallyFiniteType_isLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicFiniteTypeIsLocal.lean, line 111. The attribute's comment: “local_property”.
Stacks 0GBW. Being adic and topologically of finite type is a local property of morphisms of weakly admissible adic-star rings: it ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets.
public theorem adicTopologicallyFiniteType_isLocal :
AdicStarPropertyIsLocal.{u}
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsAdic φ ∧ IsTopologicallyOfFiniteType φ)
TopologicalRing.adicTopologicallyFiniteType_isomorphismInvariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicFiniteTypeIsLocalRefined.lean, line 58. The attribute's comment: “local_property”.
Being adic and topologically of finite type is independent of the presentations of the source and the target.
public theorem adicTopologicallyFiniteType_isomorphismInvariant :
IsomorphismInvariant.{u}
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsAdic φ ∧ IsTopologicallyOfFiniteType φ)
(fun R ↦ ∃ I : Ideal R, I.FG ∧ _root_.IsAdic I)
TopologicalRing.adicTopologicallyFiniteType_isLocal', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicFiniteTypeIsLocalRefined.lean, line 74. The attribute's comment: “local_property”.
Being adic and topologically of finite type is a local property of morphisms of weakly admissible adic-star rings: it is independent of the presentations of the source and the target, ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets.
public theorem adicTopologicallyFiniteType_isLocal' :
AdicStarPropertyIsLocal'.{u}
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsAdic φ ∧ IsTopologicallyOfFiniteType φ)
Tag 0GBX, a remark
Tag 0GBX in the Stacks Project.
Rig.nonempty_restrictedNaiveCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/RestrictedPresentation/Construction.lean, line 476.
Stacks Project, Remark 88.14.3 (Tag 0GBX). For a presentation
B = A{x₁, …, x_r} / JofBas a topologicalA-algebra, the completed naive cotangent complexNL^∧_{B/A} = (J / J² → ⨁ i, B dxᵢ)exists: the formal partial derivatives ofA{x₁, …, x_r}exist, and the differential sending the class of a restricted power seriesg ∈ Jto the tuple of its formal partial derivatives is well defined. SinceRestrictedNaiveCotangentComplex Pis a subsingleton, this determines the complex.
public theorem nonempty_restrictedNaiveCotangentComplex
(P : RestrictedPowerSeriesPresentation A B) :
Nonempty (RestrictedNaiveCotangentComplex P)
Rig.nonempty_restrictedPowerSeriesPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/RestrictedPresentation/Construction.lean, line 536. The attribute's comment: “every adic, topologically finite type arrow has a presentation”.
Stacks Project, Tag 0GBX. An arrow of
WAdm^{adic*}which is adic and topologically of finite type can be written asB = A{x₁, …, x_r} / J, so that the construction applies to it. This is condition (7) of Lemma 0GBW.
public theorem nonempty_restrictedPowerSeriesPresentation
(hcont : Continuous (algebraMap A B))
(hA : TopologicalRing.IsAdic A) (hB : TopologicalRing.IsAdic B)
(hAfg : ∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧ I.FG)
(hBfg : ∃ J : Ideal B, TopologicalRing.IsIdealOfDefinition J ∧ J.FG)
(hadic : _root_.RingHom.IsAdic (algebraMap A B))
(hft : TopologicalRing.IsTopologicallyOfFiniteType (algebraMap A B)) :
Nonempty (RestrictedPowerSeriesPresentation A B)
Rig.exists_noetherianPresentationComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/RestrictedPresentation/NoetherianComparison.lean, line 569. The attribute's comment: “agreement with Equation 0AJR”.
Stacks Project, Tag 0GBX. When
Ais Noetherian andIis an ideal of definition for its topology, the complex of Tag 0GBX reproduces the completed naive cotangent complex ofBover(A, I)defined by Equation 0AJR.
public theorem exists_noetherianPresentationComparison
{I : Ideal A} (_hI : TopologicalRing.IsIdealOfDefinition I) (hIadic : _root_.IsAdic I)
{C : Type v} [CommRing C] [Algebra A C] [TopologicalSpace C] [IsTopologicalRing C]
[IsLinearTopology C C]
(hc : IsAdicComplete (I.map (algebraMap A C)) C)
[Algebra.FiniteType (A ⧸ I) (C ⧸ I.map (algebraMap A C))]
(P : RestrictedPowerSeriesPresentation A C) :
∃ Q : CompletedPolynomialPresentation I (AdicFiniteTypeAlgebra.of C hc),
Nonempty (NoetherianPresentationComparison (restrictedNaiveCotangentComplex P) hc Q)
Rig.nonempty_homotopyEquiv_of_idealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/RestrictedPresentation/NoetherianComparison.lean, line 672. The attribute's comment: “independence of the ideal of definition”. References: SGA 6 0 (4.4), “partial”.
Stacks Project, Tag 0GBX. For
Aan adic Noetherian topological ring, the completed naive cotangent complex of Equation 0AJR is independent of the choice of the ideal of definitionI ⊆ A: both are the complex of Tag 0GBX, which is built from the topology ofAalone.
public theorem nonempty_homotopyEquiv_of_idealOfDefinition
{I I' : Ideal A}
(hI : TopologicalRing.IsIdealOfDefinition I) (hIadic : _root_.IsAdic I)
(hI' : TopologicalRing.IsIdealOfDefinition I') (hIadic' : _root_.IsAdic I')
{C : Type v} [CommRing C] [Algebra A C] [TopologicalSpace C] [IsTopologicalRing C]
[IsLinearTopology C C]
(hc : IsAdicComplete (I.map (algebraMap A C)) C)
[Algebra.FiniteType (A ⧸ I) (C ⧸ I.map (algebraMap A C))]
(hc' : IsAdicComplete (I'.map (algebraMap A C)) C)
[Algebra.FiniteType (A ⧸ I') (C ⧸ I'.map (algebraMap A C))]
(P : RestrictedPowerSeriesPresentation A C)
(Q : CompletedPolynomialPresentation I (AdicFiniteTypeAlgebra.of C hc))
(Q' : CompletedPolynomialPresentation I' (AdicFiniteTypeAlgebra.of C hc')) :
Nonempty (HomotopyEquiv
(Rig.completedNaiveCotangentComplex (AdicFiniteTypeAlgebra.of C hc) Q).cochainComplex
(Rig.completedNaiveCotangentComplex
(AdicFiniteTypeAlgebra.of C hc') Q').cochainComplex)
Rig.exists_restrictedPresentationComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/RestrictedPresentation/PresentationComparison.lean, line 732. The attribute's comment: “well defined in K(B)”.
Stacks Project, Tag 0GBX. Any two presentations of
Bare related by a morphism of presentations, and the map of complexes it induces is a homotopy equivalence. This is the existence half of "the complex is well defined inK(B)".
public theorem exists_restrictedPresentationComparison :
Nonempty (RestrictedPresentationComparison K L)
Rig.homotopy_of_restrictedPresentationComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/RestrictedPresentation/PresentationComparison.lean, line 773. The attribute's comment: “unique isomorphism in K(B)”.
Stacks Project, Tag 0GBX. The isomorphism in
K(B)is unique: any two morphisms of presentations induce homotopic maps of complexes. This is Step 2 of the proof of Lemma 0GAE.
public theorem homotopy_of_restrictedPresentationComparison
(e e' : RestrictedPresentationComparison K L) :
Nonempty (Homotopy e.equiv.hom e'.equiv.hom)
Tag 0GBY, a lemma
Tag 0GBY in the Stacks Project.
TopologicalRing.adicAndFiniteType_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Restricted/FiniteTypeBaseChange.lean, line 221.
Adic morphisms of topologically finite type in the category of weakly admissible adic-star rings form a local property which is stable under completed tensor-product base change.
public theorem adicAndFiniteType_isStableUnderBaseChange :
TopologicalRing.AdicStarPropertyIsStableUnderBaseChange.{u}
(fun φ => RingHom.IsAdic φ ∧ TopologicalRing.IsTopologicallyOfFiniteType φ)
Tag 0GBZ, a lemma
Tag 0GBZ in the Stacks Project.
TopologicalRing.adicTopologicallyFiniteType_isStableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicFiniteTypeIsLocal.lean, line 156.
Stacks 0GBZ. The local property of Stacks 0GBW — being adic and topologically of finite type — is stable under composition on weakly admissible adic-star rings.
public theorem adicTopologicallyFiniteType_isStableUnderComposition :
AdicStarPropertyIsStableUnderComposition.{u}
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsAdic φ ∧ IsTopologicallyOfFiniteType φ)
TopologicalRing.adicTopologicallyFiniteType_isStableUnderComposition', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicFiniteTypeIsLocalRefined.lean, line 87.
Being adic and topologically of finite type is stable under composition on weakly admissible adic-star rings.
public theorem adicTopologicallyFiniteType_isStableUnderComposition' :
AdicStarPropertyIsStableUnderComposition'.{u}
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsAdic φ ∧ IsTopologicallyOfFiniteType φ)
Tag 0GC0, a lemma
Tag 0GC0 in the Stacks Project.
AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_adicStar_tfae', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicFiniteTypeCharacterizationRefined.lean, line 59. The attribute's comment: “all four conditions, with all six equivalences proved, from one named hypothesis this library does not have: Stacks 0AKX in the adic* form of Stacks 0AKT together with Stacks 0AIC as hchart. The library's Stacks 0ANW is unconditional, so nothing is forwarded from it; the covering refinement of Stacks 0AJ2 and the implication (2) implies (1) of Stacks 0AKX, which used to be forwarded as href and h0AKX, are theorems. Stacks 0AJ3, the implication (4) implies (1) of Stacks 0ANL and Stacks 0ANV on countably indexed charts are no longer among them: Stacks 0AJ3 is proved for a base which is a formal algebraic space, (4) implies (1) is obtained as (4) implies (5) implies (1), and Stacks 0ANV on countably indexed charts is proved. Neither are the locality axioms of Situation 0CBA for tautness with topological finite type: they follow from the locality of Stacks 0ANU”.
For a morphism
f : X ⟶ Yof locally adic* formal algebraic spaces overS, the condition that every affine representable étale square overfcarry an adic, topologically of finite type arrow ofWAdm^{adic*}, the existence of an affine étale covering ofYtogether with affine étale coverings of the fibre products of its members withXon which that condition holds, the existence of an affine étale covering ofXwhose members factor through affine representable étale charts ofYby such arrows, andfbeing locally of finite type, are all equivalent, provided chart presentations are adic*.
theorem isLocallyOfFiniteType_adicStar_tfae' {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
(hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y)
(hchart : ChartPresentationIsAdicStar B S hS) :
List.TFAE
[HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar
TopologicalRing.IsAdicTopologicallyOfFiniteTypeHom f,
HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar
TopologicalRing.IsAdicTopologicallyOfFiniteTypeHom f,
HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar
TopologicalRing.IsAdicTopologicallyOfFiniteTypeHom f,
IsLocallyOfFiniteType B S hS f]
AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_tfae_of_isLocallyAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicFiniteTypeCharacterizationUnconditional.lean, line 89.
Stacks 0GC0. Let
f : X ⟶ Ybe a morphism of locally adic* formal algebraic spaces overS. The following are equivalent:
- for every commutative square with
U,Vaffine formal algebraic spaces andU ⟶ X,V ⟶ Yrepresentable by algebraic spaces and étale, the morphismU ⟶ Vcorresponds to an arrow ofWAdm^{adic*}which is adic and topologically of finite type;- there are a covering
{Yⱼ ⟶ Y}as in Definition 0AIM and for eachja covering{Xⱼᵢ ⟶ Yⱼ ×_Y X}as in Definition 0AIM such that eachXⱼᵢ ⟶ Yⱼcorresponds to an arrow ofWAdm^{adic*}which is adic and topologically of finite type;- there are a covering
{Xᵢ ⟶ X}as in Definition 0AIM and for eachia factorizationXᵢ ⟶ Yᵢ ⟶ YwhereYᵢis an affine formal algebraic space,Yᵢ ⟶ Yis representable by algebraic spaces and étale, andXᵢ ⟶ Yᵢcorresponds to an arrow ofWAdm^{adic*}which is adic and topologically of finite type;fis locally of finite type.This is the source's proof. By Stacks 0AKX for the adic* property together with Stacks 0AIC (
chartPresentationIsAdicStarOfWeaklyAdmissible) every weakly admissible ring presenting an affine chart ofXorYis adic*, so on each chart the adic, topologically of finite type condition and the taut, topologically of finite type condition agree by Stacks 0GBW (hasPropertyOnAffineChartMap_adicStar_iff_of_isWeaklyAdmissible); and Stacks 0ANW (isLocallyOfFiniteType_tfae'), for the locally countably indexed spacesXandY, identifies the three resulting conditions withfbeing locally of finite type.
theorem isLocallyOfFiniteType_tfae_of_isLocallyAdicStar {X Y : FppfSheaf B S hS}
(f : X ⟶ Y) (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y) :
List.TFAE
[HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar
TopologicalRing.IsAdicTopologicallyOfFiniteTypeHom f,
HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar
TopologicalRing.IsAdicTopologicallyOfFiniteTypeHom f,
HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar
TopologicalRing.IsAdicTopologicallyOfFiniteTypeHom f,
IsLocallyOfFiniteType B S hS f]
Sources
Section88.12 Finite type on reductions#
Section 88.12 of the Stacks Project, Tag 0GC1. 7 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GC2, a lemma
Tag 0GC2 in the Stacks Project.
Rig.IsFiniteTypeOnReductions, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Reduction.lean, line 62. The attribute's comment: “finite_type_on_reductions”.
A continuous homomorphism of linearly topologized commutative rings is of finite type on reductions if the induced homomorphism between the quotients by their topological nilradicals is of finite type.
public abbrev IsFiniteTypeOnReductions {A B : Type*} [CommRing A] [TopologicalSpace A]
[IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsLinearTopology B B]
(φ : A →+* B) (hφ : Continuous φ) : Prop
Rig.finiteTypeOnReductionsProperty_localizationPreserves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ReductionLocality.lean, line 194. The attribute's comment: “localization_preserves”.
Finite type on reductions ascends along a completed étale localization diagram of countably indexed weakly admissible rings: the first locality axiom of Situation 0CBA.
public theorem finiteTypeOnReductionsProperty_localizationPreserves :
TopologicalRing.LocalizationPreserves.{u} TopologicalRing.IsCountablyWeaklyAdmissible
TopologicalRing.FiniteTypeOnReductionsProperty
Rig.finiteTypeOnReductionsProperty_finiteProductPreserves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ReductionLocality.lean, line 287. The attribute's comment: “finite_product”.
Finite type on reductions is preserved by a finite product of targets: the third locality axiom of Situation 0CBA. Topological nilpotence in a product is a coordinatewise condition, so the reduction of the product is a quotient of the product of the reductions.
public theorem finiteTypeOnReductionsProperty_finiteProductPreserves :
TopologicalRing.FiniteProductPreserves.{u} TopologicalRing.IsCountablyWeaklyAdmissible
TopologicalRing.FiniteTypeOnReductionsProperty
Rig.finiteTypeOnReductionsProperty_faithfullyFlatDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ReductionLocality.lean, line 426. The attribute's comment: “faithfully_flat_descent”.
Finite type on reductions descends along a completed étale localization diagram of countably indexed weakly admissible rings whose horizontal map is faithfully flat: the second locality axiom of Situation 0CBA. The reduced diagonal of the diagram is of finite type, being the reduction of the canonical map into the completion of an étale algebra followed by the reduction of the completed morphism, and finite type descends along the faithfully flat, finitely presented reduction of the horizontal map.
public theorem finiteTypeOnReductionsProperty_faithfullyFlatDescent :
TopologicalRing.FaithfullyFlatDescent.{u} TopologicalRing.IsCountablyWeaklyAdmissible
TopologicalRing.FiniteTypeOnReductionsProperty
Rig.isFiniteTypeOnReductions_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ReductionLocality.lean, line 454.
Finite type on reductions is a local property of morphisms of countably indexed weakly admissible topological rings: it ascends along completed étale localization diagrams, descends along those whose horizontal map is faithfully flat, and is preserved by finite products of targets.
public theorem isFiniteTypeOnReductions_local :
TopologicalRing.PropertyIsLocal.{u} TopologicalRing.FiniteTypeOnReductionsProperty
TopologicalRing.IsCountablyWeaklyAdmissible
Tag 0GC3, a lemma
Tag 0GC3 in the Stacks Project.
Rig.isFiniteTypeOnReductions_stableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Restricted/ReductionBaseChange.lean, line 319.
Finite type on reductions is a local property of countably indexed weakly admissible rings that is preserved by completed tensor-product base change.
public theorem isFiniteTypeOnReductions_stableUnderBaseChange :
TopologicalRing.IsStableUnderBaseChange TopologicalRing.FiniteTypeOnReductionsProperty
Tag 0GC4, a lemma
Tag 0GC4 in the Stacks Project.
Rig.finiteTypeOnReductions_isStableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Restricted/ReductionComposition.lean, line 56.
Finite type on reductions is a composition-stable local property of morphisms of countably indexed weakly admissible topological rings.
public theorem finiteTypeOnReductions_isStableUnderComposition :
TopologicalRing.PropertyIsStableUnderComposition
TopologicalRing.FiniteTypeOnReductionsProperty.{u}
Tag 0GC5, a lemma
Tag 0GC5 in the Stacks Project.
Rig.isFiniteTypeOnReductions_of_isTaut_of_isTopologicallyOfFiniteType, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Reduction.lean, line 72.
A continuous taut homomorphism that is topologically of finite type is of finite type on reductions, provided its source has a weak ideal of definition.
public lemma isFiniteTypeOnReductions_of_isTaut_of_isTopologicallyOfFiniteType
{A B : Type*} [CommRing A] [TopologicalSpace A] [IsLinearTopology A A]
[CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
(φ : A →+* B) (hφ : Continuous φ) (hA : TopologicalRing.IsWeaklyPreAdmissible A)
(htaut : RingHom.IsTaut φ) (hft : TopologicalRing.IsTopologicallyOfFiniteType φ) :
IsFiniteTypeOnReductions φ hφ
Tag 0GC6, a lemma
Tag 0GC6 in the Stacks Project.
Rig.isTopologicallyOfFiniteType_of_isFiniteTypeOnReductions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Reduction.lean, line 280.
A continuous homomorphism into a Noetherian weakly admissible topological ring that is of finite type on reductions is topologically of finite type.
public theorem isTopologicallyOfFiniteType_of_isFiniteTypeOnReductions
{A B : Type*} [CommRing A] [TopologicalSpace A] [IsLinearTopology A A]
[CommRing B] [TopologicalSpace B]
[IsTopologicalRing B] [IsLinearTopology B B] [IsNoetherianRing B]
(φ : A →+* B) (hφ : Continuous φ) (hB : TopologicalRing.IsWeaklyAdmissible B)
(hred : IsFiniteTypeOnReductions φ hφ) :
TopologicalRing.IsTopologicallyOfFiniteType φ
Tag 0GG6, a lemma
Tag 0GG6 in the Stacks Project.
Rig.isFiniteTypeOnReductions_iff_isTopologicallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Reduction.lean, line 363.
An adic homomorphism into a Noetherian weakly admissible ring is of finite type on reductions if and only if it is topologically of finite type.
public theorem isFiniteTypeOnReductions_iff_isTopologicallyOfFiniteType
{A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsLinearTopology A A] [CommRing B] [TopologicalSpace B]
[IsTopologicalRing B] [IsLinearTopology B B] [IsNoetherianRing B]
(φ : A →+* B) (hφ : Continuous φ)
(hA : TopologicalRing.IsWeaklyPreAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(hadic : RingHom.IsAdic φ) :
IsFiniteTypeOnReductions φ hφ ↔
TopologicalRing.IsTopologicallyOfFiniteType φ
Tag 0GC7, a lemma
Tag 0GC7 in the Stacks Project.
AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeOnReductions_tfae_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeOnReductionsTfae.lean, line 247. The attribute's comment: “the four conditions, for a morphism of locally countably indexed formal algebraic spaces; condition (4) is read for every pair of reductions of the source and the target and every morphism between them over f, reductions existing and being unique up to unique isomorphism by Stacks 0AIN”.
Stacks 0GC7. For a morphism
f : X ⟶ Yof locally countably indexed formal algebraic spaces overSthe following are equivalent:
- every affine representable étale square over
fhas its upper map given by an arrow ofWAdm^{count}with the property of Stacks 0GC2;- there is an affine étale covering of
Ytogether with affine étale coverings of the fibre products of its members withXwhose maps to the members of the first covering are given by such arrows;- there is an affine étale covering of
Xwhose members factor through affine formal algebraic spaces representable étale overYby such arrows;- the morphism of reductions
f_red : X_red ⟶ Y_redis locally of finite type.The first three are the three conditions of Stacks 0ANG for the property of Stacks 0GC2, which is local on
WAdm^{count}; (3) ⟹ (4) and (4) ⟹ (1) are the affine computation of Stacks 0GB6 together with the étale locality of being locally of finite type.
theorem isLocallyOfFiniteTypeOnReductions_tfae_of_isLocallyCountablyIndexed
{X Y : FppfSheaf B S hS} (f : X ⟶ Y)
(hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y) :
List.TFAE
[HasPropertyOnEveryAffineEtaleDiagram B S hS
TopologicalRing.IsCountablyWeaklyAdmissible
TopologicalRing.FiniteTypeOnReductionsProperty f,
HasPropertyAfterTargetCover B S hS
TopologicalRing.IsCountablyWeaklyAdmissible
TopologicalRing.FiniteTypeOnReductionsProperty f,
HasPropertyAfterSourceCover B S hS
TopologicalRing.IsCountablyWeaklyAdmissible
TopologicalRing.FiniteTypeOnReductionsProperty f,
IsLocallyOfFiniteTypeOnReductions B S hS f]
Sources
Section88.13 Flat morphisms#
Section 88.13 of the Stacks Project, Tag 0GC8. 8 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GC9, a lemma
Tag 0GC9 in the Stacks Project.
TopologicalRing.flat_isLocalNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FlatLocalProperty.lean, line 311. References: SGA 3 VIIB (1.3.4), “Flatness clause”.
Flatness is a local property of morphisms of Noetherian adic topological rings (Stacks 0GC9): it ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets.
public theorem flat_isLocalNoetherian :
PropertyIsLocalNoetherian
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦ φ.Flat)
TopologicalRing.flat_isLocalNoetherian', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FlatLocalPropertyRefined.lean, line 71. References: SGA 3 VIIB (1.3.4), “Flatness clause”.
Flatness is a local property of morphisms of Noetherian adic topological rings: it is independent of the presentations of the source and the target, ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets.
public theorem flat_isLocalNoetherian' :
PropertyIsLocalNoetherian'
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦ φ.Flat)
Tag 0GCA, a lemma
Tag 0GCA in the Stacks Project.
TopologicalRing.flat_isStableUnderBaseChangeByFiniteTypeOnReductions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatBaseChange.lean, line 797. The attribute's comment: “part (1)”.
Stacks 0GCA, part (1). Flatness of morphisms of Noetherian adic topological rings (Stacks 0GC9) is stable under completed tensor-product base change along morphisms of finite type on reductions (Stacks 0GC2), in the sense of Remark 0GBG.
public theorem flat_isStableUnderBaseChangeByFiniteTypeOnReductions :
IsStableUnderBaseChangeBy
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦ φ.Flat)
FiniteTypeOnReductionsProperty
TopologicalRing.flatAdicFiniteType_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatBaseChange.lean, line 905. The attribute's comment: “part (2)”.
Stacks 0GCA, part (2). Flatness (Stacks 0GC9) together with the property of Stacks 0GBW, being adic and topologically of finite type, is stable under base change in the sense of Remark 0GBF: for continuous homomorphisms
B → AandB → Cof Noetherian adic topological rings withB → Aflat, adic and topologically of finite type, the completed tensor productA ⊗̂_B Cis Noetherian adic andC → A ⊗̂_B Cis again flat, adic and topologically of finite type. No condition is imposed onB → C.
public theorem flatAdicFiniteType_isStableUnderBaseChange :
IsStableUnderBaseChangeNoetherian
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
φ.Flat ∧ RingHom.IsAdic φ ∧ IsTopologicallyOfFiniteType φ)
TopologicalRing.flat_isStableUnderBaseChangeByFiniteTypeOnReductions', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatBaseChangeRefined.lean, line 113. The attribute's comment: “part (1)”.
Stacks 0GCA, part (1). Flatness of morphisms of Noetherian adic topological rings (Stacks 0GC9) is stable under completed tensor-product base change along morphisms of finite type on reductions (Stacks 0GC2), in the sense of Remark 0GBG.
public theorem flat_isStableUnderBaseChangeByFiniteTypeOnReductions' :
IsStableUnderBaseChangeBy'
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦ φ.Flat)
FiniteTypeOnReductionsProperty
TopologicalRing.flatAdicFiniteType_isStableUnderBaseChange', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatBaseChangeRefined.lean, line 170. The attribute's comment: “part (2)”.
Stacks 0GCA, part (2). Flatness (Stacks 0GC9) together with the property of Stacks 0GBW, being adic and topologically of finite type, is stable under base change in the sense of Remark 0GBF: for continuous homomorphisms
B → AandB → Cof Noetherian adic topological rings withB → Aflat, adic and topologically of finite type, the completed tensor productA ⊗̂_B Cis Noetherian adic andC → A ⊗̂_B Cis again flat, adic and topologically of finite type. No condition is imposed onB → C.
public theorem flatAdicFiniteType_isStableUnderBaseChange' :
IsStableUnderBaseChangeNoetherian'
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
φ.Flat ∧ RingHom.IsAdic φ ∧ IsTopologicallyOfFiniteType φ)
Tag 0GCB, a lemma
Tag 0GCB in the Stacks Project.
TopologicalRing.flat_isStableUnderCompositionNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FlatLocalProperty.lean, line 323.
Stacks 0GCB. Flatness, as a local property of morphisms of Noetherian adic topological rings (Stacks 0GC9), is stable under composition: the composite of two flat ring homomorphisms is flat.
public theorem flat_isStableUnderCompositionNoetherian :
PropertyIsStableUnderCompositionNoetherian
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦ φ.Flat)
TopologicalRing.flat_isStableUnderCompositionNoetherian', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FlatLocalPropertyRefined.lean, line 84.
Flatness, as a local property of morphisms of Noetherian adic topological rings, is stable under composition: the composite of two flat ring homomorphisms is flat.
public theorem flat_isStableUnderCompositionNoetherian' :
PropertyIsStableUnderCompositionNoetherian'
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦ φ.Flat)
Tag 0GCC, a definition
Tag 0GCC in the Stacks Project.
AlgebraicGeometry.FormalSpace.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Flat.lean, line 87.
Stacks 0GCC. A morphism of formal algebraic spaces over
Sis flat when every morphism between affine, representable, étale charts of its source and target is induced by a flat continuous homomorphism of adic Noetherian topological rings.
abbrev IsFlat (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
{X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop
Tag 0GCD, a lemma
Tag 0GCD in the Stacks Project.
AlgebraicGeometry.FormalSpace.isFlat_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatCharacterization.lean, line 165. The attribute's comment: “conditions (1) and (2) agree by Definition 0GCC, as the source's proof states; Stacks 0AJ3, the covering refinement of Stacks 0AJ2 and the locality axioms of Stacks 0GC9 read through Stacks 0AN8 and Stacks 0AN9 are carried as the hypotheses hpb, href, hasc and hdesc”.
Stacks 0GCD. For a morphism
f : X ⟶ Yof locally Noetherian formal algebraic spaces overS, flatness offin the sense of Definition 0GCC, the condition that every affine representable étale square overfcarry a flat map of Noetherian adic topological rings, the existence of an affine étale covering ofYtogether with affine étale coverings of the fibre products of its members withXon which that condition holds, and the existence of an affine étale covering ofXwhose members factor flatly through affine representable étale charts ofY, are all equivalent.The first two conditions agree by Definition 0GCC, as in the source's own proof; the last three are the three conditions of Stacks 0ANG for the class of Noetherian adic topological rings and flatness, which is a local property of such arrows by Stacks 0GC9. The hypotheses
hpb,href,hascandhdesccarry Stacks 0AJ3, the covering refinement of Stacks 0AJ2, and the locality axioms of Situation 0CBA read through Stacks 0AN8 and Stacks 0AN9.
theorem isFlat_tfae {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
(hY : IsFormalAlgebraicSpace B S hS Y)
(hpb : ∀ (V : FppfSheaf B S hS) (v : V ⟶ Y), IsAffineFormalAlgebraicSpace B S hS V →
IsRepresentableEtale B S hS v → IsFormalAlgebraicSpace B S hS (pullback v f))
(hasc : ChartPropertyAscendsAlongAffineEtale B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom)
(hdesc : ChartPropertyDescendsAlongFiniteAffineEtaleCover B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom)
(href : HasEtaleRefinementOfSourceCover B S hS f) :
List.TFAE
[IsFlat B S hS f,
HasPropertyOnEveryAffineEtaleDiagram B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom f,
HasPropertyAfterTargetCover B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom f,
HasPropertyAfterSourceCover B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom f]
AlgebraicGeometry.FormalSpace.isFlat_tfae_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatCharacterizationLocallyNoetherian.lean, line 97.
Stacks 0GCD. For a morphism
f : X ⟶ Yof locally Noetherian formal algebraic spaces overSthe following are equivalent:
fis flat in the sense of Definition 0GCC;- every commutative square with affine formal algebraic spaces
U,Vand representable étale mapsU ⟶ X,V ⟶ Ycarries a flat map of Noetherian adic topological rings onU ⟶ V;- there are an affine étale covering
{Yⱼ ⟶ Y}and affine étale coverings{Xⱼᵢ ⟶ Yⱼ ×_Y X}with eachXⱼᵢ ⟶ Yⱼcorresponding to a flat map of Noetherian adic topological rings;- there are an affine étale covering
{Xᵢ ⟶ X}and factorizationsXᵢ ⟶ Yᵢ ⟶ Ythrough affine formal algebraic spaces representable étale overYwith eachXᵢ ⟶ Yᵢcorresponding to a flat map of Noetherian adic topological rings.As in the source, (1) and (2) agree by Definition 0GCC, and (2), (3), (4) are the three conditions of the Noetherian variant of Stacks 0ANG (Remark 0ANI) for flatness, a local property of arrows of
WAdm^{Noeth}by Stacks 0GC9.
theorem isFlat_tfae_of_isLocallyNoetherian {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
(hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y) :
List.TFAE
[IsFlat B S hS f,
HasPropertyOnEveryAffineEtaleDiagram B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom f,
HasPropertyAfterTargetCover B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom f,
HasPropertyAfterSourceCover B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom f]
Tag 0GCE, a lemma
Tag 0GCE in the Stacks Project.
AlgebraicGeometry.FormalSpace.isFlat_pullback_snd_of_isLocallyOfFiniteTypeOnReductions_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Restricted/FlatBaseChangeLocallyNoetherian.lean, line 108. The attribute's comment: “part (1)”.
Stacks 0GCE, part (1). Let
f : X ⟶ Yandg : Z ⟶ Ybe morphisms of locally Noetherian formal algebraic spaces overS. Iffis flat (Definition 0GCC) and the morphism of reductionsg_red : Z_red ⟶ Y_redis locally of finite type, then the base changeX ×_Y Z ⟶ Zis flat.Flatness of arrows of
WAdm^{Noeth}is stable under base change by arrows of finite type on reductions (Stacks 0GCA, part (1)); the hypothesis ong_redgives that property on every affine étale chart map ofgby the implication (4) ⟹ (1) of Stacks 0GC7, and Stacks 0GBG transfers flatness to the second projection.
theorem isFlat_pullback_snd_of_isLocallyOfFiniteTypeOnReductions_of_isLocallyNoetherian
{X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y) (hX : IsLocallyNoetherian B S hS X)
(hY : IsLocallyNoetherian B S hS Y) (hZ : IsLocallyNoetherian B S hS Z)
(hf : IsFlat B S hS f) (hg : IsLocallyOfFiniteTypeOnReductions B S hS g) :
IsFlat B S hS (pullback.snd f g)
AlgebraicGeometry.FormalSpace.isFlat_and_isLocallyOfFiniteType_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Restricted/FlatBaseChangeLocallyNoetherian.lean, line 138. The attribute's comment: “part (2)”.
Stacks 0GCE, part (2). Let
f : X ⟶ Yandg : Z ⟶ Ybe morphisms of locally Noetherian formal algebraic spaces overS. Iffis flat (Definition 0GCC) and locally of finite type (Stacks 0AM4), then the base changeX ×_Y Z ⟶ Zis flat and locally of finite type.Flatness together with being adic and topologically of finite type is stable under arbitrary base change of arrows of
WAdm^{Noeth}(Stacks 0GCA, part (2)); the hypotheses onfgive that property on every affine étale chart map off(Stacks 0GC0 read atWAdm^{Noeth}), Stacks 0GBF transfers it to the second projection, and flatness is read off its first conjunct. The second conclusion is Stacks 0AQ5, which needs neither flatness nor the Noetherian hypotheses.
theorem isFlat_and_isLocallyOfFiniteType_pullback_snd {X Y Z : FppfSheaf B S hS}
(f : X ⟶ Y) (g : Z ⟶ Y) (hX : IsLocallyNoetherian B S hS X)
(hY : IsLocallyNoetherian B S hS Y) (hZ : IsLocallyNoetherian B S hS Z)
(hf : IsFlat B S hS f) (hft : IsLocallyOfFiniteType B S hS f) :
IsFlat B S hS (pullback.snd f g) ∧ IsLocallyOfFiniteType B S hS (pullback.snd f g)
AlgebraicGeometry.FormalSpace.isFlat_pullback_snd_of_isLocallyOfFiniteTypeOnReductions', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Restricted/FlatBaseChangeRefined.lean, line 78. The attribute's comment: “part (1), on the 0GBG transfer inputs and the 0GC7 (4) implies (1) inputs”.
Stacks 0GCE, part (1). Let
f : X ⟶ Yandg : Z ⟶ Ybe morphisms of locally Noetherian formal algebraic spaces overS. Iffis flat in the sense of Definition 0GCC and the morphism of reductionsg_red : Z_red ⟶ Y_redis locally of finite type, then the base changeX ×_Y Z ⟶ Zis flat.Flatness of arrows of
WAdm^{Noeth}is stable under base change by arrows of finite type on reductions by part (1) of Stacks 0GCA, which the library proves outright; Remark 0GBG transfers that to the second projection of the fibre product, on the two inputsh31andhcoverit carries — the invariance of flatness under isomorphism of targets is read off the locality field of the stability bundle, whose first axiom it is; and the hypothesis ong_redbecomes the chart condition the transfer consumes by the implication (4) ⟹ (1) of Stacks 0GC7, on the two inputshbridgeandhredsquare. Nothing about flatness is assumed in any of the five.
theorem isFlat_pullback_snd_of_isLocallyOfFiniteTypeOnReductions'
(h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS
TopologicalRing.IsNoetherianAdic TopologicalRing.IsFlatHom)
(hbridge : ChartPropertyIsFiniteTypeOnReductions B S hS)
(hredsquare : IsLocallyOfFiniteTypeOnReductionsOnEveryAffineEtaleSquare B S hS)
{X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
(hcover : HasBaseChangeCoverOverPullbackSnd B S hS f g)
(hZ : IsLocallyCountablyIndexed B S hS Z) (hY : IsLocallyCountablyIndexed B S hS Y)
(hf : IsFlat B S hS f) (hg : IsLocallyOfFiniteTypeOnReductions B S hS g) :
IsFlat B S hS (pullback.snd f g)
AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_pullback_snd_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Restricted/FlatBaseChangeRefined.lean, line 253. The attribute's comment: “part (2), locally of finite type, from Stacks 0AQ5 alone -- the second projection is a base change of f. No input of Remark 0GBF and no comparison of Stacks 0GC0 is used, and flatness of f is not used”.
Stacks 0GCE, part (2), locally of finite type. Let
f : X ⟶ Yandg : Z ⟶ Ybe morphisms of locally Noetherian formal algebraic spaces overS. Iffis locally of finite type in the sense of Stacks 0AM4, then the base changeX ×_Y Z ⟶ Zis locally of finite type.The second projection of the fibre product is a base change of
f, and a base change of a morphism locally of finite type is locally of finite type by Stacks 0AQ5, which the library proves outright asIsLocallyOfFiniteType.of_isPullback. Nothing else is needed, so neither flatness offnor the locally Noetherian hypotheses of the source nor the inputs of the transfer of Remark 0GBF appear: the conclusion holds at every morphism of fppf sheaves, which is at least as general as part (2) of the source.
theorem isLocallyOfFiniteType_pullback_snd_of_isLocallyOfFiniteType {X Y Z : FppfSheaf B S hS}
(f : X ⟶ Y) (g : Z ⟶ Y) (hft : IsLocallyOfFiniteType B S hS f) :
IsLocallyOfFiniteType B S hS (pullback.snd f g)
Tag 0GCF, a lemma
Tag 0GCF in the Stacks Project.
AlgebraicGeometry.FormalSpace.isFlat_comp_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatComposition.lean, line 58.
Stacks 0GCF. If
f : X ⟶ Yandg : Y ⟶ Zare flat morphisms of locally Noetherian formal algebraic spaces overS, theng ∘ fis flat.Flatness is condition (1) of Stacks 0ANG for Noetherian adic rings and flat ring maps, a local property stable under composition (Stacks 0GCB), so Remark 0GBK applies.
theorem isFlat_comp_of_isLocallyNoetherian {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
(hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
(hZ : IsLocallyNoetherian B S hS Z)
(hf : IsFlat B S hS f) (hg : IsFlat B S hS g) :
IsFlat B S hS (f ≫ g)
Tag 0GCG, a lemma
Tag 0GCG in the Stacks Project.
AlgebraicGeometry.FormalSpace.isFlat_of_hasPropertyULift_flatPropertyULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FlatOfBootstrapFlat.lean, line 223.
Stacks 0GCG. A morphism
f : X ⟶ Yof formal algebraic spaces overSwhich is representable by algebraic spaces and flat in the Bootstrap sense of Stacks 03XZ is flat in the sense of Definition 0GCC.On an affine representable étale square over
f, the homomorphismφpresenting the chart map is taut becausefis representable. Bootstrap flatness offmakesφflat modulo every weak ideal of definition of its source, and Stacks 0912 concludes thatφis flat. The source assumesXandYlocally Noetherian; the proof does not use this.
theorem isFlat_of_hasPropertyULift_flatPropertyULift {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
(hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
(hflat : Space.HasPropertyULift.{u + 1} B S hS (Space.flatPropertyULift.{u + 1} B S hS)
f.hom hrep) :
IsFlat B S hS f
Sources
Section88.14 Rig-closed points#
Section 88.14 of the Stacks Project, Tag 0GG7. 12 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GG8, a lemma
Tag 0GG8 in the Stacks Project.
Rig.rigPoint_tfae, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/RigPointCriterion.lean, line 514.
The eight equivalent characterizations of a rig point in a Noetherian adic topological ring.
public lemma rigPoint_tfae {A : Type*} [CommRing A] [TopologicalSpace A]
[IsTopologicalRing A] [IsNoetherianRing A]
[@CompleteSpace A (IsTopologicalAddGroup.rightUniformSpace A)] [T2Space A]
(_hadic : ∃ I : Ideal A, IsAdic I) (q : Ideal A) [q.IsPrime] :
List.TFAE
[ ∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧
Ideal.IsMaximalAmongPrimesAvoiding I q,
∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧
Ideal.IsClosedPointAwayFrom I q,
∀ I : Ideal A, TopologicalRing.IsIdealOfDefinition I →
Ideal.IsMaximalAmongPrimesAvoiding I q,
∀ I : Ideal A, TopologicalRing.IsIdealOfDefinition I →
Ideal.IsClosedPointAwayFrom I q,
ringKrullDim (A ⧸ q) = 1 ∧
∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧ ¬ I ≤ q,
ringKrullDim (A ⧸ q) = 1 ∧
∀ I : Ideal A, TopologicalRing.IsIdealOfDefinition I → ¬ I ≤ q,
ringKrullDim (A ⧸ q) = 1 ∧ ¬ DiscreteTopology (A ⧸ q),
Ideal.IsRigPointLocalCondition q ]
Tag 0GG9, a definition
Tag 0GG9 in the Stacks Project.
Rig.Ideal.IsRigPointLocalCondition, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/RigPointCriterion.lean, line 115. The attribute's comment: “rig-closed, via condition (8) of the rig-point criterion”.
The local description in condition (8) of the rig-point criterion. The topology and completeness on the quotient are the ones induced from
A.
public abbrev Ideal.IsRigPointLocalCondition {A : Type*} [CommRing A]
[TopologicalSpace A] [IsTopologicalRing A] (q : Ideal A) [q.IsPrime] : Prop
Rig.Ideal.IsRigClosed, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigClosedPoint.lean, line 47.
A prime
qof a topological ring is rig-closed if some ideal of definition is not contained inqandqis maximal among the primes not containing it.
public def Ideal.IsRigClosed {A : Type u} [CommRing A] [TopologicalSpace A]
(q : Ideal A) : Prop
Tag 0GGA, a lemma
Tag 0GGA in the Stacks Project.
Rig.exists_residueFieldMap_finiteType_of_rigPoint, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/RelativeCriterion.lean, line 99.
The residue field at a rig-closed point is of finite type over the quotient of the source by its ideal of topologically nilpotent elements.
public lemma exists_residueFieldMap_finiteType_of_rigPoint
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
(q : Ideal B) [q.IsPrime]
(hq : Ideal.IsRigPointLocalCondition q)
(φ : A →+* B) (hφ : Continuous φ)
(hfiniteType : (Ideal.quotientMap (I := topologicalNilradical A)
(topologicalNilradical B) φ
(by
intro x hx
exact IsTopologicallyNilpotent.map hφ
(IsTopologicallyNilpotent.mem_topologicalNilradical_iff.mp hx))).FiniteType) :
let _ : IsLocalRing (B ⧸ q) := hq.choose
∃ ψ : (A ⧸ topologicalNilradical A) →+* IsLocalRing.ResidueField (B ⧸ q),
ψ.comp (Ideal.Quotient.mk (topologicalNilradical A)) =
(IsLocalRing.residue (B ⧸ q)).comp ((Ideal.Quotient.mk q).comp φ) ∧
ψ.FiniteType
Tag 0GGB, a lemma
Tag 0GGB in the Stacks Project.
Rig.rigPoint_relative_tfae, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/RelativeCriterion.lean, line 218.
For an adic, topologically finite type morphism of Noetherian weakly admissible rings, a rig-closed prime upstairs satisfies the relative rig-closed point criterion.
public lemma rigPoint_relative_tfae {A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hadic : RingHom.IsAdic φ)
(hft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(q : Ideal B) [q.IsPrime]
(hq : Ideal.IsClosedPointAwayFrom
(topologicalNilradical B) q) :
let a := topologicalNilradical A
let p := q.comap φ
List.TFAE
[ ∃ hlocal : IsLocalRing (B ⧸ q),
letI : IsLocalRing (B ⧸ q) := hlocal
∃ ψ : (A ⧸ a) →+* IsLocalRing.ResidueField (B ⧸ q),
ψ.comp (Ideal.Quotient.mk a) =
(IsLocalRing.residue (B ⧸ q)).comp
((Ideal.Quotient.mk q).comp φ) ∧
ψ.Finite,
Ideal.IsClosedPointAwayFrom a p,
(Ideal.quotientMap (I := p) q φ le_rfl).Finite ]
Tag 0GGC, a lemma
Tag 0GGC in the Stacks Project.
Rig.isRigPointLocalCondition_comap_of_isJacobsonRing_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/RelativeCriterion.lean, line 605.
Under a Jacobson reduction of the source, the inverse image of a rig-closed prime along an adic topologically finite type morphism is rig-closed.
public theorem isRigPointLocalCondition_comap_of_isJacobsonRing_quotient
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hadic : RingHom.IsAdic φ)
(hft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(q : Ideal B) [q.IsPrime]
(hq : Ideal.IsRigPointLocalCondition q)
(hJacobson : ∃ I : Ideal A,
TopologicalRing.IsIdealOfDefinition I ∧ IsJacobsonRing (A ⧸ I)) :
Ideal.IsRigPointLocalCondition (q.comap φ)
Tag 0GGD, a lemma
Tag 0GGD in the Stacks Project.
Rig.rigPoint_lifts_iff_maximalIdeal_mem_specialFibre_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 94. The attribute's comment: “lifting criterion”.
A rig-closed prime lifts along a flat adic map of topologically finite type if and only if the closed point of its quotient is in the image on special fibres.
public theorem rigPoint_lifts_iff_maximalIdeal_mem_specialFibre_image
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hadic : RingHom.IsAdic φ)
(hft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(hflat : φ.Flat)
(p : Ideal A) [p.IsPrime]
(hp : Ideal.IsClosedPointAwayFrom
(topologicalNilradical A) p) :
( (∃ hlocal : IsLocalRing (A ⧸ p),
letI : IsLocalRing (A ⧸ p) := hlocal
∃ r : Ideal B, r.IsPrime ∧
topologicalNilradical B ≤ r ∧
r.comap φ = (IsLocalRing.maximalIdeal (A ⧸ p)).comap
(Ideal.Quotient.mk p)) ↔
(∃ q : Ideal B, ∃ hqprime : q.IsPrime,
letI : q.IsPrime := hqprime
Ideal.IsClosedPointAwayFrom
(topologicalNilradical B) q ∧ q.comap φ = p) )
Rig.rigPoint_residueFieldMap_finite_of_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 311. The attribute's comment: “relative residue-field finiteness”.
At a rig-closed lift, the induced map from the reduction of
Ato the residue field ofB / qis finite.
public theorem rigPoint_residueFieldMap_finite_of_lift
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hadic : RingHom.IsAdic φ)
(hft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(p : Ideal A) [p.IsPrime]
(hp : Ideal.IsClosedPointAwayFrom
(topologicalNilradical A) p)
(q : Ideal B) [q.IsPrime]
(hq : Ideal.IsClosedPointAwayFrom
(topologicalNilradical B) q)
(hqp : q.comap φ = p) :
∃ hlocal : IsLocalRing (B ⧸ q),
letI : IsLocalRing (B ⧸ q) := hlocal
∃ ψ : (A ⧸ topologicalNilradical A) →+*
IsLocalRing.ResidueField (B ⧸ q),
ψ.comp (Ideal.Quotient.mk (topologicalNilradical A)) =
(IsLocalRing.residue (B ⧸ q)).comp
((Ideal.Quotient.mk q).comp φ) ∧ ψ.Finite
Rig.rigPoint_quotientMap_finite_of_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 341. The attribute's comment: “relative quotient finiteness”.
At a rig-closed lift, the induced map on the quotients by the two primes is finite.
public theorem rigPoint_quotientMap_finite_of_lift
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hadic : RingHom.IsAdic φ)
(hft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(p : Ideal A) [p.IsPrime]
(hp : Ideal.IsClosedPointAwayFrom
(topologicalNilradical A) p)
(q : Ideal B) [q.IsPrime]
(hq : Ideal.IsClosedPointAwayFrom
(topologicalNilradical B) q)
(hqp : q.comap φ = p) :
(Ideal.quotientMap (I := p) q φ (by simpa only [← hqp] using le_rfl)).Finite
Tag 0GGE, a definition
Tag 0GGE in the Stacks Project.
Rig.exists_completedAway_algEquiv_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/CompletedPrincipalLocalization.lean, line 74. The attribute's comment: “independence of the ideal of definition”.
The completed principal localization is independent of the ideal of definition used to form it: for ideals of definition
IandJtheI-adic andJ-adic completions ofA[1/f]are isomorphic asA-algebras, compatibly with the maps fromA[1/f].
public theorem exists_completedAway_algEquiv_of {I J : Ideal A}
(hI : TopologicalRing.IsIdealOfDefinition I)
(hJ : TopologicalRing.IsIdealOfDefinition J) (f : A) :
∃ e : CompletedAway I f ≃ₐ[A] CompletedAway J f, ∀ x : Localization.Away f,
e (AdicCompletion.of _ (Localization.Away f) x) =
AdicCompletion.of _ (Localization.Away f) x
Declarations registered for the tag:
CompletedAwayregistered withadd_to_stacksin StacksFrontier/RingTheory/Rig/CompletedPrincipalLocalization.lean, line 39 (StacksFrontier): “the completed principal localization, along a chosen ideal”.
Tag 0GGF, a lemma
Tag 0GGF in the Stacks Project.
Rig.tensorProduct_equiv_extendedIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 653. The attribute's comment: “tensor-product description”.
Extension of scalars of
pto the completed principal localization is canonically its extended ideal.
public theorem tensorProduct_equiv_extendedIdeal
(I p : Ideal A) (f : A) [IsNoetherianRing A] :
∃ e : (CompletedAway I f ⊗[A] p) ≃ₗ[CompletedAway I f] extendedIdeal I p f,
∀ (x : p) (c : CompletedAway I f),
((e (c ⊗ₜ[A] x) : extendedIdeal I p f) : CompletedAway I f) =
algebraMap A (CompletedAway I f) (x : A) * c
Rig.adicCompletion_localizedIdeal_equiv_extendedIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 667. The attribute's comment: “completion description”.
Completing the localized ideal
p A[1/f]gives its extension to the completed principal localization, compatibly with the canonical maps.
public theorem adicCompletion_localizedIdeal_equiv_extendedIdeal
(I p : Ideal A) (f : A) [IsNoetherianRing A] :
let A_f := Localization.Away f
let J := I.map (algebraMap A A_f)
let p_f := p.map (algebraMap A A_f)
∃ e : AdicCompletion J p_f ≃ₗ[A_f] extendedIdeal I p f,
∀ x : p_f,
((e (AdicCompletion.of J p_f x) : extendedIdeal I p f) : CompletedAway I f) =
algebraMap A_f (CompletedAway I f) (x : A_f)
Rig.extendedIdeal_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 707. The attribute's comment: “primality”.
The extension of
pto the completed principal localization is prime.
public theorem extendedIdeal_isPrime
(I p : Ideal A) (f : A) [IsNoetherianRing A] [IsAdicComplete I A]
(hp : p.IsPrime)
(hf : IsUnit (Ideal.Quotient.mk p f)) :
(extendedIdeal I p f).IsPrime
Rig.quotient_extendedIdeal_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 721. The attribute's comment: “quotient”.
Quotienting the completed principal localization by the extended prime canonically recovers
A / p.
public theorem quotient_extendedIdeal_equiv
(I p : Ideal A) (f : A) [IsNoetherianRing A] [IsAdicComplete I A]
(hf : IsUnit (Ideal.Quotient.mk p f)) :
∃ e : (A ⧸ p) ≃+* (CompletedAway I f ⧸ extendedIdeal I p f),
∀ a : A,
e (Ideal.Quotient.mk p a) =
Ideal.Quotient.mk (extendedIdeal I p f)
(algebraMap A (CompletedAway I f) a)
Declarations registered for the tag:
Ideal.qoutMapEquivTensorQoutregistered withadd_to_stacksin StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 748 (StacksFrontier): “tensor-product description of the quotient”.Ideal.map_mapregistered withadd_to_stacksin StacksFrontier/RingTheory/Rig/ClosedPoint/LiftingAndCompletedAway.lean, line 753 (StacksFrontier): “transitivity of ideal extension”.
Tag 0GGG, a lemma
Tag 0GGG in the Stacks Project.
Rig.exists_isClosedPointAwayFrom_completedAway_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/Regular.lean, line 1389.
After a suitable completed principal localization, the prime below a rig-closed point is rig-closed as well.
public theorem exists_isClosedPointAwayFrom_completedAway_comap
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hadic : RingHom.IsAdic φ)
(hft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(q : Ideal B) [q.IsPrime]
(hq : Ideal.IsClosedPointAwayFrom
(topologicalNilradical B) q) :
let I := hadic.choose
let J := I.map φ
∃ f : A,
IsUnit (Ideal.Quotient.mk q (φ f)) ∧
(let A_f := CompletedAway I f
let B_f := CompletedAway J (φ f)
let ψ : A_f →+* B_f := RingHom.completedAwayMap φ I f
let I_f := I.map (algebraMap A (Localization.Away f))
let J_f := J.map (algebraMap B (Localization.Away (φ f)))
let I_hat := I_f.map (algebraMap (Localization.Away f) A_f)
let J_hat := J_f.map (algebraMap (Localization.Away (φ f)) B_f)
let q' := extendedIdeal J q (φ f)
let p' := q'.comap ψ
ψ.comp (algebraMap A A_f) = (algebraMap B B_f).comp φ ∧
(∃ hqprime : q'.IsPrime,
letI : q'.IsPrime := hqprime
∃ hpprime : p'.IsPrime,
letI : p'.IsPrime := hpprime
Ideal.IsClosedPointAwayFrom J_hat q' ∧
Ideal.IsClosedPointAwayFrom I_hat p'))
Tag 0GGH, a lemma
Tag 0GGH in the Stacks Project.
Rig.adicCompletionMap_localRingHom_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/RestrictedPowerSeries.lean, line 453.
Let
Abe a Noetherian adic topological ring, complete for an ideal of definitionI, and letqbe a prime of the restricted power series ringA{x_σ}in finitely many variables. Ifqis rig-closed and so is its contraction toA, then the canonical map from the local ring of the polynomial ring atq ∩ A[x_σ]to the local ring ofA{x_σ}atqinduces a bijection on the completions at the maximal ideals.
public theorem adicCompletionMap_localRingHom_bijective
{A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsNoetherianRing A] (I : Ideal A) (hI : IsAdic I) [IsAdicComplete I A]
(σ : Type*) [Finite σ]
(q : Ideal (RestrictedPowerSeries I σ)) [q.IsPrime]
(hq : Ideal.IsClosedPointAwayFrom (I.map (coefficientRingHom I σ)) q)
(hp : Ideal.IsClosedPointAwayFrom I (q.comap (coefficientRingHom I σ))) :
let f := polynomialRingHom I σ
let q' := q.comap f
let l := Localization.localRingHom q' q f rfl
Function.Bijective
(adicCompletionMap l
(IsLocalRing.maximalIdeal (Localization.AtPrime q'))
(IsLocalRing.maximalIdeal (Localization.AtPrime q))
(IsLocalRing.map_maximalIdeal_le l))
Tag 0GGI, a lemma
Tag 0GGI in the Stacks Project.
Rig.map_comap_eq_map_of_rigPoint_of_etale_quotient, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/EtaleReduction.lean, line 105.
Stacks 0GGI. Let
φ : A → Bbe an adic morphism of Noetherian weakly admissible topological rings which is topologically of finite type and flat and whose reduction modulo an ideal of definitionI ⊆ Ais étale. Ifq ⊆ Bis a rig-closed prime whose contraction toAis rig-closed as well, then the extension of that contraction to the local ring ofBatqis the extension ofqitself.
public lemma map_comap_eq_map_of_rigPoint_of_etale_quotient
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(_hA : TopologicalRing.IsWeaklyAdmissible A)
(hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hadic : RingHom.IsAdic φ)
(_hft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(hflat : φ.Flat)
(I : Ideal A) (hI : TopologicalRing.IsIdealOfDefinition I)
(hetale : (Ideal.quotientMap (I.map φ) φ Ideal.le_comap_map).Etale)
(q : Ideal B) [q.IsPrime]
(_hq : Ideal.IsRigPointLocalCondition q)
(hp : Ideal.IsRigPointLocalCondition (q.comap φ)) :
(q.comap φ).map ((algebraMap B (Localization.AtPrime q)).comp φ) =
q.map (algebraMap B (Localization.AtPrime q))
Tag 0GGJ, a lemma
Tag 0GGJ in the Stacks Project.
Rig.restrictedPowerSeriesBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/Regular.lean, line 400. The attribute's comment: “regular_map”.
Base change of a restricted power series ring by a rig-closed quotient is canonically the restricted power series ring over that quotient.
public noncomputable def restrictedPowerSeriesBaseChangeEquiv
{A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsNoetherianRing A]
(_hA : TopologicalRing.IsAdic A)
(I : Ideal A) (_hI : TopologicalRing.IsIdealOfDefinition I)
(p : Ideal A) [p.IsPrime]
(_hp : Ideal.IsRigPointLocalCondition p)
(n : ℕ) (_hn : 1 ≤ n) :
letI : Algebra (A ⧸ p)
(RestrictedPowerSeries I (Fin n) ⊗[A] (A ⧸ p)) :=
Algebra.TensorProduct.rightAlgebra
(RestrictedPowerSeries I (Fin n) ⊗[A] (A ⧸ p)) ≃ₐ[A ⧸ p]
RestrictedPowerSeries (I.map (Ideal.Quotient.mk p)) (Fin n)
Rig.restrictedPowerSeriesBaseChangeEquiv_coefficientProjection, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/Regular.lean, line 428. The attribute's comment: “regular_map”.
At every finite level, the base-change identification reduces a series coefficientwise modulo
p. The polynomialgis any lift of that level's coefficient polynomial, so the equation also asserts independence of lifts.
public lemma restrictedPowerSeriesBaseChangeEquiv_coefficientProjection
{A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsNoetherianRing A]
(hA : TopologicalRing.IsAdic A)
(I : Ideal A) (hI : TopologicalRing.IsIdealOfDefinition I)
(p : Ideal A) [p.IsPrime]
(hp : Ideal.IsRigPointLocalCondition p)
(n : ℕ) (hn : 1 ≤ n) (k : ℕ)
(f : RestrictedPowerSeries I (Fin n))
(g : MvPolynomial (Fin n) A)
(hg : RestrictedPowerSeries.coefficientProjection I (Fin n) k f =
MvPolynomial.map (Ideal.Quotient.mk (I ^ k)) g) :
letI : Algebra (A ⧸ p)
(RestrictedPowerSeries I (Fin n) ⊗[A] (A ⧸ p)) :=
Algebra.TensorProduct.rightAlgebra
RestrictedPowerSeries.coefficientProjection
(I.map (Ideal.Quotient.mk p)) (Fin n) k
(restrictedPowerSeriesBaseChangeEquiv hA I hI p hp n hn
((Algebra.TensorProduct.includeLeftRingHom :
RestrictedPowerSeries I (Fin n) →+*
(RestrictedPowerSeries I (Fin n) ⊗[A] (A ⧸ p))) f)) =
MvPolynomial.map (Ideal.Quotient.mk
((I.map (Ideal.Quotient.mk p)) ^ k))
(MvPolynomial.map (Ideal.Quotient.mk p) g)
Rig.isRegularRingHom_baseChange_of_rigPoint, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/Regular.lean, line 510. The attribute's comment: “regular_map”.
The canonical map from the rig-closed quotient to the base-changed restricted power series ring is regular.
public lemma isRegularRingHom_baseChange_of_rigPoint
{A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsNoetherianRing A]
(_hA : TopologicalRing.IsAdic A)
(I : Ideal A) (_hI : TopologicalRing.IsIdealOfDefinition I)
(p : Ideal A) [p.IsPrime]
(_hp : Ideal.IsRigPointLocalCondition p)
(n : ℕ) (_hn : 1 ≤ n) :
letI : Algebra (A ⧸ p)
(RestrictedPowerSeries I (Fin n) ⊗[A] (A ⧸ p)) :=
Algebra.TensorProduct.rightAlgebra
IsRegularRingHom (algebraMap (A ⧸ p)
(RestrictedPowerSeries I (Fin n) ⊗[A] (A ⧸ p)))
Rig.isGeometricallyRegular_fibre, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/Regular.lean, line 593. The attribute's comment: “geometrically_regular_fibre”.
The fibre of a restricted power series algebra at a rig-closed prime is geometrically regular over the residue field.
public lemma isGeometricallyRegular_fibre
{A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsNoetherianRing A]
(_hA : TopologicalRing.IsAdic A)
(I : Ideal A) (_hI : IsAdic I)
(p : Ideal A) [p.IsPrime]
(_hp : Ideal.IsRigPointLocalCondition p)
(n : ℕ) (_hn : 0 < n) :
letI : Algebra p.ResidueField
(RestrictedPowerSeries I (Fin n) ⊗[A]
p.ResidueField) := Algebra.TensorProduct.rightAlgebra
Algebra.IsGeometricallyRegular p.ResidueField
(RestrictedPowerSeries I (Fin n) ⊗[A]
p.ResidueField)
Sources
Section88.15 Rig-flat homomorphisms#
Section 88.15 of the Stacks Project, Tag 0GGK. 10 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GGL, a lemma
Tag 0GGL in the Stacks Project.
Rig.naivelyRigFlat_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Flat.lean, line 333.
For an adic morphism of weakly admissible adic topological rings with finitely generated ideals of definition, flatness after localization may be tested on topologically nilpotent elements of either ring, on all primes away from an ideal of definition, or on rig-closed primes.
public theorem naivelyRigFlat_tfae
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
(phi : A →+* B) (_hphi_continuous : Continuous phi)
(_hA_weaklyAdmissible : TopologicalRing.IsWeaklyAdmissible A)
(_hB_weaklyAdmissible : TopologicalRing.IsWeaklyAdmissible B)
(_hA_adicStar : ∃ I : Ideal A, IsAdic I ∧ I.FG)
(_hB_adicStar : ∃ J : Ideal B, IsAdic J ∧ J.FG)
(_hphi_adic : _root_.RingHom.IsAdic phi) :
List.TFAE
[ ∀ f : A, IsTopologicallyNilpotent f →
_root_.RingHom.Flat
((algebraMap B (Localization.Away (phi f))).comp phi),
∀ g : B, IsTopologicallyNilpotent g →
_root_.RingHom.Flat
((algebraMap B (Localization.Away g)).comp phi),
∀ (q : Ideal B) [q.IsPrime],
(∃ J : Ideal B, TopologicalRing.IsIdealOfDefinition J ∧ ¬ J ≤ q) →
_root_.RingHom.Flat
((algebraMap B (Localization.AtPrime q)).comp phi),
∀ (q : Ideal B) [q.IsPrime],
(∃ J : Ideal B, TopologicalRing.IsIdealOfDefinition J ∧
Rig.Ideal.IsMaximalAmongPrimesAvoiding J q) →
_root_.RingHom.Flat
((algebraMap B (Localization.AtPrime q)).comp phi) ]
Tag 0GGM, a definition
Tag 0GGM in the Stacks Project.
Rig.RingHom.IsNaivelyRigFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Flat.lean, line 116.
A ring homomorphism
φ : A →+* Bis naively rig-flat if it is adic, topologically of finite type, andB[1 / φ(f)]is flat overAfor every topologically nilpotentf : A.
public abbrev IsNaivelyRigFlat {A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [TopologicalSpace B] (φ : A →+* B) : Prop
Tag 0GGN, an example
Tag 0GGN in the Stacks Project.
Rig.exists_isNaivelyRigFlat_not_isNaivelyRigFlat_completedAwayMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatRecompletionExample.lean, line 594.
Stacks 0GGN. Naive rig-flatness is not preserved by passing to completed principal localizations: there is a two-dimensional Noetherian local domain
A, complete for a principal ideal(a), andf ∈ 𝔪 ∖ (a), such that the reductionBof the completed localizationC = (A_f)^∧receives a naively rig-flat adic mapφ : A → Bof topological finite type — presented by the restricted power series ringA{x}withx ↦ 1/f— while the induced mapψof completed principal localizations ofφatfis not naively rig-flat.
public theorem exists_isNaivelyRigFlat_not_isNaivelyRigFlat_completedAwayMap :
∃ (A : Type u) (_ : CommRing A) (_ : IsDomain A) (_ : IsLocalRing A)
(_ : IsNoetherianRing A) (a f : A),
ringKrullDim A = 2 ∧
IsAdicComplete (Ideal.span {a}) A ∧
f ∈ IsLocalRing.maximalIdeal A ∧
f ∉ Ideal.span {a} ∧
(let I : Ideal A := Ideal.span {a}
let Af := Localization.Away f
let If : Ideal Af := I.map (algebraMap A Af)
let C := AdicCompletion If Af
let B := C ⧸ nilradical C
let φ : A →+* B := (Ideal.Quotient.mk (nilradical C)).comp (algebraMap A C)
letI : TopologicalSpace A := I.adicTopology
letI : TopologicalSpace B := (I.map φ).adicTopology
(¬ IsReduced (Localization.Away (algebraMap A C a))) ∧
(∃ θ : RestrictedPowerSeries I (Fin 1) →+* B,
Function.Surjective θ ∧
(∀ x : A,
θ (RestrictedPowerSeries.polynomialRingHom I (Fin 1) (MvPolynomial.C x)) =
φ x) ∧
θ (RestrictedPowerSeries.polynomialRingHom I (Fin 1) (MvPolynomial.X 0)) =
Ideal.Quotient.mk (nilradical C)
(algebraMap Af C (IsLocalization.Away.invSelf (S := Af) f))) ∧
(∀ q : Ideal B, q.IsPrime → φ a ∉ q → q.comap φ = ⊥) ∧
RingHom.IsNaivelyRigFlat φ ∧
(let B_f := Localization.Away (φ f)
let J_f := (I.map φ).map (algebraMap B B_f)
let I_hat := If.map (algebraMap Af C)
let J_hat := J_f.map (algebraMap B_f (AdicCompletion J_f B_f))
letI : TopologicalSpace C := I_hat.adicTopology
letI : TopologicalSpace (AdicCompletion J_f B_f) := J_hat.adicTopology
let ψ := RingHom.completedAwayMap φ I f
(∃ e : AdicCompletion J_f B_f ≃+* B,
(∀ b : B, e ((algebraMap B_f (AdicCompletion J_f B_f))
(algebraMap B B_f b)) = b) ∧
(∀ c : C, e (ψ c) = Ideal.Quotient.mk (nilradical C) c)) ∧
let a_hat : C := algebraMap Af C (algebraMap A Af a)
(¬ _root_.RingHom.Flat (IsLocalization.Away.map (Localization.Away a_hat)
(Localization.Away (ψ a_hat)) ψ a_hat)) ∧
(¬ RingHom.IsNaivelyRigFlat ψ)))
Tag 0GGP, a definition
Tag 0GGP in the Stacks Project.
Rig.RingHom.IsRigFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/Flat.lean, line 182.
A ring homomorphism is rig-flat if it is adic and topologically of finite type, and all the induced maps between completed principal localizations are naively rig-flat.
public abbrev IsRigFlat {A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [TopologicalSpace B] (φ : A →+* B) : Prop
Tag 0GGQ, a lemma
Tag 0GGQ in the Stacks Project.
Rig.RingHom.isRigFlat_of_isNaivelyRigFlat_of_isJacobsonRing_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatJacobson.lean, line 490.
Stacks 0GGQ. A naively rig-flat arrow of
WAdm^Noethwhose source has a Jacobson reduction modulo an ideal of definition is rig-flat.
public theorem isRigFlat_of_isNaivelyRigFlat_of_isJacobsonRing_quotient
{A B : Type*} [CommRing A] [CommRing B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A) (_hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (hφ : Continuous φ)
(hJacobson : ∃ I : Ideal A,
TopologicalRing.IsIdealOfDefinition I ∧ IsJacobsonRing (A ⧸ I))
(hflat : IsNaivelyRigFlat φ) :
IsRigFlat φ
Tag 0GGR, a lemma
Tag 0GGR in the Stacks Project.
AlgebraicGeometry.FormalSpace.isRigFlat_completedTensorProduct_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlatBaseChangeAdicFiniteType.lean, line 453.
Stacks 0GGR. Let
A → BandA → Cbe arrows ofWAdm^Noeth. IfA → Bis rig-flat andA → Cis adic and topologically of finite type, thenC → B ⊗̂_A Cis rig-flat.The naive form is
AlgebraicGeometry.FormalSpace.naiveRigFlatBaseChangeByAdicFiniteType, the second to fifth paragraphs of the proof; the first paragraph upgrades it to rig-flatness throughAlgebraicGeometry.FormalSpace.rigFlat_completedTensorProduct_of_naive.
public theorem isRigFlat_completedTensorProduct_baseChange
{A B C : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[IsLinearTopology B B] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
[IsLinearTopology C C] [Algebra A B] [Algebra A C] [IsNoetherianRing A]
[IsNoetherianRing B] [IsNoetherianRing C]
(h₀ : TopologicalRing.IsAdic A) (h₁ : TopologicalRing.IsAdic B)
(h₂ : TopologicalRing.IsAdic C) (hc₁ : Continuous (algebraMap A B))
(hc₂ : Continuous (algebraMap A C)) (hP : Rig.RingHom.IsRigFlat (algebraMap A B))
(hQ : _root_.RingHom.IsAdic (algebraMap A C) ∧
TopologicalRing.IsTopologicallyOfFiniteType (algebraMap A C)) :
Rig.RingHom.IsRigFlat (algebraMap C
(CompletedTensorProduct (R := A) (M := B) (N := C)))
Rig.flat_atPrime_completedTensorProduct_restrictedPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/ClosedPoint/CompletedTensorProductFlat.lean, line 269. The attribute's comment: “the last step only: for C the restricted power series ring A{σ} on a finite set of variables rather than an arbitrary adic A → C of topologically finite type, and flatness of C → B ⊗̂_A C localized at one rig-closed prime whose contraction to A is also rig-closed, rather than rig-flatness of C → B ⊗̂_A C”.
Flatness of
A{σ} → B ⊗̂[A] A{σ}at a rig-closed point. LetA → Bbe a continuous adic and naively rig-flat homomorphism of Noetherian adic topological rings, complete along an ideal of definitionIofAand its extension toB, and letC = A{σ}be the restricted power series ring on a finite set of variables. Ifqis a rig-closed prime of the identificationB{σ}ofB ⊗̂[A] Cwhose contraction toAis rig-closed, thenC → B ⊗̂[A] Cis flat after localizing at the primeqcuts out.
public theorem flat_atPrime_completedTensorProduct_restrictedPowerSeries
{A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A] [IsNoetherianRing A]
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B] [IsNoetherianRing B]
(I : Ideal A) (hI : _root_.IsAdic I) [IsAdicComplete I A]
(hJ : _root_.IsAdic (I.map (algebraMap A B)))
[IsAdicComplete (I.map (algebraMap A B)) B]
(σ : Type u) [Finite σ]
(hcont : Continuous (algebraMap A B))
(hflat : RingHom.IsNaivelyRigFlat (algebraMap A B))
(q : Ideal (RestrictedPowerSeries (I.map (algebraMap A B)) σ)) [q.IsPrime]
(hq : Ideal.IsClosedPointAwayFrom
((I.map (algebraMap A B)).map (coefficientRingHom (I.map (algebraMap A B)) σ)) q)
(hpA : Ideal.IsClosedPointAwayFrom I
((q.comap (TopologicalRing.restrictedPowerSeriesMap (B := B) I σ)).comap
(coefficientRingHom I σ))) :
letI : IsLinearTopology (RestrictedPowerSeries I σ) (RestrictedPowerSeries I σ) :=
RestrictedPowerSeries.isLinearTopology_restrictedPowerSeries I
(Ideal.fg_of_isNoetherianRing I) σ
letI : TopologicalSpace (B ⊗[A] RestrictedPowerSeries I σ) :=
tensorProductTopology (R := A) (M := B) (N := RestrictedPowerSeries I σ)
letI : UniformSpace (B ⊗[A] RestrictedPowerSeries I σ) :=
tensorProductUniformSpace (R := A) (M := B) (N := RestrictedPowerSeries I σ)
letI : IsTopologicalRing (B ⊗[A] RestrictedPowerSeries I σ) :=
tensorProduct_isTopologicalRing (R := A) (A := B) (B := RestrictedPowerSeries I σ)
letI : IsUniformAddGroup (B ⊗[A] RestrictedPowerSeries I σ) :=
tensorProduct_isUniformAddGroup (R := A) (M := B) (N := RestrictedPowerSeries I σ)
let e := completedTensorProductRestrictedEquiv I (Ideal.fg_of_isNoetherianRing I) σ hJ
let ι : RestrictedPowerSeries I σ →+*
CompletedTensorProduct (R := A) (M := B) (N := RestrictedPowerSeries I σ) :=
(UniformSpace.Completion.coeRingHom).comp
(Algebra.TensorProduct.includeRight (R := A) (A := B)
(B := RestrictedPowerSeries I σ)).toRingHom
letI : (q.comap e.toRingHom).IsPrime := Ideal.comap_isPrime _ _
_root_.RingHom.Flat
((algebraMap (CompletedTensorProduct (R := A) (M := B) (N := RestrictedPowerSeries I σ))
(Localization.AtPrime (q.comap e.toRingHom))).comp ι)
Tag 0GGS, a lemma
Tag 0GGS in the Stacks Project.
Rig.isRigFlat_of_flat_etale_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatEtaleLocalization.lean, line 1241.
Stacks 0GGS. Rig-flatness ascends across the flat horizontal maps of a commutative square of adic homomorphisms of topological finite type between Noetherian weakly admissible rings whose lower map is étale modulo an ideal of definition: if
φis rig-flat, so isφ'.
public theorem isRigFlat_of_flat_etale_square
{A A' B B' : Type u}
[CommRing A] [CommRing A'] [CommRing B] [CommRing B']
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
[IsNoetherianRing A] [IsNoetherianRing A']
[IsNoetherianRing B] [IsNoetherianRing B']
(hA : TopologicalRing.IsWeaklyAdmissible A)
(_hA' : TopologicalRing.IsWeaklyAdmissible A')
(_hB : TopologicalRing.IsWeaklyAdmissible B)
(_hB' : TopologicalRing.IsWeaklyAdmissible B')
(φ : A →+* B) (φ' : A' →+* B')
(α : A →+* A') (β : B →+* B')
(hsquare : φ'.comp α = β.comp φ)
(hφ_cont : Continuous φ) (_hφ'_cont : Continuous φ')
(hα_cont : Continuous α) (_hβ_cont : Continuous β)
(hφ_adic : _root_.RingHom.IsAdic φ)
(hφ'_adic : _root_.RingHom.IsAdic φ')
(hα_adic : _root_.RingHom.IsAdic α)
(_hβ_adic : _root_.RingHom.IsAdic β)
(hφ_ft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(hφ'_ft : TopologicalRing.IsTopologicallyOfFiniteType φ')
(hα_ft : TopologicalRing.IsTopologicallyOfFiniteType α)
(hβ_ft : TopologicalRing.IsTopologicallyOfFiniteType β)
(hα_flat : α.Flat) (hβ_flat : β.Flat)
(I : Ideal A) (hI : TopologicalRing.IsIdealOfDefinition I)
(hφ_rigFlat : RingHom.IsRigFlat φ)
(hα_etale : (Ideal.quotientMap (I.map α) α Ideal.le_comap_map).Etale) :
RingHom.IsRigFlat φ'
Tag 0GGT, a lemma
Tag 0GGT in the Stacks Project.
Rig.RingHom.isRigFlat_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatDescent.lean, line 742.
Stacks 0GGT. Rig-flatness descends in a commutative square of adic homomorphisms of topological finite type between Noetherian weakly admissible rings whose lower horizontal map is flat and whose upper horizontal map is faithfully flat: if
φ'is rig-flat, so isφ.
public theorem isRigFlat_of_faithfullyFlat
{A A' B B' : Type*} [CommRing A] [CommRing A'] [CommRing B] [CommRing B']
[TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
[TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
[IsNoetherianRing A] [IsNoetherianRing A'] [IsNoetherianRing B] [IsNoetherianRing B']
(_hA : TopologicalRing.IsWeaklyAdmissible A) (_hA' : TopologicalRing.IsWeaklyAdmissible A')
(_hB : TopologicalRing.IsWeaklyAdmissible B) (_hB' : TopologicalRing.IsWeaklyAdmissible B')
(φ : A →+* B) (α : A →+* A') (β : B →+* B') (φ' : A' →+* B')
(hcomm : β.comp φ = φ'.comp α)
(_hφ_cont : Continuous φ) (_hα_cont : Continuous α)
(_hβ_cont : Continuous β) (_hφ'_cont : Continuous φ')
(hφ_adic : _root_.RingHom.IsAdic φ) (hα_adic : _root_.RingHom.IsAdic α)
(_hβ_adic : _root_.RingHom.IsAdic β) (hφ'_adic : _root_.RingHom.IsAdic φ')
(hφ_ft : TopologicalRing.IsTopologicallyOfFiniteType φ)
(_hα_ft : TopologicalRing.IsTopologicallyOfFiniteType α)
(_hβ_ft : TopologicalRing.IsTopologicallyOfFiniteType β)
(_hφ'_ft : TopologicalRing.IsTopologicallyOfFiniteType φ')
(hα_flat : α.Flat) (hβ_ff : β.FaithfullyFlat)
(hφ'_rigFlat : Rig.RingHom.IsRigFlat φ') :
Rig.RingHom.IsRigFlat φ
Tag 0GGU, a lemma
Tag 0GGU in the Stacks Project.
Rig.rigFlat_isLocalNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatIsLocal.lean, line 750.
Rig-flatness is a local property of arrows of
WAdm^Noeth(Stacks 0GGU): it ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets.
theorem rigFlat_isLocalNoetherian :
TopologicalRing.PropertyIsLocalNoetherian
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsRigFlat φ)
Rig.rigFlat_isLocalNoetherian', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatIsLocalRefined.lean, line 162.
Rig-flatness is a local property of arrows of
WAdm^Noeth: it is independent of the presentations of its source and target, ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets.
theorem rigFlat_isLocalNoetherian' :
TopologicalRing.PropertyIsLocalNoetherian'
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsRigFlat φ)
Tag 0GGV, a lemma
Tag 0GGV in the Stacks Project.
Rig.rigFlat_isStableUnderCompositionNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/FlatStableUnderComposition.lean, line 214.
Rig-flatness is stable under composition on
WAdm^Noeth(Stacks 0GGV). Adicness and topological finite type of the composite are Stacks 0GBZ; naive rig-flatness of the induced map of completed principal localizations isRig.RingHom.isNaivelyRigFlat_compapplied to the two factors, transported along the functorialityRig.completedAwayMap_comp.
theorem rigFlat_isStableUnderCompositionNoetherian :
TopologicalRing.PropertyIsStableUnderCompositionNoetherian
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsRigFlat φ)
Sources
Section88.16 Rig-flat morphisms#
Section 88.16 of the Stacks Project, Tag 0GGW. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GGX, a definition
Tag 0GGX in the Stacks Project.
AlgebraicGeometry.FormalSpace.IsRigFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlat.lean, line 62.
Stacks 0GGX. A morphism of formal algebraic spaces over
Sis rig-flat when every morphism between affine, representable, étale charts of its source and target is induced by a rig-flat continuous homomorphism of adic Noetherian topological rings.
abbrev IsRigFlat (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
{X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop
Tag 0GGY, a lemma
Tag 0GGY in the Stacks Project.
AlgebraicGeometry.FormalSpace.hasRigFlatSourceCovering_of_hasRigFlatTargetCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlatCriteria.lean, line 157. The attribute's comment: “(3) ⟹ (4)”.
Stacks 0GGY, (3) ⟹ (4). A target covering witnessing rig-flatness on charts yields a source covering witnessing it: the two coverings of condition (3) compose into one covering of the source, and each of its members factors through the chart of the target covering it lies over.
theorem hasRigFlatSourceCovering_of_hasRigFlatTargetCovering
{X Y : FppfSheaf B S hS} (f : X ⟶ Y) (h : HasRigFlatTargetCovering B S hS f) :
HasRigFlatSourceCovering B S hS f
AlgebraicGeometry.FormalSpace.isRigFlat_tfae_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlatCriteriaLocallyNoetherian.lean, line 98.
Stacks 0GGY. For a morphism
f : X ⟶ Yof locally Noetherian formal algebraic spaces overS, the following are equivalent:fis rig-flat (Definition 0GGX); every commutative square whose verticals are affine formal algebraic spaces representable étale overXandYcarries a rig-flat arrow ofWAdm^Noethon its top side; there are an affine étale covering ofYand affine étale coverings of the fibre products of its members withXwhose members map to the corresponding chart ofYby rig-flat maps ofWAdm^Noeth; there is an affine étale covering ofXwhose members factor through affine formal algebraic spaces representable étale overYby rig-flat maps ofWAdm^Noeth.
theorem isRigFlat_tfae_of_isLocallyNoetherian {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
(hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y) :
List.TFAE
[IsRigFlat B S hS f,
HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic
(fun {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
[CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂] (φ : R₁ →+* R₂) ↦
Rig.RingHom.IsRigFlat φ) f,
HasRigFlatTargetCovering B S hS f,
HasRigFlatSourceCovering B S hS f]
Tag 0GGZ, a lemma
Tag 0GGZ in the Stacks Project.
AlgebraicGeometry.FormalSpace.isRigFlat_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlatPullback.lean, line 86.
Stacks 0GGZ. Let
f : X ⟶ Yandg : Z ⟶ Ybe morphisms of locally Noetherian formal algebraic spaces overS. Iffis rig-flat andgis locally of finite type, then the base changeX ×_Y Z ⟶ Zis rig-flat.
theorem isRigFlat_pullback_snd {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
(hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
(hZ : IsLocallyNoetherian B S hS Z) (hf : IsRigFlat B S hS f)
(hg : IsLocallyOfFiniteType B S hS g) :
IsRigFlat B S hS (pullback.snd f g)
Tag 0GH0, a lemma
Tag 0GH0 in the Stacks Project.
AlgebraicGeometry.FormalSpace.isRigFlat_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlatComposition.lean, line 312. The attribute's comment: “the composite is rig-flat, with the geometric half of Stacks 0GBK as a hypothesis”.
Stacks 0GH0. A composite of rig-flat morphisms of locally Noetherian formal algebraic spaces is rig-flat: if
f : X ⟶ Yandg : Y ⟶ Zare rig-flat, then so isg ∘ f.
theorem isRigFlat_comp (htransfer : TransfersCompositionOnAffineEtaleDiagrams B S hS)
(f : X ⟶ Y) (g : Y ⟶ Z) (hf : IsRigFlat B S hS f) (hg : IsRigFlat B S hS g) :
IsRigFlat B S hS (f ≫ g)
AlgebraicGeometry.FormalSpace.isRigFlat_comp_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlatCompositionLocallyNoetherian.lean, line 63.
Stacks 0GH0. Let
f : X ⟶ Yandg : Y ⟶ Zbe morphisms of locally Noetherian formal algebraic spaces overS. Iffandgare rig-flat, then so isg ∘ f.
theorem isRigFlat_comp_of_isLocallyNoetherian {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y)
(g : Y ⟶ Z) (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
(hZ : IsLocallyNoetherian B S hS Z) (hf : IsRigFlat B S hS f) (hg : IsRigFlat B S hS g) :
IsRigFlat B S hS (f ≫ g)
Sources
Section88.17 Rig-smooth homomorphisms#
Section 88.17 of the Stacks Project, Tag 0GCH. 7 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GCI, a lemma
Tag 0GCI in the Stacks Project.
Rig.isRigSmooth_iff_forall_idealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmooth.lean, line 186.
Stacks Project, Tag 0GCI. Rig-smoothness of a finite-type morphism of Noetherian weakly admissible rings does not depend on the ideal of definition of its source.
public theorem isRigSmooth_iff_forall_idealOfDefinition
{A : Type u} {B : Type v}
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hA : TopologicalRing.IsWeaklyAdmissible A) (_hB : TopologicalRing.IsWeaklyAdmissible B)
(φ : A →+* B) (_hφ : Continuous φ) (hft : FiniteTypeAdicAlgebraForEveryIdeal φ) :
(∃ (I : Ideal A) (hI : TopologicalRing.IsIdealOfDefinition I),
IsRigSmooth (adicFiniteTypeAlgebra φ hft I hI)) ↔
(∀ (I : Ideal A) (hI : TopologicalRing.IsIdealOfDefinition I),
IsRigSmooth (adicFiniteTypeAlgebra φ hft I hI))
Tag 0GCJ, a definition
Tag 0GCJ in the Stacks Project.
RingHom.IsRigSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmooth.lean, line 251.
Stacks Project, Tag 0GCJ. A continuous homomorphism of Noetherian adic topological rings is rig-smooth when it is adic of topologically finite type — condition (6) of Tag 0GBW — and makes its target rig-smooth over some ideal of definition of its source. By Tag 0GCI the choice of that ideal is immaterial.
public abbrev IsRigSmooth {A : Type u} {B : Type v}
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[IsNoetherianRing A]
[CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing B]
(φ : A →+* B) : Prop
Tag 0GCK, a lemma
Tag 0GCK in the Stacks Project.
Rig.rigSmooth_isLocalNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothLocality.lean, line 451.
Stacks 0GCK. Rig-smoothness is a local property of arrows of
WAdm^Noeth: it ascends along a completed étale localization diagram, descends along one whose target-side horizontal map is faithfully flat, and is preserved by finite products of targets.
public theorem rigSmooth_isLocalNoetherian :
TopologicalRing.PropertyIsLocalNoetherian.{u}
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsRigSmoothArrow φ)
Rig.rigSmooth_isLocalNoetherian', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothLocalityRefined.lean, line 124.
Stacks 0GCK. Rig-smoothness is a local property of arrows of
WAdm^Noeth: it is independent of the presentations of its source and target, ascends along a completed étale localization diagram, descends along one whose target-side horizontal map is faithfully flat, and is preserved by finite products of targets.
public theorem rigSmooth_isLocalNoetherian' :
TopologicalRing.PropertyIsLocalNoetherian'.{u}
(fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (φ : B →+* A) ↦
RingHom.IsRigSmoothArrow φ)
Tag 0GCL, a lemma
Tag 0GCL in the Stacks Project.
TopologicalRing.rigSmooth_completedTensorProduct_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothStability.lean, line 771.
Rig-smoothness (Tag 0GCJ) is stable under base change by adic morphisms (Tag 0GBR) in the sense of Remark 0GBG: if
B → Ais rig-smooth andB → Cis adic, both arrows ofWAdm^{Noeth}, then the completed tensor productA ⊗̂_B Cis again Noetherian adic and rig-smooth overC.
public theorem rigSmooth_completedTensorProduct_of_isAdic
{B A C : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[IsLinearTopology B B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsLinearTopology A A] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
[IsLinearTopology C C] [Algebra B A] [Algebra B C] [IsNoetherianRing B]
[IsNoetherianRing A] [IsNoetherianRing C]
(hB : TopologicalRing.IsAdic B) (hA : TopologicalRing.IsAdic A)
(hC : TopologicalRing.IsAdic C)
(hBA : Continuous (algebraMap B A)) (hBC : Continuous (algebraMap B C))
(hP : RingHom.IsRigSmoothArrow (algebraMap B A))
(hQ : RingHom.IsAdic (algebraMap B C)) :
TopologicalRing.IsAdic (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C)) ∧
IsNoetherianRing (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C)) ∧
RingHom.IsRigSmoothArrow
(algebraMap C (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C)))
Tag 0GCM, a lemma
Tag 0GCM in the Stacks Project.
Rig.rigSmooth_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothStableUnderComposition.lean, line 401.
Stacks Project, Tag 0GCM. Rig-smoothness of arrows of
WAdm^Noethis stable under composition: iff : B →+* Aandg : C →+* Bare continuous rig-smooth homomorphisms of Noetherian adic topological rings, then so isf ∘ g.Condition (6) of Stacks 0GBW for the composite is
Rig.finiteTypeAdicAlgebraForEveryIdeal_comp. For rig-smoothness over an ideal of definitionI ⊆ C, Stacks 0GCI moves both hypotheses ontoIand ontoI B, Stacks 0ALM presentsAover(C, I)by combining the two presentations, andRig.hasCotangentFactorization_combinedPresentationmultiplies the two factorizations of condition (3) of Stacks 0GAJ.
public theorem rigSmooth_comp
{A B C : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
[IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
[IsLinearTopology B B] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
[IsLinearTopology C C]
(hA : TopologicalRing.IsAdic A ∧ IsNoetherianRing A)
(hB : TopologicalRing.IsAdic B ∧ IsNoetherianRing B)
(hC : TopologicalRing.IsAdic C ∧ IsNoetherianRing C)
(f : B →+* A) (g : C →+* B) (hf : Continuous f) (hg : Continuous g)
(hPf : RingHom.IsRigSmoothArrow f) (hPg : RingHom.IsRigSmoothArrow g) :
RingHom.IsRigSmoothArrow (f.comp g)
Tag 0GH1, a lemma
Tag 0GH1 in the Stacks Project.
Rig.isRigFlat_and_exists_isRegular_of_isRigSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/RigSmoothRigFlat.lean, line 640.
Stacks Project, Tag 0GH1. Let
φ : A → Bbe an arrow ofWAdm^{Noeth}— a continuous homomorphism of Noetherian adic topological rings — which is rig-smooth. Thenφis rig-flat, and for every presentationB = A⟨x₁, …, x_n⟩ / J(over an ideal of definitionIofA) and every primeJ ⊆ 𝔮 ⊆ A⟨x⟩not containing an ideal of definition, the idealJ_𝔮ofA⟨x⟩_𝔮is generated by a regular sequence.Rig-flatness asks naive rig-flatness of every map
A_{\{f\}} → B_{\{f\}}, which isRig.isNaivelyRigFlat_completedAwayMap_of_isRigSmooth; the regular sequences areRig.exists_isRegular_ofList_eq_map_presentationIdeal. Both rest on the reduction of the source's proof to a rig-closed prime lying over a rig-closed prime, through the completed principal localization of Stacks 0GGG, where the Jacobian criterion on the regular fibre (Stacks 0GGJ, 0GEE, 00MG) concludes.
public theorem isRigFlat_and_exists_isRegular_of_isRigSmooth
{A : Type u} {B : Type v}
[CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
[IsNoetherianRing A]
[CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
[IsNoetherianRing B]
(hA : TopologicalRing.IsAdic A) (hB : TopologicalRing.IsAdic B)
(φ : A →+* B) (hφ : Continuous φ) (hsm : _root_.RingHom.IsRigSmooth φ) :
RingHom.IsRigFlat φ ∧
∀ (hft : FiniteTypeAdicAlgebraForEveryIdeal φ) (I : Ideal A)
(hI : TopologicalRing.IsIdealOfDefinition I)
(P : CompletedPolynomialPresentation I (adicFiniteTypeAlgebra φ hft I hI))
(q : Ideal P.completedPolynomialRing) [q.IsPrime],
¬ I.map (algebraMap A P.completedPolynomialRing) ≤ q → P.ideal ≤ q →
∃ fs : List (Localization.AtPrime q),
RingTheory.Sequence.IsRegular (Localization.AtPrime q) fs ∧
Ideal.ofList fs =
P.ideal.map (algebraMap P.completedPolynomialRing (Localization.AtPrime q))
Tag 0GH2, a lemma
Tag 0GH2 in the Stacks Project.
Rig.CompletedPolynomialPresentation.exists_pow_adicIdeal_le_annihilator_ker_onH₁_chainMapInl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Rig/NaiveCotangent/CombinedRigSmooth.lean, line 566.
Stacks Project, Tag 0GH2. Let
A → B → Cbe morphisms of (0AL4), so thatBandCare adic and topologically of finite type overA, and supposeB → Cis rig-smooth, i.e.Cis rig-smooth over(B, I B)(Stacks 0GAI, 0GCJ). Then the kernel of the first mapH⁻¹(NL^∧_{B/A} ⊗_B C) → H⁻¹(NL^∧_{C/A})of the six-term sequence of Stacks 0ALM is annihilated by a power of the ideal of definitionI C.The presentations are the given ones:
PofBoverA, the presentationψofCoverB, and the combined presentation ofCoverAthey define.
public theorem exists_pow_adicIdeal_le_annihilator_ker_onH₁_chainMapInl
(KB : CompletedNaiveCotangentComplex P)
(KC : CompletedNaiveCotangentComplex
(P.combinedPresentation s (ψ.restrictScalars A) hψ))
(hBC : IsRigSmooth (AdicFiniteTypeAlgebra.overBase (B := B) (C := C))) :
∃ n : ℕ, C.adicIdeal ^ n ≤ Module.annihilator C.carrier
(LinearMap.ker (NaiveCotangent.chainMapInl _
(P.combinedDifferential_comp_innerCotangentMap s ψ hψ KB KC)).onH₁)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.