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

• Definition of one dimensional formal group law.

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

• Additive formal group laws and multiplicative formal group laws.

• Instance: Group instance defined by the formal group law F over the ideal PowerSeries.hasEvalIdeal.

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_iff {R : Type u_1} {inst✝ : CommRing R} {x y : FormalGroup R} : x = y ↔ x.toPowerSeries = y.toPowerSeries

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

@[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

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

Point F σ represents the mathematical space of points of a formal group $F$ taking values in the formal power series ring R⟦X_σ⟧.

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 σ = MvPowerSeries σ R

@[implicit_reducible]

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

Equations

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

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