Classification of formal group laws by height

Let K be a separably closed field of characteristic p. Lazard's theorem: two commutative formal group laws F and G over K are isomorphic exactly when they have the same height (FormalGroup.height_eq_height_iff_nonempty_formalGroupIso). Isomorphic laws have the same height by TauCeti.FormalGroupIso.height_eq, and in height ⊤ both are isomorphic to the additive law by FormalGroup.height_eq_top_iff_nonempty_formalGroupIso_𝔾ₐ. This file treats finite height h, writing q = p ^ h.

An isomorphism f : F → G is built degree by degree. Suppose the homomorphism defect Φ(X, Y) = f(F(X, Y)) - G(f(X), f(Y)) (FormalGroup.homDefect) vanishes below degree n ≥ 2. Its degree-n part is r C_n for the Lazard cocycle C_n (FormalGroup.exists_homogeneousComponent_homDefect_eq_smul_lazardCocycle), and replacing f by f + c Xⁿ adds c ((X + Y)ⁿ - Xⁿ - Yⁿ) = c d_n C_n to it.

• If n is not a power of p, then d_n is a unit in K and a unique c cancels the defect.
• If n = pᵏ, then d_n = p = 0 and adding c Xⁿ does not change the degree-n defect. Instead r is forced: -r is the coefficient of Xⁿ in f([p]_F(X)) - [p]_G(f(X)) (FormalGroup.homogeneousComponent_homDefect_eq_smul_lazardCocycle). This series vanishes below degree q, and its coefficient of X^(m q) only involves the coefficients of f up to degree m. Since [p]_G(X) = ψ(X^q) for an isomorphism ψ (FormalGroup.heightFrobeniusIso), that coefficient changes by c uᵐ - v c^q when f is replaced by f + c Xᵐ, where u, v are the coefficients of X^q in [p]_F, [p]_G. So the free coefficient of f in degree m = pʲ can be chosen, as a root of a separable polynomial -v x^q + uᵐ x + a, to make the coefficient of X^(m q) vanish, and then r = 0 in degree pʲ q. This is where separable closedness is used; the linear coefficient of f is a nonzero root of x^(q - 1) = u / v.

The defect is then zero in the limit, and f is an isomorphism since its linear coefficient is nonzero. The case G = 𝔾ₐ, [p]_F = 0 of the same obstruction argument constructs the normalised logarithm in TauCeti.RingTheory.FormalGroup.Logarithm.InfiniteHeight.

Main results

• FormalGroup.height_eq_height_iff_nonempty_formalGroupIso: over a separably closed field of characteristic p, commutative formal group laws are isomorphic exactly when their heights agree.

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, Chapter III, §2.
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Theorem A2.2.11.

theorem FormalGroup.height_eq_height_iff_nonempty_formalGroupIso {K : Type u_1} [Field K] [IsSepClosed K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (F G : FormalGroup K) [F.IsComm] [G.IsComm] : F.height p = G.height p ↔ Nonempty (TauCeti.FormalGroupIso F G)

Lazard's classification of formal group laws by height. Over a separably closed field K of characteristic p, two commutative formal group laws are isomorphic exactly when they have the same height. In height ⊤ both are isomorphic to the additive formal group law.