Formal group laws of infinite height are additive

Let p be a prime and let F be a commutative formal group law over a commutative ring R with [p]_F = 0. Then p = 0 in R, since p is the linear coefficient of [p]_F, so no logarithm in the sense of FormalGroup.log is available. Nevertheless F is strictly isomorphic to the additive formal group law, along a coordinate that is unique once normalised: there is a unique power series

g(X) = X + ∑_{i ≥ 2} aᵢ Xⁱ with a_{pᵏ} = 0 for every k ≥ 1

such that g(F(X, Y)) = g(X) + g(Y). Over a field of characteristic p, the condition [p]_F = 0 says that F has height ⊤, so the formal group laws of infinite height are exactly those isomorphic to the additive one. For p = 2 this is Quillen's normalised logarithm of a formal group law of exponent two, FormalGroup.exponentTwoLog. No coefficient field and no further hypothesis on R is used: it may have nilpotents or be the zero ring.

The power series g is constructed degree by degree. If g is additive along F up to degree n, the error Φ(X, Y) = g(F(X, Y)) - g(X) - g(Y) is the homomorphism defect of g from F to the additive formal group law, so its degree-n part is r C_n for the Lazard cocycle C_n = ((X + Y)ⁿ - Xⁿ - Yⁿ) / d_n (FormalGroup.exists_homogeneousComponent_homDefect_eq_smul_lazardCocycle).

• If n is not a power of p, then d_n is prime to p, hence a unit in R, and replacing g by g - r d_n⁻¹ Xⁿ makes g additive up to degree n + 1.
• If n = pᵏ with k ≥ 1, then d_n = p and r = 0, since r is the coefficient of Xⁿ in [p]_{𝔾ₐ}(g(X)) - g([p]_F(X)) = p g(X) - g(0) = 0 (FormalGroup.homogeneousComponent_homDefect_eq_smul_lazardCocycle).

Each step leaves the coefficients in lower degrees, and those in degrees pᵏ, unchanged, and g is the limit of these approximations. Uniqueness is the fact that a nonzero homomorphism to the additive formal group law has order a power of p (FormalGroup.exists_order_eq_pow_of_natCast_eq_zero).

Main results

• FormalGroup.existsUnique_logarithm_of_nsmulSeries_eq_zero: for commutative F with [p]_F = 0, there is a unique power series g = X + ⋯ without terms of degree pᵏ, k ≥ 1, such that g(F(X, Y)) = g(X) + g(Y).
• FormalGroup.logarithm_unique_of_natCast_eq_zero: if p = 0 in R, two such power series agree, for any formal group law F.
• FormalGroup.exists_isStrict_formalGroupIso_𝔾ₐ: a commutative formal group law with [p]_F = 0 is strictly isomorphic to the additive formal group law.
• FormalGroup.height_eq_top_iff_nonempty_formalGroupIso_𝔾ₐ: over a field of characteristic p, a commutative formal group law has height ⊤ exactly when it is isomorphic to the additive one.

References

• M. Lazard, Sur les groupes de Lie formels à un paramètre, Bull. Soc. Math. France 83 (1955).
• D. Quillen, On the formal group laws of unoriented and complex cobordism theory, Bull. Amer. Math. Soc. 75 (1969).
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Appendix A2.

theorem FormalGroup.logarithm_unique_of_natCast_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {p : ℕ} (hp : Nat.Prime p) (hpR : ↑p = 0) {g g' : PowerSeries R} (h₀ : PowerSeries.constantCoeff g = 0) (h₁ : (PowerSeries.coeff 1) g = 1) (hpow : ∀ (k : ℕ), 0 < k → (PowerSeries.coeff (p ^ k)) g = 0) (hg : PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g) (h₀' : PowerSeries.constantCoeff g' = 0) (h₁' : (PowerSeries.coeff 1) g' = 1) (hpow' : ∀ (k : ℕ), 0 < k → (PowerSeries.coeff (p ^ k)) g' = 0) (hg' : PowerSeries.subst F.toPowerSeries g' = PowerSeries.subst (MvPowerSeries.X 0) g' + PowerSeries.subst (MvPowerSeries.X 1) g') : g = g'

Uniqueness of the normalised logarithm in characteristic p. Let p be a prime with p = 0 in R, and let F be a formal group law over R, not necessarily commutative. Two power series g, g' = X + ⋯ without terms of degree pᵏ, k ≥ 1, that are additive along F agree.

Indeed g - g' is a homomorphism from F to the additive formal group law, and a nonzero such homomorphism has order a power of p.

theorem FormalGroup.existsUnique_logarithm_of_nsmulSeries_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] {p : ℕ} (hp : Nat.Prime p) (hF : F.nsmulSeries p = 0) : ∃! g : PowerSeries R, PowerSeries.constantCoeff g = 0 ∧ (PowerSeries.coeff 1) g = 1 ∧ (∀ (k : ℕ), 0 < k → (PowerSeries.coeff (p ^ k)) g = 0) ∧ PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g

The normalised logarithm of a formal group law of infinite height. Let p be a prime and let F be a commutative formal group law over a commutative ring R with [p]_F = 0. There is a unique power series g(X) = X + ∑_{i ≥ 2} aᵢ Xⁱ with a_{pᵏ} = 0 for every k ≥ 1 such that g(F(X, Y)) = g(X) + g(Y).

theorem FormalGroup.exists_isStrict_formalGroupIso_𝔾ₐ {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] {p : ℕ} (hp : Nat.Prime p) (hF : F.nsmulSeries p = 0) : ∃ (f : TauCeti.FormalGroupIso F 𝔾ₐ), f.IsStrict

A formal group law of infinite height is additive. If p is a prime and F is a commutative formal group law with [p]_F = 0, then F is strictly isomorphic to the additive formal group law.

theorem FormalGroup.height_eq_top_iff_nonempty_formalGroupIso_𝔾ₐ {K : Type u_2} [Field K] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] (F : FormalGroup K) [F.IsComm] : F.height p = ⊤ ↔ Nonempty (TauCeti.FormalGroupIso F 𝔾ₐ)

Formal group laws of infinite height are the additive ones. Over a field K of characteristic p, a commutative formal group law has height ⊤ exactly when it is isomorphic to the additive formal group law.