Formal group laws: structure, differential matrix, base change

ChabautyColeman.FormalGroupLaw O ι is an ι-dimensional commutative formal group law over O: a family of power series F i in two blocks of ι variables with F(X,0) = X, F(0,Y) = Y, F(X,Y) = F(Y,X) and F(F(X,Y),Z) = F(X,F(Y,Z)), the substitutions being Mathlib's formal MvPowerSeries.subst. This file sets up the structure and its foundational API: the HasSubst witnesses for the axiom families, the differential (Jacobian) matrix at the origin, and base change along a ring homomorphism.

Main definitions

• ChabautyColeman.FormalGroupLaw: the structure of a formal group law.
• ChabautyColeman.FormalGroupLaw.diffMatrix: the Jacobian matrix (∂ⱼ Fᵢ)(X, 0).
• ChabautyColeman.FormalGroupLaw.map: base change of a formal group law along f : O →+* O'.

Main statements

• ChabautyColeman.FormalGroupLaw.isUnit_diffMatrix: the differential matrix is invertible.
• ChabautyColeman.FormalGroupLaw.diffMatrix_map: base change commutes with diffMatrix.

Blueprint nodes: def:fgl, def:fgl-diff.

The associativity substitution families

noncomputable def ChabautyColeman.assocLeftFam {O : Type u_1} [CommRing O] {ι : Type u_2} (F : ι → MvPowerSeries (ι ⊕ ι) O) : ι ⊕ ι → MvPowerSeries (ι ⊕ ι ⊕ ι) O

The substitution family embedding F(X,Y) into the first two of three blocks of variables (for the left side of associativity).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ChabautyColeman.assocRightFam {O : Type u_1} [CommRing O] {ι : Type u_2} (F : ι → MvPowerSeries (ι ⊕ ι) O) : ι ⊕ ι → MvPowerSeries (ι ⊕ ι ⊕ ι) O

The substitution family embedding F(Y,Z) into the last two of three blocks of variables (for the right side of associativity).

Equations

• One or more equations did not get rendered due to their size.

structure ChabautyColeman.FormalGroupLaw (O : Type u_1) [CommRing O] (ι : Type u_2) : Type (max u_1 u_2)

An ι-dimensional commutative formal group law over O: a family of power series F i in two blocks of ι variables (the blocks being the two summands of ι ⊕ ι), with F(X,0) = X, F(0,Y) = Y, F(X,Y) = F(Y,X) and F(F(X,Y),Z) = F(X,F(Y,Z)).

• F : ι → MvPowerSeries (ι ⊕ ι) O

  The underlying family of power series in the variables X = inl, Y = inr.

• zero_constantCoeff (i : ι) : MvPowerSeries.constantCoeff (self.F i) = 0
• add_zero' (i : ι) : MvPowerSeries.subst (Sum.elim MvPowerSeries.X fun (x : ι) => 0) (self.F i) = MvPowerSeries.X i
• zero_add' (i : ι) : MvPowerSeries.subst (Sum.elim (fun (x : ι) => 0) MvPowerSeries.X) (self.F i) = MvPowerSeries.X i
• comm' (i : ι) : MvPowerSeries.subst (fun (s : ι ⊕ ι) => MvPowerSeries.X s.swap) (self.F i) = self.F i
• assoc' (i : ι) : MvPowerSeries.subst (assocLeftFam self.F) (self.F i) = MvPowerSeries.subst (assocRightFam self.F) (self.F i)

HasSubst witnesses for the axiom substitutions

theorem ChabautyColeman.FormalGroupLaw.hasSubst_unitR {O : Type u_1} [CommRing O] {ι : Type u_2} [Finite ι] : MvPowerSeries.HasSubst (Sum.elim MvPowerSeries.X fun (x : ι) => 0)

theorem ChabautyColeman.FormalGroupLaw.hasSubst_unitL {O : Type u_1} [CommRing O] {ι : Type u_2} [Finite ι] : MvPowerSeries.HasSubst (Sum.elim (fun (x : ι) => 0) MvPowerSeries.X)

theorem ChabautyColeman.FormalGroupLaw.hasSubst_swap {O : Type u_1} [CommRing O] {ι : Type u_2} [Finite ι] : MvPowerSeries.HasSubst fun (s : ι ⊕ ι) => MvPowerSeries.X s.swap

theorem ChabautyColeman.FormalGroupLaw.hasSubst_emb12 {O : Type u_1} [CommRing O] {ι : Type u_2} [Finite ι] : MvPowerSeries.HasSubst (Sum.elim (fun (a : ι) => MvPowerSeries.X (Sum.inl a)) fun (b : ι) => MvPowerSeries.X (Sum.inr (Sum.inl b)))

theorem ChabautyColeman.FormalGroupLaw.hasSubst_emb23 {O : Type u_1} [CommRing O] {ι : Type u_2} [Finite ι] : MvPowerSeries.HasSubst (Sum.elim (fun (a : ι) => MvPowerSeries.X (Sum.inr (Sum.inl a))) fun (b : ι) => MvPowerSeries.X (Sum.inr (Sum.inr b)))

theorem ChabautyColeman.FormalGroupLaw.hasSubst_assocLeft {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [Finite ι] : MvPowerSeries.HasSubst (assocLeftFam Φ.F)

theorem ChabautyColeman.FormalGroupLaw.hasSubst_assocRight {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [Finite ι] : MvPowerSeries.HasSubst (assocRightFam Φ.F)

The differential (Jacobian) matrix at the origin

noncomputable def ChabautyColeman.FormalGroupLaw.diffMatrix {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) : Matrix ι ι (MvPowerSeries ι O)

The Jacobian matrix M(X) = (∂F/∂Y)(X, 0) of a formal group law, with entries in the power series ring in the X-block of variables.

Equations

• Φ.diffMatrix = Matrix.of fun (i j : ι) => MvPowerSeries.subst (Sum.elim MvPowerSeries.X fun (x : ι) => 0) ((MvPowerSeries.pderiv (Sum.inr j)) (Φ.F i))

theorem ChabautyColeman.FormalGroupLaw.diffMatrix_map_constantCoeff {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [DecidableEq ι] [Finite ι] : Φ.diffMatrix.map ⇑MvPowerSeries.constantCoeff = 1

M(0) is the identity matrix.

theorem ChabautyColeman.FormalGroupLaw.isUnit_diffMatrix {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [DecidableEq ι] [Fintype ι] : IsUnit Φ.diffMatrix

The Jacobian matrix of a formal group law is invertible.

theorem ChabautyColeman.FormalGroupLaw.diffMatrixInv_map_constantCoeff {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) [DecidableEq ι] [Fintype ι] : Φ.diffMatrix⁻¹.map ⇑MvPowerSeries.constantCoeff = 1

The constant term of the inverse Jacobian matrix is the identity.

Base change along a ring homomorphism

noncomputable def ChabautyColeman.FormalGroupLaw.map {O : Type u_1} [CommRing O] {ι : Type u_2} {O' : Type u_3} [CommRing O'] [Finite ι] (f : O →+* O') (Φ : FormalGroupLaw O ι) : FormalGroupLaw O' ι

Base change of a formal group law along a ring homomorphism f : O →+* O': apply MvPowerSeries.map f to each defining power series.

Equations

• ChabautyColeman.FormalGroupLaw.map f Φ = { F := fun (i : ι) => (MvPowerSeries.map f) (Φ.F i), zero_constantCoeff := ⋯, add_zero' := ⋯, zero_add' := ⋯, comm' := ⋯, assoc' := ⋯ }

@[simp]

theorem ChabautyColeman.FormalGroupLaw.F_map {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) {O' : Type u_3} [CommRing O'] [Finite ι] (f : O →+* O') (i : ι) : (map f Φ).F i = (MvPowerSeries.map f) (Φ.F i)

theorem ChabautyColeman.FormalGroupLaw.diffMatrix_map {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) {O' : Type u_3} [CommRing O'] [Finite ι] (f : O →+* O') : (map f Φ).diffMatrix = Φ.diffMatrix.map ⇑(MvPowerSeries.map f)

The differential matrix commutes with base change.

theorem ChabautyColeman.FormalGroupLaw.diffMatrixInv_map {O : Type u_1} [CommRing O] {ι : Type u_2} (Φ : FormalGroupLaw O ι) {O' : Type u_3} [CommRing O'] [Finite ι] [Fintype ι] [DecidableEq ι] (f : O →+* O') : (map f Φ).diffMatrix⁻¹ = Φ.diffMatrix⁻¹.map ⇑(MvPowerSeries.map f)

The inverse differential matrix commutes with base change: in particular, base change of an invertible differential matrix stays invertible. This is the integrality statement for the invariant differential — the entries of M⁻¹ are already defined over O.