The invariant differential and the logarithm of a formal group law

Let F(X, Y) be a one-dimensional formal group law over a commutative ring R. Its normalised invariant differential is ω = P(T) dT with P(T) = F_X(0, T)⁻¹, where F_X is the partial derivative of F in its first variable; the constant coefficient of F_X(0, T) is 1, so the inverse exists over any R. Differentiating the associativity law F(F(U, T), S) = F(U, F(T, S)) in U and setting U = 0 shows that ω is invariant under translation: P(F(T, S)) · F_X(T, S) = P(T).

When R is an algebra over ℚ, the formal logarithm log_F(T) = ∫ P(T) dT is the power series with zero constant coefficient and derivative P. Invariance of ω makes log_F a homomorphism from F to the additive formal group law:

log_F(F(X, Y)) = log_F(X) + log_F(Y).

The logarithm has linear coefficient 1, so it has a compositional inverse, the formal exponential exp_F, and F(X, Y) = exp_F(log_F(X) + log_F(Y)): over a ℚ-algebra every formal group law is strictly isomorphic to the additive one. Up to a scalar, log_F is the only power series that is additive along F.

For the additive formal group law X + Y the invariant differential is dT and both log and exp are T. For the multiplicative formal group law X + Y + XY the invariant differential is dT / (1 + T), and log and exp are Mathlib's PowerSeries.log, the series of log(1 + T), and e^T - 1.

Main definitions

• FormalGroup.invariantDifferential: the coefficient P(T) of the normalised invariant differential ω = P(T) dT of F.
• FormalGroup.invariantDerivation: the dual derivation F_X(0, T) d/dT.
• FormalGroup.log: the formal logarithm of F, over a ℚ-algebra.
• FormalGroup.exp: the formal exponential of F, the compositional inverse of FormalGroup.log.

Main results

• TauCeti.FormalGroupHom.derivative_eq_zero_iff: a homomorphism has zero derivative exactly when its linear coefficient vanishes, over any commutative coefficient ring.

• FormalGroup.subst_invariantDifferential_mul_pderiv: the invariant differential is invariant, P(F(X, Y)) · F_X(X, Y) = P(X).

• FormalGroup.subst_invariantDifferential_mul_pderiv_one: for commutative F, the same in the second variable, P(F(X, Y)) · F_Y(X, Y) = P(Y).

• FormalGroup.invariantDifferential_mul_invariantDerivation: multiplying the invariant derivative by P(T) recovers the ordinary derivative.

• FormalGroup.invariantDerivation_log: the invariant derivative of log_F is 1.

• FormalGroup.map_invariantDerivation: the invariant derivation commutes with coefficient maps.

• FormalGroup.map_invariantDifferential: the invariant differential commutes with coefficient maps.

• FormalGroup.natCast_mul_coeff_log_mem_range: each logarithm coefficient becomes integral after multiplication by its degree.

• FormalGroup.subst_toPowerSeries_eq_add_of_derivative_eq: over a ring without additive torsion, a power series with no constant term whose derivative is P is additive along F.

• FormalGroup.subst_toPowerSeries_log: log_F(F(X, Y)) = log_F(X) + log_F(Y).

• FormalGroup.subst_subst_toPowerSeries_log: the same at any pair of power series that can be substituted.

• FormalGroup.subst_toPowerSeries_eq_add_iff: a power series g satisfies g(F(X, Y)) = g(X) + g(Y) exactly when it is a scalar multiple of log_F.

• FormalGroup.subst_exp_log and FormalGroup.subst_log_exp: log_F and exp_F are inverse.

• FormalGroup.eq_exp_of_subst_log_eq_X: exp_F is the only right inverse of log_F.

• FormalGroup.map_log and FormalGroup.map_exp: the logarithm and exponential commute with base change along homomorphisms of ℚ-algebras.

• FormalGroup.derivative_exp: exp_F'(T) = F_X(0, exp_F(T)).

• FormalGroup.toPowerSeries_eq_subst_exp: F(X, Y) = exp_F(log_F(X) + log_F(Y)).

• FormalGroup.invariantDifferential_injective: over a ℚ-algebra, a formal group law is determined by its invariant differential.

• FormalGroup.logIso: the strict isomorphism from F to the additive formal group, with forward homomorphism FormalGroup.logHom and inverse FormalGroup.expHom.

• FormalGroup.eq_logIso: this is the unique strict isomorphism to the additive formal group.

• FormalGroup.invariantDifferential_𝔾ₐ, FormalGroup.log_𝔾ₐ, FormalGroup.exp_𝔾ₐ: the additive formal group law has invariant differential dT, and logarithm and exponential T.

• FormalGroup.invariantDifferential_𝔾ₘ, FormalGroup.log_𝔾ₘ, FormalGroup.exp_𝔾ₘ: the multiplicative formal group law has invariant differential dT / (1 + T), logarithm log(1 + T) and exponential e^T - 1.

References

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

The invariant differential

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

The invariant differential of a formal group law F, recorded by its coefficient: the power series P(T) = F_X(0, T)⁻¹, so that ω = P(T) dT is the normalised invariant differential of F (Silverman IV.4.2). Here F_X is the partial derivative of F in its first variable.

@[simp]

theorem FormalGroup.constantCoeff_invariantDifferential {R : Type u_1} [CommRing R] (F : FormalGroup R) : PowerSeries.constantCoeff F.invariantDifferential = 1

The invariant differential is normalised: P(0) = 1.

theorem FormalGroup.invariantDifferential_mul_subst_pderiv {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.invariantDifferential * MvPowerSeries.subst ![0, PowerSeries.X] ((MvPowerSeries.pderiv 0) F.toPowerSeries) = 1

P(T) · F_X(0, T) = 1: the defining property of the invariant differential.

noncomputable def FormalGroup.invariantDerivation {R : Type u_1} [CommRing R] (F : FormalGroup R) : Derivation R (PowerSeries R) (PowerSeries R)

The invariant derivation F_X(0, T) d/dT of a formal group law. Its dual invariant differential is dT / F_X(0, T).

theorem FormalGroup.invariantDerivation_apply {R : Type u_1} [CommRing R] (F : FormalGroup R) (g : PowerSeries R) : F.invariantDerivation g = MvPowerSeries.subst ![0, PowerSeries.X] ((MvPowerSeries.pderiv 0) F.toPowerSeries) * PowerSeries.derivative g

@[simp]

theorem FormalGroup.map_invariantDerivation {R : Type u_1} [CommRing R] (F : FormalGroup R) {S : Type u_2} [CommRing S] (f : R →+* S) (g : PowerSeries R) : (PowerSeries.map f) (F.invariantDerivation g) = (F.map f).invariantDerivation ((PowerSeries.map f) g)

The invariant derivation commutes with change of coefficients.

@[simp]

theorem FormalGroup.map_invariantDifferential {R : Type u_1} [CommRing R] (F : FormalGroup R) {S : Type u_2} [CommRing S] (f : R →+* S) : (PowerSeries.map f) F.invariantDifferential = (F.map f).invariantDifferential

The invariant differential commutes with change of coefficients.

theorem FormalGroup.invariantDifferential_mul_invariantDerivation {R : Type u_1} [CommRing R] (F : FormalGroup R) (g : PowerSeries R) : F.invariantDifferential * F.invariantDerivation g = PowerSeries.derivative g

Multiplying the invariant derivative by the invariant differential's coefficient recovers the ordinary derivative.

theorem FormalGroup.subst_invariantDifferential_mul_pderiv {R : Type u_1} [CommRing R] (F : FormalGroup R) : PowerSeries.subst F.toPowerSeries F.invariantDifferential * (MvPowerSeries.pderiv 0) F.toPowerSeries = PowerSeries.subst (MvPowerSeries.X 0) F.invariantDifferential

The invariant differential is invariant (Silverman IV.4.2): ω(F(X, Y)) = ω(X), that is P(F(X, Y)) · F_X(X, Y) = P(X).

theorem FormalGroup.subst_invariantDifferential_mul_pderiv_one {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] : PowerSeries.subst F.toPowerSeries F.invariantDifferential * (MvPowerSeries.pderiv 1) F.toPowerSeries = PowerSeries.subst (MvPowerSeries.X 1) F.invariantDifferential

The invariant differential is invariant in the second variable for a commutative formal group law: P(F(X, Y)) · F_Y(X, Y) = P(Y), where F_Y is the partial derivative of F in its second variable.

The additive and multiplicative formal group laws

@[simp]

theorem FormalGroup.invariantDifferential_𝔾ₐ {R : Type u_1} [CommRing R] : 𝔾ₐ.invariantDifferential = 1

The invariant differential of the additive formal group law X + Y is dT.

@[simp]

theorem FormalGroup.invariantDifferential_𝔾ₘ {R : Type u_1} [CommRing R] : 𝔾ₘ.invariantDifferential = PowerSeries.mk fun (n : ℕ) => (-1) ^ n

The invariant differential of the multiplicative formal group law X + Y + XY is dT / (1 + T) = (1 - T + T² - ⋯) dT.

Antiderivatives of the invariant differential

theorem FormalGroup.subst_toPowerSeries_eq_add_of_derivative_eq {R : Type u_1} [CommRing R] (F : FormalGroup R) [HasUniqueDiv R] {g : PowerSeries R} (hg₀ : PowerSeries.constantCoeff g = 0) (hg : PowerSeries.derivative g = F.invariantDifferential) : PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g

An antiderivative of the invariant differential is additive along F: over a ring without additive torsion, a power series g with no constant term and g' = P satisfies g(F(X, Y)) = g(X) + g(Y). Over a ℚ-algebra, g is the logarithm (FormalGroup.log); the hypotheses can also hold over a ring not containing ℚ, for instance for the rescaled logarithm FormalGroup.rescaleLog.

The logarithm

noncomputable def FormalGroup.log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries R

The formal logarithm log_F(T) = ∫ P(T) dT of a formal group law F over a ℚ-algebra: the power series with zero constant coefficient whose derivative is the invariant differential (Silverman IV.5).

theorem FormalGroup.coeff_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] (n : ℕ) : (PowerSeries.coeff n) F.log = (↑n)⁻¹ • (PowerSeries.coeff (n - 1)) F.invariantDifferential

The coefficients of the logarithm: log_F(T) = ∑_{n ≥ 1} (pₙ₋₁ / n) Tⁿ for P(T) = ∑ₙ pₙ Tⁿ. At n = 0 the formula reads 0, since 0⁻¹ = 0 in ℚ.

@[simp]

theorem FormalGroup.constantCoeff_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries.constantCoeff F.log = 0

The logarithm has no constant term.

@[simp]

theorem FormalGroup.coeff_one_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : (PowerSeries.coeff 1) F.log = 1

The logarithm has linear coefficient 1: log_F(T) = T + ⋯.

@[simp]

theorem FormalGroup.derivative_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries.derivative F.log = F.invariantDifferential

The derivative of the logarithm is the invariant differential.

theorem FormalGroup.natCast_mul_coeff_log_mem_range {R : Type u_1} [CommRing R] (F : FormalGroup R) {S : Type u_2} [CommRing S] [Algebra ℚ S] (f : R →+* S) (n : ℕ) : ↑n * (PowerSeries.coeff n) (F.map f).log ∈ Set.range ⇑f

Every logarithm coefficient becomes integral after multiplication by its degree.

@[simp]

theorem FormalGroup.invariantDerivation_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : F.invariantDerivation F.log = 1

The invariant derivative of the formal logarithm is one.

theorem FormalGroup.subst_toPowerSeries_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries.subst F.toPowerSeries F.log = PowerSeries.subst (MvPowerSeries.X 0) F.log + PowerSeries.subst (MvPowerSeries.X 1) F.log

The logarithm is additive along F (Silverman IV.5.2): log_F(F(X, Y)) = log_F(X) + log_F(Y).

theorem FormalGroup.subst_subst_toPowerSeries_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] {σ : Type u_2} {f₀ f₁ : MvPowerSeries σ R} (h₀ : PowerSeries.HasSubst f₀) (h₁ : PowerSeries.HasSubst f₁) : PowerSeries.subst (MvPowerSeries.subst ![f₀, f₁] F.toPowerSeries) F.log = PowerSeries.subst f₀ F.log + PowerSeries.subst f₁ F.log

The logarithm is additive along F at any pair of power series f₀, f₁ that can be substituted: log_F(F(f₀, f₁)) = log_F(f₀) + log_F(f₁).

theorem FormalGroup.subst_toPowerSeries_eq_add_iff {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] {g : PowerSeries R} : PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g ↔ ∃ (c : R), g = c • F.log

The additive power series along F are the multiples of the logarithm: a power series g satisfies g(F(X, Y)) = g(X) + g(Y) exactly when g = c • log_F for some c : R.

noncomputable def FormalGroup.exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries R

The formal exponential exp_F of a formal group law F over a ℚ-algebra: the compositional inverse of the logarithm, which exists since log_F(T) = T + ⋯.

@[simp]

theorem FormalGroup.constantCoeff_exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries.constantCoeff F.exp = 0

The exponential has no constant term.

@[simp]

theorem FormalGroup.coeff_one_exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : (PowerSeries.coeff 1) F.exp = 1

The exponential has linear coefficient 1: exp_F(T) = T + ⋯.

@[simp]

theorem FormalGroup.subst_exp_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries.subst F.exp F.log = PowerSeries.X

log_F(exp_F(T)) = T.

@[simp]

theorem FormalGroup.subst_log_exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries.subst F.log F.exp = PowerSeries.X

exp_F(log_F(T)) = T.

@[simp]

theorem FormalGroup.subst_subst_log_exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] {σ : Type u_2} {a : MvPowerSeries σ R} (ha : PowerSeries.HasSubst a) : PowerSeries.subst (PowerSeries.subst a F.log) F.exp = a

exp_F(log_F(a)) = a for every power series a that can be substituted.

theorem FormalGroup.eq_exp_of_subst_log_eq_X {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] {Q : PowerSeries R} (hQ : PowerSeries.HasSubst Q) (h : PowerSeries.subst Q F.log = PowerSeries.X) : Q = F.exp

The exponential is the only right inverse of the logarithm: if log_F(Q(T)) = T then Q = exp_F.

@[simp]

theorem FormalGroup.map_log {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] {S : Type u_2} [CommRing S] [Algebra ℚ S] (f : R →+* S) : (PowerSeries.map f) F.log = (F.map f).log

The logarithm commutes with base change: applying a ring homomorphism f : R →+* S of ℚ-algebras to the coefficients of log_F gives the logarithm of F.map f.

@[simp]

theorem FormalGroup.map_exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] {S : Type u_2} [CommRing S] [Algebra ℚ S] (f : R →+* S) : (PowerSeries.map f) F.exp = (F.map f).exp

The exponential commutes with base change: applying a ring homomorphism f : R →+* S of ℚ-algebras to the coefficients of exp_F gives the exponential of F.map f.

theorem FormalGroup.derivative_exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : PowerSeries.derivative F.exp = PowerSeries.subst F.exp (MvPowerSeries.subst ![0, PowerSeries.X] ((MvPowerSeries.pderiv 0) F.toPowerSeries))

The formal exponential solves the invariant differential equation exp_F'(T) = F_X(0, exp_F(T)).

theorem FormalGroup.toPowerSeries_eq_subst_exp {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : F.toPowerSeries = PowerSeries.subst (PowerSeries.subst (MvPowerSeries.X 0) F.log + PowerSeries.subst (MvPowerSeries.X 1) F.log) F.exp

A formal group law over a ℚ-algebra is strictly isomorphic to the additive one (Silverman IV.5.2): F(X, Y) = exp_F(log_F(X) + log_F(Y)).

theorem FormalGroup.invariantDifferential_injective {R : Type u_1} [CommRing R] [Algebra ℚ R] : Function.Injective invariantDifferential

A formal group law over a ℚ-algebra is determined by its invariant differential: the invariant differential determines log_F, hence exp_F, and F(X, Y) = exp_F(log_F(X) + log_F(Y)).

noncomputable def FormalGroup.logHom {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : TauCeti.FormalGroupHom F 𝔾ₐ

The logarithm, bundled as a homomorphism to the additive formal group.

@[simp]

theorem FormalGroup.logHom_toPowerSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : F.logHom.toPowerSeries = F.log

noncomputable def FormalGroup.logIso {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : TauCeti.FormalGroupIso F 𝔾ₐ

The normalized logarithm is a strict isomorphism from F to the additive formal group, with the formal exponential as its inverse.

noncomputable def FormalGroup.expHom {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : TauCeti.FormalGroupHom 𝔾ₐ F

The exponential, bundled as a homomorphism from the additive formal group.

@[simp]

theorem FormalGroup.expHom_toPowerSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : F.expHom.toPowerSeries = F.exp

@[simp]

theorem FormalGroup.logIso_toHom {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : F.logIso.toHom = F.logHom

@[simp]

theorem FormalGroup.logIso_invHom {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : F.logIso.invHom = F.expHom

instance FormalGroup.instIsStrictLogIso {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] : F.logIso.IsStrict

theorem TauCeti.FormalGroupHom.toPowerSeries_eq_coeff_one_smul_log {R : Type u_1} [CommRing R] {F : FormalGroup R} [Algebra ℚ R] (f : FormalGroupHom F FormalGroup.𝔾ₐ) : f.toPowerSeries = (PowerSeries.coeff 1) f.toPowerSeries • F.log

A homomorphism to the additive group is its linear coefficient times the logarithm: f(X) = f'(0) · log_F(X).

theorem FormalGroup.eq_logHom_of_coeff_one {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] (f : TauCeti.FormalGroupHom F 𝔾ₐ) (hf : (PowerSeries.coeff 1) f.toPowerSeries = 1) : f = F.logHom

A homomorphism to the additive group with linear coefficient one is the logarithm.

theorem FormalGroup.eq_logIso {R : Type u_1} [CommRing R] (F : FormalGroup R) [Algebra ℚ R] (f : TauCeti.FormalGroupIso F 𝔾ₐ) [f.IsStrict] : f = F.logIso

The logarithm is the unique strict isomorphism from F to the additive formal group.

The logarithms of the additive and multiplicative formal group laws

@[simp]

theorem FormalGroup.log_𝔾ₐ {R : Type u_1} [CommRing R] [Algebra ℚ R] : 𝔾ₐ.log = PowerSeries.X

The logarithm of the additive formal group law is log_{𝔾ₐ}(T) = T.

@[simp]

theorem FormalGroup.exp_𝔾ₐ {R : Type u_1} [CommRing R] [Algebra ℚ R] : 𝔾ₐ.exp = PowerSeries.X

The exponential of the additive formal group law is exp_{𝔾ₐ}(T) = T.

@[simp]

theorem FormalGroup.log_𝔾ₘ {R : Type u_1} [CommRing R] [Algebra ℚ R] : 𝔾ₘ.log = PowerSeries.log R

The logarithm of the multiplicative formal group law is the logarithm series log_{𝔾ₘ}(T) = log(1 + T) = T - T² / 2 + T³ / 3 - ⋯.

@[simp]

theorem FormalGroup.exp_𝔾ₘ {R : Type u_1} [CommRing R] [Algebra ℚ R] : 𝔾ₘ.exp = PowerSeries.exp R - 1

The exponential of the multiplicative formal group law is exp_{𝔾ₘ}(T) = e^T - 1.

theorem TauCeti.FormalGroupHom.derivative_eq_zero_iff {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupHom F G) : PowerSeries.derivative f.toPowerSeries = 0 ↔ (PowerSeries.coeff 1) f.toPowerSeries = 0

A homomorphism of formal groups has zero derivative exactly when its tangent map is zero. This holds over arbitrary coefficient rings, without commutativity of the formal groups.