Documentation

TauCeti.RingTheory.FormalGroup.Height.Basic

The height of a formal group law #

Let f(T) = a Tⁿ + β‹― be a homomorphism between one-dimensional formal group laws F and G over a commutative ring R, so that f(F(X, Y)) = G(f(X), f(Y)). Since F(X, Y) = X + Y + β‹― and G(X, Y) = X + Y + β‹―, comparing the homogeneous parts of degree n gives

a (X + Y)ⁿ = a Xⁿ + a Yⁿ,

so a kills every binomial coefficient n.choose i with 0 < i < n, hence their greatest common divisor d_n (TauCeti.lazardGcd). Since d_n is p when n is a power of a prime p and 1 otherwise, if p = 0 in R then a nonzero homomorphism has order a power of p: the first nonzero term of f has degree p ^ h. This applies to multiplication by p on a commutative formal group law: either [p]_F = 0, or [p]_F(T) = a T^(p ^ h) + β‹― with a β‰  0 and h β‰₯ 1, since the linear coefficient of [p]_F is p = 0.

Over a field K of characteristic p this exponent is the height of F; it is ⊀ when [p]_F = 0, as for the additive formal group law. The multiplicative formal group law has height one, since [p](T) = (1 + T) ^ p - 1 = T ^ p. The height is unchanged by extension of the base field, and it does not depend on the coordinate: a nonzero homomorphism f from F to G satisfies f ∘ [p]_F = [p]_G ∘ f, and over a field orders multiply under substitution, so [p]_F and [p]_G have the same order. In particular isomorphic formal group laws, such as F and its change of coordinate Ο† β€’ F, have the same height. Over a ring, the leading coefficient of [p]_F need not be a unit, and the exponent no longer measures the height in the usual sense; so the height is defined over fields.

The leading coefficient a of [p]_F(T) = a T ^ (p ^ h) + β‹― depends on the coordinate, but in a controlled way. If f(T) = u T + β‹― is a homomorphism from F to G and b is the leading coefficient of [p]_G, comparing the coefficients of T ^ (p ^ h) in f ∘ [p]_F = [p]_G ∘ f gives b u ^ (p ^ h) = u a. So strict isomorphisms preserve a, and the homothety T ↦ u T with u ^ (p ^ h - 1) = a turns a into 1; over a separably closed field such a u exists (TauCeti.RingTheory.FormalGroup.Height.SepClosed). This normalization is how Lazard's classification of formal group laws over separably closed fields by their height deals with the degree p ^ h: two laws of height h become laws whose p-series have the same leading term T ^ (p ^ h), and the strict coordinate changes that match the remaining coefficients keep it.

Main definitions #

Main results #

References #

source
theorem FormalGroup.coeff_mul_lazardGcd_eq_zero_of_le_order {R : Type u_1} [CommRing R] (F G : FormalGroup R) {f : PowerSeries R} (hf : PowerSeries.subst F.toPowerSeries f = MvPowerSeries.subst (fun (i : Fin 2) => (PowerSeries.toMvPowerSeries i) f) G.toPowerSeries) {n : β„•} (hn : ↑n ≀ f.order) :
(PowerSeries.coeff n) f * ↑(TauCeti.lazardGcd n) = 0

The leading term of a formal group homomorphism. If f(F(X, Y)) = G(f(X), f(Y)) and f has order at least n, then the coefficient a of Tⁿ in f satisfies d_n a = 0, where d_n is the greatest common divisor of the binomial coefficients n.choose i, 0 < i < n.

source
theorem FormalGroup.exists_order_eq_pow_of_natCast_eq_zero {R : Type u_1} [CommRing R] (F G : FormalGroup R) {p : β„•} (hp : Nat.Prime p) (hpR : ↑p = 0) {f : PowerSeries R} (hfβ‚€ : PowerSeries.constantCoeff f = 0) (hf : PowerSeries.subst F.toPowerSeries f = MvPowerSeries.subst (fun (i : Fin 2) => (PowerSeries.toMvPowerSeries i) f) G.toPowerSeries) (hf0 : f β‰  0) :
βˆƒ (h : β„•), f.order = ↑(p ^ h)

Homomorphisms of formal group laws in characteristic p have order a power of p. If p is a prime with p = 0 in R, and f β‰  0 with zero constant coefficient satisfies f(F(X, Y)) = G(f(X), f(Y)), then the first nonzero term of f has degree a power of p.

source
theorem FormalGroup.exists_order_nsmulSeries_eq_pow {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] {p : β„•} (hp : Nat.Prime p) (hpR : ↑p = 0) (h0 : F.nsmulSeries p β‰  0) :
βˆƒ (h : β„•), h β‰  0 ∧ (F.nsmulSeries p).order = ↑(p ^ h)

The p-series has order a power of p in characteristic p: if p is a prime with p = 0 in R and F is commutative, then either [p]_F = 0 or the first nonzero term of [p]_F has degree p ^ h for some h β‰₯ 1.

source
noncomputable def FormalGroup.height {K : Type u_1} [Field K] (F : FormalGroup K) (p : β„•) :
β„•βˆž

The height of a formal group law F over a field K of characteristic p: ⊀ if multiplication by p on F is zero, and otherwise the exponent h such that the first nonzero term of [p]_F(T) has degree p ^ h (see FormalGroup.height_eq_natCast_iff).

Instances For
    source
    @[simp]
    theorem FormalGroup.height_eq_top_iff {K : Type u_1} [Field K] (F : FormalGroup K) {p : β„•} :
    F.height p = ⊀ ↔ F.nsmulSeries p = 0

    A formal group law has infinite height exactly when multiplication by p is zero.

    source
    theorem FormalGroup.height_eq_natCast_iff {K : Type u_1} [Field K] (F : FormalGroup K) {p : β„•} [CharP K p] [F.IsComm] {h : β„•} :
    F.height p = ↑h ↔ (F.nsmulSeries p).order = ↑(p ^ h)

    A commutative formal group law over a field of characteristic p has height h exactly when the first nonzero term of [p]_F(T) has degree p ^ h.

    source
    theorem FormalGroup.one_le_height {K : Type u_1} [Field K] (F : FormalGroup K) {p : β„•} [CharP K p] [F.IsComm] :
    1 ≀ F.height p

    The height of a commutative formal group law over a field of characteristic p is at least one.

    source
    theorem FormalGroup.ne_zero_of_height_eq_natCast {K : Type u_1} [Field K] (F : FormalGroup K) {p : β„•} [CharP K p] [F.IsComm] {h : β„•} (hF : F.height p = ↑h) :
    h β‰  0

    A commutative formal group law of finite height h over a field of characteristic p has h β‰  0.

    source
    theorem FormalGroup.height_eq_one_iff {K : Type u_1} [Field K] (F : FormalGroup K) {p : β„•} [CharP K p] [F.IsComm] :
    F.height p = 1 ↔ (PowerSeries.coeff p) (F.nsmulSeries p) β‰  0

    A commutative formal group law over a field of characteristic p has height one exactly when the coefficient of Tα΅– in [p]_F(T) is nonzero.

    source
    theorem FormalGroup.coeff_nsmulSeries_eq_zero_of_lt_height {K : Type u_1} [Field K] (F : FormalGroup K) {p k : β„•} (hk : ↑k < F.height p) :
    (PowerSeries.coeff (p ^ k)) (F.nsmulSeries p) = 0

    Below the height, the p-series has no terms of p-power degree: if k is less than the height of a formal group law F over a field, the coefficient of T ^ (p ^ k) in [p]_F(T) is zero.

    source
    theorem FormalGroup.coeff_nsmulSeries_ne_zero_of_height_eq {K : Type u_1} [Field K] (F : FormalGroup K) {p : β„•} [CharP K p] [F.IsComm] {h : β„•} (hF : F.height p = ↑h) :
    (PowerSeries.coeff (p ^ h)) (F.nsmulSeries p) β‰  0

    The coefficient of T ^ (p ^ h) in [p]_F(T) is nonzero when F has height h.

    source
    @[simp]
    theorem FormalGroup.height_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] (F : FormalGroup K) (Ο† : K β†’+* L) (p : β„•) :
    (F.map Ο†).height p = F.height p

    The height is invariant under extension of the base field.

    source
    @[simp]
    theorem FormalGroup.height_𝔾ₐ {K : Type u_1} [Field K] {p : β„•} [CharP K p] :
    𝔾ₐ.height p = ⊀

    The additive formal group law has infinite height.

    source
    @[simp]
    theorem FormalGroup.height_π”Ύβ‚˜ {K : Type u_1} [Field K] {p : β„•} [Fact (Nat.Prime p)] [CharP K p] :
    π”Ύβ‚˜.height p = 1

    The multiplicative formal group law has height one.

    source
    theorem TauCeti.FormalGroupHom.order_nsmulSeries_eq {R : Type u_1} [CommRing R] [NoZeroDivisors R] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : f.toPowerSeries β‰  0) (n : β„•) :
    (F.nsmulSeries n).order = (G.nsmulSeries n).order

    A nonzero homomorphism preserves the order of multiplication by n. Over an integral domain, if f is a nonzero homomorphism of formal group laws from F to G, then [n]_F and [n]_G have the same order, since f ∘ [n]_F = [n]_G ∘ f and orders multiply under substitution.

    source
    theorem TauCeti.FormalGroupHom.height_eq {K : Type u_1} [Field K] {F G : FormalGroup K} (f : FormalGroupHom F G) (hf : f.toPowerSeries β‰  0) (p : β„•) :
    F.height p = G.height p

    Height is preserved by nonzero homomorphisms: if there is a nonzero homomorphism of formal group laws from F to G over a field, then F and G have the same height.

    source
    theorem TauCeti.FormalGroupHom.coeff_nsmulSeries_mul_coeff_one_pow {K : Type u_1} [Field K] {F G : FormalGroup K} {p : β„•} [CharP K p] [F.IsComm] (f : FormalGroupHom F G) {h : β„•} (hF : F.height p = ↑h) :
    (PowerSeries.coeff (p ^ h)) (G.nsmulSeries p) * (PowerSeries.coeff 1) f.toPowerSeries ^ p ^ h = (PowerSeries.coeff 1) f.toPowerSeries * (PowerSeries.coeff (p ^ h)) (F.nsmulSeries p)

    A homomorphism relates the leading coefficients of the p-series. If F has finite height h over a field of characteristic p, and f is a homomorphism from F to G with linear coefficient u, then the coefficients a and b of T ^ (p ^ h) in [p]_F and [p]_G satisfy b u ^ (p ^ h) = u a.

    source
    theorem TauCeti.FormalGroupIso.coeff_nsmulSeries_eq_of_isStrict {K : Type u_1} [Field K] {F G : FormalGroup K} {p : β„•} [CharP K p] [F.IsComm] (e : FormalGroupIso F G) [e.IsStrict] {h : β„•} (hF : F.height p = ↑h) :
    (PowerSeries.coeff (p ^ h)) (G.nsmulSeries p) = (PowerSeries.coeff (p ^ h)) (F.nsmulSeries p)

    Strict isomorphisms preserve the leading coefficient of the p-series. If F has finite height h over a field of characteristic p and e is a strict isomorphism from F to G, then [p]_F and [p]_G have the same coefficient of T ^ (p ^ h).

    source
    theorem TauCeti.FormalGroupIso.order_nsmulSeries_eq {R : Type u_1} [CommRing R] {F G : FormalGroup R} (e : FormalGroupIso F G) (n : β„•) :
    (F.nsmulSeries n).order = (G.nsmulSeries n).order

    An isomorphism preserves the order of multiplication by n. Over any commutative ring, if e is an isomorphism of formal group laws from F to G, then [n]_F and [n]_G have the same order, since [n]_G = e ∘ [n]_F ∘ e⁻¹ and substitution into or of a series without constant term does not lower the order.

    source
    theorem TauCeti.FormalGroupIso.height_eq {K : Type u_1} [Field K] {F G : FormalGroup K} (e : FormalGroupIso F G) (p : β„•) :
    F.height p = G.height p

    Coordinate independence of height: isomorphic formal group laws over a field have the same height.

    source
    @[simp]
    theorem FormalGroup.height_smul {K : Type u_1} [Field K] (Ο† : TauCeti.FormalCoordinate K) (F : FormalGroup K) (p : β„•) :
    (Ο† β€’ F).height p = F.height p

    The height is unchanged by a change of coordinate Ο† β€’ F.

    source
    theorem FormalGroup.coeff_nsmulSeries_homothety_smul_eq_one {K : Type u_1} [Field K] {p : β„•} [CharP K p] (F : FormalGroup K) [F.IsComm] {h : β„•} (hF : F.height p = ↑h) (u : KΛ£) (hu : ↑u ^ (p ^ h - 1) = (PowerSeries.coeff (p ^ h)) (F.nsmulSeries p)) :
    (PowerSeries.coeff (p ^ h)) ((TauCeti.FormalCoordinate.homothety u β€’ F).nsmulSeries p) = 1

    Normalizing the leading coefficient of the p-series. Let F be a commutative formal group law of finite height h over a field of characteristic p, and let a be the leading coefficient of [p]_F. For any unit u with u ^ (p ^ h - 1) = a, the homothety T ↦ u T turns F into a formal group law whose p-series has leading term T ^ (p ^ h).