The symmetric 2-cocycle lemma

Let R be a commutative ring and n ≠ 0. This file proves Lazard's symmetric 2-cocycle lemma: every homogeneous symmetric additive 2-cocycle f(X, Y) of degree n over R is a multiple r • C_n of the Lazard cocycle C_n = ((X + Y)ⁿ - Xⁿ - Yⁿ) / d_n, and for n ≥ 2 the multiple r is unique. No hypothesis on R is needed: it may have torsion or positive characteristic, where (X + Y)ⁿ - Xⁿ - Yⁿ can vanish identically and division by d_n is impossible. This is the inductive step in the degree-by-degree construction of formal group laws and in Lazard's theorem that the Lazard ring is polynomial.

Implementation notes

Writing f = ∑ bᵢ XⁱYⁿ⁻ⁱ, the cocycle identity says, coefficientwise at XⁱYʲZᵏ with i, j, k ≥ 1, that (i + j).choose i • b_{i + j} = (j + k).choose j • bᵢ; symmetry says b_{n - i} = bᵢ. These are ℤ-linear conditions, so they make sense with coefficients in any abelian group M, and we classify their solutions there.

• If p • bᵢ = 0 for a prime p, the solution is determined by its value at one index m, depending only on n and p. When p ∤ n or n = p, one takes m = 1: the equations with k = 1 give (n - i) • bᵢ = (n - 1).choose i • b₁ and i • bᵢ = (n - 1).choose (i - 1) • b₁. When p ∣ n and n > p, Lucas's theorem forces b₁ = 0 and bᵢ = 0 for p ∤ i, and a ↦ b_{p a} is a solution in degree n / p (Frobenius descent).
• Since C_n is itself a solution whose coefficients have greatest common divisor 1, it does not vanish at that index modulo p, so every p-torsion solution is a multiple of C_n.
• For a general solution b, choose a Bézout combination r of its coefficients and set e = b - r • C_n. The ℤ-span N of the eᵢ is finitely generated and, by the previous step applied to M ⧸ p • N, satisfies N = p • N for every prime p; hence N = 0 by Nakayama's lemma.

Main definitions

• TauCeti.IsSymmetricCocycleCoeff n b: the coefficient equations in degree n on a sequence b in an additive commutative monoid.

Main results

• TauCeti.isSymmetricCocycleCoeff_coeff: the coefficients of a symmetric additive 2-cocycle satisfy the coefficient equations.
• TauCeti.IsSymmetricCocycleCoeff.exists_eq_nsmul: every solution of the coefficient equations in an abelian group is, at the indices 0 < i < n, a multiple of the coefficients n.choose i / d_n of C_n.
• TauCeti.exists_eq_smul_lazardCocycle: a homogeneous symmetric additive 2-cocycle of degree n ≠ 0 is r • C_n for some r.
• TauCeti.existsUnique_eq_smul_lazardCocycle: for n ≥ 2, the multiple r is unique.

References

• M. Lazard, Sur les groupes de Lie formels à un paramètre, Bull. Soc. Math. France 83 (1955).
• M. Lazard, Commutative Formal Groups, Lecture Notes in Mathematics 443 (1975).
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1.
• J. Lurie, Chromatic Homotopy Theory (Harvard lecture notes, 2010), Lectures 2 and 3.

The coefficient equations, with coefficients in an additive commutative monoid

structure TauCeti.IsSymmetricCocycleCoeff {M : Type u_1} [AddCommMonoid M] (n : ℕ) (b : ℕ → M) : Prop

The linear equations satisfied by the coefficients bᵢ of XⁱYⁿ⁻ⁱ in a symmetric additive 2-cocycle of degree n, with coefficients in an additive commutative monoid. Only ℕ-multiples and equalities enter, so the equations make sense before any subtraction is available; the classification below needs an abelian group.

• symm (i : ℕ) : i ≤ n → b (n - i) = b i

  Symmetry: b_{n - i} = bᵢ.

• rel (i j k : ℕ) : 0 < i → 0 < j → 0 < k → i + j + k = n → (i + j).choose i • b (i + j) = (j + k).choose j • b i

  The cocycle identity at XⁱYʲZᵏ with i, j, k ≥ 1: (i + j).choose i • b_{i + j} = (j + k).choose j • bᵢ.

theorem TauCeti.IsSymmetricCocycleCoeff.map {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] {n : ℕ} {b : ℕ → M} (h : IsSymmetricCocycleCoeff n b) (φ : M →+ N) : IsSymmetricCocycleCoeff n fun (i : ℕ) => φ (b i)

Solutions of the coefficient equations are preserved by additive monoid homomorphisms.

Solutions in an abelian group

theorem TauCeti.IsSymmetricCocycleCoeff.sub {M : Type u_1} [AddCommGroup M] {n : ℕ} {b b' : ℕ → M} (h : IsSymmetricCocycleCoeff n b) (h' : IsSymmetricCocycleCoeff n b') : IsSymmetricCocycleCoeff n fun (i : ℕ) => b i - b' i

The difference of two solutions of the coefficient equations is a solution.

Solutions killed by a prime

The coefficients of a symmetric 2-cocycle satisfy the coefficient equations

theorem TauCeti.isSymmetricCocycleCoeff_coeff {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} (hs : f.IsSymmetric) (hf : f.IsAddCocycle₂) (n : ℕ) : IsSymmetricCocycleCoeff n fun (i : ℕ) => f.coeff (Finsupp.single 0 i + Finsupp.single 1 (n - i))

The coefficients bᵢ of XⁱYⁿ⁻ⁱ in a symmetric additive 2-cocycle satisfy the coefficient equations in degree n.

Solutions with coefficients in an arbitrary abelian group

theorem TauCeti.IsSymmetricCocycleCoeff.exists_eq_nsmul {M : Type u_1} [AddCommGroup M] {n : ℕ} {b : ℕ → M} (hbc : IsSymmetricCocycleCoeff n b) : ∃ (r : M), ∀ (i : ℕ), 0 < i → i < n → b i = (n.choose i / lazardGcd n) • r

Every solution of the coefficient equations in degree n, with coefficients in an arbitrary abelian group, is, at the indices 0 < i < n, a multiple (n.choose i / d_n) • r of the coefficients of C_n.

The symmetric 2-cocycle lemma

theorem TauCeti.exists_eq_smul_lazardCocycle {R : Type u_1} [CommRing R] {n : ℕ} (hn : n ≠ 0) {f : MvPolynomial (Fin 2) R} (hh : f.IsHomogeneous n) (hs : f.IsSymmetric) (hf : f.IsAddCocycle₂) : ∃ (r : R), f = r • lazardCocycle n R

The symmetric 2-cocycle lemma. Over any commutative ring R, a homogeneous symmetric additive 2-cocycle f(X, Y) of degree n ≠ 0 is a multiple r • C_n of the Lazard cocycle C_n = ((X + Y)ⁿ - Xⁿ - Yⁿ) / d_n.

theorem TauCeti.existsUnique_eq_smul_lazardCocycle {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 : R, f = r • lazardCocycle n R

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