Bordism, formal groups and chromatic operations
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremThe symmetric 2-cocycle lemma, with uniqueness#
for n ≥ 2, a homogeneous symmetric
additive 2-cocycle of degree n over any commutative ring is r • C_n for a unique r.
TauCeti.existsUnique_eq_smul_lazardCocycle.{u_1} {R : Type u_1} [CommRing R] {n : ℕ} (hn : 2 ≤ n)
{f : MvPolynomial (Fin 2) R} (hh : f.IsHomogeneous n) (hs : f.IsSymmetric)
(hf : f.IsAddCocycle₂) : ∃! r, f = r • TauCeti.lazardCocycle n R
Uses 1
ℤ
TheoremThe symmetric 2-cocycle lemma when 2 = 0, at powers of two#
If 2 = 0 in R, a
homogeneous symmetric additive 2-cocycle f of degree 2ᵏ over R with zero diagonal
f(X, X) = 0 is zero.
TauCeti.eq_zero_of_two_eq_zero_of_aeval_X_X_eq_zero.{u_1} {R : Type u_1} [CommRing R] (h2 : 2 = 0)
{k : ℕ} {f : MvPolynomial (Fin 2) R} (hh : f.IsHomogeneous (2 ^ k)) (hs : f.IsSymmetric)
(hf : f.IsAddCocycle₂) (hd : (MvPolynomial.aeval ![Polynomial.X, Polynomial.X]) f = 0) : f = 0
Lean
Formalized in Tau Ceti as TauCeti.eq_zero_of_two_eq_zero_of_aeval_X_X_eq_zero.
Sources
Uses 1
ℤDefinitionLazard's computation of the indecomposables of the Lazard ring#
The ℤ-module
I ⧸ I² of indecomposables of L, for I the augmentation ideal, is free with basis the classes
of the generators xₙ ∈ L₂ₙ, n ≥ 1.
TauCeti.LazardRing.cotangentBasis : Module.Basis ℕ+ ℤ TauCeti.LazardRing.augmentationIdeal.Cotangent
Uses 1 · Used by 1
ℤDefinitionThe graded universal property of the Lazard ring#
for a commutative ring A graded by
𝒜, graded ring homomorphisms L →+*ᵍ A correspond to commutative formal group laws over A
whose coefficient of every monomial X^(d 0) Y^(d 1) lies in 𝒜 (2 (d 0 + d 1 - 1)), that is,
whose coefficient aᵢⱼ lies in 𝒜 (2 (i + j - 1)) for all i, j ≥ 1. A formal group law
corresponds to the homomorphism TauCeti.LazardRing.lift classifying it.
TauCeti.LazardRing.gradedLift.{u_1, u_5} {A : Type u_1} [CommRing A] {σ : Type u_5} [SetLike σ A]
[AddSubgroupClass σ A] {𝒜 : ℕ → σ} [SetLike.GradedMonoid 𝒜] :
{ F //
F.IsComm ∧
∀ (d : Fin 2 →₀ ℕ),
(MvPowerSeries.coeff d) F.toPowerSeries ∈ 𝒜 (2 * (Finsupp.degree d - 1)) } ≃
(TauCeti.LazardRing.grading →+*ᵍ 𝒜)
DefinitionStrict coordinate changes of commutative formal group laws are representable#
pairs of a
commutative formal group law F and a strict coordinate φ over R correspond to ring
homomorphisms L[b₁, b₂, …] →+* R. The homomorphism attached to (F, φ) restricts to the
homomorphism L →+* R classifying F and sends bᵢ to the coefficient of X^(i + 1) in φ.
TauCeti.LazardRing.coordinateChangeLift.{u_1} {R : Type u_1} [CommRing R] :
{ F // F.IsComm } × ↥TauCeti.FormalCoordinate.linearCoeff.ker ≃
(MvPolynomial ℕ+ TauCeti.LazardRing →+* R)
Uses 1 · Used by 1
TheoremCoassociativity (Δ ⊗ id) Δ = (id ⊗ Δ) Δ of the coproduct#
composition of strict
isomorphisms is associative. Both sides take values in the triple tensor product
Γ ⊗_L Γ ⊗_L Γ = MvPolynomial ℕ+ (Γ ⊗_L Γ), the pushout of Γ ⊗_L Γ along the target of its right
factor and of Γ along η_L, whose three factors are C ∘ C, C ∘ MvPolynomial.map η_R and
MvPolynomial.map (MvPolynomial.map η_R ∘ η_R). In it, Δ ⊗ id is tensorLift (C ∘ Δ, ι₃) with
ι₃ the third factor, and id ⊗ Δ is tensorLift (C ∘ C, ι₂₃ ∘ Δ) with
ι₂₃ = MvPolynomial.map (MvPolynomial.map η_R) the inclusion of the last two factors.
TauCeti.LazardRing.coproduct_coassoc :
(TauCeti.LazardRing.tensorLift
⟨(MvPolynomial.C.comp TauCeti.LazardRing.coproduct,
MvPolynomial.map
((MvPolynomial.map TauCeti.LazardRing.rightUnit).comp
TauCeti.LazardRing.rightUnit)),
⋯⟩).comp
TauCeti.LazardRing.coproduct =
(TauCeti.LazardRing.tensorLift
⟨(MvPolynomial.C.comp MvPolynomial.C,
(MvPolynomial.map (MvPolynomial.map TauCeti.LazardRing.rightUnit)).comp
TauCeti.LazardRing.coproduct),
⋯⟩).comp
TauCeti.LazardRing.coproduct
StructureTauCeti.FormalGroupHom#
A homomorphism of formal group laws is a series f with zero constant term such that
f(F(X,Y)) = G(f(X),f(Y)).
TauCeti.FormalGroupHom.{u_1} {R : Type u_1} [CommRing R] (F G : FormalGroup R) : Type u_1
StructureTauCeti.FormalGroupIso#
An isomorphism of formal group laws with specified mutually inverse homomorphisms. The inverse laws are equations of substitution operators on one-variable power series.
TauCeti.FormalGroupIso.{u_1} {R : Type u_1} [CommRing R] (F G : FormalGroup R) : Type u_1
Uses 1 · Used by 3
DefinitionFormalGroup.logIso#
The normalized logarithm is a strict isomorphism from F to the additive formal group,
with the formal exponential as its inverse.
FormalGroup.logIso.{u_1} {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] :
TauCeti.FormalGroupIso F FormalGroup.𝔾ₐ
Uses 2
DefinitionFormalGroup.height#
The height of a formal group law F over a field K of characteristic p: ⊤ if
multiplication by p on F is zero, and otherwise the exponent h such that the first nonzero
term of [p]_F(T) has degree p ^ h (see FormalGroup.height_eq_natCast_iff).
FormalGroup.height.{u_1} {K : Type u_1} [Field K] (F : FormalGroup K) (p : ℕ) : ℕ∞
Used by 1
TheoremThe p-series has order a power of p in characteristic p#
if p is a prime with
p = 0 in R and F is commutative, then either [p]_F = 0 or the first nonzero term of
[p]_F has degree p ^ h for some h ≥ 1.
FormalGroup.exists_order_nsmulSeries_eq_pow.{u_1} {R : Type u_1} [CommRing R] (F : FormalGroup R)
[F.IsComm] {p : ℕ} (hp : Nat.Prime p) (hpR : ↑p = 0) (h0 : F.nsmulSeries p ≠ 0) :
∃ h, h ≠ 0 ∧ (F.nsmulSeries p).order = ↑(p ^ h)
Used by 1
StructureFormalGroup.TopNilpotentPoint#
The points of a formal group law F in A: the elements of a topological ring A
satisfying PowerSeries.HasEval, that is, the topologically nilpotent elements. Evaluation of
power series over R at these elements converges when A is a complete, Hausdorff, linearly
topologised R-algebra; under those assumptions they form a group under x +_F y = F(x, y).
This is the analogue for A of the power-series carrier F.Point σ.
This is a structure rather than a subtype of A so that its group law, which depends on F, is
not confused with the ring operations of A.
FormalGroup.TopNilpotentPoint.{u_1, u_2} {R : Type u_1} [CommRing R] (F : FormalGroup R)
(A : Type u_2) [CommRing A] [TopologicalSpace A] : Type u_2
Used by 1
TheoremLazard's classification of formal group laws by height#
Over a separably closed field K
of characteristic p, two commutative formal group laws are isomorphic exactly when they have the
same height. In height ⊤ both are isomorphic to the additive formal group law.
FormalGroup.height_eq_height_iff_nonempty_formalGroupIso.{u_1} {K : Type u_1} [Field K]
[IsSepClosed K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (F G : FormalGroup K) [F.IsComm]
[G.IsComm] : F.height p = G.height p ↔ Nonempty (TauCeti.FormalGroupIso F G)
Lean
Formalized in Tau Ceti as FormalGroup.height_eq_height_iff_nonempty_formalGroupIso.
Sources
DefinitionLazard's theorem#
the Lazard ring is the polynomial ring ℤ[x₁, x₂, …] on the generators
xₙ = TauCeti.LazardRing.generator n. The isomorphism is evaluation at the generators.
TauCeti.LazardRing.mvPolynomialEquiv : MvPolynomial ℕ+ ℤ ≃ₐ[ℤ] TauCeti.LazardRing
Lean
Formalized in Tau Ceti as TauCeti.LazardRing.mvPolynomialEquiv.
Other forms
Lazard's theorem, generation. Formalized in Tau Ceti as TauCeti.LazardRing.adjoin_range_generator.
TauCeti.LazardRing.adjoin_range_generator :
Algebra.adjoin ℤ (Set.range TauCeti.LazardRing.generator) = ⊤
Lazard's theorem, graded. Formalized in Tau Ceti as TauCeti.LazardRing.mvPolynomialEquiv_mem_grading_iff.
TauCeti.LazardRing.mvPolynomialEquiv_mem_grading_iff {p : MvPolynomial ℕ+ ℤ} {n : ℕ} :
TauCeti.LazardRing.mvPolynomialEquiv p ∈ TauCeti.LazardRing.grading n ↔
MvPolynomial.IsWeightedHomogeneous (fun k => 2 * ↑k) p n
Lazard's theorem, integral independence. Formalized in Tau Ceti as TauCeti.LazardRing.algebraicIndependent_generator.
TauCeti.LazardRing.algebraicIndependent_generator :
AlgebraicIndependent ℤ TauCeti.LazardRing.generator
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.