The obstruction to extending a homomorphism of formal group laws

Let F and G be commutative formal group laws over a commutative ring R, and let f be a power series without constant term which is a homomorphism from F to G up to degree n: the homomorphism defect f(F(X, Y)) - G(f(X), f(Y)) (FormalGroup.homDefect) vanishes below degree n. Its degree-n part is the obstruction to improving f to a homomorphism up to degree n + 1. This file shows that the obstruction is a multiple c C_n of the Lazard cocycle C_n = ((X + Y)ⁿ - Xⁿ - Yⁿ) / d_n, and that when n = pᵏ and p = 0 in R, the scalar c is the coefficient of Xⁿ in [p]_G(f(X)) - f([p]_F(X)). Since d_n is a unit in R unless n is a power of p, only the degrees pᵏ carry a genuine obstruction, and it is read off the p-series: this is the degree-by-degree mechanism behind Lazard's classification of formal group laws over separably closed fields by their height.

The argument takes place in the group G.Point σ of power-series points of G. The defect δ(x, y) = f(x + y) - f(x) - f(y), computed there, satisfies the cocycle identity, the symmetry and the telescoping f(p x) - p f(x) = ∑_{j < p} δ(j x, x) exactly, as identities in an abelian group. The points vanishing to order N ≥ 1 form a subgroup on which the degree-N part is additive (FormalGroup.homogeneousComponent_val_sub, from FormalGroup.le_order_subst_sub_sub: G(w, v) = w + v up to degree N + 1 when w vanishes to order N), and the defect at any pair of points is obtained from the defect at the coordinate points by substitution (FormalGroup.substPointHom), so these identities pass to the degree-n part of the defect, which is then a symmetric additive 2-cocycle, hence a multiple of C_n by the symmetric 2-cocycle lemma TauCeti.exists_eq_smul_lazardCocycle; its value in degree pᵏ comes from the identity ∑_{j < p} C_{pᵏ}(j, 1) = -1 in characteristic p.

The homomorphism defect itself and its basic API are in TauCeti.RingTheory.FormalGroup.Hom.Basic.

Main results

• FormalGroup.exists_homogeneousComponent_eq_smul_lazardCocycle: the leading term of a symmetric series satisfying the 2-cocycle identity along a formal group law up to higher-order terms is a multiple of the Lazard cocycle.
• FormalGroup.exists_homogeneousComponent_homDefect_eq_smul_lazardCocycle: the leading term of the homomorphism defect is a multiple c C_n of the Lazard cocycle.
• FormalGroup.homogeneousComponent_homDefect_eq_smul_lazardCocycle: in degree pᵏ and characteristic p, the multiple is the coefficient of X^(pᵏ) in [p]_G ∘ f - f ∘ [p]_F.

References

• M. Lazard, Sur les groupes de Lie formels à un paramètre, Bull. Soc. Math. France 83 (1955).
• A. Fröhlich, Formal Groups, Lecture Notes in Mathematics 74, Springer (1968), Chapter III.
• J. Lurie, Chromatic Homotopy Theory (Harvard lecture notes, 2010), Lecture 13.

theorem FormalGroup.exists_homogeneousComponent_eq_smul_lazardCocycle {R : Type u_1} [CommRing R] (F : FormalGroup R) {n : ℕ} (hn : n ≠ 0) {Φ : MvPowerSeries (Fin 2) R} (hΦ : ↑n ≤ Φ.order) (hsymm : MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 0] Φ = Φ) (hcocycle : ↑(n + 1) ≤ (MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] Φ + MvPowerSeries.subst ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] F.toPowerSeries, MvPowerSeries.X 2] Φ - MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] F.toPowerSeries] Φ - MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] Φ).order) : ∃ (c : R), (MvPowerSeries.homogeneousComponent n) Φ = ↑(c • TauCeti.lazardCocycle n R)

Leading terms of symmetric 2-cocycles. Let F be a formal group law and let Φ(X, Y) be a symmetric series vanishing below degree n ≠ 0 that satisfies the 2-cocycle identity Φ(X, Y) + Φ(F(X, Y), Z) = Φ(X, F(Y, Z)) + Φ(Y, Z) up to terms of degree above n. Then the degree-n part of Φ is a multiple of the Lazard cocycle C_n.

theorem FormalGroup.exists_homogeneousComponent_homDefect_eq_smul_lazardCocycle {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f : PowerSeries R} [G.IsComm] [F.IsComm] (hf : PowerSeries.constantCoeff f = 0) {n : ℕ} (hn : n ≠ 0) (h : ↑n ≤ (F.homDefect G f).order) : ∃ (c : R), (MvPowerSeries.homogeneousComponent n) (F.homDefect G f) = ↑(c • TauCeti.lazardCocycle n R)

The leading defect of an approximate homomorphism is a multiple of the Lazard cocycle. Let F and G be commutative formal group laws and let f be a power series without constant term which is a homomorphism from F to G up to degree n ≠ 0: the homomorphism defect f(F(X, Y)) - G(f(X), f(Y)) vanishes below degree n. Then its degree-n part is c C_n for some c, where C_n is the Lazard cocycle.

theorem FormalGroup.homogeneousComponent_homDefect_eq_smul_lazardCocycle {R : Type u_1} [CommRing R] {F G : FormalGroup R} {f : PowerSeries R} [G.IsComm] [F.IsComm] (hf : PowerSeries.constantCoeff f = 0) {p : ℕ} (hp : Nat.Prime p) (hpR : ↑p = 0) {k : ℕ} (h : ↑(p ^ k) ≤ (F.homDefect G f).order) : (MvPowerSeries.homogeneousComponent (p ^ k)) (F.homDefect G f) = ↑((PowerSeries.coeff (p ^ k)) (PowerSeries.subst f (G.nsmulSeries p) - PowerSeries.subst (F.nsmulSeries p) f) • TauCeti.lazardCocycle (p ^ k) R)

The obstruction in degree pᵏ is read off the p-series. Let p be a prime with p = 0 in R, let F and G be commutative formal group laws over R, and let f be a power series without constant term whose homomorphism defect f(F(X, Y)) - G(f(X), f(Y)) vanishes below degree n = pᵏ. Then the degree-n part of the defect is c C_n, where c is the coefficient of Xⁿ in [p]_G(f(X)) - f([p]_F(X)). In particular the defect vanishes in degree n exactly when f commutes with multiplication by p up to degree n.