The Lazard symmetric 2-cocycles C_n(X, Y)

A two-variable polynomial f(X, Y) over a commutative ring R is an additive 2-cocycle if

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

Symmetric additive 2-cocycles are the first-order deformations of the additive formal group law X + Y: if F(X, Y) ≡ X + Y + f(X, Y) modulo terms of degree > n and f is homogeneous of degree n, then commutativity and associativity of F modulo terms of degree > n say exactly that f is a symmetric additive 2-cocycle. This is why they govern the degree-by-degree construction of formal group laws and Lazard's theorem that the Lazard ring is polynomial.

For n ≥ 2 the basic example is (X + Y)ⁿ - Xⁿ - Yⁿ. Its coefficients n.choose i, 0 < i < n, have greatest common divisor d_n, which is the prime p when n is a power of p and 1 otherwise (Choose.gcd_choose_eq_minFac_of_isPrimePow, Choose.gcd_choose_eq_one_of_not_isPrimePow). Dividing by it gives the integral polynomial C_n(X, Y) with d_n • C_n = (X + Y)ⁿ - Xⁿ - Yⁿ, defined here over every commutative ring by casting its natural-number coefficients n.choose i / d_n. It is a homogeneous symmetric additive 2-cocycle of degree n, compatible with every change of coefficients, and its coefficients generate the unit ideal of ℤ. Consequently r • C_n = 0 forces r = 0 in every commutative ring R, including rings with torsion: the multiple of C_n representing a cocycle is unique. The converse, existence, is the symmetric 2-cocycle lemma: every homogeneous symmetric additive 2-cocycle of degree n is a multiple of C_n (TauCeti.exists_eq_smul_lazardCocycle, in TauCeti.RingTheory.FormalGroup.SymmetricCocycle.Classification).

Main definitions

• MvPolynomial.IsAddCocycle₂: f(X, Y) + f(X + Y, Z) = f(X, Y + Z) + f(Y, Z).
• TauCeti.lazardGcd n: the greatest common divisor d_n of the n.choose i, 0 < i < n.
• TauCeti.lazardCocycle n R: the polynomial C_n(X, Y) over R.

Main results

• MvPolynomial.IsAddCocycle₂.coeff_eq: the cocycle identity at the coefficient of XⁱYʲZᵏ, [k = 0] c_{i,j} + (i + j).choose i * c_{i+j,k} = (j + k).choose j * c_{i,j+k} + [i = 0] c_{j,k} where c_{a,b} is the coefficient of XᵃYᵇ in f.
• MvPolynomial.IsAddCocycle₂.coeff_single_one_eq_zero: the coefficient of Yⁿ in an additive 2-cocycle vanishes for n ≠ 0.
• TauCeti.lazardGcd_eq_minFac_of_isPrimePow, TauCeti.lazardGcd_eq_one_of_not_isPrimePow: d_n is p for n = pᵏ, and 1 for n ≥ 2 not a prime power.
• TauCeti.prime_dvd_lazardGcd_iff: for n ≠ 0 and a prime p, p ∣ d_n exactly when n is a power of p. In particular d_n is odd unless n is a power of two.
• TauCeti.isUnit_lazardGcd: if p = 0 in A and n ≠ 0 is not a power of p, then d_n is a unit in A.
• Nat.Prime.exists_not_dvd_choose: if n ≠ 0 is not a power of the prime p, then p does not divide some n.choose i with 0 < i < n.
• TauCeti.lazardGcd_dvd_pow_succ_sub: d_(n+1) divides k^(n + 1) - k.
• TauCeti.gcd_choose_div_lazardGcd_eq_one: for n ≥ 2, the coefficients n.choose i / d_n have greatest common divisor 1.
• TauCeti.coeff_lazardCocycle: the coefficient of XⁱYʲ in C_n is n.choose i / d_n when i + j = n and i, j ≠ 0, and 0 otherwise.
• TauCeti.lazardGcd_nsmul_lazardCocycle: d_n • C_n = (X + Y)ⁿ - Xⁿ - Yⁿ for n ≠ 0.
• TauCeti.aeval_diag_lazardCocycle: the diagonal C_n(a, a) is ((2ⁿ - 2) / d_n) • aⁿ.
• TauCeti.sum_aeval_natCast_mul_lazardCocycle: if p = 0, then ∑_{j < p} C_n(j t, t) = -tⁿ for n = pᵏ, k ≥ 1.
• TauCeti.map_lazardCocycle: C_n is compatible with ring homomorphisms.
• TauCeti.isHomogeneous_lazardCocycle, TauCeti.isSymmetric_lazardCocycle, TauCeti.isAddCocycle₂_lazardCocycle: C_n is a homogeneous symmetric additive 2-cocycle of degree n.
• TauCeti.smul_lazardCocycle_eq_zero_iff: for n ≥ 2, r • C_n = 0 ↔ r = 0.

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 (the symmetric 2-cocycle lemma).

def MvPolynomial.IsAddCocycle₂ {R : Type u_1} [CommRing R] (f : MvPolynomial (Fin 2) R) : Prop

A two-variable polynomial f(X, Y) is an additive 2-cocycle if f(X, Y) + f(X + Y, Z) = f(X, Y + Z) + f(Y, Z) in R[X, Y, Z].

theorem MvPolynomial.isAddCocycle₂_iff {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} : f.IsAddCocycle₂ ↔ (aeval ![X 0, X 1]) f + (aeval ![X 0 + X 1, X 2]) f = (aeval ![X 0, X 1 + X 2]) f + (aeval ![X 1, X 2]) f

Unfolding MvPolynomial.IsAddCocycle₂.

@[simp]

theorem MvPolynomial.IsAddCocycle₂.zero {R : Type u_1} [CommRing R] : IsAddCocycle₂ 0

The zero polynomial is an additive 2-cocycle.

theorem MvPolynomial.IsAddCocycle₂.add {R : Type u_1} [CommRing R] {f g : MvPolynomial (Fin 2) R} (hf : f.IsAddCocycle₂) (hg : g.IsAddCocycle₂) : (f + g).IsAddCocycle₂

Additive 2-cocycles are closed under addition.

theorem MvPolynomial.IsAddCocycle₂.smul {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} (r : R) (hf : f.IsAddCocycle₂) : (r • f).IsAddCocycle₂

Additive 2-cocycles are closed under scalar multiplication.

theorem MvPolynomial.IsAddCocycle₂.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : MvPolynomial (Fin 2) R} (hf : f.IsAddCocycle₂) (φ : R →+* S) : ((MvPolynomial.map φ) f).IsAddCocycle₂

Additive 2-cocycles are preserved by a change of coefficients.

theorem MvPolynomial.IsAddCocycle₂.coeff_eq {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} (hf : f.IsAddCocycle₂) (i j k : ℕ) : (if k = 0 then f.coeff (Finsupp.single 0 i + Finsupp.single 1 j) else 0) + ↑((i + j).choose i) * f.coeff (Finsupp.single 0 (i + j) + Finsupp.single 1 k) = ↑((j + k).choose j) * f.coeff (Finsupp.single 0 i + Finsupp.single 1 (j + k)) + if i = 0 then f.coeff (Finsupp.single 0 j + Finsupp.single 1 k) else 0

The cocycle identity at the coefficient of XⁱYʲZᵏ.

theorem MvPolynomial.IsAddCocycle₂.coeff_single_one_eq_zero {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} (hf : f.IsAddCocycle₂) {n : ℕ} (hn : n ≠ 0) : f.coeff (Finsupp.single 1 n) = 0

The coefficient of Yⁿ in an additive 2-cocycle vanishes for n ≠ 0.

def TauCeti.lazardGcd (n : ℕ) : ℕ

The greatest common divisor d_n of the binomial coefficients n.choose i, 0 < i < n. For n ≥ 2 it is the prime p if n is a power of p, and 1 otherwise (lazardGcd_eq_minFac_of_isPrimePow, lazardGcd_eq_one_of_not_isPrimePow); for n < 2 the range is empty and d_n = 0 (lazardGcd_eq_zero_of_lt_two).

theorem TauCeti.lazardGcd_eq_minFac_of_isPrimePow {n : ℕ} (h : IsPrimePow n) : lazardGcd n = n.minFac

If n = pᵏ with k ≥ 1, then d_n = p.

theorem TauCeti.lazardGcd_eq_one_of_not_isPrimePow {n : ℕ} (hn : 1 < n) (h : ¬IsPrimePow n) : lazardGcd n = 1

If n ≥ 2 is not a prime power, then d_n = 1.

theorem TauCeti.lazardGcd_eq_zero_of_lt_two {n : ℕ} (hn : n < 2) : lazardGcd n = 0

d_0 = d_1 = 0: the range 0 < i < n is empty.

theorem TauCeti.lazardGcd_prime_pow {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : lazardGcd (p ^ k) = p

For a prime p and k ≠ 0, d_{pᵏ} = p.

theorem TauCeti.prime_dvd_lazardGcd_iff {n p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : p ∣ lazardGcd n ↔ ∃ (k : ℕ), n = p ^ k

For n ≠ 0 and a prime p, p divides d_n exactly when n is a power of p.

theorem TauCeti.isUnit_lazardGcd {A : Type u_3} [CommSemiring A] {n p : ℕ} (hp : Nat.Prime p) (hpA : ↑p = 0) (hn : n ≠ 0) (h : ¬∃ (k : ℕ), n = p ^ k) : IsUnit ↑(lazardGcd n)

If p is a prime with p = 0 in A and n ≠ 0 is not a power of p, then d_n is a unit in A: it is prime to p (prime_dvd_lazardGcd_iff).

theorem TauCeti.dvd_lazardGcd_iff {n d : ℕ} : d ∣ lazardGcd n ↔ ∀ (i : ℕ), 0 < i → i < n → d ∣ n.choose i

d ∣ d_n if and only if d divides every n.choose i, 0 < i < n.

theorem Nat.Prime.exists_not_dvd_choose {p n : ℕ} (hp : Prime p) (hn0 : n ≠ 0) (hn : ∀ (k : ℕ), n ≠ p ^ k) : ∃ (i : ℕ), 0 < i ∧ i < n ∧ ¬p ∣ n.choose i

If n ≠ 0 is not a power of the prime p, some binomial coefficient n.choose i with 0 < i < n is not divisible by p. This is the converse of Nat.Prime.dvd_choose_pow.

theorem TauCeti.lazardGcd_dvd_choose {n i : ℕ} (hi : 0 < i) (hin : i < n) : lazardGcd n ∣ n.choose i

d_n divides n.choose i for 0 < i < n.

theorem TauCeti.lazardGcd_mul_choose_div_lazardGcd {n i : ℕ} (hi : 0 < i) (hin : i < n) : lazardGcd n * (n.choose i / lazardGcd n) = n.choose i

d_n * (n.choose i / d_n) = n.choose i for 0 < i < n.

theorem TauCeti.lazardGcd_ne_zero {n : ℕ} (hn : 2 ≤ n) : lazardGcd n ≠ 0

d_n ≠ 0 for n ≥ 2.

theorem TauCeti.lazardGcd_succ_ne_zero {n : ℕ} (hn : n ≠ 0) : lazardGcd (n + 1) ≠ 0

d_{n+1} ≠ 0 for n ≠ 0.

theorem TauCeti.lazardGcd_dvd_self {n : ℕ} (hn : n ≠ 1) : lazardGcd n ∣ n

d_n divides n for n ≠ 1.

theorem TauCeti.lazardGcd_dvd_pow_succ_sub (k : ℕ) (n : ℕ+) : ↑(lazardGcd (↑n + 1)) ∣ ↑k ^ (↑n + 1) - ↑k

d_(n+1) divides k^(n + 1) - k for every k: if n + 1 = pʲ then d_(n+1) = p and this is Fermat's little theorem, and otherwise d_(n+1) = 1.

theorem TauCeti.gcd_choose_div_lazardGcd_eq_one {n : ℕ} (hn : 2 ≤ n) : ((Finset.Icc 1 (n - 1)).gcd fun (i : ℕ) => n.choose i / lazardGcd n) = 1

For n ≥ 2, the numbers n.choose i / d_n, 0 < i < n, have greatest common divisor 1.

noncomputable def TauCeti.lazardCocycle (n : ℕ) (R : Type u_3) [CommRing R] : MvPolynomial (Fin 2) R

The Lazard 2-cocycle C_n(X, Y), whose coefficient of XⁱYⁿ⁻ⁱ is n.choose i / d_n for 0 < i < n, where d_n = lazardGcd n; thus d_n • C_n = (X + Y)ⁿ - Xⁿ - Yⁿ for n ≠ 0 (lazardGcd_nsmul_lazardCocycle). Its coefficients are natural numbers, cast into R. For n < 2 it is 0.

theorem TauCeti.coeff_lazardCocycle {R : Type u_1} [CommRing R] (n : ℕ) (d : Fin 2 →₀ ℕ) : (lazardCocycle n R).coeff d = if d 0 + d 1 = n ∧ d 0 ≠ 0 ∧ d 1 ≠ 0 then ↑(n.choose (d 0) / lazardGcd n) else 0

The coefficient of XⁱYʲ in C_n is n.choose i / d_n if i + j = n and i, j ≠ 0, and 0 otherwise.

theorem TauCeti.coeff_single_add_single_lazardCocycle {R : Type u_1} [CommRing R] {n i : ℕ} (hi : 0 < i) (hin : i < n) : (lazardCocycle n R).coeff (Finsupp.single 0 i + Finsupp.single 1 (n - i)) = ↑(n.choose i / lazardGcd n)

The coefficient of XⁱYⁿ⁻ⁱ in C_n, for 0 < i < n, is n.choose i / d_n.

@[simp]

theorem TauCeti.map_lazardCocycle {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (n : ℕ) : (MvPolynomial.map φ) (lazardCocycle n R) = lazardCocycle n S

C_n is compatible with every change of coefficients.

theorem TauCeti.lazardCocycle_eq_zero_of_lt_two {R : Type u_1} [CommRing R] {n : ℕ} (hn : n < 2) : lazardCocycle n R = 0

C_0 = C_1 = 0.

theorem TauCeti.lazardGcd_nsmul_lazardCocycle {R : Type u_1} [CommRing R] {n : ℕ} (hn : n ≠ 0) : lazardGcd n • lazardCocycle n R = (MvPolynomial.X 0 + MvPolynomial.X 1) ^ n - MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n

For n ≠ 0, d_n • C_n = (X + Y)ⁿ - Xⁿ - Yⁿ, where d_n = lazardGcd n is the greatest common divisor of the n.choose i, 0 < i < n.

theorem TauCeti.lazardGcd_nsmul_aeval_lazardCocycle {R : Type u_1} [CommRing R] {A : Type u_3} [CommRing A] [Algebra R A] {n : ℕ} (hn : n ≠ 0) (a b : A) : lazardGcd n • (MvPolynomial.aeval ![a, b]) (lazardCocycle n R) = (a + b) ^ n - a ^ n - b ^ n

d_n • C_n(a, b) = (a + b)ⁿ - aⁿ - bⁿ for elements a, b of any commutative R-algebra.

@[simp]

theorem TauCeti.aeval_diag_lazardCocycle {R : Type u_1} [CommRing R] {A : Type u_3} [CommRing A] [Algebra R A] (n : ℕ) (a : A) : (MvPolynomial.aeval ![a, a]) (lazardCocycle n R) = ((2 ^ n - 2) / lazardGcd n) • a ^ n

The diagonal C_n(a, a) of the Lazard cocycle, for an element a of any commutative R-algebra, is ((2ⁿ - 2) / d_n) • aⁿ: the coefficients n.choose i, 0 < i < n, of (X + Y)ⁿ - Xⁿ - Yⁿ sum to 2ⁿ - 2. For n < 2 both sides vanish.

theorem TauCeti.isHomogeneous_lazardCocycle {R : Type u_1} [CommRing R] (n : ℕ) : (lazardCocycle n R).IsHomogeneous n

C_n is homogeneous of degree n.

theorem TauCeti.sum_aeval_natCast_mul_lazardCocycle {R : Type u_1} [CommRing R] {p : ℕ} (hp : Nat.Prime p) {A : Type u_3} [CommRing A] [Algebra R A] (hpA : ↑p = 0) {k : ℕ} (hk : k ≠ 0) (t : A) : ∑ j ∈ Finset.range p, (MvPolynomial.aeval ![↑j * t, t]) (lazardCocycle (p ^ k) R) = -t ^ p ^ k

The values C_n(j t, t), j < p, sum to -tⁿ in characteristic p for n = pᵏ, k ≥ 1. Over the integers p C_n(j, 1) = (j + 1)ⁿ - jⁿ - 1, which telescopes to p ∑_{j < p} C_n(j, 1) = pⁿ - p, and pⁿ⁻¹ - 1 = -1 when p = 0. This is the degree-n part of the p-series [p](X) of a formal group law X + Y + c C_n(X, Y) + ⋯.

theorem TauCeti.isSymmetric_lazardCocycle {R : Type u_1} [CommRing R] (n : ℕ) : (lazardCocycle n R).IsSymmetric

C_n(X, Y) = C_n(Y, X).

theorem TauCeti.isAddCocycle₂_lazardCocycle {R : Type u_1} [CommRing R] (n : ℕ) : (lazardCocycle n R).IsAddCocycle₂

C_n is an additive 2-cocycle.

@[simp]

theorem TauCeti.smul_lazardCocycle_eq_zero_iff {R : Type u_1} [CommRing R] {n : ℕ} (hn : 2 ≤ n) {r : R} : r • lazardCocycle n R = 0 ↔ r = 0

For n ≥ 2, r • C_n = 0 ↔ r = 0 in every commutative ring R, including rings with torsion.

theorem TauCeti.smul_lazardCocycle_injective {R : Type u_1} [CommRing R] {n : ℕ} (hn : 2 ≤ n) : Function.Injective fun (r : R) => r • lazardCocycle n R

For n ≥ 2, r ↦ r • C_n is injective.