Formal group laws of finite height over separably closed fields

Let F be a commutative formal group law of finite height h over a field K of characteristic p, so that [p]_F(T) = a T ^ (p ^ h) + ⋯ with a ≠ 0. The homothety T ↦ u T turns a into 1 whenever u ^ (p ^ h - 1) = a (FormalGroup.coeff_nsmulSeries_homothety_smul_eq_one). Since p ^ h - 1 is -1 in K, the polynomial X ^ (p ^ h - 1) - a is separable, so over a separably closed field such a u exists. This is the normalization in degree p ^ h in Lazard's classification of formal group laws over separably closed fields by their height.

Main results

• FormalGroup.exists_coeff_nsmulSeries_homothety_smul_eq_one: over a separably closed field, a homothety makes the leading coefficient of the p-series equal to one.

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.

theorem FormalGroup.exists_coeff_nsmulSeries_homothety_smul_eq_one {K : Type u_1} [Field K] [IsSepClosed K] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] (F : FormalGroup K) [F.IsComm] {h : ℕ} (hF : F.height p = ↑h) : ∃ (u : Kˣ), (PowerSeries.coeff (p ^ h)) ((TauCeti.FormalCoordinate.homothety u • F).nsmulSeries p) = 1

Normalizing the leading coefficient of the p-series over a separably closed field. Over a separably closed field of characteristic p, a commutative formal group law F of finite height h becomes, after the homothety T ↦ u T by a suitable unit u, a formal group law whose p-series has leading term T ^ (p ^ h).