Integer multiplication on formal groups

FormalGroup.zsmulSeries extends the native natural-number multiplication series to all integers, using the group of substitutable power-series points. Negative indices use the formal inverse, not coefficientwise negation. Substitution into a point with nilpotent constant term computes integer multiplication on that point.

The addition and composition identities hold without commutativity of the formal group. For a commutative formal group, integer multiplication is bundled as an endomorphism. Multiplication series commute with coefficient base change and with every homomorphism; in particular an isomorphism identifies them by conjugation of coordinates, so isomorphic laws are killed by the same integers.

References

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

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

Multiplication by an integer on a formal group, evaluated at its tautological point.

@[simp]

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

Integer multiplication extends the existing natural-number multiplication series.

@[simp]

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

@[simp]

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

theorem FormalGroup.zsmulSeries_neg {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℤ) : F.zsmulSeries (-n) = PowerSeries.subst (F.zsmulSeries n) F.addInvX

Negating an index composes with the formal inverse.

@[simp]

theorem FormalGroup.zsmulSeries_neg_one {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.zsmulSeries (-1) = F.addInvX

Multiplication by minus one is the formal inverse.

@[simp]

theorem FormalGroup.constantCoeff_zsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℤ) : PowerSeries.constantCoeff (F.zsmulSeries n) = 0

Every integer multiplication series has zero constant coefficient.

theorem FormalGroup.hasSubst_zsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℤ) : PowerSeries.HasSubst (F.zsmulSeries n)

Integer multiplication series admit formal substitution.

@[simp]

theorem FormalGroup.coeff_one_zsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℤ) : (PowerSeries.coeff 1) (F.zsmulSeries n) = ↑n

Integer multiplication has linear coefficient equal to its index.

theorem FormalGroup.subst_zsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) {σ : Type u_3} (x : F.Point σ) (n : ℤ) : PowerSeries.subst (↑x) (F.zsmulSeries n) = ↑(n • x)

Evaluating the integer multiplication series at a substitutable point computes its integer multiple, including points with nonzero nilpotent constant coefficient.

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

The series of a sum of indices is the formal-group sum of their series.

theorem FormalGroup.zsmulSeries_mul {R : Type u_1} [CommRing R] (F : FormalGroup R) (m n : ℤ) : F.zsmulSeries (m * n) = PowerSeries.subst (F.zsmulSeries n) (F.zsmulSeries m)

The series of a product of indices is the composite of their series.

theorem FormalGroup.subst_addInvX_zsmulSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) (n : ℤ) : PowerSeries.subst F.addInvX (F.zsmulSeries n) = F.zsmulSeries (-n)

The formal inverse commutes with every integer multiplication series.

@[simp]

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

Integer multiplication commutes with base change of the coefficient ring.

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

Integer multiplication is an endomorphism when the formal group is commutative.

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

Integer multiplication as a bundled endomorphism of a commutative formal group.

@[simp]

theorem FormalGroup.zsmulHom_toPowerSeries {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] (n : ℤ) : (F.zsmulHom n).toPowerSeries = F.zsmulSeries n

@[simp]

theorem FormalGroup.map_zsmulHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (F : FormalGroup R) [F.IsComm] (f : R →+* S) (n : ℤ) : (F.zsmulHom n).map f = (F.map f).zsmulHom n

Integer multiplication commutes with base change as a bundled endomorphism.

@[simp]

theorem FormalGroup.zsmulHom_applyPoint {R : Type u_1} [CommRing R] (F : FormalGroup R) [F.IsComm] {σ : Type u_3} (x : F.Point σ) (n : ℤ) : (F.zsmulHom n).applyPoint x = n • x

The bundled integer endomorphism acts by integer multiplication on points.

@[simp]

theorem FormalGroup.zsmulSeries_𝔾ₐ {R : Type u_1} [CommRing R] (n : ℤ) : 𝔾ₐ.zsmulSeries n = ↑n * PowerSeries.X

On the additive formal group, integer multiplication is ordinary scalar multiplication.

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

Every formal-group homomorphism commutes with integer multiplication, without any commutativity assumption on its source or target.

theorem TauCeti.FormalGroupIso.zsmulSeries_eq_subst {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) (n : ℤ) : G.zsmulSeries n = PowerSeries.subst f.invHom.toPowerSeries (PowerSeries.subst (F.zsmulSeries n) f.toHom.toPowerSeries)

An isomorphism transports integer multiplication by conjugation with its forward and inverse coordinates.

theorem TauCeti.FormalGroupIso.zsmulSeries_eq_zero_iff {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) (n : ℤ) : F.zsmulSeries n = 0 ↔ G.zsmulSeries n = 0

Isomorphic formal group laws are killed by the same integers: [n]_F = 0 exactly when [n]_G = 0.

theorem TauCeti.FormalGroupIso.nsmulSeries_eq_zero_iff {R : Type u_1} [CommRing R] {F G : FormalGroup R} (f : FormalGroupIso F G) (n : ℕ) : F.nsmulSeries n = 0 ↔ G.nsmulSeries n = 0

Isomorphic formal group laws are killed by the same natural numbers: [n]_F = 0 exactly when [n]_G = 0.