Formal group laws over commutative ring

Let R be a commutative ring, a one dimensional formal group law is a formal power series F(X,Y) ∈ R⟦X,Y⟧ such that

• F(X,Y) = X + Y + higher order terms.
• F(F(X,Y),Z) = F(X,F(Y,Z)).

Under this definition, we can prove that F(X,0) = X and F(0,X) = X. Moreover, there is a unique power series i(X) such that F(X, i(X)) = 0, which is considered to be the inverse of the formal group law F(X,Y).

Main definitions/lemmas

• FormalGroup R: definition of one dimensional formal group law over commutative ring R.

• Properties: F(X,0) = X and F(0,X) = X.

• Additive formal group laws 𝔾ₐ and multiplicative formal group laws 𝔾ₘ.

• F.Point σ taking values in the formal power series ring MvPowerSeries σ R with the property that constant coefficient is nilpotent. We have the following typeclass:

• AddMonoid (F.Point σ) when F is a commutative formal group law
• AddCommMonoid (F.Point σ)

References

• Hazewinkel, Michiel. Formal Groups and Applications

structure FormalGroup (R : Type u_1) [CommRing R] : Type u_1

A structure for a 1-dimensional formal group law over R.

• toPowerSeries : MvPowerSeries (Fin 2) R

  The underlying power series $F(X, Y)$ in two variables.

• zero_constantCoeff : MvPowerSeries.constantCoeff self.toPowerSeries = 0

  The constant coefficient of the formal group law is zero.

• lin_coeff_X : (MvPowerSeries.coeff (Finsupp.single 0 1)) self.toPowerSeries = 1

  The coefficient of $X$ in $F(X, Y)$ is 1.

• lin_coeff_Y : (MvPowerSeries.coeff (Finsupp.single 1 1)) self.toPowerSeries = 1

  The coefficient of $Y$ in $F(X, Y)$ is 1.

• assoc : MvPowerSeries.subst ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] self.toPowerSeries, MvPowerSeries.X 2] self.toPowerSeries = MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] self.toPowerSeries] self.toPowerSeries

  Associativity condition: $F(F(X, Y), Z) = F(X, F(Y, Z))$.

theorem FormalGroup.ext {R : Type u_1} {inst✝ : CommRing R} {x y : FormalGroup R} (toPowerSeries : x.toPowerSeries = y.toPowerSeries) : x = y

theorem FormalGroup.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : FormalGroup R} : x = y ↔ x.toPowerSeries = y.toPowerSeries

@[implicit_reducible]

instance FormalGroup.coeToPowerSeries {R : Type u_1} [CommRing R] : Coe (FormalGroup R) (MvPowerSeries (Fin 2) R)

The natural inclusion from formal group law into formal power series.

Equations

• FormalGroup.coeToPowerSeries = { coe := FormalGroup.toPowerSeries }

class FormalGroup.IsComm {R : Type u_1} [CommRing R] (F : FormalGroup R) : Prop

Given a formal group F, F.IsComm is a proposition that $F(X,Y) = F(Y,X)$.

• comm : F.toPowerSeries = MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 0] F.toPowerSeries

theorem FormalGroup.assoc' {R : Type u_1} [CommRing R] {σ : Type u_3} (F : FormalGroup R) {f₀ f₁ f₂ : MvPowerSeries σ R} (h₀ : PowerSeries.HasSubst f₀) (h₁ : PowerSeries.HasSubst f₁) (h₂ : PowerSeries.HasSubst f₂) : MvPowerSeries.subst ![MvPowerSeries.subst ![f₀, f₁] F.toPowerSeries, f₂] F.toPowerSeries = MvPowerSeries.subst ![f₀, MvPowerSeries.subst ![f₁, f₂] F.toPowerSeries] F.toPowerSeries

theorem FormalGroup.comm' {R : Type u_1} [CommRing R] {σ : Type u_3} (F : FormalGroup R) [F.IsComm] {f g : MvPowerSeries σ R} (hf : PowerSeries.HasSubst f) (hg : PowerSeries.HasSubst g) : MvPowerSeries.subst ![f, g] F.toPowerSeries = MvPowerSeries.subst ![g, f] F.toPowerSeries

def FormalGroup.Point {R : Type u_1} [CommRing R] (F : FormalGroup R) (σ : Type u_6) : Type (max 0 u_1 u_6)

F.Point σ represents the mathematical space of points of a formal group $F$ taking values in the formal power series ring MvPowerSeries σ R with the property that constant coefficient is nilpotent.

TODO: Mathematically, a 1-dimensional formal group law $F$ over a ring $R$ defines a group structure on the elements of a complete local $R$-algebra (specifically, its maximal ideal) via the substitution operation $x +_F y = F(x, y)$.

Equations

• F.Point σ = { f : MvPowerSeries σ R // PowerSeries.HasSubst f }

@[implicit_reducible]

noncomputable instance FormalGroup.instAddPoint {R : Type u_1} [CommRing R] {σ : Type u_5} (F : FormalGroup R) : Add (F.Point σ)

Equations

• F.instAddPoint = { add := fun (x y : F.Point σ) => ⟨MvPowerSeries.subst ![↑x, ↑y] F.toPowerSeries, ⋯⟩ }

@[simp]

theorem FormalGroup.add_apply {R : Type u_1} [CommRing R] {σ : Type u_5} (F : FormalGroup R) {x y : F.Point σ} : ↑(x + y) = MvPowerSeries.subst ![↑x, ↑y] F.toPowerSeries

@[implicit_reducible]

instance FormalGroup.instZeroPoint {R : Type u_1} [CommRing R] {σ : Type u_5} (F : FormalGroup R) : Zero (F.Point σ)

Equations

• F.instZeroPoint = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem FormalGroup.zero_apply {R : Type u_1} [CommRing R] {σ : Type u_5} (F : FormalGroup R) : ↑0 = 0

noncomputable def FormalGroup.𝔾ₐ {R : Type u_1} [CommRing R] : FormalGroup R

Additive formal group law 𝔾ₐ(X,Y) = X + Y.

Equations

• FormalGroup.𝔾ₐ = { toPowerSeries := MvPowerSeries.X 0 + MvPowerSeries.X 1, zero_constantCoeff := ⋯, lin_coeff_X := ⋯, lin_coeff_Y := ⋯, assoc := ⋯ }

@[simp]

theorem FormalGroup.𝔾ₐ_toPowerSeries {R : Type u_1} [CommRing R] : 𝔾ₐ.toPowerSeries = MvPowerSeries.X 0 + MvPowerSeries.X 1

instance FormalGroup.instIsComm𝔾ₐ {R : Type u_1} [CommRing R] : 𝔾ₐ.IsComm

noncomputable def FormalGroup.𝔾ₘ {R : Type u_1} [CommRing R] : FormalGroup R

Multiplicative formal group law 𝔾ₘ(X,Y) = X + Y + XY.

Equations

• FormalGroup.𝔾ₘ = { toPowerSeries := MvPowerSeries.X 0 + MvPowerSeries.X 1 + MvPowerSeries.X 0 * MvPowerSeries.X 1, zero_constantCoeff := ⋯, lin_coeff_X := ⋯, lin_coeff_Y := ⋯, assoc := ⋯ }

@[simp]

theorem FormalGroup.𝔾ₘ_toPowerSeries {R : Type u_1} [CommRing R] : 𝔾ₘ.toPowerSeries = MvPowerSeries.X 0 + MvPowerSeries.X 1 + MvPowerSeries.X 0 * MvPowerSeries.X 1

instance FormalGroup.instIsComm𝔾ₘ {R : Type u_1} [CommRing R] : 𝔾ₘ.IsComm

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

Given an algebra map f : R →+* S and a formal group law F over R, then f_* F is a formal group law formal group law over S. This is constructed by applying f to all coefficients of the underlying power series.

Equations

• F.map f = { toPowerSeries := (MvPowerSeries.map f) F.toPowerSeries, zero_constantCoeff := ⋯, lin_coeff_X := ⋯, lin_coeff_Y := ⋯, assoc := ⋯ }

@[simp]

theorem FormalGroup.map_toPowerSeries {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (F : FormalGroup R) (f : R →+* S) : (F.map f).toPowerSeries = (MvPowerSeries.map f) F.toPowerSeries

@[reducible, inline]

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

An abbreviation of $F(X,0)$ for a formal group $F$.

Equations

• F.Xzero = MvPowerSeries.subst ![PowerSeries.X, 0] F.toPowerSeries

theorem FormalGroup.constantCoeff_Xzero {R : Type u_1} [CommRing R] (F : FormalGroup R) : PowerSeries.constantCoeff F.Xzero = 0

@[simp]

theorem FormalGroup.coeff_one_Xzero {R : Type u_1} [CommRing R] (F : FormalGroup R) : (PowerSeries.coeff 1) F.Xzero = 1

@[simp]

theorem FormalGroup.Xzero_subst_Xzero {R : Type u_1} [CommRing R] (F : FormalGroup R) : PowerSeries.subst F.Xzero F.Xzero = F.Xzero

theorem FormalGroup.Xzero_eq_X {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.Xzero = PowerSeries.X

@[reducible, inline]

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

An abbreviation of $F(0,X)$ for a formal group $F$.

Equations

• F.zeroX = MvPowerSeries.subst ![0, PowerSeries.X] F.toPowerSeries

theorem FormalGroup.constantCoeff_zeroX {R : Type u_1} [CommRing R] (F : FormalGroup R) : PowerSeries.constantCoeff F.zeroX = 0

@[simp]

theorem FormalGroup.coeff_one_zeroX {R : Type u_1} [CommRing R] (F : FormalGroup R) : (PowerSeries.coeff 1) F.zeroX = 1

@[simp]

theorem FormalGroup.zeroX_subst_zeroX {R : Type u_1} [CommRing R] (F : FormalGroup R) : PowerSeries.subst F.zeroX F.zeroX = F.zeroX

theorem FormalGroup.zeroX_eq_X {R : Type u_1} [CommRing R] (F : FormalGroup R) : F.zeroX = PowerSeries.X

theorem FormalGroup.add_zero {R : Type u_1} [CommRing R] {σ : Type u_3} (F : FormalGroup R) {f : MvPowerSeries σ R} (hf : PowerSeries.HasSubst f) : MvPowerSeries.subst ![f, 0] F.toPowerSeries = f

theorem FormalGroup.zero_add {R : Type u_1} [CommRing R] {σ : Type u_3} (F : FormalGroup R) {f : MvPowerSeries σ R} (hf : PowerSeries.HasSubst f) : MvPowerSeries.subst ![0, f] F.toPowerSeries = f

@[implicit_reducible]

noncomputable instance FormalGroup.instAddMonoidPoint {R : Type u_1} [CommRing R] {σ : Type u_3} (F : FormalGroup R) : AddMonoid (F.Point σ)

Equations

• F.instAddMonoidPoint = { toAdd := F.instAddPoint, add_assoc := ⋯, toZero := F.instZeroPoint, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRec, nsmul_zero := ⋯, nsmul_succ := ⋯ }

@[implicit_reducible]

noncomputable instance FormalGroup.instAddCommMonoidPointOfIsComm {R : Type u_1} [CommRing R] {σ : Type u_3} (F : FormalGroup R) [F.IsComm] : AddCommMonoid (F.Point σ)

Equations

• F.instAddCommMonoidPointOfIsComm = { toAddMonoid := F.instAddMonoidPoint, add_comm := ⋯ }