Base change of formal group laws

Mathlib constructs the base change F.map f of a formal group law by applying f to every coefficient. This file supplies its basic functorial API: identity and composition laws, preservation and reflection of commutativity, descent along injective coefficient maps, and compatibility with the additive and multiplicative formal group laws.

Main results

• FormalGroup.map_id and FormalGroup.map_comp: base change is functorial.
• FormalGroup.map_injective: base change along an injective homomorphism is injective.
• FormalGroup.isComm_map and FormalGroup.isComm_of_map: preservation and reflection of commutativity.
• FormalGroup.ofMap: descend a law whose coefficients lift along an injective map.
• FormalGroup.map_𝔾ₐ and FormalGroup.map_𝔾ₘ: the standard laws are stable under base change.
• FormalGroup.subst_map_toPowerSeries_map: a power series additive along F stays additive along F after base change.

theorem FormalGroup.map_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) : Function.Injective fun (F : FormalGroup R) => F.map f

Base change along an injective coefficient homomorphism is injective.

@[simp]

theorem FormalGroup.map_id {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.map (RingHom.id R) = F

Base-changing a formal group law along the identity homomorphism changes nothing.

@[simp]

theorem FormalGroup.map_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] (F : FormalGroup R) (f : R →+* S) (g : S →+* T) : (F.map f).map g = F.map (g.comp f)

Successive base changes of a formal group law agree with base change along the composite.

instance FormalGroup.isComm_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (F : FormalGroup R) [F.IsComm] (f : R →+* S) : (F.map f).IsComm

A base change of a commutative formal group law is commutative.

theorem FormalGroup.isComm_of_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : FormalGroup R} {f : R →+* S} (hf : Function.Injective ⇑f) [(F.map f).IsComm] : F.IsComm

An injective coefficient map reflects commutativity.

def FormalGroup.ofMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Injective ⇑f) (g : MvPowerSeries (Fin 2) R) (F : FormalGroup S) (hg : (MvPowerSeries.map f) g = F.toPowerSeries) : FormalGroup R

Descend a formal group law along an injective coefficient map, given a power series whose coefficient extension is that law.

@[simp]

theorem FormalGroup.ofMap_toPowerSeries {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Injective ⇑f) (g : MvPowerSeries (Fin 2) R) (F : FormalGroup S) (hg : (MvPowerSeries.map f) g = F.toPowerSeries) : (ofMap f hf g F hg).toPowerSeries = g

The underlying series of the descended formal group is the given series.

@[simp]

theorem FormalGroup.map_ofMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Injective ⇑f) (g : MvPowerSeries (Fin 2) R) (F : FormalGroup S) (hg : (MvPowerSeries.map f) g = F.toPowerSeries) : (ofMap f hf g F hg).map f = F

Extending coefficients of the descended formal group recovers the original law.

@[simp]

theorem FormalGroup.map_𝔾ₐ {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) : 𝔾ₐ.map f = 𝔾ₐ

The additive formal group law is unchanged by base change.

@[simp]

theorem FormalGroup.map_𝔾ₘ {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) : 𝔾ₘ.map f = 𝔾ₘ

The multiplicative formal group law is unchanged by base change.

theorem FormalGroup.subst_map_toPowerSeries_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (F : FormalGroup R) (f : R →+* S) {g : PowerSeries R} (hg : PowerSeries.subst F.toPowerSeries g = PowerSeries.subst (MvPowerSeries.X 0) g + PowerSeries.subst (MvPowerSeries.X 1) g) : PowerSeries.subst (F.map f).toPowerSeries ((PowerSeries.map f) g) = PowerSeries.subst (MvPowerSeries.X 0) ((PowerSeries.map f) g) + PowerSeries.subst (MvPowerSeries.X 1) ((PowerSeries.map f) g)

A power series additive along F stays additive along F after base change.