Documentation

TauCeti.RingTheory.FormalGroup.Frobenius.Factorization

Iterated Frobenius factorization #

A nonzero homomorphism of one-dimensional formal groups over a field of characteristic p factors as relative Frobenius iterated h times followed by an isomorphism. The integer h is characterized by the order p ^ h of its underlying series. For this fixed exponent the isomorphism is unique, and its coefficients are those of the original homomorphism in degrees divisible by p ^ h.

This separates the inseparable part of a homomorphism from its invertible coordinate, as used in the classification of formal groups of finite height. No perfectness or commutativity hypothesis is needed for this factorization. Applied to multiplication by p, it identifies a finite-height commutative group with its height-fold coefficient Frobenius twist.

References #

source
theorem TauCeti.FormalGroupHom.coeff_of_comp_iterateFrobeniusHom_eq {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (f : FormalGroupHom F G) (h : ℕ) (g : FormalGroupHom (F.map (iterateFrobenius R p h)) G) (hg : g.comp (F.iterateFrobeniusHom p h) = f) (n : ℕ) :
(PowerSeries.coeff n) g.toPowerSeries = (PowerSeries.coeff (p ^ h * n)) f.toPowerSeries

The factor's coefficients are selected from the original series at multiples of p ^ h.

source
noncomputable def TauCeti.FormalGroupHom.iterateFrobeniusIso {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {F G : FormalGroup K} (f : FormalGroupHom F G) (h : ℕ) (hf : f.toPowerSeries.order = ↑(p ^ h)) :
FormalGroupIso (F.map (iterateFrobenius K p h)) G

The invertible factor remaining after removing h relative Frobenius factors from a homomorphism of order p ^ h.

Instances For
    source
    @[simp]
    theorem TauCeti.FormalGroupHom.iterateFrobeniusIso_comp_iterateFrobeniusHom {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {F G : FormalGroup K} (f : FormalGroupHom F G) (h : ℕ) (hf : f.toPowerSeries.order = ↑(p ^ h)) :
    (f.iterateFrobeniusIso h hf).toHom.comp (F.iterateFrobeniusHom p h) = f

    The invertible factor composes with iterated relative Frobenius to recover the map.

    source
    @[simp]
    theorem TauCeti.FormalGroupHom.coeff_iterateFrobeniusIso {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {F G : FormalGroup K} (f : FormalGroupHom F G) (h : ℕ) (hf : f.toPowerSeries.order = ↑(p ^ h)) (n : ℕ) :
    (PowerSeries.coeff n) (f.iterateFrobeniusIso h hf).toHom.toPowerSeries = (PowerSeries.coeff (p ^ h * n)) f.toPowerSeries

    The invertible factor selects the coefficients in degrees divisible by p ^ h.

    source
    theorem TauCeti.FormalGroupHom.existsUnique_iso_comp_iterateFrobeniusHom_of_order {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {F G : FormalGroup K} (f : FormalGroupHom F G) (h : ℕ) (hf : f.toPowerSeries.order = ↑(p ^ h)) :
    ∃! g : FormalGroupIso (F.map (iterateFrobenius K p h)) G, g.toHom.comp (F.iterateFrobeniusHom p h) = f

    For a specified order p ^ h, the remaining factor is a unique isomorphism.

    source
    theorem TauCeti.FormalGroupHom.exists_iso_comp_iterateFrobeniusHom {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {F G : FormalGroup K} (f : FormalGroupHom F G) (hf : f.toPowerSeries ≠ 0) :
    ∃ (h : ℕ) (g : FormalGroupIso (F.map (iterateFrobenius K p h)) G), f.toPowerSeries.order = ↑(p ^ h) ∧ g.toHom.comp (F.iterateFrobeniusHom p h) = f

    Every nonzero formal group homomorphism over a characteristic-p field is an iterated relative Frobenius followed by an isomorphism.

    source
    noncomputable def FormalGroup.heightFrobeniusIso {K : Type u_1} [Field K] (F : FormalGroup K) [F.IsComm] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {h : ℕ} (hh : F.height p = ↑h) :
    TauCeti.FormalGroupIso (F.map (iterateFrobenius K p h)) F

    The isomorphism from the height-fold coefficient Frobenius twist back to a finite-height formal group, obtained by factoring its p-series.

    Instances For
      source
      @[simp]
      theorem FormalGroup.coeff_heightFrobeniusIso {K : Type u_1} [Field K] (F : FormalGroup K) [F.IsComm] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {h : ℕ} (hh : F.height p = ↑h) (n : ℕ) :
      (PowerSeries.coeff n) (F.heightFrobeniusIso hh).toHom.toPowerSeries = (PowerSeries.coeff (p ^ h * n)) (F.nsmulSeries p)

      The height factor selects coefficients of the p-series in degrees divisible by p ^ h.

      source
      @[simp]
      theorem FormalGroup.heightFrobeniusIso_comp_iterateFrobeniusHom {K : Type u_1} [Field K] (F : FormalGroup K) [F.IsComm] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {h : ℕ} (hh : F.height p = ↑h) :
      (F.heightFrobeniusIso hh).toHom.comp (F.iterateFrobeniusHom p h) = F.nsmulHom p

      The height factor composed with the height-fold relative Frobenius is the p-series.

      source
      theorem FormalGroup.subst_nsmulSeries_eq_subst_pow_heightFrobeniusIso {K : Type u_1} [Field K] (F : FormalGroup K) [F.IsComm] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {h : ℕ} (hh : F.height p = ↑h) {f : PowerSeries K} (hf : PowerSeries.constantCoeff f = 0) :
      PowerSeries.subst f (F.nsmulSeries p) = PowerSeries.subst (f ^ p ^ h) (F.heightFrobeniusIso hh).toHom.toPowerSeries

      For a formal group of finite height h, [p]_F(f) = ψ(f^(p^h)) for every series f with zero constant coefficient, where ψ is the height factor FormalGroup.heightFrobeniusIso.

      source
      theorem FormalGroup.existsUnique_iso_comp_iterateFrobeniusHom_eq_nsmulHom_of_height_eq {K : Type u_1} [Field K] (F : FormalGroup K) [F.IsComm] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {h : ℕ} (hh : F.height p = ↑h) :
      ∃! g : TauCeti.FormalGroupIso (F.map (iterateFrobenius K p h)) F, g.toHom.comp (F.iterateFrobeniusHom p h) = F.nsmulHom p

      For a formal group of finite height h, multiplication by p is the h-fold relative Frobenius followed by a unique isomorphism from the Frobenius twist back to the group.