Symmetric 2-cocycles over rings with 2 = 0

Let R be a commutative ring in which 2 = 0, with no further hypothesis: R may be the zero ring or have nilpotents. This file specializes the symmetric 2-cocycle lemma (TauCeti.exists_eq_smul_lazardCocycle) to R and adds the diagonal condition f(X, X) = 0, which is the obstruction lemma behind the degree-by-degree construction of a strict logarithm for a commutative formal group law F with [2]_F = 0. There the first nonvanishing homogeneous part f of the error g(F(X, Y)) - g(X) - g(Y) of a truncated logarithm g is a homogeneous symmetric additive 2-cocycle, and F(X, X) = 0 forces f(X, X) = 0.

The answer depends on whether the degree n is a power of two, through the parity of the greatest common divisor d_n of the binomial coefficients n.choose i, 0 < i < n.

• If n ≠ 0 is not a power of two, then d_n is odd (TauCeti.prime_dvd_lazardGcd_iff), hence equal to 1 in R, so the Lazard cocycle C_n is (X + Y)ⁿ - Xⁿ - Yⁿ and every homogeneous symmetric additive 2-cocycle of degree n is a unique multiple of it. Its diagonal (2X)ⁿ - 2Xⁿ vanishes, so the diagonal condition holds automatically and is not assumed.
• If n = 2ᵏ with k ≥ 1, then d_n = 2, the polynomial (X + Y)ⁿ - Xⁿ - Yⁿ vanishes in R, and the integral cocycle C_n = ((X + Y)ⁿ - Xⁿ - Yⁿ) / 2 reduced mod 2 has diagonal C_n(X, X) = (2ⁿ⁻¹ - 1) • Xⁿ = Xⁿ, as 2ⁿ⁻¹ - 1 is odd. Hence the diagonal of r • C_n is r • Xⁿ, whose coefficient of Xⁿ is r, so its vanishing forces r = 0 (also over the zero ring), and a homogeneous symmetric additive 2-cocycle of degree n with zero diagonal is 0.

No coefficient field and no division by two is used: everything is deduced from the classification over an arbitrary commutative ring and binomial-coefficient arithmetic.

Main results

• TauCeti.lazardCocycle_eq_add_pow_sub_pow_sub_pow_of_two_eq_zero: if 2 = 0 in R and n ≠ 0 is not a power of two, then C_n = (X + Y)ⁿ - Xⁿ - Yⁿ.
• TauCeti.aeval_diag_lazardCocycle_two_pow: if 2 = 0 in R and k ≠ 0, then C_{2ᵏ}(a, a) = a^{2ᵏ} for every element a of an R-algebra.
• TauCeti.existsUnique_eq_smul_add_pow_sub_pow_sub_pow_of_two_eq_zero: if 2 = 0 in R and n ≠ 0 is not a power of two, a homogeneous symmetric additive 2-cocycle of degree n is r • ((X + Y)ⁿ - Xⁿ - Yⁿ) for a unique r : R.
• TauCeti.eq_zero_of_two_eq_zero_of_aeval_X_X_eq_zero: if 2 = 0 in R, a homogeneous symmetric additive 2-cocycle f of degree 2ᵏ with f(X, X) = 0 is zero.

References

• M. Lazard, Commutative Formal Groups, Lecture Notes in Mathematics 443 (1975).
• D. Quillen, On the formal group laws of unoriented and complex cobordism theory, Bull. Amer. Math. Soc. 75 (1969), for formal group laws with [2]_F = 0.
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.1.

theorem TauCeti.lazardCocycle_eq_add_pow_sub_pow_sub_pow_of_two_eq_zero {R : Type u_1} [CommRing R] (h2 : 2 = 0) {n : ℕ} (hn0 : n ≠ 0) (hn : ∀ (k : ℕ), n ≠ 2 ^ k) : lazardCocycle n R = (MvPolynomial.X 0 + MvPolynomial.X 1) ^ n - MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n

If 2 = 0 in R and n ≠ 0 is not a power of two, the Lazard cocycle C_n is (X + Y)ⁿ - Xⁿ - Yⁿ: the greatest common divisor d_n of the n.choose i, 0 < i < n, is odd, so d_n = 1 in R.

@[simp]

theorem TauCeti.aeval_diag_lazardCocycle_two_pow {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] (h2 : 2 = 0) {k : ℕ} (hk : k ≠ 0) (a : A) : (MvPolynomial.aeval ![a, a]) (lazardCocycle (2 ^ k) R) = a ^ 2 ^ k

If 2 = 0 in R and k ≠ 0, the diagonal of the Lazard cocycle of degree 2ᵏ is C_{2ᵏ}(a, a) = a^{2ᵏ} for an element a of any commutative R-algebra: its integral coefficient (2^{2ᵏ} - 2) / 2 is odd.

theorem TauCeti.existsUnique_eq_smul_add_pow_sub_pow_sub_pow_of_two_eq_zero {R : Type u_1} [CommRing R] (h2 : 2 = 0) {n : ℕ} (hn0 : n ≠ 0) (hn : ∀ (k : ℕ), n ≠ 2 ^ k) {f : MvPolynomial (Fin 2) R} (hh : f.IsHomogeneous n) (hs : f.IsSymmetric) (hf : f.IsAddCocycle₂) : ∃! r : R, f = r • ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n - MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n)

The symmetric 2-cocycle lemma when 2 = 0, away from powers of two. If 2 = 0 in R and n ≠ 0 is not a power of two, a homogeneous symmetric additive 2-cocycle of degree n over R is r • ((X + Y)ⁿ - Xⁿ - Yⁿ) for a unique r : R.

theorem TauCeti.eq_zero_of_two_eq_zero_of_aeval_X_X_eq_zero {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

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