Formal group laws with square-zero coefficients

Write a formal group law over a commutative ring A as F(X, Y) = X + Y + G(X, Y). If the coefficients of G pairwise multiply to zero — for instance, if they lie in an ideal of square zero — then substituting into G only sees the linear part X + Y of F, and associativity of F says exactly that G is an additive 2-cocycle:

G(X, Y) + G(X + Y, Z) = G(X, Y + Z) + G(Y, Z).

When F is commutative, G is moreover symmetric. Conversely, a polynomial additive 2-cocycle f with no constant term and square-zero coefficients gives the formal group law X + Y + f, a first-order deformation of the additive formal group law, which is commutative when f is symmetric.

This is how the symmetric 2-cocycle lemma computes the indecomposables of the Lazard ring: modulo the square of its augmentation ideal, the nonlinear part of the universal formal group law has square-zero coefficients, so they satisfy the symmetric cocycle equations (FormalGroup.isSymmetricCocycleCoeff_coeff) and TauCeti.IsSymmetricCocycleCoeff.exists_eq_nsmul applies to them.

Main definitions

• MvPolynomial.IsAddCocycle₂.formalGroup: the formal group law X + Y + f(X, Y) attached to an additive 2-cocycle f without constant term whose coefficients pairwise multiply to zero.

Main results

• FormalGroup.subst_add_subst_eq: if the coefficients of G = F - X - Y pairwise multiply to zero, then G satisfies the additive 2-cocycle identity.
• FormalGroup.choose_mul_coeff_eq: the cocycle identity at the coefficient of XⁱYʲZᵏ with i, k ≥ 1, (i + j).choose i * a_{i+j,k} = (j + k).choose j * a_{i,j+k}.
• FormalGroup.isSymmetricCocycleCoeff_coeff: for a commutative such F, the coefficients of the monomials of each total degree n satisfy the coefficient equations of a symmetric additive 2-cocycle of degree n.
• MvPolynomial.IsAddCocycle₂.isComm_formalGroup: the formal group law X + Y + f(X, Y) is commutative when f is symmetric.

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.subst_add_subst_eq {A : Type u_1} [CommRing A] (F : FormalGroup A) (hF : ∀ (d e : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) * (MvPowerSeries.coeff e) (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) = 0) : MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) + MvPowerSeries.subst ![MvPowerSeries.X 0 + MvPowerSeries.X 1, MvPowerSeries.X 2] (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) = MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1 + MvPowerSeries.X 2] (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) + MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1))

The nonlinear part of a formal group law with square-zero coefficients is an additive 2-cocycle. If the coefficients of G = F(X, Y) - X - Y pairwise multiply to zero, then G(X, Y) + G(X + Y, Z) = G(X, Y + Z) + G(Y, Z).

theorem FormalGroup.choose_mul_coeff_eq {A : Type u_1} [CommRing A] (F : FormalGroup A) (hF : ∀ (d e : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) * (MvPowerSeries.coeff e) (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) = 0) {i k : ℕ} (hi : i ≠ 0) (hk : k ≠ 0) (j : ℕ) : ↑((i + j).choose i) * (MvPowerSeries.coeff (Finsupp.single 0 (i + j) + Finsupp.single 1 k)) F.toPowerSeries = ↑((j + k).choose j) * (MvPowerSeries.coeff (Finsupp.single 0 i + Finsupp.single 1 (j + k))) F.toPowerSeries

The additive 2-cocycle identity for the nonlinear part of a formal group law with square-zero coefficients, at the coefficient of XⁱYʲZᵏ with i, k ≥ 1: writing a_{i,j} for the coefficient of XⁱYʲ, (i + j).choose i * a_{i+j,k} = (j + k).choose j * a_{i,j+k}.

theorem FormalGroup.isSymmetricCocycleCoeff_coeff {A : Type u_1} [CommRing A] (F : FormalGroup A) [F.IsComm] (hF : ∀ (d e : Fin 2 →₀ ℕ), (MvPowerSeries.coeff d) (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) * (MvPowerSeries.coeff e) (F.toPowerSeries - (MvPowerSeries.X 0 + MvPowerSeries.X 1)) = 0) (n : ℕ) : TauCeti.IsSymmetricCocycleCoeff n fun (i : ℕ) => (MvPowerSeries.coeff (Finsupp.single 0 i + Finsupp.single 1 (n - i))) F.toPowerSeries

For a commutative formal group law whose nonlinear coefficients pairwise multiply to zero, the coefficients bᵢ of XⁱYⁿ⁻ⁱ satisfy the coefficient equations of a symmetric additive 2-cocycle of degree n.

noncomputable def MvPolynomial.IsAddCocycle₂.formalGroup {A : Type u_1} [CommRing A] {f : MvPolynomial (Fin 2) A} (hf : f.IsAddCocycle₂) (h0 : constantCoeff f = 0) (hff : ∀ (d e : Fin 2 →₀ ℕ), f.coeff d * f.coeff e = 0) : FormalGroup A

The formal group law X + Y + f(X, Y) attached to an additive 2-cocycle f without constant term whose coefficients pairwise multiply to zero: a first-order deformation of the additive formal group law.

@[simp]

theorem MvPolynomial.IsAddCocycle₂.toPowerSeries_formalGroup {A : Type u_1} [CommRing A] {f : MvPolynomial (Fin 2) A} (hf : f.IsAddCocycle₂) (h0 : constantCoeff f = 0) (hff : ∀ (d e : Fin 2 →₀ ℕ), f.coeff d * f.coeff e = 0) : (hf.formalGroup h0 hff).toPowerSeries = MvPowerSeries.X 0 + MvPowerSeries.X 1 + ↑f

The underlying power series of hf.formalGroup h0 hff is X + Y + f(X, Y).

theorem MvPolynomial.IsAddCocycle₂.isComm_formalGroup {A : Type u_1} [CommRing A] {f : MvPolynomial (Fin 2) A} (hf : f.IsAddCocycle₂) (h0 : constantCoeff f = 0) (hff : ∀ (d e : Fin 2 →₀ ℕ), f.coeff d * f.coeff e = 0) (hs : f.IsSymmetric) : (hf.formalGroup h0 hff).IsComm

The formal group law X + Y + f(X, Y) is commutative when f is symmetric.