Documentation

TauCeti.RingTheory.FormalGroup.Logarithm.Rescale

Integral logarithms of rescaled formal group laws #

Let F be a formal group law over a commutative ring R, with invariant differential P(T) = ∑ pₙ Tⁿ, and let s ∈ R. The rescaling F^s, with s · F^s(X, Y) = F(s X, s Y) (FormalGroup.rescale), has invariant differential P(s T) (FormalGroup.invariantDifferential_rescale), so over a ℚ-algebra its logarithm is

log_{F^s}(T) = ∑_{n ≥ 0} (sⁿ / (n + 1)) pₙ Tⁿ⁺¹,

that is s · log_{F^s}(T) = log_F(s T) (FormalGroup.smul_log_rescale). The denominators of log_F are cancelled by the powers of s as soon as n + 1 divides sⁿ in R for every n. Then the series above has coefficients in R, even though R need not contain ℚ. This series is FormalGroup.rescaleLog. Over a ring without additive torsion it is additive along F^s, and its linear coefficient is 1. So it is a strict isomorphism from F^s to the additive formal group law, defined over R (FormalGroup.rescaleLogIso). After base change to any ℚ-algebra it becomes the logarithm of F^s, and its inverse becomes the exponential of F^s (FormalGroup.map_rescaleLog, FormalGroup.map_invHom_rescaleLogIso).

The divisibility hypothesis holds when p ∣ s ^ (p - 1) for a prime p and every natural number prime to p is a unit of R (TauCeti.natCast_add_one_dvd_pow). For the ring of integers of a finite extension of ℚ_p with normalised valuation v, this asks v(s) ≥ v(p) / (p - 1); for ℤ_p one may take s = p, including p = 2. Since the points of F^s in the maximal ideal 𝔪 are carried to the points of F in s 𝔪 by t ↦ s t, this is the formal input to the comparison of the formal group F(s 𝔪) with the additive group s 𝔪 through the logarithm (Silverman IV.6.4).

Main definitions #

Main results #

References #

source
theorem FormalGroup.smul_log_rescale {R : Type u_1} [CommRing R] (F : FormalGroup R) (s : R) [Algebra ℚ R] :
s • (F.rescale s).log = (PowerSeries.rescale s) F.log

The logarithm of the rescaling: over a ℚ-algebra, s · log_{F^s}(T) = log_F(s T). So log_{F^s}(T) = s⁻¹ log_F(s T) when s is a unit.

source
noncomputable def FormalGroup.rescaleLog {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) :
PowerSeries R

The integral logarithm of the rescaling F^s, when n + 1 divides sⁿ for every n: the power series ∑_{n ≥ 0} (sⁿ / (n + 1)) pₙ Tⁿ⁺¹ with coefficients in R, where P(T) = ∑ pₙ Tⁿ is the invariant differential of F. Its derivative is the invariant differential of F^s (FormalGroup.derivative_rescaleLog), and after base change to a ℚ-algebra it is the logarithm of F^s (FormalGroup.map_rescaleLog). The quotient sⁿ / (n + 1) is a chosen witness of the divisibility; it is unique when R has no additive torsion, which is the case in which the series is additive along F^s.

Instances For
    source
    theorem FormalGroup.coeff_succ_rescaleLog {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) (n : ℕ) :
    (PowerSeries.coeff (n + 1)) (F.rescaleLog hs) = Exists.choose ⋯ * (PowerSeries.coeff n) F.invariantDifferential

    The coefficient of Tⁿ⁺¹ in the integral logarithm is the chosen quotient sⁿ / (n + 1) times the coefficient pₙ of the invariant differential of F.

    source
    @[simp]
    theorem FormalGroup.constantCoeff_rescaleLog {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) :
    PowerSeries.constantCoeff (F.rescaleLog hs) = 0

    The integral logarithm has no constant term.

    source
    @[simp]
    theorem FormalGroup.derivative_rescaleLog {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) :
    PowerSeries.derivative (F.rescaleLog hs) = (F.rescale s).invariantDifferential

    The derivative of the integral logarithm of F^s is the invariant differential of F^s: the coefficient of Tⁿ⁺¹ times n + 1 is sⁿ pₙ.

    source
    @[simp]
    theorem FormalGroup.coeff_one_rescaleLog {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) :
    (PowerSeries.coeff 1) (F.rescaleLog hs) = 1

    The integral logarithm has linear coefficient 1.

    source
    theorem FormalGroup.eq_rescaleLog_of_derivative_eq {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) [HasUniqueDiv R] {g : PowerSeries R} (hg₀ : PowerSeries.constantCoeff g = 0) (hg : PowerSeries.derivative g = (F.rescale s).invariantDifferential) :
    g = F.rescaleLog hs

    Over a ring without additive torsion, the integral logarithm of F^s is the only power series with no constant term whose derivative is the invariant differential of F^s. In particular it does not depend on the chosen quotients sⁿ / (n + 1).

    source
    @[simp]
    theorem FormalGroup.map_rescaleLog {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) {S : Type u_2} [CommRing S] [Algebra ℚ S] (f : R →+* S) :
    (PowerSeries.map f) (F.rescaleLog hs) = ((F.rescale s).map f).log

    The integral logarithm becomes the logarithm of F^s after base change to a ℚ-algebra.

    source
    noncomputable def FormalGroup.rescaleLogHom {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) [HasUniqueDiv R] :
    TauCeti.FormalGroupHom (F.rescale s) 𝔾ₐ

    The integral logarithm of F^s, as a homomorphism from F^s to the additive formal group law, over a ring without additive torsion.

    Instances For
      source
      @[simp]
      theorem FormalGroup.rescaleLogHom_toPowerSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) [HasUniqueDiv R] :
      (F.rescaleLogHom hs).toPowerSeries = F.rescaleLog hs
      source
      noncomputable def FormalGroup.rescaleLogIso {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) [HasUniqueDiv R] :
      TauCeti.FormalGroupIso (F.rescale s) 𝔾ₐ

      The integral logarithm is a strict isomorphism from F^s to the additive formal group law, defined over R, when R has no additive torsion and n + 1 divides sⁿ for every n.

      Instances For
        source
        @[simp]
        theorem FormalGroup.rescaleLogIso_toHom {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) [HasUniqueDiv R] :
        (F.rescaleLogIso hs).toHom = F.rescaleLogHom hs
        source
        instance FormalGroup.instIsStrictRescaleLogIso {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) [HasUniqueDiv R] :
        (F.rescaleLogIso hs).IsStrict
        source
        theorem FormalGroup.map_invHom_rescaleLogIso {R : Type u_1} [CommRing R] (F : FormalGroup R) {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) [HasUniqueDiv R] {S : Type u_2} [CommRing S] [Algebra ℚ S] (f : R →+* S) :
        (PowerSeries.map f) (F.rescaleLogIso hs).invHom.toPowerSeries = ((F.rescale s).map f).exp

        The inverse of the integral logarithm becomes the exponential of F^s after base change to a ℚ-algebra. So the exponential of F^s has coefficients in R.

        source
        theorem TauCeti.FormalGroupHom.toPowerSeries_eq_coeff_one_smul_rescaleLog {R : Type u_1} [CommRing R] [HasUniqueDiv R] {F : FormalGroup R} {s : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) (f : FormalGroupHom (F.rescale s) FormalGroup.𝔾ₐ) :
        f.toPowerSeries = (PowerSeries.coeff 1) f.toPowerSeries • F.rescaleLog hs

        A homomorphism from a rescaled formal group to the additive law is its linear coefficient times the integral logarithm.

        source
        theorem TauCeti.FormalGroupHom.subst_rescaleLog {R : Type u_1} [CommRing R] [HasUniqueDiv R] {F G : FormalGroup R} {s t : R} (hs : ∀ (n : ℕ), ↑n + 1 ∣ s ^ n) (ht : ∀ (n : ℕ), ↑n + 1 ∣ t ^ n) (f : FormalGroupHom (F.rescale s) (G.rescale t)) :
        PowerSeries.subst f.toPowerSeries (G.rescaleLog ht) = (PowerSeries.coeff 1) f.toPowerSeries • F.rescaleLog hs

        Integral logarithms are natural along homomorphisms, including when the tangent map is not a unit: log_G(f(T)) = f'(0) log_F(T).