Base change for multiplication series of formal groups

The multiplication series [n]_F of a formal group law is natural in its coefficient ring: applying a ring homomorphism to its coefficients gives the multiplication series of the base-changed formal group.

Main results

• FormalGroup.map_nsmulSeries: [n]_F commutes with base change.
• FormalGroup.coeff_nsmulSeries_map: coefficientwise form of the base-change identity.
• FormalGroup.map_nsmulHom: the bundled endomorphism [n] commutes with base change.

@[simp]

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

Multiplication by n commutes with base change of the coefficient ring.

@[simp]

theorem FormalGroup.coeff_nsmulSeries_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (F : FormalGroup R) (f : R →+* S) (n k : ℕ) : (PowerSeries.coeff k) ((F.map f).nsmulSeries n) = f ((PowerSeries.coeff k) (F.nsmulSeries n))

The coefficients of multiplication series are preserved by base change.

@[simp]

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

Multiplication by n commutes with base change as a bundled endomorphism.