Multiplication by n on a formal group law

Let F(X, Y) be a one-dimensional formal group law over a commutative ring R. Multiplication by n on F is the power series [n]_F(T) with [0]_F(T) = 0 and [n + 1]_F(T) = F([n]_F(T), T): it is n times the tautological point T in Mathlib's monoid F.Point Unit of power-series points of F.

When F is commutative, [n]_F multiplies the invariant differential ω = P(T) dT by n, by the chain rule and the invariance of ω in both variables (FormalGroup.subst_invariantDifferential_mul_pderiv and FormalGroup.subst_invariantDifferential_mul_pderiv_one):

P([n]_F(T)) · [n]_F'(T) = n · P(T).

Since P has constant coefficient 1, P([n]_F(T)) is a unit, so the derivative of [n]_F is divisible by n. Reading this coefficientwise, n divides the coefficient of Tᵏ in [n]_F for every k coprime to n. For a prime p this gives the shape of [p]_F that controls p-torsion in formal groups:

[p]_F(T) = p T u(T) + Tᵖ h(T) with u(0) = 1

(Silverman IV.4.4 records the stronger [p]_F(T) = p f(T) + g(Tᵖ)). At a nonzero point t of a complete local domain, the first term can only cancel the second if p is divisible by t ^ (p - 1); this is how p-torsion in the points of a formal group is bounded (Silverman IV.6.1).

The same identity, read in degree p - 1, determines the coefficient of Tᵖ in [p]_F modulo p when p is not a zero divisor. Write P(T) = ∑ₙ pₙ Tⁿ. The terms of [p]_F and of its derivative below degree p are multiples of p, so P([p]_F(T)) ≡ 1 modulo p and Tᵖ, and the coefficient of Tᵖ⁻¹ gives p · [Tᵖ] [p]_F ≡ p · pₚ₋₁ modulo p². Cancelling p, the coefficient of Tᵖ in [p]_F is pₚ₋₁ modulo p. In characteristic p that coefficient decides whether the height is one, so for the reduction of a formal group law defined over a ring without p-torsion, such as the formal group of a Weierstrass curve, the height-one locus is read off the invariant differential.

Main definitions

• FormalGroup.nsmulSeries: the multiplication-by-n series [n]_F(T).
• FormalGroup.nsmulHom: multiplication by n as an endomorphism of a commutative formal group.

Main results

• FormalGroup.nsmulSeries_succ: [n + 1]_F(T) = F([n]_F(T), T).
• FormalGroup.coeff_nsmulSeries_succ_of_eq_addInvX_add_X_pow_mul: if [n](T) agrees with the inverse below degree k, adding T retains the coefficient of their difference in degree k.
• FormalGroup.nsmulSeries_add: [m + n]_F(T) = F([m]_F(T), [n]_F(T)).
• FormalGroup.nsmulSeries_mul: [m n]_F(T) = [m]_F([n]_F(T)).
• FormalGroup.subst_nsmulSeries: [n]_F(x) = n • x for every power-series point x of F.
• FormalGroup.subst_toPowerSeries_nsmulSeries: for commutative F, [n]_F is an endomorphism, [n]_F(F(X, Y)) = F([n]_F(X), [n]_F(Y)).
• FormalGroup.nsmulSeries_𝔾ₐ and FormalGroup.nsmulSeries_𝔾ₘ: [n](T) = n T on the additive formal group law and [n](T) = (1 + T) ^ n - 1 on the multiplicative one.
• FormalGroup.subst_nsmulSeries_invariantDifferential_mul_derivative: P([n]_F(T)) · [n]_F'(T) = n · P(T).
• FormalGroup.coeff_one_nsmulSeries: [n]_F(T) = n T + ⋯.
• FormalGroup.natCast_eq_zero_of_nsmulSeries_eq_zero: if [n]_F = 0 then n = 0 in R.
• FormalGroup.natCast_eq_zero_of_two_le_order_nsmulSeries: if [n]_F has order at least two then n = 0 in R.
• FormalGroup.natCast_dvd_derivative_nsmulSeries: n divides the derivative of [n]_F.
• FormalGroup.natCast_dvd_coeff_nsmulSeries: n divides the coefficient of Tᵏ in [n]_F for k coprime to n.
• FormalGroup.exists_nsmulSeries_eq_of_prime: [p]_F(T) = p T u(T) + Tᵖ h(T) with u(0) = 1.
• FormalGroup.natCast_dvd_coeff_nsmulSeries_sub_coeff_invariantDifferential: if p is not a zero divisor, the coefficient of Tᵖ in [p]_F is congruent modulo p to the coefficient of Tᵖ⁻¹ in the invariant differential.
• TauCeti.FormalGroupHom.subst_nsmulSeries: a homomorphism f from F to G commutes with multiplication by n, f([n]_F(T)) = [n]_G(f(T)).
• TauCeti.FormalGroupHom.coeff_nsmulSeries_mul_coeff_one_pow_of_le_order: if f = u T + ⋯ and [n]_F, [n]_G both have order at least q, their coefficients a, b of T ^ q satisfy b u ^ q = u a.

References

• J. Silverman, The Arithmetic of Elliptic Curves, IV.2, IV.4 and IV.6.

noncomputable def FormalGroup.nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : PowerSeries R

Multiplication by n on a formal group law F: the power series [n]_F(T), which is n times the tautological point T in the monoid F.Point Unit of power-series points of F.

@[simp]

theorem FormalGroup.nsmulSeries_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.nsmulSeries 0 = 0

theorem FormalGroup.nsmulSeries_succ {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : F.nsmulSeries (n + 1) = MvPowerSeries.subst ![F.nsmulSeries n, PowerSeries.X] F.toPowerSeries

[n + 1]_F(T) = F([n]_F(T), T).

theorem FormalGroup.nsmulSeries_add {R : Type u_1} [CommRing R] (F : FormalGroup R) (m n : ℕ) : F.nsmulSeries (m + n) = MvPowerSeries.subst ![F.nsmulSeries m, F.nsmulSeries n] F.toPowerSeries

[m + n]_F(T) = F([m]_F(T), [n]_F(T)).

@[simp]

theorem FormalGroup.nsmulSeries_one {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.nsmulSeries 1 = PowerSeries.X

@[simp]

theorem FormalGroup.constantCoeff_nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : PowerSeries.constantCoeff (F.nsmulSeries n) = 0

[n]_F(T) has no constant term.

theorem FormalGroup.hasSubst_nsmulSeries_X {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : MvPowerSeries.HasSubst ![F.nsmulSeries n, PowerSeries.X]

[n]_F(T) and T can be substituted into a bivariate power series.

theorem FormalGroup.coeff_nsmulSeries_succ_of_eq_addInvX_add_X_pow_mul {R : Type u_1} [CommRing R] (F : FormalGroup R) {n k m : ℕ} {s : PowerSeries R} (h : F.nsmulSeries n = F.addInvX + PowerSeries.X ^ k * s) (hk : k ≠ 0) (hm : m ≤ k) : (PowerSeries.coeff m) (F.nsmulSeries (n + 1)) = if m = k then PowerSeries.constantCoeff s else 0

If [n]_F(T) = i(T) + Tᵏ s(T) with k ≠ 0, then [n + 1]_F vanishes below degree k and has coefficient s(0) in degree k. No commutativity hypothesis on F is needed.

theorem FormalGroup.nsmulSeries_mul {R : Type u_1} [CommRing R] (F : FormalGroup R) (m n : ℕ) : F.nsmulSeries (m * n) = PowerSeries.subst (F.nsmulSeries n) (F.nsmulSeries m)

[m n]_F(T) = [m]_F([n]_F(T)): multiplication by m n is the composite of multiplication by m and by n.

theorem FormalGroup.subst_nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) {σ : Type u_2} (x : F.Point σ) (n : ℕ) : PowerSeries.subst (↑x) (F.nsmulSeries n) = ↑(n • x)

Substituting a power-series point x of F into [n]_F(T) gives n • x.

theorem FormalGroup.subst_toPowerSeries_nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (n : ℕ) : PowerSeries.subst F.toPowerSeries (F.nsmulSeries n) = MvPowerSeries.subst (fun (i : Fin 2) => (PowerSeries.toMvPowerSeries i) (F.nsmulSeries n)) F.toPowerSeries

Multiplication by n is an endomorphism of a commutative formal group law F: [n]_F(F(X, Y)) = F([n]_F(X), [n]_F(Y)).

noncomputable def FormalGroup.nsmulHom {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (n : ℕ) : TauCeti.FormalGroupHom F F

Multiplication by n as an endomorphism of a commutative formal group law.

@[simp]

theorem FormalGroup.nsmulHom_toPowerSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (n : ℕ) : (F.nsmulHom n).toPowerSeries = F.nsmulSeries n

@[simp]

theorem FormalGroup.nsmulSeries_𝔾ₐ {R : Type u_1} [CommRing R] (n : ℕ) : 𝔾ₐ.nsmulSeries n = ↑n * PowerSeries.X

Multiplication by n on the additive formal group law X + Y is [n](T) = n T.

@[simp]

theorem FormalGroup.nsmulSeries_𝔾ₘ {R : Type u_1} [CommRing R] (n : ℕ) : 𝔾ₘ.nsmulSeries n = (1 + PowerSeries.X) ^ n - 1

Multiplication by n on the multiplicative formal group law X + Y + X Y is [n](T) = (1 + T) ^ n - 1.

theorem FormalGroup.subst_nsmulSeries_invariantDifferential_mul_derivative {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (n : ℕ) : PowerSeries.subst (F.nsmulSeries n) F.invariantDifferential * PowerSeries.derivative (F.nsmulSeries n) = ↑n * F.invariantDifferential

Multiplication by n multiplies the invariant differential by n (Silverman IV.4.3): P([n]_F(T)) · [n]_F'(T) = n · P(T) for a commutative formal group law F.

theorem FormalGroup.isUnit_subst_nsmulSeries_invariantDifferential {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : IsUnit (PowerSeries.subst (F.nsmulSeries n) F.invariantDifferential)

P([n]_F(T)) is a unit, its constant coefficient being 1.

@[simp]

theorem FormalGroup.coeff_one_nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℕ) : (PowerSeries.coeff 1) (F.nsmulSeries n) = ↑n

[n]_F(T) has linear coefficient n: [n]_F(T) = n T + ⋯.

theorem FormalGroup.natCast_eq_zero_of_nsmulSeries_eq_zero {R : Type u_1} [CommRing R] (F : FormalGroup R) {n : ℕ} (h : F.nsmulSeries n = 0) : ↑n = 0

If [n]_F = 0 then n = 0 in R, as n is the linear coefficient of [n]_F.

theorem FormalGroup.natCast_eq_zero_of_two_le_order_nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) {n : ℕ} (h : 2 ≤ (F.nsmulSeries n).order) : ↑n = 0

If [n]_F has order at least two then n = 0 in R, as n is the linear coefficient of [n]_F.

theorem FormalGroup.natCast_dvd_derivative_nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (n : ℕ) : ↑n ∣ PowerSeries.derivative (F.nsmulSeries n)

The derivative of [n]_F is divisible by n, for a commutative formal group law F.

theorem FormalGroup.natCast_dvd_coeff_nsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] {n k : ℕ} (hk : k.Coprime n) : ↑n ∣ (PowerSeries.coeff k) (F.nsmulSeries n)

n divides the coefficients of [n]_F in degrees coprime to n, for a commutative formal group law F.

theorem FormalGroup.exists_nsmulSeries_eq_of_prime {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] {p : ℕ} (hp : Nat.Prime p) : ∃ (u : PowerSeries R) (h : PowerSeries R), PowerSeries.constantCoeff u = 1 ∧ F.nsmulSeries p = ↑p * PowerSeries.X * u + PowerSeries.X ^ p * h

The shape of multiplication by a prime (compare Silverman IV.4.4): for a commutative formal group law F and a prime p, [p]_F(T) = p T u(T) + Tᵖ h(T) for power series u and h with u(0) = 1.

theorem FormalGroup.natCast_dvd_coeff_nsmulSeries_sub_coeff_invariantDifferential {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] {p : ℕ} (hp : Nat.Prime p) (hpR : IsLeftRegular ↑p) : ↑p ∣ (PowerSeries.coeff p) (F.nsmulSeries p) - (PowerSeries.coeff (p - 1)) F.invariantDifferential

The coefficient of Tᵖ in [p]_F modulo p: for a commutative formal group law F over a ring in which the prime p is not a zero divisor, the coefficient of Tᵖ in [p]_F(T) is congruent modulo p to the coefficient of Tᵖ⁻¹ in the invariant differential P(T) dT.

theorem TauCeti.FormalGroupHom.subst_nsmulSeries {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (n : ℕ) : PowerSeries.subst (F.nsmulSeries n) f.toPowerSeries = PowerSeries.subst f.toPowerSeries (G.nsmulSeries n)

Homomorphisms commute with multiplication by n: if f is a homomorphism of formal group laws from F to G, then f([n]_F(T)) = [n]_G(f(T)). Neither law needs to be commutative.

theorem TauCeti.FormalGroupHom.coeff_nsmulSeries_mul_coeff_one_pow_of_le_order {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) (n : ℕ) {q : ℕ} (hF : ↑q ≤ (F.nsmulSeries n).order) (hG : ↑q ≤ (G.nsmulSeries n).order) : (PowerSeries.coeff q) (G.nsmulSeries n) * (PowerSeries.coeff 1) f.toPowerSeries ^ q = (PowerSeries.coeff 1) f.toPowerSeries * (PowerSeries.coeff q) (F.nsmulSeries n)

A homomorphism relates the leading coefficients of multiplication by n. If f is a homomorphism of formal group laws from F to G with linear coefficient u, and [n]_F and [n]_G both have order at least q, then their coefficients a and b of T ^ q satisfy b u ^ q = u a.