The Lazard ring, its universal formal group law and its grading

A one-dimensional formal group law F(X, Y) over a commutative ring R satisfies F(X, 0) = X and F(0, Y) = Y, so it has the shape

F(X, Y) = X + Y + ∑_{i, j ≥ 1} aᵢⱼ Xⁱ Yʲ

and is determined by its coefficients aᵢⱼ ∈ R. Conversely, for a family a of coefficients the power series TauCeti.lazardSeries a = X + Y + ∑ aᵢⱼ Xⁱ Yʲ is a commutative formal group law exactly when the coefficients of G(G(X, Y), Z) - G(X, G(Y, Z)) and of G(X, Y) - G(Y, X) vanish. These coefficients are integral polynomials in the aᵢⱼ, so commutative formal group laws over R are the ring homomorphisms to R from the Lazard ring

L = ℤ[aᵢⱼ | i, j ≥ 1] ⧸ (the coefficients of associativity and commutativity).

The images of the variables aᵢⱼ in L form the coefficients of a commutative formal group law over L, the universal formal group law, and every commutative formal group law over R is its base change along exactly one ring homomorphism L →+* R.

Give aᵢⱼ the homological degree 2 (i + j - 1): this is the degree of the corresponding coefficient of the formal group law of a complex oriented cohomology theory, whose orientation has cohomological degree 2. The coefficients of associativity and commutativity are homogeneous for this weighting, so L is graded, L = ⨁ₙ Lₙ. Homogeneity is proved with the rescaling F^s(X, Y) = s⁻¹ F(s X, s Y) (FormalGroup.rescale): rescaling the universal formal group law by T² over L[T] is classified by a ring homomorphism L → L[T] sending the class of aᵢⱼ to T ^ (2 (i + j - 1)) aᵢⱼ, and the coefficient of Tⁿ in its value on the class of a polynomial is the class of the homogeneous component of degree n of that polynomial. The universal property then has a graded form: for a commutative ring A graded by 𝒜, the homomorphism L →+* A classifying a commutative formal group law over A is graded exactly when the coefficient of Xⁱ Yʲ lies in 𝒜 (2 (i + j - 1)) for all i, j.

Main definitions

• TauCeti.lazardSeries a: the power series X + Y + ∑_{i, j ≥ 1} aᵢⱼ Xⁱ Yʲ.
• TauCeti.LazardRing.relations: the ideal of ℤ[aᵢⱼ] generated by the coefficients of associativity and commutativity of the generic series X + Y + ∑ aᵢⱼ Xⁱ Yʲ.
• TauCeti.LazardRing: the Lazard ring, the quotient of ℤ[aᵢⱼ] by these relations, with quotient map TauCeti.LazardRing.mk.
• TauCeti.LazardRing.formalGroup: the universal commutative formal group law over the Lazard ring.
• TauCeti.LazardRing.lift: the bijection between commutative formal group laws over R and ring homomorphisms LazardRing →+* R.
• TauCeti.LazardRing.degree: the homological degree 2 (i + j - 1) of aᵢⱼ.
• TauCeti.LazardRing.grading: the grading of the Lazard ring by homological degree, with its GradedAlgebra instance.
• TauCeti.LazardRing.gradedLift: the bijection between commutative formal group laws over a graded ring whose coefficients are homogeneous of the matching degrees and graded ring homomorphisms out of the Lazard ring.

Main results

• FormalGroup.coeff_single_zero, FormalGroup.coeff_single_one: the coefficients of Xⁿ and Yⁿ in a formal group law are 1 for n = 1 and 0 otherwise.
• TauCeti.coeff_lazardSeries_eq: the coefficient of an arbitrary monomial in X + Y + ∑ aᵢⱼ Xⁱ Yʲ.
• TauCeti.lazardSeries_coeff_toPowerSeries: every formal group law is the series X + Y + ∑ aᵢⱼ Xⁱ Yʲ of its coefficients.
• TauCeti.LazardRing.coeff_formalGroup: the coefficient of Xⁱ Yʲ in the universal formal group law is the class of aᵢⱼ.
• TauCeti.LazardRing.map_lift: the universal formal group law base-changes along lift F to F.
• TauCeti.LazardRing.hom_ext: a ring homomorphism out of the Lazard ring is determined by the base change of the universal formal group law along it.
• TauCeti.LazardRing.lift_map: the bijection is natural in the coefficient ring.
• TauCeti.LazardRing.isHomogeneous_relations: the ideal of Lazard relations is homogeneous.
• TauCeti.LazardRing.coeff_formalGroup_mem_grading: the coefficient of Xⁱ Yʲ in the universal formal group law has degree 2 (i + j - 1).
• TauCeti.LazardRing.lift_mem_iff: the homomorphism classifying F is graded exactly when the coefficients of F are homogeneous of the matching degrees, for a target graded over any additive monoid receiving the degrees of L, such as ℤ.

References

• M. Lazard, Sur les groupes de Lie formels à un paramètre, Bull. Soc. Math. France 83 (1955).
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1.

theorem FormalGroup.coeff_single_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : (MvPowerSeries.coeff (Finsupp.single 0 n)) F.toPowerSeries = if n = 1 then 1 else 0

The coefficient of Xⁿ in a formal group law F(X, Y): since F(X, 0) = X, it is 1 for n = 1 and 0 otherwise.

theorem FormalGroup.coeff_single_one {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : (MvPowerSeries.coeff (Finsupp.single 1 n)) F.toPowerSeries = if n = 1 then 1 else 0

The coefficient of Yⁿ in a formal group law F(X, Y): since F(0, Y) = Y, it is 1 for n = 1 and 0 otherwise.

def TauCeti.lazardSeries {A : Type u_1} [Semiring A] (a : ℕ+ × ℕ+ → A) : MvPowerSeries (Fin 2) A

The power series X + Y + ∑_{i, j ≥ 1} aᵢⱼ Xⁱ Yʲ in two variables, for a family a of coefficients indexed by pairs of positive integers.

theorem TauCeti.coeff_lazardSeries_eq {A : Type u_1} [Semiring A] (a : ℕ+ × ℕ+ → A) (d : Fin 2 →₀ ℕ) : (MvPowerSeries.coeff d) (lazardSeries a) = if d 0 ≠ 0 ∧ d 1 ≠ 0 then a ((d 0).toPNat', (d 1).toPNat') else if d 0 + d 1 = 1 then 1 else 0

The coefficient of an arbitrary monomial X^(d 0) Y^(d 1) in X + Y + ∑ aᵢⱼ Xⁱ Yʲ: it is aᵢⱼ when both exponents are positive, 1 for the monomials X and Y, and 0 otherwise.

@[simp]

theorem TauCeti.coeff_lazardSeries {A : Type u_1} [Semiring A] (a : ℕ+ × ℕ+ → A) (i j : ℕ+) : (MvPowerSeries.coeff (Finsupp.single 0 ↑i + Finsupp.single 1 ↑j)) (lazardSeries a) = a (i, j)

The coefficient of Xⁱ Yʲ in X + Y + ∑ aᵢⱼ Xⁱ Yʲ is aᵢⱼ for i, j ≥ 1.

@[simp]

theorem TauCeti.coeff_single_zero_lazardSeries {A : Type u_1} [Semiring A] (a : ℕ+ × ℕ+ → A) (n : ℕ) : (MvPowerSeries.coeff (Finsupp.single 0 n)) (lazardSeries a) = if n = 1 then 1 else 0

The coefficient of Xⁿ in X + Y + ∑ aᵢⱼ Xⁱ Yʲ is 1 for n = 1 and 0 otherwise.

@[simp]

theorem TauCeti.coeff_single_one_lazardSeries {A : Type u_1} [Semiring A] (a : ℕ+ × ℕ+ → A) (n : ℕ) : (MvPowerSeries.coeff (Finsupp.single 1 n)) (lazardSeries a) = if n = 1 then 1 else 0

The coefficient of Yⁿ in X + Y + ∑ aᵢⱼ Xⁱ Yʲ is 1 for n = 1 and 0 otherwise.

@[simp]

theorem TauCeti.constantCoeff_lazardSeries {A : Type u_1} [Semiring A] (a : ℕ+ × ℕ+ → A) : MvPowerSeries.constantCoeff (lazardSeries a) = 0

The series X + Y + ∑ aᵢⱼ Xⁱ Yʲ has constant coefficient zero.

@[simp]

theorem TauCeti.map_lazardSeries {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] (φ : A →+* B) (a : ℕ+ × ℕ+ → A) : (MvPowerSeries.map φ) (lazardSeries a) = lazardSeries (⇑φ ∘ a)

Changing coefficients in X + Y + ∑ aᵢⱼ Xⁱ Yʲ applies the ring homomorphism to each aᵢⱼ.

theorem TauCeti.lazardSeries_coeff_toPowerSeries {R : Type u_3} [CommRing R] (F : FormalGroup R) : (lazardSeries fun (ij : ℕ+ × ℕ+) => (MvPowerSeries.coeff (Finsupp.single 0 ↑ij.1 + Finsupp.single 1 ↑ij.2)) F.toPowerSeries) = F.toPowerSeries

Every formal group law F(X, Y) is the series X + Y + ∑ aᵢⱼ Xⁱ Yʲ of its coefficients aᵢⱼ.

noncomputable def TauCeti.LazardRing.relations : Ideal (MvPolynomial (ℕ+ × ℕ+) ℤ)

The Lazard relations: the ideal of ℤ[aᵢⱼ | i, j ≥ 1] generated by the coefficients of G(G(X, Y), Z) - G(X, G(Y, Z)) and of G(X, Y) - G(Y, X), where G = X + Y + ∑ aᵢⱼ Xⁱ Yʲ is the generic series.

def TauCeti.LazardRing : Type

The Lazard ring L = ℤ[aᵢⱼ | i, j ≥ 1] ⧸ LazardRing.relations: the quotient of the polynomial ring on the coefficients aᵢⱼ of X + Y + ∑ aᵢⱼ Xⁱ Yʲ by the coefficients of associativity and commutativity. Ring homomorphisms out of it classify commutative formal group laws (TauCeti.LazardRing.lift).

@[instance_reducible]

noncomputable instance TauCeti.instCommRingLazardRing : CommRing LazardRing

noncomputable def TauCeti.LazardRing.mk : MvPolynomial (ℕ+ × ℕ+) ℤ →+* LazardRing

The quotient map ℤ[aᵢⱼ] →+* LazardRing.

theorem TauCeti.LazardRing.mk_surjective : Function.Surjective ⇑mk

Every element of the Lazard ring is the class of a polynomial in the aᵢⱼ.

theorem TauCeti.LazardRing.ker_mk : RingHom.ker mk = relations

The kernel of the quotient map ℤ[aᵢⱼ] →+* LazardRing is the ideal of Lazard relations.

noncomputable def TauCeti.LazardRing.formalGroup : FormalGroup LazardRing

The universal formal group law X + Y + ∑ aᵢⱼ Xⁱ Yʲ over the Lazard ring, whose coefficients are the classes of the variables aᵢⱼ.

theorem TauCeti.LazardRing.formalGroup_toPowerSeries : formalGroup.toPowerSeries = lazardSeries fun (ij : ℕ+ × ℕ+) => mk (MvPolynomial.X ij)

The universal formal group law is X + Y + ∑ aᵢⱼ Xⁱ Yʲ, with aᵢⱼ the classes of the variables of ℤ[aᵢⱼ] in the Lazard ring.

@[simp]

theorem TauCeti.LazardRing.coeff_formalGroup (i j : ℕ+) : (MvPowerSeries.coeff (Finsupp.single 0 ↑i + Finsupp.single 1 ↑j)) formalGroup.toPowerSeries = mk (MvPolynomial.X (i, j))

The coefficient of Xⁱ Yʲ in the universal formal group law is the class of aᵢⱼ.

instance TauCeti.LazardRing.instIsCommFormalGroup : formalGroup.IsComm

The universal formal group law is commutative.

theorem TauCeti.LazardRing.hom_ext {R : Type u_3} [CommRing R] {φ ψ : LazardRing →+* R} (h : formalGroup.map φ = formalGroup.map ψ) : φ = ψ

A ring homomorphism out of the Lazard ring is determined by the base change of the universal formal group law along it.

noncomputable def TauCeti.LazardRing.lift {R : Type u_3} [CommRing R] : { F : FormalGroup R // F.IsComm } ≃ (LazardRing →+* R)

The universal property of the Lazard ring: commutative formal group laws over R correspond to ring homomorphisms LazardRing →+* R. The homomorphism attached to F sends the class of aᵢⱼ to the coefficient of Xⁱ Yʲ in F; conversely a homomorphism φ gives the base change of the universal formal group law along φ.

@[simp]

theorem TauCeti.LazardRing.lift_mk_X {R : Type u_3} [CommRing R] (F : { F : FormalGroup R // F.IsComm }) (ij : ℕ+ × ℕ+) : (lift F) (mk (MvPolynomial.X ij)) = (MvPowerSeries.coeff (Finsupp.single 0 ↑ij.1 + Finsupp.single 1 ↑ij.2)) (↑F).toPowerSeries

The homomorphism lift F sends the class of aᵢⱼ to the coefficient of Xⁱ Yʲ in F.

theorem TauCeti.LazardRing.lift_comp_mk {R : Type u_3} [CommRing R] (F : { F : FormalGroup R // F.IsComm }) : (lift F).comp mk = (MvPolynomial.aeval fun (ij : ℕ+ × ℕ+) => (MvPowerSeries.coeff (Finsupp.single 0 ↑ij.1 + Finsupp.single 1 ↑ij.2)) (↑F).toPowerSeries).toRingHom

On polynomials in the aᵢⱼ, the homomorphism lift F evaluates aᵢⱼ at the coefficient of Xⁱ Yʲ in F.

@[simp]

theorem TauCeti.LazardRing.map_lift {R : Type u_3} [CommRing R] (F : { F : FormalGroup R // F.IsComm }) : formalGroup.map (lift F) = ↑F

The universal formal group law base-changes along lift F to F.

@[simp]

theorem TauCeti.LazardRing.coe_lift_symm {R : Type u_3} [CommRing R] (φ : LazardRing →+* R) : ↑(lift.symm φ) = formalGroup.map φ

The commutative formal group law attached to φ : LazardRing →+* R is the base change of the universal formal group law along φ.

theorem TauCeti.LazardRing.lift_map {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (F : FormalGroup R) [F.IsComm] (g : R →+* S) : lift ⟨F.map g, ⋯⟩ = g.comp (lift ⟨F, ⋯⟩)

The universal property is natural in the coefficient ring: the homomorphism classifying the base change of F along g is g composed with the homomorphism classifying F.

The grading

def TauCeti.LazardRing.degree (ij : ℕ+ × ℕ+) : ℕ

The homological degree 2 (i + j - 1) of the coefficient aᵢⱼ of Xⁱ Yʲ in a formal group law.

@[simp]

theorem TauCeti.LazardRing.degree_apply (i j : ℕ+) : degree (i, j) = 2 * (↑i + ↑j - 1)

The coefficient aᵢⱼ has homological degree 2 (i + j - 1).

theorem TauCeti.LazardRing.isHomogeneous_relations : Ideal.IsHomogeneous (MvPolynomial.weightedHomogeneousSubmodule ℤ degree) relations

The Lazard relations are homogeneous: the ideal of ℤ[aᵢⱼ] generated by the coefficients of associativity and commutativity of X + Y + ∑ aᵢⱼ Xⁱ Yʲ is homogeneous when aᵢⱼ has degree 2 (i + j - 1).

noncomputable def TauCeti.LazardRing.grading (n : ℕ) : Submodule ℤ LazardRing

The grading of the Lazard ring by homological degree: Lₙ consists of the classes of the polynomials in the aᵢⱼ that are homogeneous of degree n when aᵢⱼ has degree 2 (i + j - 1).

theorem TauCeti.LazardRing.mem_grading_iff {n : ℕ} {x : LazardRing} : x ∈ grading n ↔ ∃ (p : MvPolynomial (ℕ+ × ℕ+) ℤ), MvPolynomial.IsWeightedHomogeneous degree p n ∧ mk p = x

An element of the Lazard ring has degree n exactly when it is the class of a polynomial in the aᵢⱼ that is homogeneous of degree n.

theorem TauCeti.LazardRing.mk_mem_grading {n : ℕ} {p : MvPolynomial (ℕ+ × ℕ+) ℤ} (hp : MvPolynomial.IsWeightedHomogeneous degree p n) : mk p ∈ grading n

The class of a polynomial that is homogeneous of degree n has degree n.

instance TauCeti.LazardRing.instGradedMonoidNatSubmoduleIntGrading : SetLike.GradedMonoid grading

Multiplication adds degrees in the Lazard ring.

theorem TauCeti.LazardRing.isInternal_grading : DirectSum.IsInternal grading

The Lazard ring is the direct sum of its graded pieces Lₙ.

@[instance_reducible]

noncomputable instance TauCeti.LazardRing.instGradedAlgebraNatIntGrading : GradedAlgebra grading

The Lazard ring is graded by homological degree.

theorem TauCeti.LazardRing.coeff_formalGroup_mem_grading (d : Fin 2 →₀ ℕ) : (MvPowerSeries.coeff d) formalGroup.toPowerSeries ∈ grading (2 * (Finsupp.degree d - 1))

The coefficient of X^(d 0) Y^(d 1) in the universal formal group law has degree 2 (d 0 + d 1 - 1).

theorem TauCeti.LazardRing.lift_mem_iff {A : Type u_1} [CommRing A] {σ : Type u_5} [SetLike σ A] [AddSubgroupClass σ A] {ι : Type u_6} [AddMonoid ι] {𝒜 : ι → σ} [SetLike.GradedMonoid 𝒜] (e : ℕ →+ ι) (F : { F : FormalGroup A // F.IsComm }) : (∀ ⦃n : ℕ⦄ ⦃x : LazardRing⦄, x ∈ grading n → (lift F) x ∈ 𝒜 (e n)) ↔ ∀ (d : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) (↑F).toPowerSeries ∈ 𝒜 (e (2 * (Finsupp.degree d - 1)))

The graded universal property of the Lazard ring, pointwise: let A be graded by 𝒜 over an additive monoid ι receiving the degrees of L along e : ℕ →+ ι (for instance ι = ℕ with e = id, or ι = ℤ with e the inclusion or its negative). The homomorphism L →+* A classifying a commutative formal group law F over A maps each Lₙ into 𝒜 (e n) exactly when the coefficient of every monomial X^(d 0) Y^(d 1) in F lies in 𝒜 (e (2 (d 0 + d 1 - 1))). Since the coefficients of X and Y are 1 and those of the other monomials Xⁿ and Yⁿ vanish, this says that the coefficient aᵢⱼ of F lies in 𝒜 (e (2 (i + j - 1))) for all i, j ≥ 1.

noncomputable def TauCeti.LazardRing.gradedLift {A : Type u_1} [CommRing A] {σ : Type u_5} [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [SetLike.GradedMonoid 𝒜] : { F : FormalGroup A // F.IsComm ∧ ∀ (d : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) F.toPowerSeries ∈ 𝒜 (2 * (Finsupp.degree d - 1)) } ≃ (grading →+*ᵍ 𝒜)

The 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.

@[simp]

theorem TauCeti.LazardRing.toRingHom_gradedLift {A : Type u_1} [CommRing A] {σ : Type u_5} [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [SetLike.GradedMonoid 𝒜] (F : { F : FormalGroup A // F.IsComm ∧ ∀ (d : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) F.toPowerSeries ∈ 𝒜 (2 * (Finsupp.degree d - 1)) }) : ↑(gradedLift F) = lift ⟨↑F, ⋯⟩

The graded homomorphism attached to F is the homomorphism classifying F.

@[simp]

theorem TauCeti.LazardRing.coe_gradedLift {A : Type u_1} [CommRing A] {σ : Type u_5} [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [SetLike.GradedMonoid 𝒜] (F : { F : FormalGroup A // F.IsComm ∧ ∀ (d : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) F.toPowerSeries ∈ 𝒜 (2 * (Finsupp.degree d - 1)) }) : ⇑(gradedLift F) = ⇑(lift ⟨↑F, ⋯⟩)

The graded homomorphism attached to F is, as a function, the homomorphism classifying F.

@[simp]

theorem TauCeti.LazardRing.coe_gradedLift_symm {A : Type u_1} [CommRing A] {σ : Type u_5} [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [SetLike.GradedMonoid 𝒜] (φ : grading →+*ᵍ 𝒜) : ↑(gradedLift.symm φ) = formalGroup.map ↑φ

The formal group law attached to a graded homomorphism φ is the base change of the universal formal group law along φ.