23 Divided Power Algebra
Chapter 23 of the Stacks Project, Divided Power Algebra, Tag 09PD: the 11 sections of its 12 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 63 tags are carried by 149 declarations of the repository (all in StacksFrontier) and 12 registered declarations.
Section23.2 Divided powers#
Section 23.2 of the Stacks Project, Tag 07GK. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07GL, a definition
Tag 07GL in the Stacks Project.
Declarations registered for the tag:
DividedPowersregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 34 (StacksFrontier).
Tag 07GM, a lemma
Tag 07GM in the Stacks Project.
DividedPowers.instSubsingletonDividedPowers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Criteria.lean, line 75. The attribute's comment: “uniqueness”.
A divided power structure on an ideal in a ring torsion-free as a
ℤ-module is unique.
public instance instSubsingletonDividedPowers {A : Type*} [CommRing A]
[Module.IsTorsionFree ℤ A] (I : Ideal A) : Subsingleton (_root_.DividedPowers I)
DividedPowers.exists_dividedPowers_iff_factorial_mul_eq_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Criteria.lean, line 94. The attribute's comment: “factorial_criterion”.
Over a torsion-free commutative ring, maps on an ideal are divided power operations if and only if their products with the corresponding factorials are the corresponding powers.
public theorem exists_dividedPowers_iff_factorial_mul_eq_pow
{A : Type*} [CommRing A] [Module.IsTorsionFree ℤ A] (I : Ideal A)
(γ : ℕ → I → I) :
(∃ dp : _root_.DividedPowers I,
∀ (n : ℕ) (x : I), 0 < n → dp.dpow n (x : A) = (γ n x : A)) ↔
∀ (n : ℕ) (x : I), 0 < n →
(n.factorial : A) * (γ n x : A) = (x : A) ^ n
DividedPowers.nonempty_dividedPowers_iff_exists_generators_pow_mem_factorial_mul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Criteria.lean, line 194. The attribute's comment: “generator_criterion”.
Let
Ibe an ideal in a torsion-free commutative ring. ThenIadmits a divided power structure if and only if it has a set of ideal generatorsssuch that, for everyx ∈ sand every positiven, the powerx ^ nbelongs to(n!) I.
public lemma nonempty_dividedPowers_iff_exists_generators_pow_mem_factorial_mul
{A : Type*} [CommRing A] [HasUniqueDiv A] (I : Ideal A) :
Nonempty (_root_.DividedPowers I) ↔
∃ s : Set A, (Ideal.span s = I ∧
∀ x ∈ s, ∀ n : ℕ, (1 ≤ n →
x ^ n ∈ Ideal.span {(n.factorial : A)} * I))
Declarations registered for the tag:
DividedPowers.factorial_mul_dpow_eq_powregistered withadd_to_stacksin StacksFrontier/RingTheory/DividedPowers/Criteria.lean, line 71 (StacksFrontier): “factorial_identity”.
Tag 07GN, an example
Tag 07GN in the Stacks Project.
DividedPowers.exists_dividedPowers_span_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/IntegersAtPrime.lean, line 169.
If
Ais aℤ_(p)-algebra, the ideal generated byphas the divided power structure given byγₙ(p * a) = (p ^ n / n!) * a ^ n.The function
qin the conclusion consists of the coefficientsp ^ n / n!inℤ_(p); the first two properties say that these quotients exist and lie inpℤ_(p)in positive degrees.
public theorem exists_dividedPowers_span_natCast
{A : Type*} [CommRing A] (p : ℕ) [Fact p.Prime] [Algebra (IntegersAtPrime p) A] :
∃ (q : ℕ → IntegersAtPrime p) (γ : DividedPowers (Ideal.span {(p : A)})),
(∀ n : ℕ, (n.factorial : IntegersAtPrime p) * q n = (p : IntegersAtPrime p) ^ n) ∧
(∀ n : ℕ, n ≠ 0 → q n ∈ Ideal.span {(p : IntegersAtPrime p)}) ∧
∀ (n : ℕ) (a : A),
γ.dpow n ((p : A) * a) = algebraMap (IntegersAtPrime p) A (q n) * a ^ n
Tag 07GP, a lemma
Tag 07GP in the Stacks Project.
DividedPowers.exists_dividedPowers_of_axioms_on_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Criteria.lean, line 563.
The product and iteration axioms for divided powers need only be checked on a set of generators of the ideal, provided the other divided power axioms hold everywhere.
public theorem exists_dividedPowers_of_axioms_on_generators
{A : Type*} [CommRing A] (I : Ideal A) (dpow : ℕ → A → A) (S : Set A)
(hS : I = Ideal.span S)
(dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1)
(dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x)
(dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I)
(dpow_add : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I →
dpow n (x + y) = (antidiagonal n).sum fun k ↦ dpow k.1 x * dpow k.2 y)
(dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I →
dpow n (a * x) = a ^ n * dpow n x)
(mul_dpow_on_generators : ∀ {m n : ℕ} {x : A}, x ∈ S →
dpow m x * dpow n x = (choose (m + n) m : A) * dpow (m + n) x)
(dpow_comp_on_generators : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ S →
dpow m (dpow n x) = (uniformBell m n : A) * dpow (m * n) x) :
∃ hI : _root_.DividedPowers I, ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = dpow n x
Tag 07GQ, a lemma
Tag 07GQ in the Stacks Project.
DividedPowers.existsUnique_on_ideal_add, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Criteria.lean, line 766. The attribute's comment: “part (2)”.
Divided power structures which agree on the intersection of their ideals extend uniquely to the sum of the ideals.
public lemma existsUnique_on_ideal_add {A : Type*} [CommRing A] {I J : Ideal A}
(γ : _root_.DividedPowers I)
(δ : _root_.DividedPowers J)
(h : ∀ (n : ℕ) {x : A}, x ∈ I ⊓ J → γ.dpow n x = δ.dpow n x) :
∃! ε : _root_.DividedPowers (I + J),
(∀ (n : ℕ) {x : A}, x ∈ I → ε.dpow n x = γ.dpow n x) ∧
(∀ (n : ℕ) {x : A}, x ∈ J → ε.dpow n x = δ.dpow n x)
Declarations registered for the tag:
DividedPowers.coincide_on_smulregistered withadd_to_stacksin StacksFrontier/RingTheory/DividedPowers/Criteria.lean, line 704 (StacksFrontier): “part (1)”.
Tag 07GR, a lemma
Tag 07GR in the Stacks Project.
DividedPowers.locallyNilpotent_iff_isNilpotent_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Nilpotent.lean, line 46.
Let
pbe a prime number, letγbe a divided power structure on an idealIof a commutative ringA, and assumepis nilpotent inA ⧸ I. ThenIis locally nilpotent, i.e. every element ofIis nilpotent, if and only ifpis nilpotent inA.
public theorem locallyNilpotent_iff_isNilpotent_natCast {A : Type*} [CommRing A] {p : ℕ}
(hp : p.Prime) {I : Ideal A} (γ : DividedPowers I) (hpI : IsNilpotent (p : A ⧸ I)) :
I.LocallyNilpotent ↔ IsNilpotent (p : A)
Sources
Section23.3 Divided power rings#
Section 23.3 of the Stacks Project, Tag 07GT. 5 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07GU, a definition
Tag 07GU in the Stacks Project.
DividedPowerRing, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/Basic.lean, line 61. The attribute's comment: “divided power rings”.
A divided power ring is a commutative ring equipped with an ideal and a divided power structure on that ideal.
public structure DividedPowerRing
Declarations registered for the tag:
DividedPowers.DPMorphismregistered withadd_to_stacksin StacksFrontier/RingTheory/DividedPowers/Ring/Basic.lean, line 75 (StacksFrontier): “homomorphisms of divided power rings”.
Tag 07GV, a lemma
Tag 07GV in the Stacks Project.
DividedPowerRing.hasLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/Basic.lean, line 365. The attribute's comment: “existence of limits”.
The category of divided power rings has all small limits.
public instance hasLimits : HasLimits DividedPowerRing.{u}
DividedPowerRing.forgetPreservesLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/Basic.lean, line 371. The attribute's comment: “agreement with limits of rings”.
Limits of divided power rings are computed on their underlying commutative rings.
public noncomputable instance forgetPreservesLimits :
PreservesLimits DividedPowerRing.forget.{u}
Tag 07GW, a lemma
Tag 07GW in the Stacks Project.
DividedPowerRing.isCorepresentable_of_cardinal_solutionSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/Basic.lean, line 433.
A limit-preserving functor on divided power rings is corepresentable when every one of its elements is obtained from an element over a divided power ring whose underlying type has uniformly bounded cardinality.
public theorem isCorepresentable_of_cardinal_solutionSet
(F : DividedPowerRing.{u} ⥤ Type u)
[PreservesLimitsOfSize.{u, u} F]
(hF : ∃ κ : Cardinal.{u}, ∀ (A : DividedPowerRing.{u}) (f : F.obj A),
∃ (A' : DividedPowerRing.{u}) (f' : F.obj A') (g : A' ⟶ A),
F.map g f' = f ∧ Cardinal.mk A' ≤ κ) :
F.IsCorepresentable
Tag 07GX, a lemma
Tag 07GX in the Stacks Project.
DividedPowerRing.instHasColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/Colimits.lean, line 513.
The category of divided power rings has all colimits.
public instance instHasColimits : HasColimits (DividedPowerRing.{u})
Tag 0H86, a remark
Tag 0H86 in the Stacks Project.
DividedPowerRing.tensorProductQuotientEquivPushoutQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/PushoutQuotient.lean, line 154. The attribute's comment: “quotient_of_pushout”.
For a pushout of divided power rings, the tensor product of the quotients of the two factors over the quotient of the base is canonically isomorphic to the quotient of the pushout.
public noncomputable def tensorProductQuotientEquivPushoutQuotient
{A B B' B'' : DividedPowerRing.{u}} (f : A ⟶ B) (f' : A ⟶ B')
(g : B ⟶ B'') (g' : B' ⟶ B'') (h : IsPushout f f' g g') :
letI : Algebra (A ⧸ A.ideal) (B ⧸ B.ideal) := (quotientRingHom f).toAlgebra
letI : Algebra (A ⧸ A.ideal) (B' ⧸ B'.ideal) := (quotientRingHom f').toAlgebra
{e : (B ⧸ B.ideal) ⊗[A ⧸ A.ideal] (B' ⧸ B'.ideal) ≃+* (B'' ⧸ B''.ideal) //
∀ (b : B) (b' : B'),
e (Ideal.Quotient.mk B.ideal b ⊗ₜ[A ⧸ A.ideal] Ideal.Quotient.mk B'.ideal b') =
Ideal.Quotient.mk B''.ideal (g b * g' b')}
DividedPowerRing.tensorProductToPushout_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/PushoutTensor.lean, line 436. The attribute's comment: “tensor_map_surjective”.
In a pushout of divided power rings, the canonical map from the tensor product of the underlying rings to the underlying ring of the pushout is surjective.
public theorem tensorProductToPushout_surjective
{A B B' B'' : DividedPowerRing.{u}} (f : A ⟶ B) (f' : A ⟶ B')
(g : B ⟶ B'') (g' : B' ⟶ B'') (h : IsPushout f f' g g') :
Function.Surjective (tensorProductToPushout f f' g g' h.w)
DividedPowerRing.dividedPowerIdeal_surjective_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Ring/PushoutTensor.lean, line 490. The attribute's comment: “ideal_map_surjective”.
In a pushout of divided power rings, the canonical map from the sum of the two extended divided power ideals onto the distinguished ideal of the pushout is surjective.
public theorem dividedPowerIdeal_surjective_of_isPushout
{A B B' B'' : DividedPowerRing.{u}}
(f : A ⟶ B) (g : A ⟶ B') (h : B ⟶ B'') (h' : B' ⟶ B'')
(H : IsPushout f g h h') :
letI : Algebra A B := f.toRingHom.toAlgebra
letI : Algebra A B' := g.toRingHom.toAlgebra
∀ y : B''.ideal,
∃ x : (Ideal.map Algebra.TensorProduct.includeLeftRingHom B.ideal +
Ideal.map Algebra.TensorProduct.includeRight.toRingHom B'.ideal :
Ideal (B ⊗[A] B')),
canonicalTensorProductHom f g h h' H.w x.1 = y.1
Sources
Section23.4 Extending divided powers#
Section 23.4 of the Stacks Project, Tag 07GZ. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07H0, a definition
Tag 07H0 in the Stacks Project.
DividedPowers.Extends, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/Existence.lean, line 71.
A divided power structure
γonIextends alongf : A →+* Bif the extended idealI.map fadmits a divided power structure makingfa divided power morphism.
public abbrev Extends
{A B : Type*} [CommSemiring A] [CommSemiring B] {I : Ideal A}
(γ : _root_.DividedPowers I) (f : A →+* B) : Prop
Tag 07H1, a lemma
Tag 07H1 in the Stacks Project.
DividedPowers.existsUnique_extension, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/Existence.lean, line 79. The attribute's comment: “uniqueness”.
If a divided power structure extends along a ring homomorphism, the divided power structure on the extended ideal making that homomorphism a divided power morphism is unique.
public lemma existsUnique_extension {A B : Type*} [CommSemiring A] [CommSemiring B]
{I : Ideal A} (γ : _root_.DividedPowers I) (f : A →+* B)
(h : Extends γ f) :
∃! δ : _root_.DividedPowers (I.map f),
_root_.DividedPowers.IsDPMorphism γ δ f
DividedPowers.DividedPowerRing.dividedPowers_extends_of_map_eq_bot_or_isPrincipal_or_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/Existence.lean, line 705. The attribute's comment: “existence”.
Divided powers extend along a ring homomorphism if the mapped ideal is zero, the source ideal is principal, or the homomorphism is flat.
public theorem DividedPowerRing.dividedPowers_extends_of_map_eq_bot_or_isPrincipal_or_flat
(A : DividedPowerRing.{u}) {B : Type v} [CommRing B] (f : A →+* B)
(h : (A.ideal.map f = ⊥) ∨ A.ideal.IsPrincipal ∨ f.Flat) :
Extends A.dividedPowers f
DividedPowers.DividedPowerRing.isDPMorphism_extendedDividedPowersOfMapEqBotOrIsPrincipalOrFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/Existence.lean, line 755. The attribute's comment: “existence”.
The chosen divided powers on the mapped ideal make the original ring homomorphism a divided power morphism.
public theorem
DividedPowerRing.isDPMorphism_extendedDividedPowersOfMapEqBotOrIsPrincipalOrFlat
(A : DividedPowerRing.{u}) {B : Type v} [CommRing B] (f : A →+* B)
(h : (A.ideal.map f = ⊥) ∨ A.ideal.IsPrincipal ∨ f.Flat) :
_root_.DividedPowers.IsDPMorphism A.dividedPowers
(DividedPowerRing.extendedDividedPowersOfMapEqBotOrIsPrincipalOrFlat A f h) f
Tag 07H2, a lemma
Tag 07H2 in the Stacks Project.
Declarations registered for the tag:
DividedPowers.isSubDPIdeal_kerregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 21 (StacksFrontier): “(1) Ker(φ) ∩ I is preserved by the γₙ, n ≥ 1”.DividedPowers.Quotient.dividedPowersregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 22 (StacksFrontier): “(2) (a) => (b): the divided power structure on I(A/𝔞)”.DividedPowers.Quotient.isDPMorphismregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 24 (StacksFrontier): “(2) (a) => (b): A → A/𝔞 is a divided power homomorphism for it”.DividedPowers.subDPIdeal_inf_of_quotregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 26 (StacksFrontier): “(2) (b) => (a): the sub-dp-ideal with carrier 𝔞 ⊓ I (by definition)”.DividedPowers.span_isSubDPIdeal_iffregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 28 (StacksFrontier): “(2) (a) <=> (c), for I' = span S with S ⊆ I”.
Tag 07H3, a lemma
Tag 07H3 in the Stacks Project.
Declarations registered for the tag:
DividedPowers.SubDPIdeal.spanregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 29 (StacksFrontier): “the smallest sub-dp-ideal containing E (the infimum of those containing E)”.DividedPowers.SubDPIdeal.span_carrier_eq_dpow_spanregistered withadd_to_stacksin StacksFrontier/MathlibRegistrations/Ch23.lean, line 31 (StacksFrontier): “its ideal is generated by the γₙ(f), n ≥ 1, f ∈ E”.
Tag 07KD, a lemma
Tag 07KD in the Stacks Project.
DividedPowers.completedDividedPowers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/CompletedDividedPowers.lean, line 583. The attribute's comment: “part (3), extension”.
Part (3), extension: the divided powers on
Iextend to its completed ideal. The subtype records the naturality on the dense image ofI.
public noncomputable def completedDividedPowers
(hp : IsNilpotent (Ideal.Quotient.mk I (p : A))) :
{ δ : DividedPowers (completionIdeal I p hp) //
∀ (n : ℕ) (x : A) (_hx : x ∈ I) (xhat : completionIdeal I p hp),
(xhat : AdicCompletion (pAdicIdeal (A := A) p) A) =
algebraMap A (AdicCompletion (pAdicIdeal (A := A) p) A) x →
δ.dpow n xhat =
algebraMap A (AdicCompletion (pAdicIdeal (A := A) p) A) (γ.dpow n x) }
DividedPowers.eventually_isDividedPowerCompletionLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/CompletedDividedPowers.lean, line 741. The attribute's comment: “part (4)”.
Part (4): over
ℤ_(p), sufficiently high powers of(p)are stable under the divided powers and the completed divided power ring has the inverse-limit universal property for the resulting quotient divided power rings.
public theorem eventually_isDividedPowerCompletionLimit [Fact p.Prime]
[Algebra (IntegersAtPrime p) A]
(hp : IsNilpotent (Ideal.Quotient.mk I (p : A))) :
∃ N, ∃ hlevel : ∀ e, N ≤ e →
(pAdicIdeal (A := A) p ^ e ≤ I) ∧
γ.IsSubDPIdeal (pAdicIdeal (A := A) p ^ e),
IsDividedPowerCompletionLimit I γ p hp N hlevel
DividedPowers.completionToQuotient_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/Completion.lean, line 178. The attribute's comment: “part (1)”.
Part (1): the
p-adic completion maps onto the quotient by the divided power ideal.
public theorem completionToQuotient_surjective
(hp : IsNilpotent (Ideal.Quotient.mk I (p : A))) :
Function.Surjective (completionToQuotient I p hp)
DividedPowers.completionIdealEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/Completion.lean, line 333. The attribute's comment: “part (2)”.
Part (2): the completion of
I, mapped into the completion ofA, is canonically the kernel of the map toA/I.
public noncomputable def completionIdealEquiv
(hp : IsNilpotent (Ideal.Quotient.mk I (p : A))) :
{ e : AdicCompletion (pAdicIdeal (A := A) p) I ≃ₗ[
AdicCompletion (pAdicIdeal (A := A) p) A] completionIdeal I p hp //
∀ x, ((e x : completionIdeal I p hp) :
AdicCompletion (pAdicIdeal (A := A) p) A) =
AdicCompletion.map (pAdicIdeal (A := A) p) I.subtype x }
DividedPowers.dpow_pAdic_continuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Extend/Completion.lean, line 368. The attribute's comment: “part (3), continuity”.
Part (3), continuity: changing an element of
Iby an element ofp^e Ichanges every divided power by an element ofp^e I.
public theorem dpow_pAdic_continuous (n e : ℕ) {x y : A}
(hx : x ∈ I) (hy : y ∈ I) :
γ.dpow n (x + (p : A) ^ e * y) - γ.dpow n x ∈
pAdicIdeal (A := A) p ^ e • (I : Submodule A A)
Sources
Section23.5 Divided power polynomial algebras#
Section 23.5 of the Stacks Project, Tag 07H4. 4 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 07H5, a lemma
Tag 07H5 in the Stacks Project.
DividedPowers.dividedPowerPolynomialDividedPowers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Basic.lean, line 1188. The attribute's comment: “divided power structure”.
The canonical divided power structure on the divided power ideal of a finite-variable divided power polynomial algebra.
public noncomputable def dividedPowerPolynomialDividedPowers (A : DividedPowerRing.{u})
(ι : Type w) [Finite ι] : _root_.DividedPowers (dividedPowerPolynomialIdeal A.ideal ι)
DividedPowers.dividedPowerPolynomialDividedPowers_dpow_variable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Basic.lean, line 1201. The attribute's comment: “value on variables”.
The canonical divided powers send
xᵢto the distinguished monomialxᵢ^[n].
public theorem dividedPowerPolynomialDividedPowers_dpow_variable
(A : DividedPowerRing.{u}) (ι : Type w) [Finite ι] (i : ι) (n : ℕ) :
(dividedPowerPolynomialDividedPowers A ι).dpow n
(dividedPowerPolynomialVariable A i) =
dividedPowerPolynomialVariableMonomial A i n
DividedPowers.dividedPowerPolynomialCoefficient_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Basic.lean, line 1211. The attribute's comment: “coefficient morphism”.
The coefficient map into the divided power polynomial algebra is a morphism of divided power rings.
public theorem dividedPowerPolynomialCoefficient_isDPMorphism
(A : DividedPowerRing.{u}) (ι : Type w) [Finite ι] :
_root_.DividedPowers.IsDPMorphism A.dividedPowers
(dividedPowerPolynomialDividedPowers A ι)
(algebraMap A (DividedPowerAlgebra A (ι →₀ A)))
DividedPowers.dividedPowerPolynomialDividedPowers_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Basic.lean, line 1228. The attribute's comment: “uniqueness”.
The canonical structure is the unique divided power structure which has the prescribed values on variables and makes the coefficient map a divided power morphism.
public theorem dividedPowerPolynomialDividedPowers_unique
(A : DividedPowerRing.{u}) (ι : Type w) [Finite ι]
(δ : _root_.DividedPowers (dividedPowerPolynomialIdeal A.ideal ι))
(hvar : ∀ (i : ι) (n : ℕ),
δ.dpow n (dividedPowerPolynomialVariable A i) =
dividedPowerPolynomialVariableMonomial A i n)
(hcoeff : _root_.DividedPowers.IsDPMorphism A.dividedPowers δ
(algebraMap A (DividedPowerAlgebra A (ι →₀ A)))) :
δ = dividedPowerPolynomialDividedPowers A ι
DividedPowers.existsUnique_dPMorphism_from_dividedPowerPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Basic.lean, line 1356. The attribute's comment: “universal property”.
A divided power morphism on coefficients and one element of the target divided power ideal for each variable extend uniquely to the divided power polynomial algebra.
public theorem existsUnique_dPMorphism_from_dividedPowerPolynomial
(A : DividedPowerRing.{u}) (ι : Type w) [Finite ι]
(C : DividedPowerRing.{v})
(f : _root_.DividedPowers.DPMorphism A.dividedPowers C.dividedPowers)
(k : ι → C.ideal) :
∃! φ : _root_.DividedPowers.DPMorphism (dividedPowerPolynomialDividedPowers A ι)
C.dividedPowers,
(φ.comp (dividedPowerPolynomialCoefficientDPMorphism A ι) = f ∧
∀ i : ι, φ (dividedPowerPolynomialVariable A i) = (k i : C))
Tag 07H6, a remark
Tag 07H6 in the Stacks Project.
DividedPowers.finiteStageMap_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/SetIndexed.lean, line 335. The attribute's comment: “compatible_divided_powers”.
Transition maps between finite stages preserve the canonical divided powers.
public theorem finiteStageMap_isDPMorphism (A : DividedPowerRing.{u})
{W : Type w} {E F : Finset W} (h : E ⊆ F) :
_root_.DividedPowers.IsDPMorphism
(dividedPowerPolynomialDividedPowers A E)
(dividedPowerPolynomialDividedPowers A F)
(finiteStageMap A h).toRingHom
DividedPowers.setIndexedDividedPowerPolynomialDividedPowers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/SetIndexed.lean, line 507. The attribute's comment: “compatible_divided_powers”.
The divided powers on the distinguished ideal of the divided power polynomial algebra on an arbitrary type of variables, induced from all finite-variable subalgebras.
public noncomputable def setIndexedDividedPowerPolynomialDividedPowers
(A : DividedPowerRing.{u}) (W : Type w) :
_root_.DividedPowers (dividedPowerPolynomialIdeal A.ideal W)
DividedPowers.finiteStageInclusion_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/SetIndexed.lean, line 678. The attribute's comment: “compatible_divided_powers”.
Every finite-stage inclusion preserves divided powers induced on the colimit.
public theorem finiteStageInclusion_isDPMorphism (A : DividedPowerRing.{u})
{W : Type w} (E : Finset W) :
_root_.DividedPowers.IsDPMorphism
(dividedPowerPolynomialDividedPowers A E)
(setIndexedDividedPowerPolynomialDividedPowers A W)
(finiteStageInclusion A E).toRingHom
DividedPowers.setIndexedDividedPowerPolynomialDividedPowers_dpow_variable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/SetIndexed.lean, line 692. The attribute's comment: “compatible_divided_powers”.
The induced divided powers send a variable to its divided power monomial.
public theorem setIndexedDividedPowerPolynomialDividedPowers_dpow_variable
(A : DividedPowerRing.{u}) {W : Type w} (i : W) (n : ℕ) :
(setIndexedDividedPowerPolynomialDividedPowers A W).dpow n
(dividedPowerPolynomialVariable A i) =
dividedPowerPolynomialVariableMonomial A i n
DividedPowers.setIndexedDividedPowerPolynomialCoefficient_isDPMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/SetIndexed.lean, line 717. The attribute's comment: “compatible_divided_powers”.
The coefficient map is a morphism of divided power rings.
public theorem setIndexedDividedPowerPolynomialCoefficient_isDPMorphism
(A : DividedPowerRing.{u}) (W : Type w) :
_root_.DividedPowers.IsDPMorphism A.dividedPowers
(setIndexedDividedPowerPolynomialDividedPowers A W)
(algebraMap A (setIndexedDividedPowerPolynomialAlgebra A W))
DividedPowers.setIndexedDividedPowerPolynomialDividedPowers_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/SetIndexed.lean, line 760. The attribute's comment: “compatible_divided_powers”.
Compatibility with every finite stage uniquely determines the induced divided powers.
public theorem setIndexedDividedPowerPolynomialDividedPowers_unique
(A : DividedPowerRing.{u}) (W : Type w)
(δ : _root_.DividedPowers (dividedPowerPolynomialIdeal A.ideal W))
(hδ : ∀ E : Finset W,
_root_.DividedPowers.IsDPMorphism (dividedPowerPolynomialDividedPowers A E) δ
(finiteStageInclusion A E).toRingHom) :
δ = setIndexedDividedPowerPolynomialDividedPowers A W
DividedPowers.existsUnique_dPMorphism_from_setIndexedDividedPowerPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/SetIndexedUniversalProperty.lean, line 100. The attribute's comment: “set_indexed_universal_property”.
The universal property of a divided power polynomial algebra on an arbitrary type of variables: a coefficient morphism and arbitrary images in the target ideal admit exactly one extension as a divided power morphism.
public theorem existsUnique_dPMorphism_from_setIndexedDividedPowerPolynomial
(A : DividedPowerRing.{u}) (W : Type w) (C : DividedPowerRing.{v})
(f : _root_.DividedPowers.DPMorphism A.dividedPowers C.dividedPowers)
(k : W → C.ideal) :
∃! φ : _root_.DividedPowers.DPMorphism
(setIndexedDividedPowerPolynomialDividedPowers A W) C.dividedPowers,
(φ.comp (setIndexedDividedPowerPolynomialCoefficientDPMorphism A W) = f ∧
∀ i : W, φ (dividedPowerPolynomialVariable A i) = (k i : C))
DividedPowers.finiteVariableInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Stages.lean, line 78. The attribute's comment: “finite_variable_inclusion”.
The canonical inclusion from the divided power polynomial algebra in
svariables to the one intvariables.
public noncomputable def finiteVariableInclusion (A : Type u) [CommRing A]
{s t : ℕ} (h : s ≤ t) :
DividedPowerAlgebra A (Fin s →₀ A) →ₐ[A] DividedPowerAlgebra A (Fin t →₀ A)
DividedPowers.finiteVariableInclusion_variableMonomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Stages.lean, line 85. The attribute's comment: “finite_variable_inclusion”.
The inclusion preserves each divided power monomial in an existing variable.
public theorem finiteVariableInclusion_variableMonomial (A : Type u) [CommRing A]
{s t : ℕ} (h : s ≤ t) (i : Fin s) (n : ℕ) :
finiteVariableInclusion A h (dividedPowerPolynomialVariableMonomial A i n) =
dividedPowerPolynomialVariableMonomial A (Fin.castLE h i) n
DividedPowers.setIndexedDividedPowerPolynomialAlgebra, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Stages.lean, line 93. The attribute's comment: “set_indexed_divided_power_polynomial_algebra”.
The divided power polynomial algebra with one variable for each element of
W.
public abbrev setIndexedDividedPowerPolynomialAlgebra
(A : Type u) [CommRing A] (W : Type w)
DividedPowers.finiteStageMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Stages.lean, line 99. The attribute's comment: “set_indexed_divided_power_polynomial_algebra”.
The transition map between the finite-variable divided power polynomial algebras.
public noncomputable def finiteStageMap (A : Type u) [CommRing A] {W : Type w}
{E F : Finset W} (h : E ⊆ F) :
DividedPowerAlgebra A (E →₀ A) →ₐ[A] DividedPowerAlgebra A (F →₀ A)
DividedPowers.finiteStageInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Stages.lean, line 107. The attribute's comment: “set_indexed_divided_power_polynomial_algebra”.
The canonical map from a finite-variable algebra into the set-indexed algebra.
public noncomputable def finiteStageInclusion (A : Type u) [CommRing A] {W : Type w}
(E : Finset W) :
DividedPowerAlgebra A (E →₀ A) →ₐ[A]
setIndexedDividedPowerPolynomialAlgebra A W
DividedPowers.finiteStageInclusion_existsUnique_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Polynomial/Stages.lean, line 178. The attribute's comment: “set_indexed_divided_power_polynomial_algebra”.
A compatible family of algebra maps out of all finite stages descends uniquely to the set-indexed divided power polynomial algebra.
public theorem finiteStageInclusion_existsUnique_lift (A : Type u) [CommRing A]
(W : Type w) (B : Type*) [CommRing B] [Algebra A B]
(f : (E : Finset W) → DividedPowerAlgebra A (E →₀ A) →ₐ[A] B)
(hf : ∀ (E F : Finset W) (h : E ⊆ F),
(f F).comp (finiteStageMap A h) = f E) :
∃! g : setIndexedDividedPowerPolynomialAlgebra A W →ₐ[A] B,
∀ E : Finset W, g.comp (finiteStageInclusion A E) = f E
Declarations registered for the tag:
DividedPowers.dividedPowerPolynomialIdeal, declared in the repository, registered withadd_to_stacksin StacksFrontier/RingTheory/DividedPowers/Polynomial/Stages.lean, line 251 (StacksFrontier): “set_indexed_divided_power_polynomial_algebra”.
Tag 07GS, a lemma
Tag 07GS in the Stacks Project.
DividedPowers.eq_iff_dpow_prime_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/PrimeOperation/Classification.lean, line 111. The attribute's comment: “uniqueness”.
Over a
ℤ_(p)-algebra, a divided power structure is determined by itspth operation.
public lemma eq_iff_dpow_prime_eq {A : Type*} [CommRing A] {I : Ideal A} (p : ℕ)
(hp : p.Prime) (hA : ∀ n : ℕ, ¬p ∣ n → IsUnit (n : A))
(γ γ' : _root_.DividedPowers I) :
γ = γ' ↔ ∀ x : I, γ.dpow p x = γ'.dpow p x
DividedPowers.existsUnique_of_prime_operation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/PrimeOperation/Classification.lean, line 160. The attribute's comment: “existence”.
A map satisfying the factorial, homogeneity, and addition identities for a
pth divided power operation extends uniquely to a divided power structure.
public lemma existsUnique_of_prime_operation {A : Type*} [CommRing A] (I : Ideal A) (p : ℕ)
(hp : p.Prime) (hA : ∀ n : ℕ, ¬p ∣ n → IsUnit (n : A)) (δ : I → I)
(factorial_mul : ∀ x : I, (p.factorial : A) * (δ x : A) = (x : A) ^ p)
(smul : ∀ (a : A) (x : I), δ (a • x) = a ^ p • δ x)
(add : ∀ x y : I,
(δ (x + y) : A) = (δ x : A) +
∑ ij ∈ (antidiagonal p).filter (fun ij ↦ ij.1 ≠ 0 ∧ ij.2 ≠ 0),
factorialInverse p hp hA ij.1 * factorialInverse p hp hA ij.2 *
(x : A) ^ ij.1 * (y : A) ^ ij.2 +
(δ y : A)) :
∃! γ : _root_.DividedPowers I, ∀ x : I, γ.dpow p x = δ x
Tag 0H87, a remark
Tag 0H87 in the Stacks Project.
DividedPowers.factorial_mul_of_smul_add, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/PolynomialAlgebra.lean, line 235.
Homogeneity and the divided-power addition law imply the factorial identity for the
pth operation.
public lemma factorial_mul_of_smul_add {A : Type*} [CommRing A] (I : Ideal A) (p : ℕ)
(hp : p.Prime) (hA : ∀ n : ℕ, ¬p ∣ n → IsUnit (n : A)) (δ : I → I)
(smul : ∀ (a : A) (x : I), δ (a • x) = a ^ p • δ x)
(add : ∀ x y : I,
(δ (x + y) : A) = (δ x : A) +
∑ ij ∈ (antidiagonal p).filter (fun ij ↦ ij.1 ≠ 0 ∧ ij.2 ≠ 0),
factorialInverse p hp hA ij.1 * factorialInverse p hp hA ij.2 *
(x : A) ^ ij.1 * (y : A) ^ ij.2 +
(δ y : A)) :
∀ x : I, (p.factorial : A) * (δ x : A) = (x : A) ^ p
Sources
Section23.6 Tate resolutions#
Section 23.6 of the Stacks Project, Tag 09PF. 12 tags here are carried by 60 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09PG, a definition
Tag 09PG in the Stacks Project.
DividedPowers.TateResolution.DividedPowerStructure, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/Basic.lean, line 148.
A divided power structure on the positive even part of a strictly graded-commutative graded algebra.
public structure DividedPowerStructure (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜]
[IsStrictlyGradedComm 𝒜]
Tag 09PH, an example
Tag 09PH in the Stacks Project.
DividedPowers.TateResolution.ExteriorOddVariable.equiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/ExteriorDividedPowers.lean, line 303. The attribute's comment: “exterior algebra as an iterated odd variable extension”.
The odd-variable extension of
⋀[R] Mis⋀[R] (M × R).
public noncomputable def equiv :
OddVariableExtension (exteriorGrade R M) 1 ≃ₐ[R] ExteriorAlgebra R (M × R)
DividedPowers.TateResolution.isCompatibleWithDifferential_exteriorDividedPowerStructure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/ExteriorKoszulCompatibility.lean, line 300. The attribute's comment: “compatibility with the Koszul differential”.
The divided powers of
⋀[R] (Fin r → R)are compatible with contraction by everyR-linear functional, hence with the Koszul differential of every finite sequence inR.
public theorem isCompatibleWithDifferential_exteriorDividedPowerStructure (r : ℕ) :
∀ φ : Module.Dual R (Fin r → R),
IsCompatibleWithDifferential (exteriorDividedPowerStructure R r)
(CliffordAlgebra.contractLeft φ)
DividedPowers.TateResolution.existsUnique_oddVariableDividedPowerStructure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariable/Existence.lean, line 654. The attribute's comment: “existence and uniqueness”.
There is a unique divided power structure on an odd-variable extension which extends the given divided powers on the coefficient algebra.
public theorem existsUnique_oddVariableDividedPowerStructure
(Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ] [IsStrictlyGradedComm Aᵢ]
(gamma : DividedPowerStructure Aᵢ) (d : ℕ) (hd : 0 < d) (hd_odd : Odd d) :
∃! delta : DividedPowerStructure (OddVariableExtension.grade Aᵢ d),
IsOddVariableDividedPowerExtension Aᵢ d gamma delta
DividedPowers.TateResolution.oddVariableDividedPowerStructure_dpow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariable/Existence.lean, line 690. The attribute's comment: “divided power formula”.
For
xin the positive even part andyin the odd part, thenth divided power ofx + yTisgamma_n(x) + gamma_(n - 1)(x)yT.
public theorem oddVariableDividedPowerStructure_dpow
(Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ] [IsStrictlyGradedComm Aᵢ]
(gamma : DividedPowerStructure Aᵢ) (d : ℕ) (hd : 0 < d) (hd_odd : Odd d)
(n : ℕ) (hn : n ≠ 0) (x y : A) (hx : x ∈ positiveEvenPart Aᵢ)
(hy : y ∈ oddPart Aᵢ) :
(oddVariableDividedPowerStructure Aᵢ gamma d hd hd_odd).dpow n
(inclusion Aᵢ d x + inclusion Aᵢ d y * generator Aᵢ d) =
inclusion Aᵢ d (gamma.dpow n x) +
inclusion Aᵢ d (gamma.dpow (n - 1) x * y) * generator Aᵢ d
DividedPowers.TateResolution.OddVariableExtension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariable/Extension.lean, line 197. The attribute's comment: “odd_variable_extension”.
The odd-variable extension
A⟨T⟩. Its elements are pairs(a, b), written mathematically asa + bT.
public abbrev OddVariableExtension (Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ] (d : ℕ)
DividedPowers.TateResolution.OddVariableExtension.grade, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariable/Extension.lean, line 256. The attribute's comment: “odd_variable_extension”.
The degree-
mpieceA_m ⊕ A_{m-d}Tof the odd-variable extension.
public def grade (Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ] (d m : ℕ) :
Submodule R (OddVariableExtension Aᵢ d)
DividedPowers.TateResolution.existsUnique_oddVariableExtension_ringHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/VariableLift.lean, line 222. The attribute's comment: “mapping property”.
The mapping property of the odd variable extension of Tag 09PH, for ring homomorphisms. A ring homomorphism out of
B⟨T⟩which preserves degrees is determined by, and may be prescribed by, its restriction toBtogether with the image ofT.
public theorem existsUnique_oddVariableExtension_ringHom
(h : B →+* D) (hgrade : ∀ (m : ℕ) (b : B), b ∈ ℬ m → h b ∈ 𝒟 m)
(d : ℕ) (hodd : Odd d) (t : D) (ht : t ∈ 𝒟 d) :
∃! g : OddVariableExtension ℬ d →+* D,
(∀ b : B, g (inclusion ℬ d b) = h b) ∧
g (generator ℬ d) = t ∧
(∀ (m : ℕ) (x : OddVariableExtension ℬ d), x ∈ grade ℬ d m → g x ∈ 𝒟 m)
DividedPowers.TateResolution.oddVariableExtension_ringHom_dpow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/VariableLift.lean, line 311. The attribute's comment: “mapping property”.
A degree-preserving ring homomorphism out of an odd variable extension which restricts to a divided-power compatible map on the coefficients is itself compatible with divided powers.
public theorem oddVariableExtension_ringHom_dpow
(h : B →+* D) (hgrade : ∀ (m : ℕ) (b : B), b ∈ ℬ m → h b ∈ 𝒟 m)
(hdpow : ∀ (n : ℕ) (b : B), b ∈ positiveEvenPart ℬ → δ.dpow n (h b) = h (β.dpow n b))
(d : ℕ) (hd : 0 < d) (hodd : Odd d) (t : D) (ht : t ∈ 𝒟 d)
(g : OddVariableExtension ℬ d →+* D)
(hg1 : ∀ b : B, g (inclusion ℬ d b) = h b) (hg2 : g (generator ℬ d) = t)
(n : ℕ) (x : OddVariableExtension ℬ d) (hx : x ∈ positiveEvenPart (grade ℬ d)) :
δ.dpow n (g x) = g ((oddVariableDividedPowerStructure ℬ β d hd hodd).dpow n x)
Tag 09PI, an example
Tag 09PI in the Stacks Project.
DividedPowers.TateResolution.EvenVariableAlgebra, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariable.lean, line 62. The attribute's comment: “even_variable_algebra”.
The algebra of finite divided-power polynomials in one even variable over
A.The coefficient at
nis the coefficient of the formal symbolT⁽ⁿ⁾.
public structure EvenVariableAlgebra (A : Type v) [Ring A]
DividedPowers.TateResolution.EvenVariableAlgebra.mul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariable.lean, line 131. The attribute's comment: “even_variable_algebra”.
The binomially weighted convolution product.
public def mul (x y : EvenVariableAlgebra A) : EvenVariableAlgebra A
DividedPowers.TateResolution.EvenVariableAlgebra.grade, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariable.lean, line 351. The attribute's comment: “even_variable_algebra”.
The degree-
mpiece after adjoining an even variable of degreed.Its coefficient of
T⁽ⁿ⁾lies in𝒜 (m - n * d)whenn * d ≤ m, and is zero otherwise.
public def grade (𝒜 : ℕ → Submodule R A) (d m : ℕ) :
Submodule R (EvenVariableAlgebra A)
DividedPowers.TateResolution.EvenVariableAlgebra.gradedAlgebra, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariable.lean, line 559. The attribute's comment: “even_variable_algebra”.
The shifted homogeneous pieces give an internal grading of the coefficient algebra.
public instance gradedAlgebra (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜]
(d : ℕ) : GradedAlgebra (grade 𝒜 d)
DividedPowers.TateResolution.EvenVariableAlgebra.strictlyGradedComm, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariable.lean, line 614. The attribute's comment: “even_variable_algebra”.
An even variable preserves strict graded commutativity, including vanishing odd squares.
public instance strictlyGradedComm (𝒜 : ℕ → Submodule R A) [IsStrictlyGradedComm 𝒜]
(d : ℕ) [Fact (Even d)] : IsStrictlyGradedComm (grade 𝒜 d)
DividedPowers.TateResolution.evenVariableDividedPowerStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableDividedPowers/Structure.lean, line 280. The attribute's comment: “even_variable_divided_powers”.
The divided-power structure on the algebra obtained by adjoining an even variable of positive degree.
public noncomputable def evenVariableDividedPowerStructure
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(γ : DividedPowerStructure 𝒜) :
DividedPowerStructure (EvenVariableAlgebra.grade 𝒜 d)
DividedPowers.TateResolution.dpow_coeffEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableDividedPowers/Structure.lean, line 393. The attribute's comment: “even_variable_divided_powers”.
The new divided powers restrict to the original structure on
A.
public theorem dpow_coeffEmbedding
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(γ : DividedPowerStructure 𝒜) (n : ℕ) {x : A}
(hx : x ∈ positiveEvenPart 𝒜) :
(evenVariableDividedPowerStructure d hd γ).dpow n (coeffEmbedding x) =
coeffEmbedding (γ.dpow n x)
DividedPowers.TateResolution.dpow_monomial_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableDividedPowers/Structure.lean, line 404. The attribute's comment: “even_variable_divided_powers”.
The divided powers of the formal monomial
T⁽ⁱ⁾.
public theorem dpow_monomial_one
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(γ : DividedPowerStructure 𝒜) (n i : ℕ) (hi : 0 < i) :
(evenVariableDividedPowerStructure d hd γ).dpow n (monomial i (1 : A)) =
monomial (n * i) (dividedPowerMonomialCoefficient n i • (1 : A))
DividedPowers.TateResolution.dpow_positivePolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableDividedPowers/Structure.lean, line 432. The attribute's comment: “even_variable_divided_powers”.
The multinomial expansion for a finite sum of positive-exponent terms whose coefficients are even.
public theorem dpow_positivePolynomial
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(γ : DividedPowerStructure 𝒜) (n : ℕ)
(x : EvenVariableAlgebra A)
(hzero : x.coeff 0 = 0)
(heven : ∀ i : ℕ, 0 < i → x.coeff i ∈
evenPart 𝒜) :
(evenVariableDividedPowerStructure d hd γ).dpow n x =
positivePolynomialDividedPower n x
DividedPowers.TateResolution.dpow_coeff_add_positive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableDividedPowers/Structure.lean, line 579. The attribute's comment: “even_variable_divided_powers”.
Adding a positive-even constant coefficient obeys the divided-power binomial formula.
public theorem dpow_coeff_add_positive
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(γ : DividedPowerStructure 𝒜) (n : ℕ)
{x₀ : A} (hx₀ : x₀ ∈ positiveEvenPart 𝒜)
(x : EvenVariableAlgebra A)
(hzero : x.coeff 0 = 0)
(heven : ∀ i : ℕ, 0 < i → x.coeff i ∈
evenPart 𝒜) :
(evenVariableDividedPowerStructure d hd γ).dpow n (coeffEmbedding x₀ + x) =
∑ ij ∈ Finset.antidiagonal n,
coeffEmbedding (γ.dpow ij.1 x₀) *
(evenVariableDividedPowerStructure d hd γ).dpow ij.2 x
DividedPowers.TateResolution.evenVariableDividedPowerStructure_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableDividedPowers/Structure.lean, line 607. The attribute's comment: “even_variable_divided_powers”.
Compatibility and the formal-monomial rule determine the divided-power structure uniquely.
public theorem evenVariableDividedPowerStructure_unique
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(γ : DividedPowerStructure 𝒜)
(δ : DividedPowerStructure (EvenVariableAlgebra.grade 𝒜 d))
(hcompat : ∀ (n : ℕ) {x : A},
x ∈ positiveEvenPart 𝒜 →
δ.dpow n (coeffEmbedding x) = coeffEmbedding (γ.dpow n x))
(hmonomial : ∀ (n i : ℕ), 0 < i →
δ.dpow n (monomial i (1 : A)) =
monomial (n * i) (dividedPowerMonomialCoefficient n i • (1 : A))) :
δ = evenVariableDividedPowerStructure d hd γ
DividedPowers.TateResolution.evenVariableAlgebra_ringHom_dpow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableLift.lean, line 89. The attribute's comment: “mapping property”.
A degree-preserving ring homomorphism out of an even variable algebra which restricts to a divided-power compatible map on the coefficients is itself compatible with divided powers.
public theorem evenVariableAlgebra_ringHom_dpow
(h : B →+* D)
(hdpow : ∀ (n : ℕ) (b : B), b ∈ positiveEvenPart ℬ → δ.dpow n (h b) = h (β.dpow n b))
(d : ℕ) [Fact (Even d)] (hd : 0 < d) (t : D) (ht : t ∈ 𝒟 d)
(g : EvenVariableAlgebra B →+* D)
(hg1 : ∀ b : B, g (coeffEmbedding b) = h b)
(hg2 : ∀ n : ℕ, g (monomial n (1 : B)) = δ.dpow n t)
(hg3 : ∀ (m : ℕ) (x : EvenVariableAlgebra B),
x ∈ EvenVariableAlgebra.grade ℬ d m → g x ∈ 𝒟 m)
(n : ℕ) (x : EvenVariableAlgebra B)
(hx : x ∈ positiveEvenPart (EvenVariableAlgebra.grade ℬ d)) :
δ.dpow n (g x) = g ((evenVariableDividedPowerStructure d hd β).dpow n x)
DividedPowers.TateResolution.existsUnique_evenVariableAlgebra_ringHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/VariableLift.lean, line 390. The attribute's comment: “mapping property”.
The mapping property of the even variable algebra of Tag 09PI, for ring homomorphisms. A ring homomorphism out of
B⟨T⟩is determined by, and may be prescribed by, its restriction toBtogether with a choice of images for the divided powers ofT, which must be the divided powers of a single element of degreed.
public theorem existsUnique_evenVariableAlgebra_ringHom
(h : B →+* D) (hgrade : ∀ (m : ℕ) (b : B), b ∈ ℬ m → h b ∈ 𝒟 m)
(d : ℕ) (hd : 0 < d) (heven : Even d) (t : D) (ht : t ∈ 𝒟 d) :
∃! g : EvenVariableAlgebra B →+* D,
(∀ b : B, g (coeffEmbedding b) = h b) ∧
(∀ n : ℕ, g (monomial n (1 : B)) = δ.dpow n t) ∧
(∀ (m : ℕ) (x : EvenVariableAlgebra B),
x ∈ EvenVariableAlgebra.grade ℬ d m → g x ∈ 𝒟 m)
Tag 0F4I, a remark
Tag 0F4I in the Stacks Project.
DividedPowers.TateResolution.ringHom_dpow_of_finiteVariableStage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/GradedProduct.lean, line 153. The attribute's comment: “divided powers on a finite stage”.
Compatibility with divided powers propagates from the coefficients and the adjoined variables to a whole finite variable stage. The argument is that the graph of the homomorphism is a subring of the product containing the images of the generators, and that finite variable stages of the product are stable under its divided powers.
This supersedes the
privatemap_dpow_of_finiteVariableStageofStacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/Construction.lean, generalized from an algebra homomorphism to a ring homomorphism commuting with the structure maps.
public theorem ringHom_dpow_of_finiteVariableStage
{R : Type u} {P : Type v} {C : Type z} {D : Type*} {J : Type w}
[CommRing R] [Ring P] [Ring C] [Ring D]
[Algebra R P] [Algebra R C] [Algebra R D]
(Pᵢ : ℕ → Submodule R P) [GradedAlgebra Pᵢ]
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ] [IsStrictlyGradedComm Cᵢ]
(Dᵢ : ℕ → Submodule R D) [GradedAlgebra Dᵢ] [IsStrictlyGradedComm Dᵢ]
(δ : DividedPowerStructure Cᵢ) (ε : DividedPowerStructure Dᵢ)
(ι : P →ₐ[R] C) (T : J → C) (S : Finset J) (d : ℕ)
(hgrade : ∀ (m : ℕ) (a : P), a ∈ Pᵢ m → ι a ∈ Cᵢ m)
(hT : ∀ j : J, T j ∈ Cᵢ d)
(hclosed : ∀ (n : ℕ) (a : P), ι a ∈ positiveEvenPart Cᵢ →
δ.dpow n (ι a) ∈ Set.range ι)
(f : C →+* D) (hf : ∀ (m : ℕ) (x : C), x ∈ Cᵢ m → f x ∈ Dᵢ m)
(hfalg : ∀ r : R, f (algebraMap R C r) = algebraMap R D r)
(hcoeff : ∀ (n : ℕ) (a : P), ι a ∈ positiveEvenPart Cᵢ →
ε.dpow n (f (ι a)) = f (δ.dpow n (ι a)))
(hgen : ∀ (n : ℕ) (j : J), T j ∈ positiveEvenPart Cᵢ →
ε.dpow n (f (T j)) = f (δ.dpow n (T j)))
{x : C} (hx : x ∈ finiteVariableStage δ ι T S)
(hp : x ∈ positiveEvenPart Cᵢ) (n : ℕ) :
ε.dpow n (f x) = f (δ.dpow n x)
DividedPowers.TateResolution.finiteVariableStages_directedColimit_addHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableDerivation.lean, line 153. The attribute's comment: “directed colimit of finite stages, additively”.
The additive analogue of
finiteVariableStages_directedColimit: if the finite variable stages cover the extension, a family of additive maps out of them which agree wherever their arguments agree extends uniquely to an additive map out of the whole extension.
public theorem finiteVariableStages_directedColimit_addHom
{R : Type u} {A : Type v} {C : Type z} {D : Type w} {J : Type*}
[CommRing R] [Ring A] [Ring C] [AddCommGroup D] [Algebra R A] [Algebra R C]
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ]
[IsStrictlyGradedComm Cᵢ] (δ : DividedPowerStructure Cᵢ)
(ι : A →ₐ[R] C) (T : J → C)
(hfinite : ∀ x : C, ∃ S : Finset J, x ∈ finiteVariableStage δ ι T S)
(f : (S : Finset J) → finiteVariableStage δ ι T S →+ D)
(hcompat : ∀ (S U : Finset J)
(x : finiteVariableStage δ ι T S)
(y : finiteVariableStage δ ι T U),
(x : C) = (y : C) → f S x = f U y) :
∃! g : C →+ D,
∀ (S : Finset J) (x : finiteVariableStage δ ι T S),
g (x : C) = f S x
DividedPowers.TateResolution.exists_gradedDividedPowerColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/Construction/DirectLimit.lean, line 299. The attribute's comment: “directed colimit of graded algebras with divided powers”.
The colimit of a directed system of strictly graded-commutative nonnegatively graded algebras with divided powers on their positive even parts, indexed by an arbitrary nonempty directed preorder.
The colimit is graded by the elements coming from a homogeneous element of some stage, carries the unique divided power structure for which every stage map preserves divided powers, and has both the algebra and the module universal property: the first produces maps of graded algebras with divided powers, the second — which is what a colimit of differentials needs, a differential being linear and not multiplicative — produces
R-linear maps. Every element of the colimit, homogeneous or not, comes from a stage, and two stage elements with the same image in the colimit already agree at a later stage.
public theorem exists_gradedDividedPowerColimit
{R : Type u} [CommRing R] {I : Type w}
[Preorder I] [IsDirectedOrder I] [Nonempty I]
(B : I → Type v) [stageRing : ∀ S, Ring (B S)] [stageAlgebra : ∀ S, Algebra R (B S)]
(Bᵢ : (S : I) → ℕ → Submodule R (B S))
[stageGraded : ∀ S, GradedAlgebra (Bᵢ S)]
[stageComm : ∀ S, IsStrictlyGradedComm (Bᵢ S)]
(γ : (S : I) → DividedPowerStructure (Bᵢ S))
(transition : ∀ {S T : I}, S ≤ T → B S →ₐ[R] B T)
(htransition_self : ∀ (S : I) (x : B S), transition (le_refl S) x = x)
(htransition_comp : ∀ {S T U : I} (h : S ≤ T) (h' : T ≤ U) (x : B S),
transition h' (transition h x) = transition (h.trans h') x)
(htransition_grade : ∀ {S T : I} (h : S ≤ T) (m : ℕ) (x : B S),
x ∈ Bᵢ S m → transition h x ∈ Bᵢ T m)
(htransition_dpow : ∀ {S T : I} (h : S ≤ T) (n : ℕ) (x : B S),
x ∈ positiveEvenPart (Bᵢ S) →
transition h ((γ S).dpow n x) = (γ T).dpow n (transition h x)) :
∃ (C : Type (max v w)) (ringC : Ring C),
letI : Ring C := ringC
∃ algebraC : Algebra R C,
letI : Algebra R C := algebraC
∃ (Cᵢ : ℕ → Submodule R C) (gradedC : GradedAlgebra Cᵢ),
letI : GradedAlgebra Cᵢ := gradedC
∃ strictC : IsStrictlyGradedComm Cᵢ,
letI : IsStrictlyGradedComm Cᵢ := strictC
∃ (δ : DividedPowerStructure Cᵢ) (incl : (S : I) → B S →ₐ[R] C),
(∀ {S T : I} (h : S ≤ T) (x : B S), incl T (transition h x) = incl S x) ∧
(∀ (S : I) (m : ℕ) (x : B S), x ∈ Bᵢ S m → incl S x ∈ Cᵢ m) ∧
(∀ (m : ℕ) (x : C), x ∈ Cᵢ m →
∃ (S : I) (y : B S), y ∈ Bᵢ S m ∧ incl S y = x) ∧
(∀ x : C, ∃ (S : I) (y : B S), incl S y = x) ∧
(∀ (S : I) (n : ℕ) (x : B S), x ∈ positiveEvenPart (Bᵢ S) →
δ.dpow n (incl S x) = incl S ((γ S).dpow n x)) ∧
(∀ (S T : I) (x : B S) (y : B T), incl S x = incl T y →
∃ U : I, ∃ (hS : S ≤ U) (hT : T ≤ U),
transition hS x = transition hT y) ∧
(∀ {D : Type z} [Ring D] [Algebra R D] (Dᵢ : ℕ → Submodule R D)
[GradedAlgebra Dᵢ] [IsStrictlyGradedComm Dᵢ]
(ε : DividedPowerStructure Dᵢ) (g : (S : I) → B S →ₐ[R] D),
(∀ {S T : I} (h : S ≤ T) (x : B S), g T (transition h x) = g S x) →
(∀ (S : I) (m : ℕ) (x : B S), x ∈ Bᵢ S m → g S x ∈ Dᵢ m) →
(∀ (S : I) (n : ℕ) (x : B S), x ∈ positiveEvenPart (Bᵢ S) →
ε.dpow n (g S x) = g S ((γ S).dpow n x)) →
∃! F : C →ₐ[R] D,
(∀ (S : I) (x : B S), F (incl S x) = g S x) ∧
(∀ (m : ℕ) (x : C), x ∈ Cᵢ m → F x ∈ Dᵢ m) ∧
(∀ (n : ℕ) (x : C), x ∈ positiveEvenPart Cᵢ →
ε.dpow n (F x) = F (δ.dpow n x))) ∧
∀ {M : Type y} [AddCommGroup M] [Module R M] (g : (S : I) → B S →ₗ[R] M),
(∀ {S T : I} (h : S ≤ T) (x : B S), g T (transition h x) = g S x) →
∃! F : C →ₗ[R] M, ∀ (S : I) (x : B S), F (incl S x) = g S x
DividedPowers.TateResolution.exists_setVariableDividedPowerExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/Construction/Existence.lean, line 414. The attribute's comment: “set-indexed construction”.
A set of positive-degree variables has a free strictly graded-commutative algebra with divided powers over a graded divided-power algebra. Every element involves only finitely many variables (including their divided powers). The universal property fixes the coefficient and generator maps, and requires target maps to preserve grading and divided powers.
public theorem exists_setVariableDividedPowerExtension
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ]
[IsStrictlyGradedComm Aᵢ] (γ : DividedPowerStructure Aᵢ)
(J : Type w) (deg : J → ℕ) (hdeg : ∀ j, 0 < deg j) :
∃ (C : Type (max u v w)) (ringC : Ring C),
letI : Ring C := ringC
∃ (algebraC : Algebra R C),
letI : Algebra R C := algebraC
∃ (Cᵢ : ℕ → Submodule R C) (gradedC : GradedAlgebra Cᵢ),
letI : GradedAlgebra Cᵢ := gradedC
∃ (strictC : IsStrictlyGradedComm Cᵢ),
letI : IsStrictlyGradedComm Cᵢ := strictC
∃ (δ : DividedPowerStructure Cᵢ) (ι : A →ₐ[R] C) (T : J → C),
Function.Injective ι ∧
(∀ (m : ℕ) (a : A), a ∈ Aᵢ m → ι a ∈ Cᵢ m) ∧
(∀ (n : ℕ) (a : A), a ∈ positiveEvenPart Aᵢ →
δ.dpow n (ι a) = ι (γ.dpow n a)) ∧
(∀ j : J, T j ∈ Cᵢ (deg j)) ∧
(∀ x : C, ∃ S : Finset J,
x ∈ finiteVariableStage δ ι T S) ∧
(∀ (S : Finset J) (j : J), j ∉ S →
letI : DecidableEq J := Classical.decEq J
∃ (aS : Algebra R (finiteVariableStage δ ι T S)),
letI : Algebra R (finiteVariableStage δ ι T S) := aS
(∀ r : R, ((algebraMap R (finiteVariableStage δ ι T S) r :
finiteVariableStage δ ι T S) : C) = algebraMap R C r) ∧
∃ (Sᵢ : ℕ → Submodule R (finiteVariableStage δ ι T S))
(gS : GradedAlgebra Sᵢ),
letI : GradedAlgebra Sᵢ := gS
∃ (cS : IsStrictlyGradedComm Sᵢ),
letI : IsStrictlyGradedComm Sᵢ := cS
∃ δS : DividedPowerStructure Sᵢ,
(∀ (n : ℕ) (b : finiteVariableStage δ ι T S),
b ∈ positiveEvenPart Sᵢ →
(δS.dpow n b : C) = δ.dpow n (b : C)) ∧
(∀ hodd : Odd (deg j),
∃ e : OddVariableExtension Sᵢ (deg j) ≃+*
finiteVariableStage δ ι T (insert j S),
(∀ b : finiteVariableStage δ ι T S,
((e (OddVariableExtension.inclusion
Sᵢ (deg j) b) : finiteVariableStage δ ι T (insert j S)) : C) = b) ∧
((e (OddVariableExtension.generator
Sᵢ (deg j)) : finiteVariableStage δ ι T (insert j S)) : C) = T j ∧
(∀ (m : ℕ)
(x : OddVariableExtension Sᵢ (deg j)),
x ∈
OddVariableExtension.grade
Sᵢ (deg j) m ↔
(e x : C) ∈ Cᵢ m) ∧
(∀ (n : ℕ)
(x : OddVariableExtension Sᵢ (deg j)),
x ∈ positiveEvenPart
(OddVariableExtension.grade Sᵢ (deg j)) →
δ.dpow n (e x : C) =
(e ((oddVariableDividedPowerStructure
Sᵢ δS (deg j) (hdeg j) hodd).dpow n x) : C))) ∧
(∀ heven : Even (deg j),
letI : Fact (Even (deg j)) := ⟨heven⟩
∃ e : EvenVariableAlgebra
(finiteVariableStage δ ι T S) ≃+*
finiteVariableStage δ ι T (insert j S),
(∀ b : finiteVariableStage δ ι T S,
((e (EvenVariableAlgebra.coeffEmbedding
b) :
finiteVariableStage δ ι T (insert j S)) : C) = b) ∧
((e (EvenVariableAlgebra.monomial
1 1) : finiteVariableStage δ ι T (insert j S)) : C) = T j ∧
(∀ (m : ℕ)
(x : EvenVariableAlgebra
(finiteVariableStage δ ι T S)),
x ∈
EvenVariableAlgebra.grade
Sᵢ (deg j) m ↔
(e x : C) ∈ Cᵢ m) ∧
(∀ (n : ℕ)
(x : EvenVariableAlgebra
(finiteVariableStage δ ι T S)),
x ∈ positiveEvenPart
(EvenVariableAlgebra.grade Sᵢ (deg j)) →
δ.dpow n (e x : C) =
(e ((evenVariableDividedPowerStructure (deg j) (hdeg j)
δS).dpow n x) : C)))) ∧
(∀ {D : Type z} [Ring D] [Algebra R D]
(Dᵢ : ℕ → Submodule R D) [GradedAlgebra Dᵢ]
[IsStrictlyGradedComm Dᵢ] (ε : DividedPowerStructure Dᵢ)
(f : A →ₐ[R] D) (t : J → D),
(∀ (m : ℕ) (a : A), a ∈ Aᵢ m → f a ∈ Dᵢ m) →
(∀ (n : ℕ) (a : A), a ∈ positiveEvenPart Aᵢ →
ε.dpow n (f a) = f (γ.dpow n a)) →
(∀ j : J, t j ∈ Dᵢ (deg j)) →
∃! g : C →ₐ[R] D,
(∀ a : A, g (ι a) = f a) ∧
(∀ j : J, g (T j) = t j) ∧
(∀ (m : ℕ) (x : C), x ∈ Cᵢ m → g x ∈ Dᵢ m) ∧
(∀ (n : ℕ) (x : C), x ∈ positiveEvenPart Cᵢ →
ε.dpow n (g x) = g (δ.dpow n x)))
DividedPowers.TateResolution.finiteVariableStage_insert, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/FiniteStage/DirectedColimit.lean, line 74. The attribute's comment: “finite iterated one-variable extensions”.
A successor finite stage is obtained by adjoining its new variable and all of its divided powers to the preceding stage. For an odd-degree variable its positive divided powers vanish, recovering the exterior successor; in even degree this is the divided-power successor. Iterating this equation over an enumeration of a finite set gives the finite stages used in the directed colimit.
public theorem finiteVariableStage_insert
{R : Type u} {A : Type v} {C : Type z} {J : Type w}
[CommRing R] [Ring A] [Ring C] [Algebra R A] [Algebra R C]
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ]
[IsStrictlyGradedComm Cᵢ] (δ : DividedPowerStructure Cᵢ)
(ι : A →ₐ[R] C) (T : J → C) (S U : Finset J) (j : J)
(hSU : S ⊆ U) (hj : j ∈ U)
(hU : ∀ k : J, k ∈ U → (k ∈ S ∨ k = j)) :
finiteVariableStage δ ι T U =
Subring.closure
((finiteVariableStage δ ι T S : Set C) ∪
{x : C | x = T j ∨ ∃ n : ℕ, x = δ.dpow n (T j)})
DividedPowers.TateResolution.finiteVariableStage_empty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/FiniteStage/DirectedColimit.lean, line 114. The attribute's comment: “initial finite stage”.
The initial finite stage is generated by the coefficient algebra.
public theorem finiteVariableStage_empty
{R : Type u} {A : Type v} {C : Type z} {J : Type w}
[CommRing R] [Ring A] [Ring C] [Algebra R A] [Algebra R C]
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ]
[IsStrictlyGradedComm Cᵢ] (δ : DividedPowerStructure Cᵢ)
(ι : A →ₐ[R] C) (T : J → C) :
finiteVariableStage δ ι T ∅ = Subring.closure (Set.range ι)
DividedPowers.TateResolution.finiteVariableStages_directedColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/FiniteStage/DirectedColimit.lean, line 141. The attribute's comment: “directed colimit of finite stages”.
If the finite-variable stages cover the algebra, they present it as their directed colimit: a family of ring homomorphisms out of the stages which agree wherever their arguments agree in the ambient algebra extends uniquely to a ring homomorphism out of the whole algebra.
public theorem finiteVariableStages_directedColimit
{R : Type u} {A : Type v} {C : Type z} {D : Type w} {J : Type*}
[CommRing R] [Ring A] [Ring C] [Ring D] [Algebra R A] [Algebra R C]
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ]
[IsStrictlyGradedComm Cᵢ] (δ : DividedPowerStructure Cᵢ)
(ι : A →ₐ[R] C) (T : J → C)
(hfinite : ∀ x : C, ∃ S : Finset J,
x ∈ finiteVariableStage δ ι T S)
(f : (S : Finset J) → finiteVariableStage δ ι T S →+* D)
(hcompat : ∀ (S U : Finset J)
(x : finiteVariableStage δ ι T S)
(y : finiteVariableStage δ ι T U),
(x : C) = (y : C) → f S x = f U y) :
∃! g : C →+* D,
∀ (S : Finset J) (x : finiteVariableStage δ ι T S),
g (x : C) = f S x
DividedPowers.TateResolution.existsUnique_dividedPowerStructure_of_finiteStages, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/FiniteStage/DividedPowerStructure.lean, line 457. The attribute's comment: “finite-stage extension”.
Let a directed system of strictly graded-commutative graded algebras with divided powers, indexed by a nonempty directed preorder, map compatibly to a strictly graded-commutative graded algebra
Cin such a way that homogeneous elements ofClift to some stage and two stage elements with the same image inCalready agree at a later stage. ThenCcarries exactly one divided power structure for which every stage map preserves divided powers.The index order is an arbitrary nonempty directed one; the finite subsets of a set ordered by inclusion, which is the indexing of the set-variable construction of Tag 0F4I, are the special case
I = Finset J, and anℕ-indexed tower is the caseI = ℕ.
public theorem existsUnique_dividedPowerStructure_of_finiteStages
{R : Type u} [CommRing R] {I : Type w} [LE I] [IsDirectedOrder I] [Nonempty I]
(B : I → Type v)
[stageRing : ∀ S, Ring (B S)]
[stageAlgebra : ∀ S, Algebra R (B S)]
(Bᵢ : (S : I) → ℕ → Submodule R (B S))
[stageGraded : ∀ S, GradedAlgebra (Bᵢ S)]
[stageComm : ∀ S, IsStrictlyGradedComm (Bᵢ S)]
(γ : (S : I) → DividedPowerStructure (Bᵢ S))
{C : Type z} [Ring C] [Algebra R C]
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ] [IsStrictlyGradedComm Cᵢ]
(transition : ∀ {S T : I}, S ≤ T → B S →ₐ[R] B T)
(ι : (S : I) → B S →ₐ[R] C)
(hι : ∀ {S T : I} (h : S ≤ T) (x : B S),
ι T (transition h x) = ι S x)
(hgrade : ∀ (S : I) (m : ℕ) (x : B S),
x ∈ Bᵢ S m → ι S x ∈ Cᵢ m)
(hgrade_lift : ∀ (m : ℕ) (x : C), x ∈ Cᵢ m →
∃ (S : I) (y : B S), y ∈ Bᵢ S m ∧ ι S y = x)
(heq : ∀ (S T : I) (x : B S) (y : B T),
ι S x = ι T y →
∃ U : I, ∃ (hS : S ≤ U) (hT : T ≤ U),
transition hS x = transition hT y)
(htransition_grade : ∀ {S T : I} (h : S ≤ T)
(m : ℕ) (x : B S), x ∈ Bᵢ S m → transition h x ∈ Bᵢ T m)
(htransition_dpow : ∀ {S T : I} (h : S ≤ T)
(n : ℕ) (x : B S), x ∈ positiveEvenPart (Bᵢ S) →
transition h ((γ S).dpow n x) = (γ T).dpow n (transition h x)) :
∃! δ : DividedPowerStructure Cᵢ,
∀ (S : I) (n : ℕ) (x : B S),
x ∈ positiveEvenPart (Bᵢ S) →
δ.dpow n (ι S x) = ι S ((γ S).dpow n x)
DividedPowers.TateResolution.finiteVariableStage_dpow_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/FiniteStage/DividedPowerStructure.lean, line 705. The attribute's comment: “finite stages preserve divided powers”.
Divided powers of elements supported on a finite set of homogeneous variables over a graded coefficient algebra are still supported on that set. The variables need not all have the same degree: each
T jis homogeneous of its own degreedeg j. The coefficient map preserves grading, as do the inclusions in the extensions of Tags 09PH and 09PI. Thus every finite-variable stage is a divided-power subalgebra.
public theorem finiteVariableStage_dpow_mem
{R : Type u} {A : Type v} {C : Type z} {J : Type w}
[CommRing R] [Ring A] [Ring C] [Algebra R A] [Algebra R C]
(Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ]
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ]
[IsStrictlyGradedComm Cᵢ] (δ : DividedPowerStructure Cᵢ)
(ι : A →ₐ[R] C) (T : J → C) (S : Finset J) (deg : J → ℕ)
(hgrade : ∀ (m : ℕ) (a : A), a ∈ Aᵢ m → ι a ∈ Cᵢ m)
(hT : ∀ j : J, T j ∈ Cᵢ (deg j))
(hcoeff : ∀ (n : ℕ) (a : A), ι a ∈ positiveEvenPart Cᵢ →
δ.dpow n (ι a) ∈ Set.range ι)
(n : ℕ) (x : C)
(hx : x ∈ finiteVariableStage δ ι T S)
(hpositive : x ∈ positiveEvenPart Cᵢ) :
δ.dpow n x ∈ finiteVariableStage δ ι T S
DividedPowers.TateResolution.dividedPowerStructure_unique_of_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableExtension/FiniteStage/DividedPowerStructure.lean, line 1195. The attribute's comment: “uniqueness”.
On a set-indexed extension, divided powers are forced by their restriction to the coefficient algebra and by their values on the adjoined generators.
public theorem dividedPowerStructure_unique_of_generators
{R : Type u} {A : Type v} {C : Type z} {J : Type w}
[CommRing R] [Ring A] [Ring C] [Algebra R A] [Algebra R C]
(Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ]
(d : ℕ) (hd : 0 < d)
(Cᵢ : ℕ → Submodule R C) [GradedAlgebra Cᵢ]
[IsStrictlyGradedComm Cᵢ]
(δ ε : DividedPowerStructure Cᵢ) (ι : A →ₐ[R] C) (T : J → C)
(hgrade : ∀ (m : ℕ) (a : A), a ∈ Aᵢ m → ι a ∈ Cᵢ m)
(hT : ∀ j : J, T j ∈ Cᵢ d)
(hfinite : ∀ x : C, ∃ S : Finset J, x ∈ finiteVariableStage δ ι T S)
(hcoeff : ∀ (n : ℕ) (a : A), ι a ∈ positiveEvenPart Cᵢ →
ε.dpow n (ι a) = δ.dpow n (ι a))
(hgenerator : ∀ (n : ℕ) (j : J), T j ∈ positiveEvenPart Cᵢ →
ε.dpow n (T j) = δ.dpow n (T j)) :
ε = δ
Tag 09PJ, a definition
Tag 09PJ in the Stacks Project.
DividedPowers.TateResolution.IsCompatibleWithDifferential, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/Basic.lean, line 261.
A divided power structure is compatible with a differential if the differential of every positive divided power has the expected divided-power derivative.
public class IsCompatibleWithDifferential {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜]
[IsStrictlyGradedComm 𝒜] (γ : DividedPowerStructure 𝒜) (d : A →ₗ[R] A) : Prop
Tag 09PK, a lemma
Tag 09PK in the Stacks Project.
DividedPowers.TateResolution.dividedPowerStructureOnHomology_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/Homology/DividedPowerStructure.lean, line 37.
A surjective morphism from a positively acyclic divided-power DGA induces divided powers on the actual homology quotient of its target. The induced operations agree with the original operations on homogeneous cycles.
public theorem dividedPowerStructureOnHomology_of_surjective
{R : Type u} {A : Type v} {B : Type w}
[CommRing R] [Ring A] [Ring B]
[Algebra R A] [Algebra R B]
(𝒜 : ℕ → Submodule R A) (ℬ : ℕ → Submodule R B)
[GradedAlgebra 𝒜] [GradedAlgebra ℬ]
[IsStrictlyGradedComm 𝒜] [IsStrictlyGradedComm ℬ]
(dA : A →ₗ[R] A) (dB : B →ₗ[R] B)
[IsDifferentialGradedAlgebra 𝒜 dA] [IsDifferentialGradedAlgebra ℬ dB]
(γA : DividedPowerStructure 𝒜) (γB : DividedPowerStructure ℬ)
[IsCompatibleWithDifferential γA dA] [IsCompatibleWithDifferential γB dB]
(f : A →ₐ[R] B)
(hf_grade : ∀ {n : ℕ} {x : A}, x ∈ 𝒜 n → f x ∈ ℬ n)
(hf_d : ∀ x : A, f (dA x) = dB (f x))
(hf_dpow : ∀ {n : ℕ} {x : A}, x ∈ positiveEvenPart 𝒜 →
f (γA.dpow n x) = γB.dpow n (f x))
(hf_surjective : Function.Surjective f)
(hA : ∀ {n : ℕ}, 0 < n → ∀ {x : A}, x ∈ 𝒜 n → dA x = 0 →
∃ z : A, z ∈ 𝒜 (n + 1) ∧ dA z = x)
: ∃ hRing : Ring (Homology (𝒜 := ℬ) dB),
letI : Ring (Homology (𝒜 := ℬ) dB) := hRing
∃ hAlgebra : Algebra R (Homology (𝒜 := ℬ) dB),
letI : Algebra R (Homology (𝒜 := ℬ) dB) := hAlgebra
letI : AddCommMonoid (Homology (𝒜 := ℬ) dB) := hRing.toAddCommMonoid
letI : Module R (Homology (𝒜 := ℬ) dB) := Algebra.toModule
let ℋ : ℕ → Submodule R (Homology (𝒜 := ℬ) dB) := fun n =>
Submodule.span R {z | ∃ x : cycles dB, (x : B) ∈ ℬ n ∧
(Submodule.Quotient.mk x : Homology (𝒜 := ℬ) dB) = z}
∃ hGraded : GradedAlgebra ℋ,
letI : GradedAlgebra ℋ := hGraded
∃ hStrict : IsStrictlyGradedComm ℋ,
letI : IsStrictlyGradedComm ℋ := hStrict
∃ γH : @DividedPowerStructure R (Homology (𝒜 := ℬ) dB)
_ hRing hAlgebra ℋ hGraded hStrict,
(Submodule.Quotient.mk (0 : cycles dB) :
Homology (𝒜 := ℬ) dB) = 0 ∧
(∀ x y : cycles dB,
(Submodule.Quotient.mk (x + y) : Homology (𝒜 := ℬ) dB) =
Submodule.Quotient.mk x + Submodule.Quotient.mk y) ∧
(∀ (r : R) (x : cycles dB),
(Submodule.Quotient.mk (r • x) : Homology (𝒜 := ℬ) dB) =
r • (Submodule.Quotient.mk x : Homology (𝒜 := ℬ) dB)) ∧
(∃ h1 : dB (1 : B) = 0,
(Submodule.Quotient.mk (⟨1, h1⟩ : cycles dB) :
Homology (𝒜 := ℬ) dB) = 1) ∧
(∀ {x y : B} (hx : dB x = 0) (hy : dB y = 0),
∃ hxy : dB (x * y) = 0,
(Submodule.Quotient.mk (⟨x * y, hxy⟩ : cycles dB) :
Homology (𝒜 := ℬ) dB) =
Submodule.Quotient.mk (⟨x, hx⟩ : cycles dB) *
Submodule.Quotient.mk (⟨y, hy⟩ : cycles dB)) ∧
(∀ {n : ℕ} {x : B} (_hx : x ∈ positiveEvenPart ℬ)
(hd : dB x = 0),
∃ hγ : dB (γB.dpow n x) = 0,
γH.dpow n (Submodule.Quotient.mk (⟨x, hd⟩ : cycles dB)) =
Submodule.Quotient.mk (⟨γB.dpow n x, hγ⟩ : cycles dB))
Tag 09PL, a lemma
Tag 09PL in the Stacks Project.
DividedPowers.TateResolution.exists_dividedPowerStructure_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/FlatTensor/DividedPowerStructure.lean, line 709.
Divided powers and their compatibility with the differential extend under arbitrary base change: for a ring map
R → R', the differential graded algebraR' ⊗[R] Awith grading(𝒜 i).baseChange R'and differentiald.baseChange R'carries divided powersγ'compatible with that differential, andγ'ₙ (1 ⊗ₜ x) = 1 ⊗ₜ γₙ xforxin the positive even part.
public theorem exists_dividedPowerStructure_baseChange
{R : Type u} {R' : Type v} {A : Type w}
[CommRing R] [CommRing R'] [Ring A] [Algebra R R'] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜) (d : A →ₗ[R] A) [IsCompatibleWithDifferential γ d]
(d_sq : d.comp d = 0)
(d_grade_zero : ∀ x : A, x ∈ 𝒜 0 → d x = 0)
(d_mem : ∀ (n : ℕ) (x : A), x ∈ 𝒜 (n + 1) → d x ∈ 𝒜 n)
(d_mul : ∀ (i j : ℕ) (x y : A), x ∈ 𝒜 i → y ∈ 𝒜 j →
d (x * y) = d x * y + (-1 : R) ^ i • (x * d y)) :
let 𝒜' : ℕ → Submodule R' (R' ⊗[R] A) := fun i ↦ (𝒜 i).baseChange R'
let d' := LinearMap.baseChange R' d
∃ hcomm : IsStrictlyGradedComm 𝒜',
letI := hcomm
∃ γ' : DividedPowerStructure 𝒜',
d'.comp d' = 0 ∧
(∀ x : R' ⊗[R] A, x ∈ 𝒜' 0 → d' x = 0) ∧
(∀ (n : ℕ) (x : R' ⊗[R] A), x ∈ 𝒜' (n + 1) → d' x ∈ 𝒜' n) ∧
(∀ (i j : ℕ) (x y : R' ⊗[R] A), x ∈ 𝒜' i → y ∈ 𝒜' j →
d' (x * y) = d' x * y + (-1 : R') ^ i • (x * d' y)) ∧
IsCompatibleWithDifferential γ' d' ∧
∀ (n : ℕ) (x : A), x ∈ positiveEvenPart 𝒜 →
γ'.dpow n (1 ⊗ₜ[R] x) = 1 ⊗ₜ[R] γ.dpow n x
Tag 09PM, a lemma
Tag 09PM in the Stacks Project.
DividedPowers.TateResolution.existsUnique_differential_mixedDegreeSetVariableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableDifferential.lean, line 645. The attribute's comment: “set of variables of prescribed degrees”.
A cycle of degree
deg j - 1for each adjoined variablejdetermines the unique divided-power-compatible differential on an extension by a set of variables of degreesdeg.The extension enters through the data and the properties that the set-indexed construction of Tag 0F4I produces: a grading- and divided-power-preserving coefficient map
ι, variablesTwithT jhomogeneous of degreedeg j, the presentation of every element inside a finite-variable stage, and the universal mapping property. This is Tag 09PM for a whole set of variables of arbitrary prescribed degrees at once, which is what an algebra with variables in every positive degree needs; its single-variable forms areexistsUnique_differential_oddVariableExtensionandexistsUnique_differential_evenVariableAlgebra, and its form for the variables of a single degree, which needs no universal property, isexistsUnique_differential_setVariableExtension.
public theorem existsUnique_differential_mixedDegreeSetVariableExtension
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜) (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] [IsCompatibleWithDifferential γ dA]
(𝒞 : ℕ → Submodule R C) [GradedAlgebra 𝒞] [IsStrictlyGradedComm 𝒞]
(δ : DividedPowerStructure 𝒞) (ι : A →ₐ[R] C) (T : J → C) (deg : J → ℕ)
(hdeg : ∀ j : J, 0 < deg j)
(hι_grade : ∀ (m : ℕ) (a : A), a ∈ 𝒜 m → ι a ∈ 𝒞 m)
(hι_dpow : ∀ (n : ℕ) (a : A), a ∈ positiveEvenPart 𝒜 → δ.dpow n (ι a) = ι (γ.dpow n a))
(hT : ∀ j : J, T j ∈ 𝒞 (deg j))
(hgen : ∀ x : C, ∃ S : Finset J, x ∈ finiteVariableStage δ ι T S)
(huniv : ∀ {D : Type z} [Ring D] [Algebra R D]
(𝒟 : ℕ → Submodule R D) [GradedAlgebra 𝒟] [IsStrictlyGradedComm 𝒟]
(ε : DividedPowerStructure 𝒟) (f : A →ₐ[R] D) (t : J → D),
(∀ (m : ℕ) (a : A), a ∈ 𝒜 m → f a ∈ 𝒟 m) →
(∀ (n : ℕ) (a : A), a ∈ positiveEvenPart 𝒜 → ε.dpow n (f a) = f (γ.dpow n a)) →
(∀ j : J, t j ∈ 𝒟 (deg j)) →
∃! g : C →ₐ[R] D,
(∀ a : A, g (ι a) = f a) ∧ (∀ j : J, g (T j) = t j) ∧
(∀ (m : ℕ) (x : C), x ∈ 𝒞 m → g x ∈ 𝒟 m) ∧
(∀ (n : ℕ) (x : C), x ∈ positiveEvenPart 𝒞 → ε.dpow n (g x) = g (δ.dpow n x)))
(e : J → A) (he_grade : ∀ j : J, e j ∈ 𝒜 (deg j - 1))
(he_cycle : ∀ j : J, dA (e j) = 0) :
∃! dC : C →ₗ[R] C,
IsDifferentialGradedAlgebra 𝒞 dC ∧ (∀ a : A, dC (ι a) = ι (dA a)) ∧
(∀ j : J, dC (T j) = ι (e j)) ∧ IsCompatibleWithDifferential δ dC
DividedPowers.TateResolution.existsUnique_differential_setVariableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SetVariableDifferential.lean, line 973. The attribute's comment: “set of variables”.
The differential of a set-variable divided power extension, the set-indexed form of Tag 09PM. A differential on the coefficient algebra, compatible with its divided powers, together with a cycle of degree
d - 1prescribed as the value on each adjoined variable of degreed, determines the unique divided-power-compatible differential on the extension.This is the inductive step of Tate's construction: at a stage whose cycles in degree
nare to be killed, the variables adjoined in degreen + 1are indexed by those cycles, and the cycle condition is exactly what makes the extended operator square-zero.The variant for variables of arbitrary prescribed degrees, which instead needs the universal property of the extension, is
existsUnique_differential_mixedDegreeSetVariableExtension.
public theorem existsUnique_differential_setVariableExtension
(hC : IsSetVariableExtension Aᵢ γ Cᵢ δ ι T d hd)
(dA : A →ₗ[R] A) [IsDifferentialGradedAlgebra Aᵢ dA] [IsCompatibleWithDifferential γ dA]
(ev : J → A) (hev : ∀ j : J, ev j ∈ Aᵢ (d - 1)) (hcycle : ∀ j : J, dA (ev j) = 0) :
∃! D : C →ₗ[R] C,
IsDifferentialGradedAlgebra Cᵢ D ∧ (∀ a : A, D (ι a) = ι (dA a)) ∧
(∀ j : J, D (T j) = ι (ev j)) ∧ IsCompatibleWithDifferential δ D
DividedPowers.TateResolution.existsUnique_differential_oddVariableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/VariableDifferential/ExistsUnique.lean, line 410. The attribute's comment: “odd variable”.
A closed element of degree
d - 1determines the unique divided-power-compatible differential after adjoining an odd variable of degreed.
public theorem existsUnique_differential_oddVariableExtension
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜) (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] [IsCompatibleWithDifferential γ dA]
(d : ℕ) (hd : 0 < d) (hd_odd : Odd d)
(f : A) (hf_grade : f ∈ 𝒜 (d - 1)) (hf_cycle : dA f = 0) :
∃! dExt : OddVariableExtension 𝒜 d →ₗ[R] OddVariableExtension 𝒜 d,
(IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 d) dExt ∧
(∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 d x) =
OddVariableExtension.inclusion 𝒜 d (dA x)) ∧
dExt (OddVariableExtension.generator 𝒜 d) =
OddVariableExtension.inclusion 𝒜 d f ∧
IsCompatibleWithDifferential
(oddVariableDividedPowerStructure 𝒜 γ d hd hd_odd) dExt)
DividedPowers.TateResolution.existsUnique_differential_evenVariableAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/VariableDifferential/ExistsUnique.lean, line 445. The attribute's comment: “even variable”.
A closed element of degree
d - 1determines the unique divided-power-compatible differential after adjoining an even divided-power variable of degreed.
public theorem existsUnique_differential_evenVariableAlgebra
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜) (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] [IsCompatibleWithDifferential γ dA]
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(f : A) (hf_grade : f ∈ 𝒜 (d - 1)) (hf_cycle : dA f = 0) :
∃! dExt : EvenVariableAlgebra A →ₗ[R] EvenVariableAlgebra A,
(IsDifferentialGradedAlgebra (EvenVariableAlgebra.grade 𝒜 d) dExt ∧
(∀ x : A, dExt (EvenVariableAlgebra.coeffEmbedding x) =
EvenVariableAlgebra.coeffEmbedding (dA x)) ∧
dExt (EvenVariableAlgebra.monomial 1 1) =
EvenVariableAlgebra.coeffEmbedding f ∧
IsCompatibleWithDifferential
(evenVariableDividedPowerStructure d hd γ) dExt)
DividedPowers.TateResolution.existsUnique_gradedDerivation_oddVariableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/VariableDifferential/ExistsUnique.lean, line 500. The attribute's comment: “odd variable, as a graded derivation”.
An element of degree
d - 1, with no cycle condition imposed on it, determines the unique divided-power-compatible graded derivation on the algebra obtained by adjoining an odd variable of degreed. The extension is square-zero precisely when the prescribed value is a cycle, which isexistsUnique_differential_oddVariableExtension; this form is what the square-zero lift of Tag 09PS needs, since there the lifted operator is not square-zero.
public theorem existsUnique_gradedDerivation_oddVariableExtension
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜) (dA : A →ₗ[R] A)
[IsGradedDerivation 𝒜 dA] [IsCompatibleWithDifferential γ dA]
(d : ℕ) (hd : 0 < d) (hd_odd : Odd d)
(f : A) (hf_grade : f ∈ 𝒜 (d - 1)) :
∃! dExt : OddVariableExtension 𝒜 d →ₗ[R] OddVariableExtension 𝒜 d,
(IsGradedDerivation (OddVariableExtension.grade 𝒜 d) dExt ∧
(∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 d x) =
OddVariableExtension.inclusion 𝒜 d (dA x)) ∧
dExt (OddVariableExtension.generator 𝒜 d) =
OddVariableExtension.inclusion 𝒜 d f ∧
IsCompatibleWithDifferential
(oddVariableDividedPowerStructure 𝒜 γ d hd hd_odd) dExt)
DividedPowers.TateResolution.existsUnique_gradedDerivation_evenVariableAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/VariableDifferential/ExistsUnique.lean, line 531. The attribute's comment: “even variable, as a graded derivation”.
An element of degree
d - 1, with no cycle condition imposed on it, determines the unique divided-power-compatible graded derivation on the algebra obtained by adjoining an even divided-power variable of degreed. The extension is square-zero precisely when the prescribed value is a cycle, which isexistsUnique_differential_evenVariableAlgebra.
public theorem existsUnique_gradedDerivation_evenVariableAlgebra
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜) (dA : A →ₗ[R] A)
[IsGradedDerivation 𝒜 dA] [IsCompatibleWithDifferential γ dA]
(d : ℕ) [Fact (Even d)] (hd : 0 < d)
(f : A) (hf_grade : f ∈ 𝒜 (d - 1)) :
∃! dExt : EvenVariableAlgebra A →ₗ[R] EvenVariableAlgebra A,
(IsGradedDerivation (EvenVariableAlgebra.grade 𝒜 d) dExt ∧
(∀ x : A, dExt (EvenVariableAlgebra.coeffEmbedding x) =
EvenVariableAlgebra.coeffEmbedding (dA x)) ∧
dExt (EvenVariableAlgebra.monomial 1 1) =
EvenVariableAlgebra.coeffEmbedding f ∧
IsCompatibleWithDifferential
(evenVariableDividedPowerStructure d hd γ) dExt)
Tag 09PN, a lemma
Tag 09PN in the Stacks Project.
DividedPowers.TateResolution.finiteTateResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/FiniteTateResolution.lean, line 524. The attribute's comment: “finite generators in each degree, for a prescribed presentation”.
Tate's resolution with finitely many generators in each degree, for a prescribed presentation. Let
φ : R[xᵢ] → Sbe a surjection from a polynomial ring whose coefficient ring is Noetherian, and lets₀be a finite generating family ofker φ. Thenφextends to a divided power differential graded algebra overR, free overRin every degree, which is a graded divided power polynomial algebra overR[xᵢ]on finitely many variables in each degree, and whose augmentation toSis a quasi-isomorphism.The algebra is the colimit of the degreewise finite tower over
R[xᵢ]withs₀as the family of degree-zero cycles to be killed. Exactness in degree zero iss₀generatingker φ; exactness in positive degrees is that the finite family killed at each stage spans the cycles of its degree, which isDividedPowers.TateResolution.hasFiniteSpanningCycles_finiteTateStage. The finiteness of the index sets isDividedPowers.TateResolution.finite_finiteTateIndex.
public noncomputable def finiteTateResolution (φ : MvPolynomial σ R →ₐ[R] S)
(hφ : Function.Surjective φ) (s₀ : Finset (resolutionCoefficientRing R S σ))
(hs₀ : Ideal.span (↑s₀ : Set (resolutionCoefficientRing R S σ)) =
RingHom.ker (resolutionPresentation φ))
[IsNoetherianRing (resolutionCoefficientRing R S σ)] :
Resolution R S σ φ
DividedPowers.TateResolution.finite_finiteTateResolution_polynomialIndices, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/FiniteTateResolution.lean, line 582. The attribute's comment: “finite generators in each degree, for a prescribed presentation”.
The degreewise finite Tate resolution really is degreewise finite: it has finitely many variables in each degree, which is the finiteness assertion of Tag 09PN. The variables of degree
i + 1are the family chosen at the stageiof the tower, which is finite by construction.
public theorem finite_finiteTateResolution_polynomialIndices (φ : MvPolynomial σ R →ₐ[R] S)
(hφ : Function.Surjective φ) (s₀ : Finset (resolutionCoefficientRing R S σ))
(hs₀ : Ideal.span (↑s₀ : Set (resolutionCoefficientRing R S σ)) =
RingHom.ker (resolutionPresentation φ))
[IsNoetherianRing (resolutionCoefficientRing R S σ)] (i : ℕ) :
Finite ((finiteTateResolution φ hφ s₀ hs₀).polynomialIndices i)
DividedPowers.TateResolution.exists_finite_tateResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/FiniteTateResolution.lean, line 605. The attribute's comment: “finite generators in each degree”.
The finiteness half of Tag 09PN. A Noetherian commutative ring
Rand anR-algebraSof finite type admit a surjectionφ : R[x₁, …, x_k] → Sfrom a polynomial ring in finitely many variables together with a Tate resolution ofSalongφhaving finitely many generators in each degree.The presentation is a finite one, which exists because
Sis of finite type; its coefficient ringR[x₁, …, x_k]is Noetherian becauseRis, byMvPolynomial.isNoetherianRing, so its kernel is generated by a finite family, andDividedPowers.TateResolution.finiteTateResolutionresolves that data.
public theorem exists_finite_tateResolution (R S : Type u) [CommRing R] [CommRing S]
[Algebra R S] [IsNoetherianRing R] [Algebra.FiniteType R S] :
∃ (k : ℕ) (φ : MvPolynomial (Fin k) R →ₐ[R] S) (A : Resolution R S (Fin k) φ),
Function.Surjective φ ∧ ∀ i : ℕ, Finite (A.polynomialIndices i)
DividedPowers.TateResolution.exists_boundary_of_gradeZero_combination, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/FiniteTateTower.lean, line 131. The attribute's comment: “a spanning family kills every cycle of its degree, degree-zero coefficients”.
A combination with coefficients of degree zero of cycles killed by variables is a boundary. If the variable
T jof degreen + 1hasv jfor boundary, then the boundary of the corresponding combination of theT jis the combination of thev j, by linearity of the differential over degree-zero coefficients, and that combination is homogeneous of degreen + 1.So a family of variables whose prescribed cycles span the cycles of a degree kills all of them. This is what makes the degreewise finite tower acyclic; the existence half of Tag 09PN instead prescribes every cycle individually, which is what costs it degreewise finiteness.
public theorem exists_boundary_of_gradeZero_combination {J : Type y} (v T : J → A) (n : ℕ)
(hT : ∀ j : J, T j ∈ Aᵢ (n + 1)) (hdT : ∀ j : J, d (T j) = v j)
(s : Finset J) (c : J → A) (hc : ∀ j : J, c j ∈ Aᵢ 0) :
∃ b : A, b ∈ Aᵢ (n + 1) ∧ d b = ∑ j ∈ s, c j * v j
DividedPowers.TateResolution.hasFiniteSpanningCycles_finiteTateStage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/FiniteTateTower.lean, line 402. The attribute's comment: “finitely many variables suffice at each step over a Noetherian base”.
Over a Noetherian coefficient ring every degree of every stage of the degreewise finite tower has a finite spanning family of cycles, so the empty fallback of
DividedPowers.TateResolution.chosenCycleFinsetis never taken and the tower really does kill every cycle.This is where the two ingredients meet. The stage
Nis a graded divided power polynomial algebra overPbyDividedPowers.TateResolution.chainStagePresentation, with finitely many variables in each degree because the index sets of the tower are finite unconditionally; so each of its homogeneous pieces is a finitely generatedP-module byDividedPowers.TateResolution.GradedDividedPowerPolynomial.fg_coefficientGrade, and over the Noetherian ringPthe submodule of cycles is finitely generated too, which isDividedPowers.TateResolution.exists_finite_spanning_cycles. Its coefficients lie inP, and the coefficient morphism carriesPinto degree zero, which is the spellingDividedPowers.TateResolution.HasFiniteSpanningCyclesasks for.
public theorem hasFiniteSpanningCycles_finiteTateStage [IsNoetherianRing P] (N m : ℕ) :
HasFiniteSpanningCycles
(finiteTateStage (finiteTateBase.{u, v} (R := R) P s₀) N).datum m
DividedPowers.TateResolution.GradedDividedPowerPolynomial.free_grade, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/GradedBasis.lean, line 1080. The attribute's comment: “freeness of the homogeneous pieces”.
Each homogeneous piece is free over the ground ring as soon as the coefficient algebra is. This is the
freefield of a Tate resolution, Tag 09PN.
public theorem free_grade (G : GradedDividedPowerPolynomial Aᵢ γ ι) [Module.Free R P] (n : ℕ) :
Module.Free R ↥(Aᵢ n)
DividedPowers.TateResolution.GradedDividedPowerPolynomial.finite_grade, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/GradedBasis.lean, line 1089. The attribute's comment: “finiteness of the homogeneous pieces”.
Each homogeneous piece is module finite over the ground ring as soon as the coefficient algebra is and there are only finitely many variables in each degree: there are then only finitely many monomials of each degree.
public theorem finite_grade (G : GradedDividedPowerPolynomial Aᵢ γ ι) [Module.Finite R P]
[∀ i : ℕ, Finite (G.indices i)] (n : ℕ) : Module.Finite R ↥(Aᵢ n)
DividedPowers.TateResolution.existsUnique_gradedDividedPowerPolynomial_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/GradedPolynomialMap.lean, line 638. The attribute's comment: “mapping property”.
The mapping property of an iterated graded divided-power polynomial algebra. The target may live in a universe independent of the source and its variables.
public theorem existsUnique_gradedDividedPowerPolynomial_map
{R : Type u} {P : Type v} {A : Type w} {D : Type z}
[CommRing R] [Ring P] [Algebra R P] [Ring A] [Algebra R A]
[Ring D] [Algebra R D]
(Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ]
[IsStrictlyGradedComm Aᵢ] (γ : DividedPowerStructure Aᵢ)
(ι : P →ₐ[R] A) (h : GradedDividedPowerPolynomial Aᵢ γ ι)
(Dᵢ : ℕ → Submodule R D) [GradedAlgebra Dᵢ]
[IsStrictlyGradedComm Dᵢ] (δ : DividedPowerStructure Dᵢ)
(f : P →ₐ[R] D) (hf : ∀ p : P, f p ∈ Dᵢ 0)
(t : (Σ n : ℕ, h.indices n) → D)
(ht : ∀ j, t j ∈ Dᵢ (j.1 + 1)) :
∃! g : A →ₐ[R] D,
(∀ p : P, g (ι p) = f p) ∧
(∀ j : Σ n : ℕ, h.indices n, g (h.generator j) = t j) ∧
(∀ (n : ℕ) (a : A), a ∈ Aᵢ n → g a ∈ Dᵢ n) ∧
(∀ (n : ℕ) (a : A), a ∈ positiveEvenPart Aᵢ →
g (γ.dpow n a) = δ.dpow n (g a))
DividedPowers.TateResolution.existsUnique_algEquiv_gradedDividedPowerPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/GradedPolynomialMap.lean, line 759. The attribute's comment: “uniqueness of the presentation”.
Two graded divided power polynomial algebras over the same coefficient algebra, whose index data are identified degreewise, are uniquely isomorphic over the coefficients and the variables, and the isomorphism preserves the grading and the divided powers in both directions. This is the form in which one recognises a graded divided power polynomial algebra as a base change of another.
public theorem existsUnique_algEquiv_gradedDividedPowerPolynomial
{R : Type u} {P : Type v} {A : Type w} {A' : Type z}
[CommRing R] [Ring P] [Algebra R P] [Ring A] [Algebra R A] [Ring A'] [Algebra R A']
(Aᵢ : ℕ → Submodule R A) [GradedAlgebra Aᵢ] [IsStrictlyGradedComm Aᵢ]
(γ : DividedPowerStructure Aᵢ) (ι : P →ₐ[R] A)
(h : GradedDividedPowerPolynomial Aᵢ γ ι)
(Aᵢ' : ℕ → Submodule R A') [GradedAlgebra Aᵢ'] [IsStrictlyGradedComm Aᵢ']
(γ' : DividedPowerStructure Aᵢ') (ι' : P →ₐ[R] A')
(h' : GradedDividedPowerPolynomial Aᵢ' γ' ι')
(σ : (Σ n : ℕ, h.indices n) ≃ (Σ n : ℕ, h'.indices n))
(hσ : ∀ j, (σ j).1 = j.1) :
∃! e : A ≃ₐ[R] A',
(∀ p : P, e (ι p) = ι' p) ∧
(∀ j, e (h.generator j) = h'.generator (σ j)) ∧
(∀ (n : ℕ) (a : A), a ∈ Aᵢ n → e a ∈ Aᵢ' n) ∧
(∀ (n : ℕ) (a : A), a ∈ positiveEvenPart Aᵢ → e (γ.dpow n a) = γ'.dpow n (e a)) ∧
(∀ (n : ℕ) (a : A'), a ∈ Aᵢ' n → e.symm a ∈ Aᵢ n) ∧
(∀ (n : ℕ) (a : A'), a ∈ positiveEvenPart Aᵢ' →
e.symm (γ'.dpow n a) = γ.dpow n (e.symm a))
DividedPowers.TateResolution.exists_gradedDividedPowerPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/MixedDegreeConstruction.lean, line 79. The attribute's comment: “graded divided power polynomial algebra over a prescribed degree-zero algebra”.
A graded divided-power polynomial algebra exists over any prescribed commutative degree-zero algebra
P, with one homogeneous variable of degreen + 1for each element ofindices n. Its mapping property isexistsUnique_restrictedStageGradedDividedPowerPolynomial_map.
public theorem exists_gradedDividedPowerPolynomial {R : Type u} [CommRing R] (P : Type v)
[CommRing P] [Algebra R P] (indices : ℕ → Type (max u v w)) :
∃ (A : Type (max u v w)) (ringA : Ring A),
letI : Ring A := ringA
∃ algebraA : Algebra R A,
letI : Algebra R A := algebraA
∃ (Aᵢ : ℕ → Submodule R A) (gradedA : GradedAlgebra Aᵢ),
letI : GradedAlgebra Aᵢ := gradedA
∃ strictA : IsStrictlyGradedComm Aᵢ,
letI : IsStrictlyGradedComm Aᵢ := strictA
∃ (γ : DividedPowerStructure Aᵢ) (ι : P →ₐ[R] A)
(h : RestrictedStageGradedDividedPowerPolynomial Aᵢ γ ι), h.indices = indices
DividedPowers.TateResolution.existsUnique_restrictedStageGradedDividedPowerPolynomial_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/MixedDegreePolynomial.lean, line 596. The attribute's comment: “mapping property of a graded divided-power polynomial algebra”.
The mapping property of an iterated graded divided-power polynomial algebra: prescribing the values on the coefficient algebra and on the variables, subject to the degree conditions, determines a unique map of graded algebras with divided powers. The target may live in a universe independent of the source and its variables.
The hypothesis is
RestrictedStageGradedDividedPowerPolynomial, which also requires each stage'sR-algebra structure to be restricted from the ambient algebra.existsUnique_gradedDividedPowerPolynomial_mapofStacksFrontier.RingTheory.DividedPowers.TateResolution.GradedPolynomialMaphas the identical conclusion under the hypothesis without that clause, so it is the stronger of the two; this one is the form thatexists_gradedDividedPowerPolynomialapplies, since Tag 0F4I's construction delivers the clause.
public theorem existsUnique_restrictedStageGradedDividedPowerPolynomial_map
(γ : DividedPowerStructure Aᵢ) (ι : P →ₐ[R] A)
(h : RestrictedStageGradedDividedPowerPolynomial Aᵢ γ ι)
(δ : DividedPowerStructure Dᵢ) (f : P →ₐ[R] D) (hf : ∀ p : P, f p ∈ Dᵢ 0)
(t : (Σ n : ℕ, h.indices n) → D) (ht : ∀ j, t j ∈ Dᵢ (j.1 + 1)) :
∃! g : A →ₐ[R] D,
(∀ p : P, g (ι p) = f p) ∧
(∀ j : Σ n : ℕ, h.indices n, g (h.generator j) = t j) ∧
(∀ (n : ℕ) (a : A), a ∈ Aᵢ n → g a ∈ Dᵢ n) ∧
(∀ (n : ℕ) (a : A), a ∈ positiveEvenPart Aᵢ →
g (γ.dpow n a) = δ.dpow n (g a))
DividedPowers.TateResolution.exists_boundary_of_coefficient_combination, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/NoetherianCycles.lean, line 223. The attribute's comment: “a spanning family of variables kills every cycle of its degree”.
A combination of the cycles killed by the variables of degree
n + 1is a boundary. The boundary of the corresponding combination of the variables is it, by linearity of the differential over the coefficients, and that combination is homogeneous of degreen + 1because the coefficients are homogeneous of degree zero.So a family of variables whose prescribed cycles span the cycles of a degree kills all of them. This is what makes a degreewise finite Tate tower acyclic; the existence half of Tag 09PN instead prescribes every cycle individually, which costs it degreewise finiteness.
public theorem exists_boundary_of_coefficient_combination
(h0 : ∀ p : P, algebraMap P A p ∈ Aᵢ 0) {J : Type*} (v T : J → A) (n : ℕ)
(hT : ∀ j : J, T j ∈ Aᵢ (n + 1)) (hdT : ∀ j : J, d (T j) = v j)
(s : Finset J) (c : J → P) :
∃ b : A, b ∈ Aᵢ (n + 1) ∧ d b = ∑ j ∈ s, c j • v j
DividedPowers.TateResolution.GradedDividedPowerPolynomial.fg_coefficientGrade, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/NoetherianCycles.lean, line 272. The attribute's comment: “finite generation of the homogeneous pieces over the coefficients”.
Each homogeneous piece is finitely generated over the coefficient algebra as soon as the variables are finite in each degree: there are then only finitely many divided power monomials of each degree, and they span that degree over the coefficients.
This is the coefficient-algebra analogue of
DividedPowers.TateResolution.GradedDividedPowerPolynomial.finite_grade, and it is the form the finiteness half of Tag 09PN needs: there the coefficient algebra is a polynomial ring over the ground ring, hence not module finite over it, sofinite_gradesays nothing.
public theorem fg_coefficientGrade (G : GradedDividedPowerPolynomial Aᵢ γ ι)
[∀ i : ℕ, Finite (G.indices i)] (h0 : ∀ p : P, algebraMap P A p ∈ Aᵢ 0)
(hι : ∀ p : P, algebraMap P A p = ι p) (n : ℕ) :
(coefficientGrade Aᵢ h0 n).FG
DividedPowers.TateResolution.exists_finite_spanning_cycles, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/NoetherianCycles.lean, line 315. The attribute's comment: “a finite generating family of the cycles of a degree”.
A finite family of degree-
ncycles that every degree-ncycle is a combination of.This is what lets the variables of degree
n + 1of Tate's tower be finite in number: the existence half of Tag 09PN adjoins one variable for every cycle of degreen, which makes acyclicity free of a homology computation but makes the resolution infinite in each degree. Over a Noetherian coefficient algebra a finite family suffices, byDividedPowers.TateResolution.exists_boundary_of_coefficient_combination.
public theorem exists_finite_spanning_cycles (G : GradedDividedPowerPolynomial Aᵢ γ ι)
[∀ i : ℕ, Finite (G.indices i)] [IsNoetherianRing P]
(h0 : ∀ p : P, algebraMap P A p ∈ Aᵢ 0) (hι : ∀ p : P, algebraMap P A p = ι p) (n : ℕ) :
∃ s : Finset A, (∀ y ∈ s, y ∈ Aᵢ n ∧ d y = 0) ∧
∀ x : A, x ∈ Aᵢ n → d x = 0 → ∃ c : A → P, ∑ y ∈ s, c y • y = x
DividedPowers.TateResolution.chainStagePresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/StagePresentation.lean, line 237. The attribute's comment: “each finite stage is a graded divided power polynomial algebra”.
The stage
Nof a chain of set-variable divided power extensions is a graded divided power polynomial algebra over the base of the chain, on the variables of degrees1, …, N.This is
DividedPowers.TateResolution.gradedDividedPowerPolynomialOfMappingPropertyfed the two statements above. Its use is finiteness: the degree-mpiece of the stage is spanned over the base by the divided power monomials of degreemin those variables, of which there are finitely many when the chain adjoins finitely many variables at each step.
public noncomputable def chainStagePresentation
(hbase0 : ∀ p : (B 0).carrier, p ∈ (B 0).grade 0)
(hbase : ∀ (E : GradedDPAlgebra.{u, v} R) (f : (B 0).carrier →ₐ[R] E.carrier),
(∀ p : (B 0).carrier, f p ∈ E.grade 0) →
∃ F : GradedDPHom (B 0) E, ∀ p : (B 0).carrier, F.hom p = f p)
(N : ℕ) :
GradedDividedPowerPolynomial (B N).grade (B N).gamma (chainStageCoefficient B step N)
DividedPowers.TateResolution.tateResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/TateColimitResolution.lean, line 499. The attribute's comment: “resolution of any polynomial presentation”.
Tate's resolution of a prescribed polynomial presentation. Every surjection
φ : R[xᵢ] → Sfrom a polynomial ring extends to a divided power differential graded algebra overR, free overRin every degree, whose degree-zero algebra isR[xᵢ]alongφ, which is a graded divided power polynomial algebra overR[xᵢ], and whose augmentation toSis a quasi-isomorphism: it kills the positive-degree part and every boundary, it is surjective, its degree-zero kernel is exactly the boundaries from degree one, and the complex is exact in every positive degree.The algebra is the colimit of Tate's tower over
R[xᵢ]withker φas the ideal to be killed in degree one. Acyclicity is not a homology computation: the variables adjoined in degreen + 1are indexed by all cycles of degreen, with the boundary of a variable being the cycle indexing it, so a cycle of degreenis the boundary of its own variable by construction.
public noncomputable def tateResolution (φ : MvPolynomial σ R →ₐ[R] S)
(hφ : Function.Surjective φ) : Resolution R S σ φ
Tag 0BZ9, a lemma
Tag 0BZ9 in the Stacks Project.
DividedPowers.TateResolution.exists_finite_tateResolution_of_pseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/PseudoCoherentTateResolution.lean, line 78.
A pseudo-coherent ring map admits a Tate resolution with finitely many generators in each degree. If
R → Sis pseudo-coherent then there are a surjectionφ : R[x₁, …, x_k] → Sfrom a polynomial ring in finitely many variables and a Tate resolution ofSalongφwhose variables are finite in number in every degree.This is the conclusion of Tag 09PN with its hypotheses —
RNoetherian andR → Sof finite type — replaced by pseudo-coherence ofR → S.
public theorem exists_finite_tateResolution_of_pseudoCoherent
(R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
[h : Algebra.PseudoCoherent R S] :
∃ (k : ℕ) (φ : MvPolynomial (Fin k) R →ₐ[R] S) (A : Resolution R S (Fin k) φ),
Function.Surjective φ ∧ ∀ i : ℕ, Finite (A.polynomialIndices i)
Tag 09PP, a lemma
Tag 09PP in the Stacks Project.
DividedPowers.TateResolution.exists_dividedPowerDGAMap_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/DividedPowerDGALift.lean, line 842.
A map from a graded divided-power polynomial DGA to a positively acyclic divided-power DGA lifting a prescribed map on zeroth homology.
public theorem exists_dividedPowerDGAMap_lift
{R : Type u} {A : Type v} {B : Type w} {σ : Type z}
[CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B]
(𝒜 : ℕ → Submodule R A) (ℬ : ℕ → Submodule R B)
[GradedAlgebra 𝒜] [GradedAlgebra ℬ]
[IsStrictlyGradedComm 𝒜] [IsStrictlyGradedComm ℬ]
(γA : DividedPowerStructure 𝒜) (γB : DividedPowerStructure ℬ)
(dA : A →ₗ[R] A) (dB : B →ₗ[R] B)
[IsDifferentialGradedAlgebra 𝒜 dA]
[IsDifferentialGradedAlgebra ℬ dB]
[IsCompatibleWithDifferential γA dA]
[IsCompatibleWithDifferential γB dB]
(ι : MvPolynomial σ R →ₐ[R] A)
(hA : GradedDividedPowerPolynomial 𝒜 γA ι)
(hB : ∀ (n : ℕ) (b : B), 0 < n → b ∈ ℬ n → dB b = 0 →
∃ c : B, c ∈ ℬ (n + 1) ∧ dB c = b)
(φ₀ : zerothHomology 𝒜 dA →ₐ[R] zerothHomology ℬ dB) :
∃ φ : A →ₐ[R] B,
(∀ (n : ℕ) (a : A), a ∈ 𝒜 n → φ a ∈ ℬ n) ∧
(∀ a : A, φ (dA a) = dB (φ a)) ∧
(∀ (n : ℕ) (a : A), a ∈ positiveEvenPart 𝒜 →
φ (γA.dpow n a) = γB.dpow n (φ a)) ∧
(∀ a : A,
φ₀ ((zerothHomologyCongruence 𝒜 dA).mk' a) =
(zerothHomologyCongruence ℬ dB).mk' (φ a))
Tag 09PQ, a lemma
Tag 09PQ in the Stacks Project.
DividedPowers.TateResolution.exists_dividedPowerStructure_torDirectSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/TorDividedPowerAlgebra.lean, line 1056.
Divided powers on
Tor_*^R(S, T). For a commutative ringRand commutativeR-algebrasSandT, the direct sum⨁ n, Tor_n^R(S, T)carries a ring structure, anR-algebra structure, a grading whose degree-npiece is the range of then-th inclusion of the direct sum, a graded algebra structure for that grading, strict graded commutativity, and a divided power structure — with the addition and the scalar multiplication being the direct sum's own.The structure is the one transported along
DividedPowers.TateResolution.torDirectSumEquivHomologyfrom the induced structure on the homology ofT ⊗[R] A, forAthe Tate resolution ofSalong the tautological presentation: the class mapκof that identification, which sends a cycle ofT ⊗[R] Ato the element of the direct sum corresponding to its homology class, is unital and multiplicative, takes a cycle of degreeninto the degree-npiece, and takes the divided powers ofT ⊗[R] Ato those of the direct sum. Those divided powers are in turn the base change of the divided powers of the Tate resolution.
public theorem exists_dividedPowerStructure_torDirectSum
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] :
∃ Res : Resolution R S S (tautologicalPresentation R S),
Res = tateResolution (tautologicalPresentation R S)
(surjective_tautologicalPresentation R S) ∧
(let ℬ : ℕ → Submodule R (T ⊗[R] Res.A) :=
restrictGrade R fun i => (Res.grade i).baseChange T
let dB : T ⊗[R] Res.A →ₗ[R] T ⊗[R] Res.A :=
(LinearMap.baseChange T Res.differential).restrictScalars R
∃ hStrict : IsStrictlyGradedComm ℬ,
letI := hStrict
∃ γB : DividedPowerStructure ℬ,
IsCompatibleWithDifferential γB dB ∧
(∀ (n : ℕ) (x : Res.A), x ∈ positiveEvenPart Res.grade →
γB.dpow n (1 ⊗ₜ[R] x) = 1 ⊗ₜ[R] Res.gamma.dpow n x) ∧
(let κ : cycles dB →ₗ[R] DirectSum ℕ fun n => torGraded R S T n :=
directSumClass (torDirectSumEquivHomology Res T
(surjective_tautologicalPresentation R S))
∃ hRing : Ring (DirectSum ℕ fun n => torGraded R S T n),
∃ hAlgebra : @Algebra R (DirectSum ℕ fun n => torGraded R S T n) _
hRing.toSemiring,
hRing.toAddCommGroup =
(inferInstance : AddCommGroup (DirectSum ℕ fun n => torGraded R S T n)) ∧
@Algebra.toSMul R (DirectSum ℕ fun n => torGraded R S T n) _
hRing.toSemiring hAlgebra =
(inferInstance : SMul R (DirectSum ℕ fun n => torGraded R S T n)) ∧
(letI := hRing
letI := hAlgebra
letI : AddCommMonoid (DirectSum ℕ fun n => torGraded R S T n) :=
hRing.toAddCommMonoid
letI : Module R (DirectSum ℕ fun n => torGraded R S T n) := Algebra.toModule
∃ 𝒟 : ℕ → Submodule R (DirectSum ℕ fun n => torGraded R S T n),
(∀ n, (𝒟 n : Set (DirectSum ℕ fun m => torGraded R S T m)) =
Set.range (DirectSum.lof R ℕ (fun m => torGraded R S T m) n)) ∧
∃ hGraded : GradedAlgebra 𝒟,
letI := hGraded
∃ hStrictD : IsStrictlyGradedComm 𝒟,
letI := hStrictD
∃ γD : @DividedPowerStructure R
(DirectSum ℕ fun n => torGraded R S T n) _ hRing hAlgebra 𝒟
hGraded hStrictD,
(∀ (n : ℕ) (x : T ⊗[R] Res.A) (h : dB x = 0), x ∈ ℬ n →
κ ⟨x, h⟩ ∈ 𝒟 n) ∧
(∃ h1 : dB (1 : T ⊗[R] Res.A) = 0, κ ⟨1, h1⟩ = 1) ∧
(∀ {x y : T ⊗[R] Res.A} (hx : dB x = 0) (hy : dB y = 0),
∃ hxy : dB (x * y) = 0,
κ ⟨x * y, hxy⟩ = κ ⟨x, hx⟩ * κ ⟨y, hy⟩) ∧
(∀ {n : ℕ} {x : T ⊗[R] Res.A}, x ∈ positiveEvenPart ℬ →
∀ hd : dB x = 0,
∃ hγ : dB (γB.dpow n x) = 0,
γD.dpow n (κ ⟨x, hd⟩) = κ ⟨γB.dpow n x, hγ⟩))))
Sources
Section23.7 Application to complete intersections#
Section 23.7 of the Stacks Project, Tag 09PR. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09PS, a lemma
Tag 09PS in the Stacks Project.
DividedPowers.TateResolution.squareZeroExtensionDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/SquareZeroLift.lean, line 180.
The degree-minus-two derivation of Tag 09PS. Let
q : R' → Rbe a surjection of commutative rings whose kernel is generated by a single elementfof square zero, let(A, 𝒜, γ, d)be a graded divided power polynomial algebra overR[xᵢ]with a differential compatible with its divided powers, and letIbe the image underqof the annihilator off. ThenA/IAcarries anR-linear operatorθwhich obeys the Leibniz rule, lowers degrees by two, and vanishes in degrees zero and one.The construction the source retains is part of the statement:
θis the square of an operatorDliftingdto a divided power polynomial algebraBoverR'[xᵢ]on the same variables, compared intoA/IAby division byf.
public noncomputable def squareZeroExtensionDerivation
{R' : Type u} {R : Type v} {A : Type w} {σ : Type z}
[CommRing R'] [CommRing R] [Ring A] [Algebra R A]
(q : R' →+* R) (hq : Function.Surjective q)
(f : R') (hker : RingHom.ker q = Ideal.span {f})
(_hsq : (RingHom.ker q) ^ 2 = ⊥)
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜)
(d : A →ₗ[R] A) [IsDifferentialGradedAlgebra 𝒜 d] [IsCompatibleWithDifferential γ d]
(ι : MvPolynomial σ R →ₐ[R] A)
(hpoly : GradedDividedPowerPolynomial 𝒜 γ ι)
(_hfinite₀ : Finite σ)
(_hfinite : ∀ n : ℕ, Finite (hpoly.indices n)) :
{ θ : (A ⧸ squareZeroAnnihilatorSMul q f A) →ₗ[R]
(A ⧸ squareZeroAnnihilatorSMul q f A) //
(∀ x y : A, ∃ u v : A,
θ (Submodule.Quotient.mk x) = Submodule.Quotient.mk u ∧
θ (Submodule.Quotient.mk y) = Submodule.Quotient.mk v ∧
θ (Submodule.Quotient.mk (x * y)) =
Submodule.Quotient.mk (u * y + x * v)) ∧
(∀ (n : ℕ) (x : A), x ∈ 𝒜 (n + 2) →
∃ y : A, y ∈ 𝒜 n ∧
θ (Submodule.Quotient.mk x) = Submodule.Quotient.mk y) ∧
(∀ (x : A), x ∈ 𝒜 0 → θ (Submodule.Quotient.mk x) = 0) ∧
(∀ (x : A), x ∈ 𝒜 1 → θ (Submodule.Quotient.mk x) = 0) ∧
(∃ (B : Type (max u v w z)) (hB : Ring B),
letI : Ring B := hB
∃ hAlg : Algebra R' B,
letI : Algebra R' B := hAlg
∃ (ℬ : ℕ → Submodule R' B) (hGr : GradedAlgebra ℬ),
letI : GradedAlgebra ℬ := hGr
∃ hComm : IsStrictlyGradedComm ℬ,
letI : IsStrictlyGradedComm ℬ := hComm
∃ (δ : DividedPowerStructure ℬ)
(ι' : MvPolynomial σ R' →ₐ[R'] B)
(hpolyB : GradedDividedPowerPolynomial ℬ δ ι')
(e : ∀ n : ℕ, hpoly.indices n ≃ hpolyB.indices n)
(π : B →+* A) (D : B →ₗ[R'] B)
(κ : RingHom.ker π →+ (A ⧸ squareZeroAnnihilatorSMul q f A)),
Function.Surjective π ∧
(∀ r' : R', π (algebraMap R' B r') = algebraMap R A (q r')) ∧
(∀ p' : MvPolynomial σ R',
π (ι' p') = ι (MvPolynomial.map q p')) ∧
(∀ (n : ℕ) (j : hpoly.indices n),
π (hpolyB.generator ⟨n, e n j⟩) = hpoly.generator ⟨n, j⟩) ∧
(∀ (n : ℕ) (b : B), b ∈ ℬ n → π b ∈ 𝒜 n) ∧
(∀ (n : ℕ) (b : B), b ∈ positiveEvenPart ℬ →
π (δ.dpow n b) = γ.dpow n (π b)) ∧
(∀ b : B, π b = 0 ↔ ∃ c : B, b = algebraMap R' B f * c) ∧
(∀ (b : B), b ∈ ℬ 0 → D b = 0) ∧
(∀ (n : ℕ) (b : B), b ∈ ℬ (n + 1) → D b ∈ ℬ n) ∧
(∀ (i j : ℕ) (b c : B), b ∈ ℬ i → c ∈ ℬ j →
D (b * c) = D b * c + (-1 : R') ^ i • (b * D c)) ∧
(∀ (n : ℕ) (b : B), n ≠ 0 → b ∈ positiveEvenPart ℬ →
D (δ.dpow n b) = D b * δ.dpow (n - 1) b) ∧
(∀ b : B, π (D b) = d (π b)) ∧
(∀ (b : B) (hb : algebraMap R' B f * b ∈ RingHom.ker π),
κ ⟨algebraMap R' B f * b, hb⟩ =
Submodule.Quotient.mk (π b)) ∧
(∀ b : B, ∃ hb : D (D b) ∈ RingHom.ker π,
θ (Submodule.Quotient.mk (π b)) = κ ⟨D (D b), hb⟩)) }
Tag 09PT, a lemma
Tag 09PT in the Stacks Project.
DividedPowers.TateResolution.exists_mem_grade_two_derivation_eq_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/LiftedRelation.lean, line 180.
Stacks 09PT. A relation
∑ rⱼ Fⱼ = 0with all coefficients inI, lifting to∑ r'ⱼ F'ⱼ = g f, yields a classξ ∈ 𝒜 2which is a cycle moduloI·Aand on which the derivation of the square-zero lift takes the valueg, read inS / IS.
public theorem exists_mem_grade_two_derivation_eq_lift
{R' : Type u} {R : Type v} {A : Type w} {B : Type x} {σ : Type z} {S : Type t}
[CommRing R'] [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R' B]
[CommRing S] [Algebra R S]
{q : R' →+* R} {f : R'}
{𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
{d : A →ₗ[R] A} [IsDifferentialGradedAlgebra 𝒜 d]
{ℬ : ℕ → Submodule R' B} [GradedAlgebra ℬ]
{π : B →+* A} {D : B →ₗ[R'] B}
{κ : RingHom.ker π →+ (A ⧸ squareZeroAnnihilatorSMul q f A)}
(h : IsSquareZeroLift q f 𝒜 d ℬ π D κ)
(hker : RingHom.ker q = Ideal.span {f})
(ι : MvPolynomial σ R →ₐ[R] A) (ι' : MvPolynomial σ R' →ₐ[R'] B)
(hι₀ : ∀ a : A, a ∈ 𝒜 0 → ∃ p, ι p = a)
(hι'mem : ∀ p : MvPolynomial σ R', ι' p ∈ ℬ 0)
(hπι : ∀ p : MvPolynomial σ R', π (ι' p) = ι (MvPolynomial.map q p))
(ε : A →ₐ[R] S)
(hε₀ : ∀ s : S, ∃ a : A, a ∈ 𝒜 0 ∧ ε a = s)
(hεd : ∀ a : A, ε (d a) = 0)
(hH₀ : ∀ a : A, a ∈ 𝒜 0 → ε a = 0 → ∃ b : A, b ∈ 𝒜 1 ∧ d b = a)
(hH₁ : ∀ a : A, a ∈ 𝒜 1 → d a = 0 → ∃ b : A, b ∈ 𝒜 2 ∧ d b = a)
(n m : ℕ)
(φ : MvPolynomial (Fin n) R →ₐ[R] S)
(F r : Fin m → MvPolynomial (Fin n) R)
(hkerφ : RingHom.ker φ.toRingHom = Ideal.span (Set.range F))
(hrel : ∑ j, r j * F j = 0)
(hcoeff : ∀ (j : Fin m) (e : Fin n →₀ ℕ),
(r j).coeff e ∈ squareZeroAnnihilator q f)
(F' r' : Fin m → MvPolynomial (Fin n) R')
(g : MvPolynomial (Fin n) R')
(hF : ∀ j, MvPolynomial.map q (F' j) = F j)
(hr : ∀ j, MvPolynomial.map q (r' j) = r j)
(hlift : ∑ j, r' j * F' j = g * MvPolynomial.C f) :
∃ ξ y : A,
ξ ∈ 𝒜 2 ∧ d ξ ∈ squareZeroAnnihilatorSMul q f A ∧ y ∈ 𝒜 0 ∧
h.derivation (Submodule.Quotient.mk ξ) = Submodule.Quotient.mk y ∧
Ideal.Quotient.mk (Ideal.map (algebraMap R S) (squareZeroAnnihilator q f)) (ε y) =
Ideal.Quotient.mk (Ideal.map (algebraMap R S) (squareZeroAnnihilator q f))
(φ (MvPolynomial.map q g))
DividedPowers.TateResolution.squareZeroExtensionDerivation_liftedRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/LiftedRelationDerivation.lean, line 64.
A relation with coefficients annihilating the square-zero generator yields a degree-two class whose derivation is the coefficient of the lifted relation.
public theorem squareZeroExtensionDerivation_liftedRelation
{R' : Type u} {R : Type v} {A : Type w} {σ : Type z} {S : Type t}
[CommRing R'] [CommRing R] [Ring A] [Algebra R A]
[CommRing S] [Algebra R S]
(q : R' →+* R) (hq : Function.Surjective q)
(f : R') (hker : RingHom.ker q = Ideal.span {f})
(hsq : (RingHom.ker q) ^ 2 = ⊥)
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜]
[IsStrictlyGradedComm 𝒜]
(γ : DividedPowerStructure 𝒜)
(d : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 d]
[IsCompatibleWithDifferential γ d]
(ι : MvPolynomial σ R →ₐ[R] A)
(hpoly : GradedDividedPowerPolynomial 𝒜 γ ι)
(hfinite₀ : Finite σ)
(hfinite : ∀ n : ℕ, Finite (hpoly.indices n))
(ε : A →ₐ[R] S)
(hε₀ : ∀ s : S, ∃ a : A, a ∈ 𝒜 0 ∧ ε a = s)
(hεd : ∀ a : A, ε (d a) = 0)
(hH₀ : ∀ a : A, a ∈ 𝒜 0 → ε a = 0 →
∃ b : A, b ∈ 𝒜 1 ∧ d b = a)
(hH₁ : ∀ a : A, a ∈ 𝒜 1 → d a = 0 →
∃ b : A, b ∈ 𝒜 2 ∧ d b = a)
(n m : ℕ)
(φ : MvPolynomial (Fin n) R →ₐ[R] S)
(_hφ : Function.Surjective φ)
(F r : Fin m → MvPolynomial (Fin n) R)
(hkerφ : RingHom.ker φ.toRingHom = Ideal.span (Set.range F))
(hrel : ∑ j, r j * F j = 0)
(hcoeff : ∀ (j : Fin m) (e : Fin n →₀ ℕ),
(r j).coeff e ∈
Ideal.map q (Ideal.span {f}).annihilator)
(F' r' : Fin m → MvPolynomial (Fin n) R')
(g : MvPolynomial (Fin n) R')
(hF : ∀ j, MvPolynomial.map q (F' j) = F j)
(hr : ∀ j, MvPolynomial.map q (r' j) = r j)
(hlift : ∑ j, r' j * F' j = g * MvPolynomial.C f) :
let I : Ideal R := Ideal.map q (Ideal.span {f}).annihilator
let J : Submodule R A := I • ⊤
let IS : Ideal S := Ideal.map (algebraMap R S) I
let θ := (squareZeroExtensionDerivation q hq f hker hsq 𝒜 γ d ι hpoly
hfinite₀ hfinite).val
∃ ξ y : A,
ξ ∈ 𝒜 2 ∧ d ξ ∈ J ∧ y ∈ 𝒜 0 ∧
θ (Submodule.Quotient.mk ξ) = Submodule.Quotient.mk y ∧
Ideal.Quotient.mk IS (ε y) =
Ideal.Quotient.mk IS (φ (MvPolynomial.map q g))
Tag 09PU, a lemma
Tag 09PU in the Stacks Project.
StacksDraft.Rodicio.gulliksenObstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Rodicio/GulliksenObstruction.lean, line 208.
Gulliksen's obstruction, Stacks Tag 09PU. A relation among the equations of a finite-type presentation whose coefficients annihilate the square-zero generator, and which lifts to a non-nilpotent multiple of that generator, forces the presented algebra to have infinite Tor dimension over the base.
This is
StacksDraft.Rodicio.not_exists_tor_vanishing_of_lifted_relationat the source's own presented algebraR[x₁,…,x_n]/(F₁,…,F_m), which is a finite-typeR-algebra because it is a quotient of a polynomial ring in finitely many variables.
public theorem gulliksenObstruction : GulliksenObstruction.{u}
Tag 09PV, a lemma
Tag 09PV in the Stacks Project.
StacksDraft.Rodicio.injective_mapQ_maximalIdeal_of_finite_torDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/Rodicio/GulliksenObstruction.lean, line 224.
Rodicio's theorem, Stacks Tag 09PV. For proper ideals
I ⊆ Jof a Noetherian local ringAwithA/Jof finite Tor dimension overA/I, the canonical mapI/𝔪I → J/𝔪Jis injective.Finite Tor dimension is spelled as in Stacks Tag 0652: a degree beyond which
Tor_i^{A/I}(A/J, N)vanishes for everyA/I-moduleN.This is
StacksDraft.Rodicio.injective_mapQ_maximalIdeal_of_gulliksenObstructionwith its Tag 09PU hypothesis discharged byStacksDraft.Rodicio.gulliksenObstruction.
public theorem injective_mapQ_maximalIdeal_of_finite_torDimension
{A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(I J : Ideal A) (hI : I ≠ ⊤) (hJ : J ≠ ⊤) (hIJ : I ≤ J)
(hTor : ∃ b : ℕ,
letI : Algebra (A ⧸ I) (A ⧸ J) := (Ideal.Quotient.factor hIJ).toAlgebra
∀ (N : ModuleCat.{u} (A ⧸ I)) (i : ℕ), b < i →
Limits.IsZero (((Tor (ModuleCat.{u} (A ⧸ I)) i).obj
(ModuleCat.of (A ⧸ I) (A ⧸ J))).obj N)) :
let f : I →ₗ[A] J := Submodule.inclusion hIJ
Function.Injective
((IsLocalRing.maximalIdeal A • (⊤ : Submodule A I)).mapQ
(IsLocalRing.maximalIdeal A • (⊤ : Submodule A J)) f
(Submodule.smul_top_le_comap_smul_top _ f))
Tag 09PW, a lemma
Tag 09PW in the Stacks Project.
Stacks.CompleteIntersection.exists_isRegular_of_finite_torDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/CompleteIntersection/NestedIdeals.lean, line 53. References: EGA IV (19.1.6), “more general”.
Let
I ⊆ Jbe proper ideals of a Noetherian local ringA. IfA / Jhas finite Tor dimension overA / IandJis generated by a regular sequence, thenIis generated by a regular sequence and the image ofJinA / Iis generated by a regular sequence ofA / I.
theorem exists_isRegular_of_finite_torDimension
{A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(I J : Ideal A) (hI : I ≠ ⊤) (hJ : J ≠ ⊤) (hIJ : I ≤ J)
(hTor : ∃ b : ℕ,
letI : Algebra (A ⧸ I) (A ⧸ J) := (Ideal.Quotient.factor hIJ).toAlgebra
∀ (N : ModuleCat.{u} (A ⧸ I)) (i : ℕ), b < i →
Limits.IsZero (((Tor (ModuleCat.{u} (A ⧸ I)) i).obj
(ModuleCat.of (A ⧸ I) (A ⧸ J))).obj N))
(hJreg : ∃ rs : List A, IsRegular A rs ∧ Ideal.ofList rs = J) :
(∃ rs : List A, IsRegular A rs ∧ Ideal.ofList rs = I) ∧
∃ qs : List (A ⧸ I), IsRegular (A ⧸ I) qs ∧
Ideal.ofList qs = J.map (Ideal.Quotient.mk I)
Tag 09PX, a lemma
Tag 09PX in the Stacks Project.
Stacks.CompleteIntersection.regularSequence_quotient_tfae_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/CompleteIntersection/RegularSequenceTFAE.lean, line 400.
Stacks 09PX. Let
R → Sbe a flat local homomorphism of Noetherian local rings whose closed fibre is a regular local ring, letI ⊆ 𝔪_Rand letJbe an ideal ofScontainingI S. The following are equivalent:
Jis generated by a regular sequence andS / Jhas finite Tor dimension overR / I;Jis generated by a regular sequence and theTorgroups ofS / Jagainst the residue field ofRvanish in all large degrees;Iis generated by a regular sequence ofRandJ / ISis generated by a regular sequence ofS / IS.The quotient ideal
J / ISis represented by the image ofJunderS → S / IS, and the residue field ofRis represented as theR / I-moduleR / 𝔪_R.
public theorem regularSequence_quotient_tfae_of_flat
{R S : Type u} [CommRing R] [CommRing S]
[IsNoetherianRing R] [IsNoetherianRing S] [IsLocalRing R] [IsLocalRing S]
[Algebra R S] [IsLocalHom (algebraMap R S)] [Module.Flat R S]
(I : Ideal R) (J : Ideal S) (hI : I ≤ IsLocalRing.maximalIdeal R)
(hIJ : I.map (algebraMap R S) ≤ J)
(hfiber : IsRegularLocalRing
(S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S))) :
List.TFAE [
(Ideal.IsGeneratedByRegularSequence J ∧
FiniteTorDimension (quotientModule
(Ideal.quotientMap J (algebraMap R S) ((Ideal.map_le_iff_le_comap).mp hIJ)))),
(Ideal.IsGeneratedByRegularSequence J ∧
∃ n : ℕ, ∀ p : ℕ, n < p → IsZero
(((Tor (ModuleCat.{u} (R ⧸ I)) p).obj
(quotientModule
(Ideal.quotientMap J (algebraMap R S) ((Ideal.map_le_iff_le_comap).mp hIJ)))).obj
(quotientModule
(Ideal.quotientMap (IsLocalRing.maximalIdeal R) (RingHom.id R)
(by simpa using hI))))),
(Ideal.IsGeneratedByRegularSequence I ∧
Ideal.IsGeneratedByRegularSequence
(J.map (Ideal.Quotient.mk (I.map (algebraMap R S)))))]
Sources
Section23.8 Local complete intersection rings#
Section 23.8 of the Stacks Project, Tag 09PY. 9 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09PZ, a lemma
Tag 09PZ in the Stacks Project.
LocalCompleteIntersection.forall_regularPresentation_iff_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Basic.lean, line 451. References: EGA IV (19.3.2), “special case”.
Let
Abe a Noetherian complete local ring. The kernel of every surjection ontoAfrom a regular local ring is generated by a regular sequence if and only if this holds for one such surjection.
public theorem forall_regularPresentation_iff_exists
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
[IsAdicComplete (maximalIdeal A) A] :
(∀ (R : Type u) [CommRing R] [IsRegularLocalRing R] (f : R →+* A),
Function.Surjective f →
∃ rs : List R, RingTheory.Sequence.IsRegular R rs ∧
Ideal.ofList rs = RingHom.ker f) ↔
∃ (R : Type u) (_ : CommRing R) (_ : IsRegularLocalRing R) (f : R →+* A),
Function.Surjective f ∧
∃ rs : List R, RingTheory.Sequence.IsRegular R rs ∧
Ideal.ofList rs = RingHom.ker f
Tag 09Q0, a lemma
Tag 09Q0 in the Stacks Project.
LocalCompleteIntersection.isCompleteIntersectionCompleteLocalRing_adicCompletion_quotientAtPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Basic.lean, line 186. References: EGA IV (19.3.2), “reg seq ⇒ CI”.
Stacks 09Q0. If
Ris regular,pis a prime ofR, andrsis a regular sequence contained inp, then the completion ofRₚ/(rs)Rₚat its maximal ideal is a complete intersection.
public theorem isCompleteIntersectionCompleteLocalRing_adicCompletion_quotientAtPrime
(R : Type u) [CommRing R] [IsRegularRing R] (p : Ideal R) [p.IsPrime] (rs : List R)
(hrs : IsRegular R rs) (hmem : ∀ x ∈ rs, x ∈ p) :
let Rp := Localization.AtPrime p
let rs' : List Rp := rs.map (algebraMap R Rp)
let I : Ideal Rp := Ideal.ofList rs'
let A := Rp ⧸ I
IsCompleteIntersectionCompleteLocalRing
(AdicCompletion ((maximalIdeal Rp).map (Ideal.Quotient.mk I)) A)
Tag 09Q1, a lemma
Tag 09Q1 in the Stacks Project.
LocalCompleteIntersection.quotient_regular_ring_tfae, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Basic.lean, line 608. References: EGA IV (19.3.2).
For a quotient of the localization of a regular ring at a prime, the completion is a complete intersection if and only if the extended ideal is generated by a regular sequence, if and only if its conormal module can be generated by the codimension number of elements.
public lemma quotient_regular_ring_tfae
{R : Type u} [CommRing R] [IsRegularRing R]
(p : Ideal R) [p.IsPrime] (I : Ideal R) (hIp : I ≤ p)
(Rp : Type u) [CommRing Rp] [Algebra R Rp] [IsLocalization.AtPrime Rp p]
(A : Type v) [CommRing A] [IsLocalRing A]
(q : Rp →+* A) (hq : Function.Surjective q)
(hker : RingHom.ker q = I.map (algebraMap R Rp)) :
List.TFAE
[IsCompleteIntersectionCompleteLocalRing
(AdicCompletion (maximalIdeal A) A),
∃ rs : List Rp, IsRegular Rp rs ∧
Ideal.ofList rs = I.map (algebraMap R Rp),
∃ c : ℕ,
ringKrullDim A + (c : WithBot ℕ∞) = ringKrullDim Rp ∧
(⊤ : Submodule
(Rp ⧸ (I.map (algebraMap R Rp)))
(I.map (algebraMap R Rp)).Cotangent).spanFinrank ≤ c]
Tag 09Q2, a proposition
Tag 09Q2 in the Stacks Project.
LocalCompleteIntersection.isCompleteIntersectionCompleteLocalRing_adicCompletion_iff_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FlatLocalHomomorphism.lean, line 530.
Stacks 09Q2. For a flat local homomorphism
A → Bof Noetherian local rings, the completion ofBis a complete intersection if and only if the completion ofAand the completion of the closed fibreB / 𝔪_A Bboth are.
theorem isCompleteIntersectionCompleteLocalRing_adicCompletion_iff_of_flat
(A : Type u) (B : Type v) [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
[Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Flat A B] :
let I := (maximalIdeal A).map (algebraMap A B)
let _ : Nontrivial (B ⧸ I) :=
Ideal.Quotient.nontrivial_iff.mpr
(IsLocalRing.map_maximalIdeal_lt_top (algebraMap A B)).ne
let _ : IsLocalHom (Ideal.Quotient.mk I) :=
IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
let _ : IsLocalRing (B ⧸ I) :=
IsLocalRing.of_surjective _ Ideal.Quotient.mk_surjective
IsCompleteIntersectionCompleteLocalRing (AdicCompletion (maximalIdeal B) B) ↔
(IsCompleteIntersectionCompleteLocalRing (AdicCompletion (maximalIdeal A) A) ∧
IsCompleteIntersectionCompleteLocalRing
(AdicCompletion (maximalIdeal (B ⧸ I)) (B ⧸ I)))
Tag 09Q3, a definition
Tag 09Q3 in the Stacks Project.
LocalCompleteIntersection.IsCompleteIntersectionRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Basic.lean, line 114. The attribute's comment: “(1)”. References: EGA IV (19.3.1), “local ring definition”; SGA 3 VIIB (5.5).
Stacks 09Q3 (1). A Noetherian local ring is a complete intersection if its completion at the maximal ideal is a quotient of a regular local ring by an ideal generated by a regular sequence.
public def IsCompleteIntersectionRing (A : Type u) [CommRing A] [IsNoetherianRing A]
[IsLocalRing A] : Prop
LocalCompleteIntersection.IsLocalCompleteIntersectionRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Basic.lean, line 135. The attribute's comment: “(2)”.
Stacks 09Q3 (2). A Noetherian ring is a local complete intersection if every localization at a prime ideal is a complete intersection local ring.
public def IsLocalCompleteIntersectionRing (A : Type u) [CommRing A] [IsNoetherianRing A] : Prop
Tag 09Q4, a lemma
Tag 09Q4 in the Stacks Project.
LocalCompleteIntersection.isCompleteIntersectionRing_localizationAtPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Localization.lean, line 57.
Stacks 09Q4. The localization of a Noetherian local complete intersection ring at a prime ideal is a complete intersection ring.
theorem isCompleteIntersectionRing_localizationAtPrime
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(p : Ideal A) [p.IsPrime] (hA : IsCompleteIntersectionRing A) :
IsCompleteIntersectionRing (Localization.AtPrime p)
Tag 09Q5, a lemma
Tag 09Q5 in the Stacks Project.
LocalCompleteIntersection.isLocalCompleteIntersectionRing_iff_localizationsAtMaximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Localization.lean, line 104.
Stacks 09Q5. A Noetherian ring is a local complete intersection precisely when its localizations at the maximal ideals are complete intersections.
theorem isLocalCompleteIntersectionRing_iff_localizationsAtMaximal
(A : Type u) [CommRing A] [IsNoetherianRing A] :
IsLocalCompleteIntersectionRing A ↔
∀ (m : Ideal A) [m.IsMaximal],
IsCompleteIntersectionRing (Localization.AtPrime m)
Tag 09Q6, a lemma
Tag 09Q6 in the Stacks Project.
LocalCompleteIntersection.isCompleteIntersection_atPrime_iff_isCompleteIntersectionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Basic.lean, line 825. The attribute's comment: “part (1)”.
Stacks 09Q6 (1). For a finite type algebra over a field, its local ring at a prime is a complete intersection over the field if and only if it is a complete intersection ring in the completion-based sense.
public theorem isCompleteIntersection_atPrime_iff_isCompleteIntersectionRing
(k : Type u) [Field k] (S : Type v) [CommRing S] [Algebra k S]
[Algebra.FiniteType k S] (q : Ideal S) [q.IsPrime] :
letI : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing k S
letI : IsNoetherianRing (Localization.AtPrime q) :=
IsLocalization.isNoetherianRing q.primeCompl _ inferInstance
IsCompleteIntersection k (Localization.AtPrime q) ↔
IsCompleteIntersectionRing (Localization.AtPrime q)
LocalCompleteIntersection.isLocalCompleteIntersection_iff_isLocalCompleteIntersectionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/Basic.lean, line 865. The attribute's comment: “part (2)”.
Stacks 09Q6 (2). For a finite type algebra over a field, being a local complete intersection over that field is equivalent to being a local complete intersection ring in the completion-based sense.
public theorem isLocalCompleteIntersection_iff_isLocalCompleteIntersectionRing
(k : Type u) [Field k] (S : Type v) [CommRing S] [Algebra k S]
[Algebra.FiniteType k S] :
letI : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing k S
IsLocalCompleteIntersection k S ↔ IsLocalCompleteIntersectionRing S
Tag 09Q7, a lemma
Tag 09Q7 in the Stacks Project.
LocalCompleteIntersection.isCompleteIntersectionRing_iff_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FlatDescent.lean, line 81.
Stacks 09Q7. For a flat local homomorphism
A → Bof Noetherian local rings,Bis a complete intersection if and only ifAand the closed fibreB / 𝔪_A Bare.
theorem isCompleteIntersectionRing_iff_of_flat :
letI I := (maximalIdeal A).map (algebraMap A B)
letI _ : Nontrivial (B ⧸ I) :=
Ideal.Quotient.nontrivial_iff.mpr
(IsLocalRing.map_maximalIdeal_lt_top (algebraMap A B)).ne
letI _ : IsLocalHom (Ideal.Quotient.mk I) :=
IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
letI _ : IsLocalRing (B ⧸ I) :=
IsLocalRing.of_surjective _ Ideal.Quotient.mk_surjective
IsCompleteIntersectionRing B ↔
(IsCompleteIntersectionRing A ∧ IsCompleteIntersectionRing (B ⧸ I))
Sources
Section23.9 Local complete intersection maps#
Section 23.9 of the Stacks Project, Tag 09Q9. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09QA, a lemma
Tag 09QA in the Stacks Project.
LocalCompleteIntersection.isCompleteIntersectionHom_iff_forall_goodFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/CompleteIntersectionHom.lean, line 954.
For a local homomorphism of Noetherian complete local rings, the kernel is generated by a regular sequence in one good factorization if and only if it is so generated in every good factorization.
public theorem isCompleteIntersectionHom_iff_forall_goodFactorization
{A : Type u} {B : Type v} [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
[IsAdicComplete (maximalIdeal A) A] [IsAdicComplete (maximalIdeal B) B]
(h : A →+* B) [IsLocalHom h] :
IsCompleteIntersectionHom h ↔
∀ (S : Type (max u v w)) [CommRing S] [IsNoetherianRing S] [IsLocalRing S]
(f : A →+* S) (g : S →+* B),
IsGoodFactorization h f g → (RingHom.ker g).IsGeneratedByRegularSequence
Tag 09QB, a proposition
Tag 09QB in the Stacks Project.
LocalCompleteIntersection.isCompleteIntersectionRing_and_eventually_tor_isZero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/TorCriterion.lean, line 381.
Avramov's characterization for a local homomorphism of Noetherian local rings.
public theorem isCompleteIntersectionRing_and_eventually_tor_isZero_iff
{A B : Type u} [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B]
[IsLocalRing A] [IsLocalRing B]
(f : A →+* B) [IsLocalHom f] :
(letI : Algebra A B := f.toAlgebra
IsCompleteIntersectionRing B ∧
∃ n : ℕ, ∀ p : ℕ, n < p →
IsZero (((Tor (ModuleCat.{u} A) p).obj (ModuleCat.of A B)).obj
(ModuleCat.of A (ResidueField A)))) ↔
(IsCompleteIntersectionRing A ∧
IsCompleteIntersectionHom
(adicCompletionMap f (maximalIdeal A) (maximalIdeal B)
(IsLocalRing.map_maximalIdeal_le f)))
Tag 09QD, a lemma
Tag 09QD in the Stacks Project.
LocalCompleteIntersection.isGeneratedByRegularSequence_ker_iff_isCompleteIntersectionHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/CompletionCriterion.lean, line 503.
In a good factorization
A → S → B, the kernel ofS → Bis generated by a regular sequence if and only if the induced mapA^∧ → B^∧is a complete intersection homomorphism.
public theorem isGeneratedByRegularSequence_ker_iff_isCompleteIntersectionHom
{A : Type u} {B : Type v} {S : Type w} [CommRing A] [CommRing B] [CommRing S]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing S]
[IsLocalRing A] [IsLocalRing B] [IsLocalRing S]
(h : A →+* B) (f : A →+* S) (g : S →+* B)
[IsLocalHom h] (hgood : IsGoodFactorization h f g) :
(RingHom.ker g).IsGeneratedByRegularSequence ↔
IsCompleteIntersectionHom
(adicCompletionMap h (maximalIdeal A) (maximalIdeal B)
(IsLocalRing.map_maximalIdeal_le h))
Tag 09QE, a lemma
Tag 09QE in the Stacks Project.
LocalCompleteIntersection.isLocalCompleteIntersection_iff_forall_isCompleteIntersectionHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FiniteTypeCriterion.lean, line 444.
A finite-type map from a Noetherian ring is a local complete intersection exactly when, at each target prime, the map between the completions of the corresponding local rings is a complete intersection homomorphism.
public theorem isLocalCompleteIntersection_iff_forall_isCompleteIntersectionHom
{A B : Type u} [CommRing A] [CommRing B] [IsNoetherianRing A]
(f : A →+* B) (hf : f.FiniteType) :
f.IsLocalCompleteIntersection ↔
letI := f.toAlgebra
letI : Algebra.FiniteType A B := hf
letI : IsNoetherianRing B := Algebra.FiniteType.isNoetherianRing A B
∀ (q : Ideal B) [q.IsPrime],
let p := q.comap f
let h := Localization.localRingHom p q f rfl
letI : IsLocalHom h := Localization.isLocalHom_localRingHom p q f rfl
IsCompleteIntersectionHom
(adicCompletionMap h (IsLocalRing.maximalIdeal (Localization.AtPrime p))
(IsLocalRing.maximalIdeal (Localization.AtPrime q))
(IsLocalRing.map_maximalIdeal_le h))
Tag 09QF, a lemma
Tag 09QF in the Stacks Project.
LocalCompleteIntersection.isLocalCompleteIntersectionRing_and_hasFiniteTorDimension_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FiniteTypeTorCriterion.lean, line 73.
Avramov's criterion for a finite-type map whose image on spectra contains all closed points of the source.
public theorem isLocalCompleteIntersectionRing_and_hasFiniteTorDimension_iff
{A B : Type u} [CommRing A] [CommRing B] [IsNoetherianRing A]
(f : A →+* B) (hf : f.FiniteType)
(himage : ∀ (m : Ideal A), m.IsMaximal →
∃ q : Ideal B, q.IsPrime ∧ q.comap f = m) :
(letI : Algebra A B := f.toAlgebra
letI : Algebra.FiniteType A B := hf
letI : IsNoetherianRing B := Algebra.FiniteType.isNoetherianRing A B
IsLocalCompleteIntersectionRing B ∧
ModuleHasFiniteTorDimension
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct A).tensor
(canonicalTensorComparison A) (canonicalTensorIsLeftDerived A)
(ModuleCat.of A B)) ↔
(IsLocalCompleteIntersectionRing A ∧ f.IsLocalCompleteIntersection)
Sources
Section23.10 Smooth ring maps and diagonals#
Section 23.10 of the Stacks Project, Tag 0FCV. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0FCW, a lemma
Tag 0FCW in the Stacks Project.
StacksDraft.Smooth.exists_smooth_isLocalization_of_hasProjectiveDimensionLT_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/PerfectDiagonal.lean, line 1211.
Stacks 0FCW. Let
A → Bbe a flat ring map, essentially of finite type, from a Noetherian ring to a local ring. IfBhas finite projective dimension overB ⊗[A] B, thenBis the localization of a smoothA-algebra.The source states this for a local homomorphism of Noetherian local rings whose diagonal is perfect; that form is
StacksDraft.Smooth.exists_smooth_isLocalization_of_isPerfect_diagonal. Finite projective dimension of the diagonal gives formal smoothness byStacksDraft.Smooth.formallySmooth_of_hasProjectiveDimensionLT_diagonal, and a formally smooth local algebra essentially of finite type is a localization of a smooth algebra byStacksDraft.Smooth.exists_smooth_isLocalization_of_formallySmooth.
public theorem exists_smooth_isLocalization_of_hasProjectiveDimensionLT_diagonal
(A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsLocalRing B] [IsNoetherianRing A]
[Algebra A B] [Module.Flat A B] [Algebra.EssFiniteType A B]
(hpd : letI := (Algebra.TensorProduct.lmul' (R := A) (S := B)).toRingHom.toAlgebra
∃ n : ℕ, HasProjectiveDimensionLT (ModuleCat.of (TensorProduct A B B) B) n) :
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C) (_ : Algebra.Smooth A C)
(M : Submonoid C) (_ : Algebra C B), IsScalarTower A C B ∧ IsLocalization M B
Tag 0FCX, a lemma
Tag 0FCX in the Stacks Project.
StacksDraft.Smooth.smooth_of_flat_of_hasProjectiveDimensionLT_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/PerfectDiagonal.lean, line 1384.
Stacks 0FCX. Let
A → Bbe a flat finite type ring map from a Noetherian ring. IfBhas finite projective dimension overB ⊗[A] B, thenBis a smoothA-algebra.The source assumes that
Bis Noetherian and that the diagonal is perfect; that form isStacksDraft.Smooth.smooth_of_flat_of_isPerfect_diagonal. Smoothness is local onB, and at a prime𝔮ofBover𝔭ofAfinite projective dimension of the diagonal passes to the localized mapA_𝔭 → B_𝔮, which is then formally smooth byStacksDraft.Smooth.formallySmooth_of_hasProjectiveDimensionLT_diagonal.
public theorem smooth_of_flat_of_hasProjectiveDimensionLT_diagonal
(A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
[IsNoetherianRing A] [Module.Flat A B] [Algebra.FiniteType A B]
(hpd : letI := (Algebra.TensorProduct.lmul' (R := A) (S := B)).toRingHom.toAlgebra
∃ n : ℕ, HasProjectiveDimensionLT (ModuleCat.of (TensorProduct A B B) B) n) :
Algebra.Smooth A B
Sources
Section23.11 Freeness of the conormal module#
Section 23.11 of the Stacks Project, Tag 0FJP. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0FJQ, a lemma
Tag 0FJQ in the Stacks Project.
Ideal.exists_isRegular_generator_of_isCompl_cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/ConormalFreeSummand.lean, line 1155.
A direct summand of
I/I²isomorphic toR/I, for an idealIof finite projective dimension in a Noetherian local ring, is generated by the class of a nonzerodivisor ofRbelonging toI.
theorem exists_isRegular_generator_of_isCompl_cotangent
(R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
(I : Ideal R) (hI : Module.projectiveDimension R I ≠ ⊤)
(F : Submodule (R ⧸ I) I.Cotangent)
(hF : ∃ F' : Submodule (R ⧸ I) I.Cotangent, IsCompl F F')
(hFfree : Nonempty (F ≃ₗ[R ⧸ I] R ⧸ I)) :
∃ (x : R) (hx : x ∈ I), IsRegular x ∧
Submodule.span (R ⧸ I) {I.toCotangent ⟨x, hx⟩} = F
Tag 0FJR, a lemma
Tag 0FJR in the Stacks Project.
Ideal.exists_isRegular_of_isCompl_cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/ConormalFreeSummand.lean, line 1139.
Stacks Project, Tag 0FJR, with the positive-rank properness correction. A finite-rank free direct summand of
I/I², for an idealIof finite projective dimension in a Noetherian local ring, lifts to a regular sequence inIwhose residue classes generate that summand, providedIis proper when the rank is positive.
theorem exists_isRegular_of_isCompl_cotangent
{R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
(I : Ideal R) (r : ℕ) (F : Submodule (R ⧸ I) I.Cotangent)
(hproper : r = 0 ∨ I ≠ ⊤)
(hpd : Module.projectiveDimension R I ≠ ⊤)
(hcompl : ∃ F' : Submodule (R ⧸ I) I.Cotangent, IsCompl F F')
(hfree : Nonempty (Module.Basis (Fin r) (R ⧸ I) F)) :
∃ x : Fin r → I,
RingTheory.Sequence.IsRegular R (List.ofFn fun i ↦ (x i : R)) ∧
Submodule.span (R ⧸ I) (Set.range fun i ↦ I.toCotangent (x i)) = F
Tag 0FJS, a proposition
Tag 0FJS in the Stacks Project.
Ideal.isRegular_of_projectiveDimension_ne_top_of_isFiniteLocallyFree_cotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RegularIdealOfLocallyFreeConormal.lean, line 364.
An ideal of a Noetherian ring which has finite projective dimension and whose conormal module is finite locally free over the quotient is a regular ideal.
public theorem isRegular_of_projectiveDimension_ne_top_of_isFiniteLocallyFree_cotangent
(I : Ideal R) (hpd : Module.projectiveDimension R I ≠ ⊤)
(hconormal : Module.IsFiniteLocallyFree (R ⧸ I) I.Cotangent) : I.IsRegular
Tag 0FJT, a lemma
Tag 0FJT in the Stacks Project.
NaiveCotangent.hasTorAmplitude_tfae_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/NaiveCotangentPerfect.lean, line 701.
Let
A → Bbe a perfect ring homomorphism of Noetherian rings. Then the naive cotangent complexNL_{B/A}has Tor amplitude in[-1, 0]if and only if it is a perfect object ofD(B)with Tor amplitude in[-1, 0], if and only ifA → Bis a local complete intersection.
public theorem hasTorAmplitude_tfae_isLocalCompleteIntersection
(A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
[IsNoetherianRing A] [IsNoetherianRing B]
(hperfect : RingHom.IsPerfectRingMap A B
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct A).tensor
(canonicalTensorComparison A) (canonicalTensorIsLeftDerived A)) :
List.TFAE
[HasTorAmplitude
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct B).tensor
(canonicalTensorComparison B) (canonicalTensorIsLeftDerived B)
(naiveCotangentObject A B) (-1) 0,
StacksDraft.Perfect.IsPerfect (naiveCotangentObject A B) ∧
HasTorAmplitude
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct B).tensor
(canonicalTensorComparison B) (canonicalTensorIsLeftDerived B)
(naiveCotangentObject A B) (-1) 0,
RingHom.IsLocalCompleteIntersection (algebraMap A B)]
Tag 0FJV, a lemma
Tag 0FJV in the Stacks Project.
NaiveCotangent.hasTorAmplitude_tfae_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/NaiveCotangentPerfect.lean, line 921.
Let
A → Bbe a flat ring homomorphism of finite presentation. Then the naive cotangent complexNL_{B/A}has Tor amplitude in[-1, 0]if and only if it is a perfect object ofD(B)with Tor amplitude in[-1, 0], if and only ifA → Bis syntomic, if and only ifA → Bis a local complete intersection.
public theorem hasTorAmplitude_tfae_syntomic
(A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
[Module.Flat A B] [Algebra.FinitePresentation A B] :
List.TFAE
[HasTorAmplitude
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct B).tensor
(canonicalTensorComparison B) (canonicalTensorIsLeftDerived B)
(naiveCotangentObject A B) (-1) 0,
StacksDraft.Perfect.IsPerfect (naiveCotangentObject A B) ∧
HasTorAmplitude
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct B).tensor
(canonicalTensorComparison B) (canonicalTensorIsLeftDerived B)
(naiveCotangentObject A B) (-1) 0,
Algebra.Syntomic A B,
RingHom.IsLocalCompleteIntersection (algebraMap A B)]
Sources
Section23.12 Koszul complexes and Tate resolutions#
Section 23.12 of the Stacks Project, Tag 0GZ3. 4 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GZ4, a lemma
Tag 0GZ4 in the Stacks Project.
DividedPowers.TateResolution.exists_tateResolution_koszulPowers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/KoszulTateComparison.lean, line 1156.
Tag 0GZ4. Let
Rbe a Noetherian ring andf₁, …, f_r ∈ R. WriteK_mfor the Koszul divided power algebraR⟨ξ₁, …, ξ_r⟩withξᵢof degree one andd(ξᵢ) = fᵢ^m, andK_M → K_mfor the transition mapξᵢ ↦ fᵢ^(M-m) ξᵢ. Then for everynthere is anN ≥ nand mapsK_N → A → R/(f₁^N, …, f_r^N)andA → K_nsuch that(A, d, γ)is a divided power differential graded algebra as in Definition 09PJ,A → R/(f₁^N, …, f_r^N)is a quasi-isomorphism, the compositionK_N → A → R/(f₁^N, …, f_r^N)is the canonical map, the compositionK_N → A → K_nis the transition map,A₀ = R → R/(f₁^N, …, f_r^N)is the canonical surjection,Ais a graded divided power polynomial algebra overRwith finitely many generators in each degree, andA → K_nis a homomorphism of differential gradedR-algebras compatible with divided powers inducing the canonical mapR/(f₁^N, …, f_r^N) → R/(f₁^n, …, f_r^n)on homology in degree zero.
public theorem exists_tateResolution_koszulPowers [IsNoetherianRing R] (f : Fin r → R) (n : ℕ) :
∃ (N : ℕ) (hN : n ≤ N) (A : GradedDPAlgebra.{u, u} R) (d : A.carrier →ₗ[R] A.carrier)
(ι : R →ₐ[R] A.carrier) (ε : A.carrier →ₐ[R] R ⧸ koszulPowerIdeal f N)
(α : ExteriorAlgebra R (Fin r → R) →ₐ[R] A.carrier)
(β : A.carrier →ₐ[R] ExteriorAlgebra R (Fin r → R)),
-- (1) `(A, d, γ)` is as in Definition 09PJ
IsDifferentialGradedAlgebra A.grade d ∧ IsCompatibleWithDifferential A.gamma d ∧
-- (6) a graded divided power polynomial algebra over `R`, degreewise finitely generated
(∃ P : GradedDividedPowerPolynomial A.grade A.gamma ι, ∀ i : ℕ, Finite (P.indices i)) ∧
-- (5) `A₀ = R`, and `A₀ → R/(f₁^N, …, f_r^N)` is the canonical surjection
Function.Injective ι ∧
(∀ a : A.carrier, a ∈ A.grade 0 ↔ ∃ c : R, ι c = a) ∧
(∀ c : R, ε (ι c) = Ideal.Quotient.mk (koszulPowerIdeal f N) c) ∧
-- (2) `ε` is a quasi-isomorphism onto `R/(f₁^N, …, f_r^N)`
Function.Surjective ε ∧
(∀ (k : ℕ) (a : A.carrier), 0 < k → a ∈ A.grade k → ε a = 0) ∧
(∀ a : A.carrier, ε (d a) = 0) ∧
(∀ a : A.carrier, a ∈ A.grade 0 → ε a = 0 → ∃ b ∈ A.grade 1, d b = a) ∧
(∀ (k : ℕ) (a : A.carrier), a ∈ A.grade (k + 1) → d a = 0 →
∃ b ∈ A.grade (k + 2), d b = a) ∧
-- `α : K_N → A` is a morphism of differential graded divided power algebras
(∀ (k : ℕ) (x : ExteriorAlgebra R (Fin r → R)),
x ∈ exteriorGrade R (Fin r → R) k → α x ∈ A.grade k) ∧
(∀ x, α (koszulPowerDifferential f N x) = d (α x)) ∧
(∀ (k : ℕ) (x : ExteriorAlgebra R (Fin r → R)),
x ∈ positiveEvenPart (exteriorGrade R (Fin r → R)) →
α ((exteriorDividedPowerStructure R r).dpow k x) = A.gamma.dpow k (α x)) ∧
-- (7) `β : A → K_n` is a morphism of differential graded divided power algebras
(∀ (k : ℕ) (a : A.carrier), a ∈ A.grade k → β a ∈ exteriorGrade R (Fin r → R) k) ∧
(∀ a, β (d a) = koszulPowerDifferential f n (β a)) ∧
(∀ (k : ℕ) (a : A.carrier), a ∈ positiveEvenPart A.grade →
β (A.gamma.dpow k a) = (exteriorDividedPowerStructure R r).dpow k (β a)) ∧
-- (3) the composition `K_N → A → R/(f₁^N, …, f_r^N)` is the canonical map
(∀ x, ε (α x) = koszulPowerAugmentation f N x) ∧
-- (4) the composition `K_N → A → K_n` is the transition map
(∀ x, β (α x) = koszulPowerTransitionHom f N n x) ∧
-- (7) `β` is the identity of `R` in degree zero, hence induces the canonical map
-- `R/(f₁^N, …, f_r^N) → R/(f₁^n, …, f_r^n)` on homology in degree zero
(∀ c : R, β (ι c) = algebraMap R (ExteriorAlgebra R (Fin r → R)) c) ∧
(∀ a : A.carrier, a ∈ A.grade 0 →
koszulPowerAugmentation f n (β a) =
Ideal.Quotient.factor (koszulPowerIdeal_le_of_le f hN) (ε a))
Tag 0GZ5, a remark
Tag 0GZ5 in the Stacks Project.
DividedPowers.TateResolution.exists_koszulTateProIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/KoszulTateProSystem.lean, line 296.
Tag 0GZ5. Let
Rbe a Noetherian ring andf₁, …, f_r ∈ R. WriteK_mfor the Koszul divided power algebra of them-th powers andK_M → K_mfor its transition maps. Then there is a sequence of exponents1 = n₀ < n₁ < n₂ < ⋯, cofinal inℕ, and for eachimapsK_{nᵢ₊₁} → Aᵢ → R/(f₁^{nᵢ₊₁}, …, f_r^{nᵢ₊₁})andAᵢ → K_{nᵢ}as in Tag 0GZ4, such that withAᵢ₊₁ → Aᵢthe compositeAᵢ₊₁ → K_{nᵢ₊₁} → Aᵢthe ladder commutes and the two inverse systems(K_n)and(Aᵢ)are pro-isomorphic as differential gradedR-algebras with compatible divided powers: the compositeK_{nᵢ₊₁} → Aᵢ → K_{nᵢ}is the Koszul transition map, and the compositeAᵢ₊₁ → K_{nᵢ₊₁} → Aᵢis the Tate transition map.
public theorem exists_koszulTateProIso (f : Fin r → R) :
∃ (n : ℕ → ℕ) (stage : ∀ i : ℕ, KoszulTateStage f (n i)),
n 0 = 1 ∧ StrictMono n ∧ (∀ k : ℕ, ∃ i : ℕ, k ≤ n i) ∧
(∀ i : ℕ, (stage i).topPower = n (i + 1)) ∧
-- the upper square of the ladder commutes
(∀ (i : ℕ) (x : ExteriorAlgebra R (Fin r → R)),
(stage (i + 1)).proTransition (stage i) ((stage (i + 1)).up x) =
(stage i).up (koszulPowerTransitionHom f (n (i + 2)) (n (i + 1)) x)) ∧
-- the lower square of the ladder commutes
(∀ (i : ℕ) (a : (stage (i + 1)).A.carrier),
(stage i).down ((stage (i + 1)).proTransition (stage i) a) =
koszulPowerTransitionHom f (n (i + 1)) (n i) ((stage (i + 1)).down a)) ∧
-- the composite `K_{nᵢ₊₁} → Aᵢ → K_{nᵢ}` is the transition map of the Koszul system
(∀ (i : ℕ) (x : ExteriorAlgebra R (Fin r → R)),
(stage i).down ((stage i).up x) =
koszulPowerTransitionHom f (n (i + 1)) (n i) x) ∧
-- the composite `Aᵢ₊₁ → K_{nᵢ₊₁} → Aᵢ` is the transition map of the Tate system
(∀ i : ℕ, (stage (i + 1)).proTransition (stage i) =
((stage i).up).comp ((stage (i + 1)).down)) ∧
-- the transition maps of the Tate system are maps of differential graded `R`-algebras
-- with compatible divided powers
(∀ (i k : ℕ) (a : (stage (i + 1)).A.carrier), a ∈ (stage (i + 1)).A.grade k →
(stage (i + 1)).proTransition (stage i) a ∈ (stage i).A.grade k) ∧
(∀ (i : ℕ) (a : (stage (i + 1)).A.carrier),
(stage (i + 1)).proTransition (stage i) ((stage (i + 1)).d a) =
(stage i).d ((stage (i + 1)).proTransition (stage i) a)) ∧
(∀ (i k : ℕ) (a : (stage (i + 1)).A.carrier),
a ∈ positiveEvenPart (stage (i + 1)).A.grade →
(stage (i + 1)).proTransition (stage i) ((stage (i + 1)).A.gamma.dpow k a) =
(stage i).A.gamma.dpow k ((stage (i + 1)).proTransition (stage i) a))
Tag 0GZ6, a lemma
Tag 0GZ6 in the Stacks Project.
DividedPowers.TateResolution.exact_degreeZeroHomology_oddVariableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/DegreeZeroHomology.lean, line 205. The attribute's comment: “degree_one”.
Multiplication by the cycle followed by the inclusion into the degree-one extension is right exact on degree-zero homology.
public theorem exact_degreeZeroHomology_oddVariableExtension
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(dA : A →ₗ[R] A) [IsDifferentialGradedAlgebra 𝒜 dA]
(f : A) (hf_grade : f ∈ 𝒜 0)
(dExt : OddVariableExtension 𝒜 1 →ₗ[R] OddVariableExtension 𝒜 1)
[IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1) dExt]
(hdExt : ∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 1 x) =
OddVariableExtension.inclusion 𝒜 1 (dA x))
(hT : dExt (OddVariableExtension.generator 𝒜 1) =
OddVariableExtension.inclusion 𝒜 1 f) :
LinearMap.range (mulOnDegreeZeroHomology 𝒜 dA f hf_grade) =
LinearMap.ker (toExtensionOnDegreeZeroHomology 𝒜 dA dExt hdExt)
DividedPowers.TateResolution.surjective_degreeZeroHomology_oddVariableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/DegreeZeroHomology.lean, line 266. The attribute's comment: “degree_one”.
The inclusion onto degree-zero homology of the extension is surjective.
public theorem surjective_degreeZeroHomology_oddVariableExtension
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜]
(dA : A →ₗ[R] A)
(dExt : OddVariableExtension 𝒜 1 →ₗ[R] OddVariableExtension 𝒜 1)
(hdExt : ∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 1 x) =
OddVariableExtension.inclusion 𝒜 1 (dA x)) :
Function.Surjective
(toExtensionOnDegreeZeroHomology 𝒜 dA dExt hdExt)
DividedPowers.TateResolution.evenVariableSpectralSequence_degree_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/EvenVariableSpectralSequence.lean, line 883. The attribute's comment: “degree_two”.
The spectral sequence of a degree-two divided-power variable, Tag 0GZ6 part (2).
Let
(A, dA)be a strictly graded-commutative differential graded algebra, letfbe a cycle of degree1 = 2 - 1, and letA⟨T⟩be the extension by a divided-power variable of degree two withdT = f, with the differential of Tag 09PM. FilteringA⟨T⟩byFᵖ = ⨁_{n ≤ p} A T⁽ⁿ⁾gives a spectral sequence, and this records the four assertions of the tag:
- its first page in the bidegree with filtration index
iand total degree2 i + qis the degree-qhomology ofA, by an isomorphism carrying the class of a degree-qcycleξto the page class of the representativeξ T⁽ⁱ⁾;- that bidegree is
(i, j)withj - i = q, so the first page in the bidegree(i, j)isH_{j - i}(A) · T⁽ⁱ⁾, as the tag writes it;- its first differential sends the class of
ξ T⁽ⁱ⁺¹⁾to the class of(signRingHom 𝒜 1 ξ * f) T⁽ⁱ⁾ = ((-1) ^ q • (ξ f)) T⁽ⁱ⁾, that is, it is multiplication byfwith the Koszul sign of the degree ofξ;- it converges, the filtration being finite in every degree, and abuts to the homology of the complex of
A⟨T⟩, whose degree-kterm is the degree-khomology ofA⟨T⟩.The sign of the first differential is the one of
evenPolynomialDifferential_monomial; the tag writesf ξunsigned, which is the same up to the unit(-1) ^ qof the coefficient ring.
public theorem evenVariableSpectralSequence_degree_two (hf_grade : f ∈ 𝒜 1) (hf_cycle : dA f = 0)
(h0 : ∀ p : P, algebraMap P A p ∈ 𝒜 0) :
letI : IsDifferentialGradedAlgebra (EvenVariableAlgebra.grade 𝒜 2)
(evenPolynomialDifferential 𝒜 dA f) :=
evenPolynomialDifferential_two_isDGA 𝒜 dA f hf_grade hf_cycle
(∀ i q : ℕ, ∃ e : coefficientHomology 𝒜 dA h0 q ≃ₗ[P]
((evenVariableSpectralSequence 𝒜 dA f h0).page 1 le_rfl).X
(filtrationBidegree true (i : ℤ) ((2 * i + q : ℕ) : ℤ)),
∀ ξ : ↥(coefficientCycles 𝒜 dA h0 q),
e (Submodule.Quotient.mk ξ) = evenVariablePageOneRep 𝒜 dA f h0 i q ξ) ∧
(∀ i q : ℕ, filtrationBidegree true (i : ℤ) ((2 * i + q : ℕ) : ℤ) =
((i : ℤ), (i : ℤ) + q)) ∧
(∀ (i q : ℕ) (ξ : ↥(coefficientCycles 𝒜 dA h0 q)),
((evenVariableSpectralSequence 𝒜 dA f h0).page 1 le_rfl).d
(filtrationBidegree true ((i + 1 : ℕ) : ℤ) ((2 * (i + 1) + q : ℕ) : ℤ))
(filtrationBidegree true (i : ℤ) ((2 * i + (q + 1) : ℕ) : ℤ))
(evenVariablePageOneRep 𝒜 dA f h0 (i + 1) q ξ) =
evenVariablePageOneRep 𝒜 dA f h0 i (q + 1)
⟨signRingHom 𝒜 1 (ξ : A) * f,
signRingHom_mul_mem_coefficientCycles 𝒜 dA f h0 hf_grade hf_cycle q ξ⟩ ∧
signRingHom 𝒜 1 (ξ : A) * f = (-1 : R) ^ q • ((ξ : A) * f)) ∧
((evenVariableFiltrationData 𝒜 dA f h0).Converges ∧
HomologicalSpectralSequenceAbutsTo (evenVariableSpectralSequence 𝒜 dA f h0)
(fun n => (evenVariableCochainComplex 𝒜 dA f h0).homology (-n)) ∧
∀ k : ℕ, Nonempty ((evenVariableCochainComplex 𝒜 dA f h0).homology (-(k : ℤ)) ≅
ModuleCat.of P (evenVariableHomology 𝒜 dA f h0 k)))
DividedPowers.TateResolution.range_mulOnGradeHomology_eq_ker_toExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 570. The attribute's comment: “degree_one”.
Exactness at the second copy of
Hₙ(A): the image of multiplication byfis the kernel of the map induced by the inclusion into the odd degree-one extension.
public theorem range_mulOnGradeHomology_eq_ker_toExtension {R : Type u} {A : Type v}
[CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] (f : A) (hf : f ∈ 𝒜 0)
(dExt : OddVariableExtension 𝒜 1 →ₗ[R] OddVariableExtension 𝒜 1)
[IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1) dExt]
(hdExt : ∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 1 x) =
OddVariableExtension.inclusion 𝒜 1 (dA x))
(hT : dExt (OddVariableExtension.generator 𝒜 1) = OddVariableExtension.inclusion 𝒜 1 f)
(n : ℕ) :
LinearMap.range (mulOnGradeHomology 𝒜 dA f hf n) =
LinearMap.ker (toExtensionOnGradeHomology 𝒜 dA dExt hdExt n)
DividedPowers.TateResolution.range_toExtensionOnGradeHomology_eq_ker_connecting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 640. The attribute's comment: “degree_one”.
Exactness at
Hₙ₊₁(A⟨T⟩): the image of the map induced by the inclusion in degreen + 1is the kernel of the connecting map out of degreen + 1.
public theorem range_toExtensionOnGradeHomology_eq_ker_connecting {R : Type u} {A : Type v}
[CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA]
(dExt : OddVariableExtension 𝒜 1 →ₗ[R] OddVariableExtension 𝒜 1)
[IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1) dExt]
(hdExt : ∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 1 x) =
OddVariableExtension.inclusion 𝒜 1 (dA x)) (n : ℕ) :
LinearMap.range (toExtensionOnGradeHomology 𝒜 dA dExt hdExt (n + 1)) =
LinearMap.ker (connectingOnGradeHomology 𝒜 dA dExt hdExt n)
DividedPowers.TateResolution.range_connectingOnGradeHomology_eq_ker_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 730. The attribute's comment: “degree_one”.
Exactness at the first copy of
Hₙ(A): the image of the connecting map out of degreen + 1is the kernel of multiplication byf.
public theorem range_connectingOnGradeHomology_eq_ker_mul {R : Type u} {A : Type v}
[CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] (f : A) (hf : f ∈ 𝒜 0)
(dExt : OddVariableExtension 𝒜 1 →ₗ[R] OddVariableExtension 𝒜 1)
[IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1) dExt]
(hdExt : ∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 1 x) =
OddVariableExtension.inclusion 𝒜 1 (dA x))
(hT : dExt (OddVariableExtension.generator 𝒜 1) = OddVariableExtension.inclusion 𝒜 1 f)
(n : ℕ) :
LinearMap.range (connectingOnGradeHomology 𝒜 dA dExt hdExt n) =
LinearMap.ker (mulOnGradeHomology 𝒜 dA f hf n)
DividedPowers.TateResolution.surjective_toExtensionOnGradeHomology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 841. The attribute's comment: “degree_one”.
The right end of the long exact sequence: the map to the degree-zero homology of the odd degree-one extension is surjective. This is
surjective_degreeZeroHomology_oddVariableExtensiontransported along the identificationgradeHomologyZeroEquivof degree-zero graded homology with the degree-zero quotient of the previous file, rather than a second proof of it.
public theorem surjective_toExtensionOnGradeHomology_zero {R : Type u} {A : Type v}
[CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA]
(dExt : OddVariableExtension 𝒜 1 →ₗ[R] OddVariableExtension 𝒜 1)
[IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1) dExt]
(hdExt : ∀ x : A, dExt (OddVariableExtension.inclusion 𝒜 1 x) =
OddVariableExtension.inclusion 𝒜 1 (dA x)) :
Function.Surjective (toExtensionOnGradeHomology 𝒜 dA dExt hdExt 0)
DividedPowers.TateResolution.range_mulOnGradeHomology_eq_ker_toExtension_oddExtensionDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 874. The attribute's comment: “degree_one”.
Exactness at the second copy of
Hₙ(A)for the differential of Tag 09PM: no differential on the extension is assumed, the one of Tag 09PM being used.
public theorem range_mulOnGradeHomology_eq_ker_toExtension_oddExtensionDifferential
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] (f : A) (hf : f ∈ 𝒜 0) (n : ℕ) :
letI : IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1)
(oddExtensionDifferential 𝒜 dA 1 f) := oddExtensionDifferential_one_isDGA 𝒜 dA f hf
LinearMap.range (mulOnGradeHomology 𝒜 dA f hf n) =
LinearMap.ker (toExtensionOnGradeHomology 𝒜 dA (oddExtensionDifferential 𝒜 dA 1 f)
(oddExtensionDifferential_inclusion 𝒜 dA 1 f) n)
DividedPowers.TateResolution.range_toExtensionOnGradeHomology_eq_ker_connecting_oddExtensionDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 891. The attribute's comment: “degree_one”.
Exactness at
Hₙ₊₁(A⟨T⟩)for the differential of Tag 09PM: no differential on the extension is assumed, the one of Tag 09PM being used.
public theorem range_toExtensionOnGradeHomology_eq_ker_connecting_oddExtensionDifferential
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] (f : A) (hf : f ∈ 𝒜 0) (n : ℕ) :
letI : IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1)
(oddExtensionDifferential 𝒜 dA 1 f) := oddExtensionDifferential_one_isDGA 𝒜 dA f hf
LinearMap.range (toExtensionOnGradeHomology 𝒜 dA (oddExtensionDifferential 𝒜 dA 1 f)
(oddExtensionDifferential_inclusion 𝒜 dA 1 f) (n + 1)) =
LinearMap.ker (connectingOnGradeHomology 𝒜 dA (oddExtensionDifferential 𝒜 dA 1 f)
(oddExtensionDifferential_inclusion 𝒜 dA 1 f) n)
DividedPowers.TateResolution.range_connectingOnGradeHomology_eq_ker_mul_oddExtensionDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 908. The attribute's comment: “degree_one”.
Exactness at the first copy of
Hₙ(A)for the differential of Tag 09PM: no differential on the extension is assumed, the one of Tag 09PM being used.
public theorem range_connectingOnGradeHomology_eq_ker_mul_oddExtensionDifferential
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] (f : A) (hf : f ∈ 𝒜 0) (n : ℕ) :
letI : IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1)
(oddExtensionDifferential 𝒜 dA 1 f) := oddExtensionDifferential_one_isDGA 𝒜 dA f hf
LinearMap.range (connectingOnGradeHomology 𝒜 dA (oddExtensionDifferential 𝒜 dA 1 f)
(oddExtensionDifferential_inclusion 𝒜 dA 1 f) n) =
LinearMap.ker (mulOnGradeHomology 𝒜 dA f hf n)
DividedPowers.TateResolution.surjective_toExtensionOnGradeHomology_zero_oddExtensionDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DividedPowers/TateResolution/OddVariableHomologySequence.lean, line 925. The attribute's comment: “degree_one”.
The right end of the long exact sequence for the differential of Tag 09PM: no differential on the extension is assumed, the one of Tag 09PM being used.
public theorem surjective_toExtensionOnGradeHomology_zero_oddExtensionDifferential
{R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A]
(𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsStrictlyGradedComm 𝒜] (dA : A →ₗ[R] A)
[IsDifferentialGradedAlgebra 𝒜 dA] (f : A) (hf : f ∈ 𝒜 0) :
letI : IsDifferentialGradedAlgebra (OddVariableExtension.grade 𝒜 1)
(oddExtensionDifferential 𝒜 dA 1 f) := oddExtensionDifferential_one_isDGA 𝒜 dA f hf
Function.Surjective (toExtensionOnGradeHomology 𝒜 dA (oddExtensionDifferential 𝒜 dA 1 f)
(oddExtensionDifferential_inclusion 𝒜 dA 1 f) 0)
Tag 0GZ7, a lemma
Tag 0GZ7 in the Stacks Project.
Koszul.exists_derivedComparisonArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Koszul/DerivedComparison.lean, line 243.
Tag 0GZ7. "For all
n ≥ t ≥ 1there exists anN > nand a mapK_t → K_n ⊗_R K_tinD(K_N, d)whose composition with the multiplication map is the transition map (in either direction)."Both composites are asserted: postcomposition with the multiplication map
μ_n : K_n ⊗_R K_t → K_tis the transition mapK_t → K_t, which is the identity, and precomposition with the multiplication mapμ_N : K_N ⊗_R K_t → K_tis the transition mapτ_{N,n} ⊗ id. HereK_tcarries the leftK_N-action throughτ_{N,t}andK_n ⊗_R K_tcarries it throughξᵢ ↦ fᵢ^{N-n} ξᵢ ⊗ 1; left differential graded modules are recorded as right modules over the graded opposite algebra.
theorem exists_derivedComparisonArrow (f : Fin r → R) {n t : ℕ} (ht : 1 ≤ t) (htn : t ≤ n) :
∃ (N : ℕ) (hnN : n < N),
∃ σ : (powDerived f N).obj (powRestrictedModule f ht (htn.trans hnN.le)) ⟶
(powDerived f N).obj (powTensorRestrictedModule f t (ht.trans htn) hnN.le),
σ ≫ (powDerived f N).map (powMulHom f ht htn hnN.le) =
CategoryStruct.id
((powDerived f N).obj (powRestrictedModule f ht (htn.trans hnN.le))) ∧
(powDerived f N).map (powMulBaseHom f ht (htn.trans hnN.le)) ≫ σ =
(powDerived f N).map (powTransitionTensorHom f t (ht.trans htn) hnN.le)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.