The height ideals of a formal group law

Let F be a formal group law over a commutative ring R and let p be a prime. The n-th height ideal I_n(F) (FormalGroup.heightIdeal) is the ideal generated by the coefficients of the p-series [p]_F(X) in degrees below pⁿ. Equivalently, a ring homomorphism φ : R →+* S kills I_n(F) exactly when the p-series of the base change of F along φ vanishes to order pⁿ (FormalGroup.heightIdeal_le_ker_iff), so R ⧸ I_n(F) is the universal quotient of R over which [p]_F vanishes to order pⁿ. Over a field of characteristic p the height ideal I_n is zero when the height of F is at least n, and the unit ideal otherwise (FormalGroup.heightIdeal_eq_bot_iff_le_height, FormalGroup.heightIdeal_eq_top_iff_height_lt).

For commutative F these are Landweber's ideals I_n = (v₀, v₁, …, v_(n-1)): I₀ = 0, I₁ = (p), and I_(n+1) = I_n + (v_n), where v_n is the coefficient of X^(pⁿ) in [p]_F (FormalGroup.heightIdeal_succ). Only the class of v_n modulo I_n matters (FormalGroup.heightIdeal_succ_eq_sup_of_sub_mem). The proof works over R ⧸ (I_n + (v_n)): there p = 0, so the p-series of a commutative formal group law is either zero or has order a power of p (FormalGroup.exists_order_nsmulSeries_eq_pow), and order greater than pⁿ then forces order at least p^(n+1).

The height ideals do not depend on the coordinate: isomorphic formal group laws have the same height ideals (TauCeti.FormalGroupIso.heightIdeal_eq), and the height ideals commute with base change (FormalGroup.map_heightIdeal). For the universal formal group law over the Lazard ring L and the universal strict coordinate change over L[b₁, b₂, …], this says that the height ideals of L are invariant ideals of the Hopf algebroid (L, L[b₁, b₂, …]): their extensions along the left and right units agree (TauCeti.LazardRing.map_rightUnit_heightIdeal, stated with the rest of the Hopf algebroid in TauCeti.RingTheory.FormalGroup.CoordinateChange.HopfAlgebroid). Through Quillen's identification of L with MU_*, these are the ideals I_(p,n) in the hypothesis of Landweber's exact functor theorem.

Main definitions

• FormalGroup.heightIdeal: the ideal generated by the coefficients of [p]_F below degree pⁿ.

Main results

• FormalGroup.heightIdeal_le_ker_iff: a ring homomorphism kills I_n(F) exactly when the p-series of the base change of F vanishes to order pⁿ.
• FormalGroup.map_heightIdeal: the height ideals commute with base change.
• TauCeti.FormalGroupIso.heightIdeal_eq: isomorphic formal group laws have the same height ideals.
• FormalGroup.heightIdeal_𝔾ₘ_eq_top and FormalGroup.heightIdeal_𝔾ₐ: I_n(𝔾ₘ) is the unit ideal for n ≥ 2, while I_n(𝔾ₐ) = (p) for n ≥ 1.
• FormalGroup.heightIdeal_succ: I_(n+1) = I_n + (v_n) for commutative F.
• FormalGroup.heightIdeal_one: I₁ = (p) for commutative F.
• FormalGroup.heightIdeal_eq_span: I_n = (v₀, …, v_(n-1)) for commutative F.
• FormalGroup.heightIdeal_eq_bot_iff_le_height: over a field of characteristic p, I_n = 0 exactly when F has height at least n.

References

• P. S. Landweber, Homological properties of comodules over MU_*(MU) and BP_*(BP), Amer. J. Math. 98 (1976), 591–610.
• D. C. Ravenel, Complex Cobordism and Stable Homotopy Groups of Spheres, Chapter 4.

noncomputable def FormalGroup.heightIdeal {R : Type u_1} [CommRing R] (F : FormalGroup R) (p n : ℕ) : Ideal R

The n-th height ideal of a formal group law F at p: the ideal generated by the coefficients of the p-series [p]_F(X) in degrees below pⁿ, that is, the smallest ideal modulo which [p]_F vanishes to order pⁿ.

theorem FormalGroup.heightIdeal_le_iff {R : Type u_1} [CommRing R] {F : FormalGroup R} {p n : ℕ} {I : Ideal R} : F.heightIdeal p n ≤ I ↔ ∀ k < p ^ n, (PowerSeries.coeff k) (F.nsmulSeries p) ∈ I

The height ideal I_n(F) is contained in an ideal I exactly when the coefficients of [p]_F below degree pⁿ lie in I.

theorem FormalGroup.coeff_nsmulSeries_mem_heightIdeal {R : Type u_1} [CommRing R] {F : FormalGroup R} {p n k : ℕ} (hk : k < p ^ n) : (PowerSeries.coeff k) (F.nsmulSeries p) ∈ F.heightIdeal p n

The coefficients of [p]_F below degree pⁿ lie in the height ideal I_n(F).

theorem FormalGroup.heightIdeal_le_ker_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : FormalGroup R} {p n : ℕ} (φ : R →+* S) : F.heightIdeal p n ≤ RingHom.ker φ ↔ ↑(p ^ n) ≤ ((F.map φ).nsmulSeries p).order

The universal property of the height ideal. A ring homomorphism φ kills I_n(F) exactly when the p-series of the base change of F along φ vanishes to order pⁿ.

theorem FormalGroup.heightIdeal_eq_bot_iff {R : Type u_1} [CommRing R] {F : FormalGroup R} {p n : ℕ} : F.heightIdeal p n = ⊥ ↔ ↑(p ^ n) ≤ (F.nsmulSeries p).order

The height ideal I_n(F) vanishes exactly when [p]_F vanishes to order pⁿ.

@[simp]

theorem FormalGroup.heightIdeal_zero {R : Type u_1} [CommRing R] {F : FormalGroup R} {p : ℕ} : F.heightIdeal p 0 = ⊥

The zeroth height ideal is zero, since [p]_F has no constant term.

theorem FormalGroup.heightIdeal_mono {R : Type u_1} [CommRing R] {F : FormalGroup R} {p : ℕ} : Monotone (F.heightIdeal p)

The height ideals increase with n.

@[simp]

theorem FormalGroup.map_heightIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : FormalGroup R} {p : ℕ} (φ : R →+* S) (n : ℕ) : Ideal.map φ (F.heightIdeal p n) = (F.map φ).heightIdeal p n

The height ideals commute with base change.

theorem TauCeti.FormalGroupIso.heightIdeal_eq {R : Type u_1} [CommRing R] {F G : FormalGroup R} (e : FormalGroupIso F G) (p n : ℕ) : F.heightIdeal p n = G.heightIdeal p n

Coordinate independence of the height ideals: isomorphic formal group laws have the same height ideals.

@[simp]

theorem FormalGroup.heightIdeal_smul {R : Type u_1} [CommRing R] {p : ℕ} (φ : TauCeti.FormalCoordinate R) (F : FormalGroup R) (n : ℕ) : (φ • F).heightIdeal p n = F.heightIdeal p n

The height ideals are unchanged by a change of coordinate φ • F.

@[simp]

theorem FormalGroup.heightIdeal_𝔾ₘ_eq_top {R : Type u_1} [CommRing R] {p : ℕ} (hp : 1 < p) {n : ℕ} (hn : 2 ≤ n) : 𝔾ₘ.heightIdeal p n = ⊤

The height ideals of the multiplicative formal group law X + Y + XY from I₂ on are the unit ideal: the coefficient of Xᵖ in its p-series (1 + X)ᵖ - 1 is 1.

@[simp]

theorem FormalGroup.heightIdeal_𝔾ₐ {R : Type u_1} [CommRing R] {p : ℕ} (hp : 1 < p) {n : ℕ} (hn : n ≠ 0) : 𝔾ₐ.heightIdeal p n = Ideal.span {↑p}

The height ideals I_n of the additive formal group law X + Y with n ≥ 1 are all (p): its p-series p X has no coefficient beyond the linear one.

theorem FormalGroup.heightIdeal_succ {R : Type u_1} [CommRing R] {p : ℕ} (F : FormalGroup R) [F.IsComm] (hp : Nat.Prime p) (n : ℕ) : F.heightIdeal p (n + 1) = F.heightIdeal p n ⊔ Ideal.span {(PowerSeries.coeff (p ^ n)) (F.nsmulSeries p)}

Landweber's recursion for the height ideals. For a commutative formal group law F and a prime p, I_(n+1)(F) = I_n(F) + (v_n), where v_n is the coefficient of X^(pⁿ) in [p]_F.

theorem FormalGroup.heightIdeal_succ_eq_sup_of_sub_mem {R : Type u_1} [CommRing R] {p : ℕ} (F : FormalGroup R) [F.IsComm] (hp : Nat.Prime p) {n : ℕ} {v : R} (hv : v - (PowerSeries.coeff (p ^ n)) (F.nsmulSeries p) ∈ F.heightIdeal p n) : F.heightIdeal p (n + 1) = F.heightIdeal p n ⊔ Ideal.span {v}

The recursion I_(n+1) = I_n + (v_n) holds for every lift v of v_n modulo I_n.

theorem FormalGroup.heightIdeal_one {R : Type u_1} [CommRing R] {p : ℕ} (F : FormalGroup R) [F.IsComm] (hp : Nat.Prime p) : F.heightIdeal p 1 = Ideal.span {↑p}

The first height ideal is generated by p.

theorem FormalGroup.heightIdeal_eq_span {R : Type u_1} [CommRing R] {p : ℕ} (F : FormalGroup R) [F.IsComm] (hp : Nat.Prime p) (n : ℕ) : F.heightIdeal p n = Ideal.span ((fun (i : ℕ) => (PowerSeries.coeff (p ^ i)) (F.nsmulSeries p)) '' Set.Iio n)

Landweber's generators. I_n(F) = (v₀, …, v_(n-1)), where v_i is the coefficient of X^(pⁱ) in [p]_F; in particular v₀ = p.

theorem FormalGroup.heightIdeal_fg {R : Type u_1} [CommRing R] {p : ℕ} (F : FormalGroup R) [F.IsComm] (hp : Nat.Prime p) (n : ℕ) : (F.heightIdeal p n).FG

The height ideals of a commutative formal group law are finitely generated.

theorem FormalGroup.heightIdeal_eq_bot_iff_le_height {K : Type u_1} [Field K] (F : FormalGroup K) [F.IsComm] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] {n : ℕ} : F.heightIdeal p n = ⊥ ↔ ↑n ≤ F.height p

Over a field of characteristic p, the height ideal I_n(F) is zero exactly when F has height at least n.

theorem FormalGroup.heightIdeal_eq_top_iff_height_lt {K : Type u_1} [Field K] (F : FormalGroup K) [F.IsComm] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP K p] {n : ℕ} : F.heightIdeal p n = ⊤ ↔ F.height p < ↑n

Over a field of characteristic p, the height ideal I_n(F) is the unit ideal exactly when F has height less than n.