Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FormalGroup_PointTransport.lean

definition module

Homomorphisms and isomorphisms of formal group laws; base change

Throughout, R is a commutative ring and F, G are formal group laws over R in Mathlib's sense, each given by its two-variable power series toPowerSeries in MvPowerSeries (Fin 2) R. The helper FormalGroup.LawHom.substX i φ is the substitution of the variable X_i (i \in \{0,1\}) into a one-variable series φ, i.e. φ(X_i) regarded as an element of R[[X_0,X_1]].

FormalGroup.LawHom F G is a structure whose data is a single power series series = φ \in R[[Z]], together with two fields that are propositions: φ has vanishing constant coefficient, and the compatibility φ(F(X_0,X_1)) = G(φ(X_0), φ(X_1)) holds in R[[X_0,X_1]], the left side being the substitution of F's series into φ and the right side the substitution of the pair (φ(X_0), φ(X_1)) into G's series. Thus the axioms of a homomorphism are carried as fields of the structure. FormalGroup.LawIso F G extends this by the further requirement that the linear coefficient \mathrm{coeff}_1 φ be a unit of R; invertibility of φ under substitution is therefore not part of the data.

The action on points is LawHom.app: for a commutative R-algebra A equipped with a uniform structure, φ.app x is the evaluation evalSeries φ.series x, namely \mathrm{eval}_2 of φ along algebraMap R A at x, with R given the discrete uniformity. LawHom.appAdic φ I x is the same evaluation performed in the uniform structure attached to an ideal I \subseteq A.

Finally, FormalGroup.IsBaseChange F f G, for a ring homomorphism f : R \to S and a formal group law G over S, is the relation asserting the equality of series G(X_0,X_1) = f_*F(X_0,X_1), where f_* applies f to coefficients. It is a predicate on a pair of given laws, not a construction of G from F.

Relation to Mathlib

Built on Mathlib's FormalGroup (a one-dimensional formal group law presented by its series in MvPowerSeries (Fin 2) R); the homomorphism and isomorphism structures are the project's own, kept under the names LawHom/LawIso, and carry no identity, composition or inverse as data.

Where it is used

This vocabulary supports the transport arguments for Drinfeld level structures on formal groups: isomorphisms of Weierstrass models induce isomorphisms of the associated formal group laws, Drinfeld bases are carried along such isomorphisms, and the universal property of the Lubin–Tate deformation ring with Drinfeld level structure is phrased using LawIso together with the base-change relation.

References

  1. M. Hazewinkel, Formal Groups and Applications, Pure and Applied Mathematics 78, Academic Press, 1978
  2. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, Chapter 5
  3. J. Lubin and J. Tate, Formal moduli for one-parameter formal Lie groups, Bulletin de la Société Mathématique de France 94 (1966), 49–59

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_FormalGroup_PointTransport.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_FormalGroup_NSeries

set_option autoImplicit false

noncomputable section

namespace FormalGroup

variable {R : Type*} [CommRing R]

def LawHom.substX (i : Fin 2) (φ : PowerSeries R) : MvPowerSeries (Fin 2) R :=
  PowerSeries.subst (MvPowerSeries.X i : MvPowerSeries (Fin 2) R) φ

structure LawHom (F G : FormalGroup R) where

  series : PowerSeries R

  constantCoeff_series : PowerSeries.constantCoeff series = 0

  comm : PowerSeries.subst F.toPowerSeries series =
    MvPowerSeries.subst ![LawHom.substX 0 series, LawHom.substX 1 series] G.toPowerSeries

structure LawIso (F G : FormalGroup R) extends LawHom F G where

  isUnit_coeff_one : IsUnit (PowerSeries.coeff 1 series)

namespace LawHom

variable {F G : FormalGroup R}

def app {A : Type*} [CommRing A] [UniformSpace A] [Algebra R A] (φ : LawHom F G) (x : A) : A :=
  FormalGroup.evalSeries φ.series x

def appAdic {A : Type*} [CommRing A] [Algebra R A] (φ : LawHom F G) (I : Ideal A) (x : A) : A :=
  letI : WithIdeal A := ⟨I⟩
  φ.app x

end LawHom

def IsBaseChange (F : FormalGroup R) {S : Type*} [CommRing S] (f : R →+* S) (G : FormalGroup S) : Prop :=
  G.toPowerSeries = MvPowerSeries.map f F.toPowerSeries

end FormalGroup

end

Statements phrased using this module (174)

… and 24 more statements (search for the module name to find them).