Homomorphisms of formal group laws modulo a degree

Let F and G be formal group laws over a commutative ring R. The homomorphism defect Φ(X, Y) = g(F(X, Y)) - G(g(X), g(Y)) (FormalGroup.homDefect) of a power series g with zero constant term vanishes exactly when g is a homomorphism from F to G. When Φ has order at least n, the series g is a homomorphism up to terms of degree n. This file builds such approximate homomorphisms degree by degree, following Lazard's proof that formal group laws over a separably closed field are classified by their height.

Suppose that F and G are commutative and that Φ vanishes below degree n ≥ 2. Then the degree-n part of Φ is r C_n for the Lazard cocycle C_n = ((X + Y)ⁿ - Xⁿ - Yⁿ) / d_n (FormalGroup.exists_homogeneousComponent_homDefect_eq_smul_lazardCocycle).

• If d_n is a unit in R, replacing g by g - r d_n⁻¹ Xⁿ makes the defect vanish below degree n + 1 (FormalGroup.exists_succ_le_order_homDefect_sub_smul_X_pow). This applies to every n that is not a power of p when p = 0 in R.
• If p is a prime with p = 0 in R and n = pᵏ, the coefficient r is the coefficient of Xⁿ in [p]_G(g(X)) - g([p]_F(X)) (FormalGroup.homogeneousComponent_homDefect_eq_smul_lazardCocycle). For g = X + ⋯, if [p]_F and [p]_G have order at least n and the same coefficient of Xⁿ, then r = 0 (FormalGroup.succ_le_order_homDefect_of_coeff_nsmulSeries_eq).

Starting from g = X, these two steps reach every degree up to pʰ when the p-series of F and G have order at least pʰ and the same coefficient of X^(pʰ): then some g = X + ⋯ is a homomorphism from F to G up to terms of degree greater than pʰ (FormalGroup.exists_le_order_homDefect_of_coeff_nsmulSeries_eq). Over a field of characteristic p this applies to two formal group laws of height h whose p-series have the same leading coefficient. In the degrees pᵏ with k > h the obstruction no longer vanishes automatically; over a separably closed field it is removed by solving an Artin–Schreier type equation. Those degrees are not treated in this file.

Main results

• FormalGroup.le_order_homDefect_sub_smul_X_pow, FormalGroup.homogeneousComponent_homDefect_sub_smul_X_pow: subtracting c Xⁿ from g subtracts c ((X + Y)ⁿ - Xⁿ - Yⁿ) from the degree-n part of the defect.
• FormalGroup.exists_succ_le_order_homDefect_sub_smul_X_pow: in a degree n with d_n a unit, the defect can be removed by subtracting a multiple of Xⁿ.
• FormalGroup.succ_le_order_homDefect_of_coeff_nsmulSeries_eq: in a degree pᵏ where both p-series have order at least pᵏ and the same coefficient of X^(pᵏ), the defect of g = X + ⋯ vanishes automatically.
• FormalGroup.exists_le_order_homDefect_of_coeff_nsmulSeries_eq: commutative formal group laws whose p-series have order at least pʰ and the same coefficient of X^(pʰ) are strictly isomorphic up to degree pʰ.

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 (1968).
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.2.

theorem FormalGroup.le_order_homDefect_sub_smul_X_pow {R : Type u_1} [CommRing R] {F G : FormalGroup R} {n : ℕ} (hn₀ : n ≠ 0) {g : PowerSeries R} (hg : PowerSeries.constantCoeff g = 0) (hn : ↑n ≤ (F.homDefect G g).order) (c : R) : ↑n ≤ (F.homDefect G (g - c • PowerSeries.X ^ n)).order

If the homomorphism defect of g vanishes below degree n ≠ 0, so does that of g - c Xⁿ.

theorem FormalGroup.homogeneousComponent_homDefect_sub_smul_X_pow {R : Type u_1} [CommRing R] {F G : FormalGroup R} {n : ℕ} (hn₀ : n ≠ 0) {g : PowerSeries R} (hg : PowerSeries.constantCoeff g = 0) (c : R) : (MvPowerSeries.homogeneousComponent n) (F.homDefect G (g - c • PowerSeries.X ^ n)) = (MvPowerSeries.homogeneousComponent n) (F.homDefect G g) - ↑(c • ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n - MvPolynomial.X 0 ^ n - MvPolynomial.X 1 ^ n))

Correcting the leading defect. For n ≠ 0, subtracting c Xⁿ from g subtracts c ((X + Y)ⁿ - Xⁿ - Yⁿ) from the degree-n part of the homomorphism defect.

theorem FormalGroup.exists_succ_le_order_homDefect_sub_smul_X_pow {R : Type u_1} [CommRing R] {F G : FormalGroup R} [F.IsComm] [G.IsComm] {n : ℕ} (hn₂ : 2 ≤ n) (hd : IsUnit ↑(TauCeti.lazardGcd n)) {g : PowerSeries R} (hg : PowerSeries.constantCoeff g = 0) (hn : ↑n ≤ (F.homDefect G g).order) : ∃ (c : R), ↑(n + 1) ≤ (F.homDefect G (g - c • PowerSeries.X ^ n)).order

Correcting the defect in degrees with invertible d_n. Let F and G be commutative and let the homomorphism defect of g vanish below degree n ≥ 2. If d_n = TauCeti.lazardGcd n is a unit in R, for instance if n is not a power of a prime p with p = 0 in R, then for some c the defect of g - c Xⁿ vanishes below degree n + 1.

theorem FormalGroup.succ_le_order_homDefect_of_coeff_nsmulSeries_eq {R : Type u_1} [CommRing R] {F G : FormalGroup R} [F.IsComm] [G.IsComm] {p : ℕ} (hp : Nat.Prime p) {k : ℕ} {g : PowerSeries R} (hg : PowerSeries.constantCoeff g = 0) (hg₁ : (PowerSeries.coeff 1) g = 1) (hn : ↑(p ^ k) ≤ (F.homDefect G g).order) (hF : ↑(p ^ k) ≤ (F.nsmulSeries p).order) (hG : ↑(p ^ k) ≤ (G.nsmulSeries p).order) (hFG : (PowerSeries.coeff (p ^ k)) (F.nsmulSeries p) = (PowerSeries.coeff (p ^ k)) (G.nsmulSeries p)) : ↑(p ^ k + 1) ≤ (F.homDefect G g).order

No defect in degree pᵏ when the p-series agree. Let F and G be commutative and let the homomorphism defect of g = X + ⋯ vanish below degree n = pᵏ. If the p-series of F and G both have order at least n and the same coefficient of Xⁿ, the defect of g vanishes below degree n + 1.

theorem FormalGroup.exists_le_order_homDefect_of_coeff_nsmulSeries_eq {R : Type u_1} [CommRing R] {F G : FormalGroup R} [F.IsComm] [G.IsComm] {p : ℕ} (hp : Nat.Prime p) {h : ℕ} (hF : ↑(p ^ h) ≤ (F.nsmulSeries p).order) (hG : ↑(p ^ h) ≤ (G.nsmulSeries p).order) (hFG : (PowerSeries.coeff (p ^ h)) (F.nsmulSeries p) = (PowerSeries.coeff (p ^ h)) (G.nsmulSeries p)) : ∃ (g : PowerSeries R), PowerSeries.constantCoeff g = 0 ∧ (PowerSeries.coeff 1) g = 1 ∧ ↑(p ^ h + 1) ≤ (F.homDefect G g).order

Formal group laws with matching p-series agree up to degree pʰ. Let p be a prime and let F and G be commutative formal group laws over a commutative ring R whose p-series both have order at least pʰ and the same coefficient of X^(pʰ). Then some power series g = X + ⋯ is a homomorphism from F to G up to terms of degree greater than pʰ: g(F(X, Y)) - G(g(X), g(Y)) has order at least pʰ + 1.

Over a field of characteristic p, this applies to two formal group laws of height h whose p-series have the same leading coefficient.