Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Dieudonne_ModpRealization.lean

definition module

Mod-p Dieudonné realisations of finite Hopf algebras

Fix a field k of characteristic p (for a prime p) and a commutative k-algebra A with a Hopf algebra structure over k. Two submodule-level invariants of A are defined. First, primitives is the k-submodule of A given as the kernel of the k-linear map a \mapsto \Delta a - a \otimes 1 - 1 \otimes a, where \Delta is the comultiplication; that is, the space of primitive elements P(A). Second, cotangentSpace is Ideal.Cotangent of the kernel of the counit algebra map \varepsilon \colon A \to k, i.e. the k-module I_\varepsilon/I_\varepsilon^2; for A = \mathcal O(G) this is the cotangent space \omega_G at the identity.

The structure ModpDieudonneRealization is then defined for A finite and free as a k-module with cocommutative comultiplication, and for a k-module D that is finite as a k-module. Its data consist of a field datum, a DieudonneDatum over the base ring k at the scalar \ell = (p : k) on D: a pair of k-linear endomorphisms F, V of D with F \circ V = V \circ F = \ell \cdot \mathrm{id}; since k has characteristic p, the scalar \ell is 0, so both composites vanish. Three further fields are numerical constraints carried as part of the data: \dim_k A = p^{\dim_k D}; \dim_k \ker F = \dim_k (I_\varepsilon/I_\varepsilon^2); and \dim_k \ker V = \dim_k P(A).

Thus a realisation is a choice of module D with F and V on it, pinned only by these three dimension identities; the definition asserts neither functoriality in A nor uniqueness of D.

Relation to Mathlib

The Hopf/coalgebra interface used here (HopfAlgebra, Coalgebra.comul, Coalgebra.IsCocomm, Bialgebra.counitAlgHom) and the cotangent module Ideal.Cotangent are Mathlib's; Mathlib has no Dieudonné theory, so primitives and ModpDieudonneRealization are the project's own, built on the project's DieudonneDatum.

Where it is used

These definitions provide the mod-p interface for Dieudonné modules of finite commutative p-group schemes, used in the classification of group schemes of order p by the F–V type of their realisation and, through it, in the mod-p layer of the flatness and finite-flat conditions imposed on the Galois deformation problems.

References

  1. T. Oda, The first de Rham cohomology group and Dieudonné modules, Annales scientifiques de l'École Normale Supérieure (4) 2 (1969), 63–135
  2. J. Tate and F. Oort, Group schemes of prime order, Annales scientifiques de l'École Normale Supérieure (4) 3 (1970), 1–21
  3. J.-M. Fontaine, Groupes p-divisibles sur les corps locaux, Astérisque 47–48, Société Mathématique de France, 1977

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_Dieudonne_ModpRealization.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_Dieudonne_DatumAndHonda

set_option autoImplicit false

open scoped TensorProduct
open Deformation

universe u v w

section Realization

variable (k : Type u) [Field k] (p : ℕ) [Fact p.Prime] [CharP k p]
variable (A : Type v) [CommRing A] [HopfAlgebra k A]

noncomputable def primitives : Submodule k A :=
  LinearMap.ker (Coalgebra.comul (R := k) (A := A)
    - (TensorProduct.mk k A A).flip 1 - TensorProduct.mk k A A 1)

abbrev cotangentSpace : Type v :=
  (RingHom.ker (Bialgebra.counitAlgHom k A)).Cotangent

structure ModpDieudonneRealization
    [Module.Finite k A] [Module.Free k A] [Coalgebra.IsCocomm k A]
    (D : Type w) [AddCommGroup D] [Module k D] [Module.Finite k D] where

  datum : DieudonneDatum ((p : ℕ) : k) D

  order_eq : Module.finrank k A = p ^ Module.finrank k D

  finrank_kerFrob : Module.finrank k (LinearMap.ker datum.F)
    = Module.finrank k (cotangentSpace k A)

  finrank_kerVer : Module.finrank k (LinearMap.ker datum.V)
    = Module.finrank k (primitives k A)

end Realization

Statements phrased using this module (35)