Documentation

TauCeti.RingTheory.FormalGroup.Frobenius.Basic

Frobenius factorization of formal group homomorphisms #

Over a commutative ring of prime characteristic p, the series X ^ p is a homomorphism from a formal group to its coefficient Frobenius twist. Its h-fold iterate has series X ^ (p ^ h) and composes by expanding the outer series. It is natural with respect to homomorphisms, whose Frobenius twists are their base changes along Frobenius. A homomorphism with zero linear coefficient factors uniquely through this Frobenius homomorphism. Its factor is obtained by selecting the coefficients in degrees divisible by p, using the residue-zero Cartier operator. The coefficient ring may have nilpotents, and the formal groups need not be commutative.

This is the Frobenius factorization argument of Silverman, The Arithmetic of Elliptic Curves, IV.7, Proposition 7.2, using the derivative criterion over arbitrary coefficient rings.

source
noncomputable def FormalGroup.iterateFrobeniusHom {R : Type u_1} [CommRing R] (F : FormalGroup R) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (h : ℕ) :
TauCeti.FormalGroupHom F (F.map (iterateFrobenius R p h))

Relative Frobenius iterated h times, with series X ^ (p ^ h), maps to the corresponding coefficient Frobenius twist.

Instances For
    source
    @[simp]
    theorem FormalGroup.iterateFrobeniusHom_toPowerSeries {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (F : FormalGroup R) (h : ℕ) :
    (F.iterateFrobeniusHom p h).toPowerSeries = PowerSeries.X ^ p ^ h
    source
    noncomputable def FormalGroup.frobeniusHom {R : Type u_1} [CommRing R] (F : FormalGroup R) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] :
    TauCeti.FormalGroupHom F (F.map (frobenius R p))

    Relative Frobenius is the homomorphism with series X ^ p to the coefficient Frobenius twist.

    Instances For
      source
      @[simp]
      theorem FormalGroup.frobeniusHom_toPowerSeries {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (F : FormalGroup R) :
      (F.frobeniusHom p).toPowerSeries = PowerSeries.X ^ p
      source
      theorem TauCeti.FormalGroupHom.comp_iterateFrobeniusHom_toPowerSeries {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (h : ℕ) (g : FormalGroupHom (F.map (iterateFrobenius R p h)) G) :
      (g.comp (F.iterateFrobeniusHom p h)).toPowerSeries = (PowerSeries.expand (p ^ h) ⋯) g.toPowerSeries

      Composition with iterated relative Frobenius expands the outer series.

      source
      theorem TauCeti.FormalGroupHom.map_comp_iterateFrobeniusHom {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (f : FormalGroupHom F G) (h : ℕ) :
      (f.map (iterateFrobenius R p h)).comp (F.iterateFrobeniusHom p h) = (G.iterateFrobeniusHom p h).comp f

      Iterated relative Frobenius is natural: the coefficient Frobenius twist of f after Frobenius on the source equals Frobenius on the target after f, that is, f^(p^h)(X ^ (p ^ h)) = f(X) ^ (p ^ h).

      source
      theorem TauCeti.FormalGroupHom.map_comp_frobeniusHom {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (f : FormalGroupHom F G) :
      (f.map (frobenius R p)).comp (F.frobeniusHom p) = (G.frobeniusHom p).comp f

      Relative Frobenius is natural: the coefficient Frobenius twist of f after Frobenius on the source equals Frobenius on the target after f, that is, f^(p)(X ^ p) = f(X) ^ p.

      source
      noncomputable def TauCeti.FormalGroupHom.frobeniusFactor {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : (PowerSeries.coeff 1) f.toPowerSeries = 0) :
      FormalGroupHom (F.map (frobenius R p)) G

      The factor of a homomorphism with zero tangent map through relative Frobenius.

      Instances For
        source
        @[simp]
        theorem TauCeti.FormalGroupHom.frobeniusFactor_toPowerSeries {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : (PowerSeries.coeff 1) f.toPowerSeries = 0) :
        (f.frobeniusFactor hf).toPowerSeries = (PowerSeries.cartier R p 0) f.toPowerSeries
        source
        @[simp]
        theorem TauCeti.FormalGroupHom.frobeniusFactor_comp_frobeniusHom {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : (PowerSeries.coeff 1) f.toPowerSeries = 0) :
        (f.frobeniusFactor hf).comp (F.frobeniusHom p) = f

        Composing the Frobenius factor with relative Frobenius recovers the original map.

        source
        theorem TauCeti.FormalGroupHom.existsUnique_comp_frobeniusHom {R : Type u_1} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {F G : FormalGroup R} (f : FormalGroupHom F G) (hf : (PowerSeries.coeff 1) f.toPowerSeries = 0) :
        ∃! g : FormalGroupHom (F.map (frobenius R p)) G, g.comp (F.frobeniusHom p) = f

        A homomorphism with zero linear coefficient factors uniquely through relative Frobenius.