Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_PDivisibleGroup_Dimension.lean

definition module

Cotangent spaces, dimension and tangent space of -divisible groups

Throughout, R is a commutative ring, p,h are natural numbers and G is a p-divisible group over R of height h in the project's sense: a system of finite free cocommutative Hopf R-algebras A_v= G.level v of rank p^{vh}, with surjective bialgebra transition maps A_{v+1}\to A_v whose kernels are the ideals generated by the image of the augmentation ideal under the p^v-fold convolution power of the identity.

For each level, augIdeal v is the augmentation ideal I_v=\ker(\varepsilon\colon A_v\to R), characterised by a\in I_v\iff\varepsilon(a)=0, and Cotangent v is I_v/I_v^2 (Mathlib's cotangent module of an ideal). Since \varepsilon commutes with the transition maps, I_{v+1} lies in the preimage of I_v, and cotangentMap v is the induced R-linear map I_{v+1}/I_{v+1}^2\to I_v/I_v^2; it is shown to be surjective, using surjectivity of the transition map together with the decomposition a=\varepsilon(a)+(a-\varepsilon(a)).

The predicate HasDimension n asserts, for each v, the mere existence of an R-linear isomorphism I_v/I_v^2\cong(R/p^vR)^n (indices in Fin n); no compatibility of these isomorphisms with the maps cotangentMap is required, and no uniqueness of n is asserted. Two complements are recorded: if every I_v is idempotent, i.e. I_v^2=I_v, then the cotangent modules vanish and HasDimension 0 holds; and at v=0 the target (R/p^0R)^n is trivial for every n.

Finally cotangentModule is the submodule of \prod_v I_v/I_v^2 of sequences (x_v) with cotangentMap v (x_{v+1})=x_v, i.e. the inverse limit \omega_G=\varprojlim_v I_v/I_v^2, together with its projections to the individual levels, and for a commutative R-algebra L the tangent space tangentSpace L is \operatorname{Hom}_R(\omega_G,L).

Relation to Mathlib

The cotangent modules are Mathlib's Ideal.Cotangent and the level maps come from Ideal.mapCotangent; the notion of p-divisible group, its augmentation ideals and the dimension predicate are the project's own, Mathlib having no theory of p-divisible groups.

Where it is used

These constructions equip the project's p-divisible groups with the invariants — cotangent spaces along the unit section, a dimension predicate, and the limit cotangent and tangent modules — needed in the study of the p-divisible groups and finite flat group schemes attached to elliptic curves over local rings, which govern the local conditions at p in the modularity lifting argument.

References

  1. J. Tate, p-divisible groups, in: Proceedings of a Conference on Local Fields (Driebergen, 1966), Springer, 1967, 158–183, §2
  2. W. Messing, The Crystals Associated to Barsotti–Tate Groups, Lecture Notes in Mathematics 264, Springer, 1972, Ch. II

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_PDivisibleGroup_Basic

set_option autoImplicit false

noncomputable section

open Coalgebra Bialgebra

namespace PDivisibleGroup

variable {R : Type} [CommRing R] {p h : ℕ} (G : PDivisibleGroup R p h)

abbrev augIdeal (v : ℕ) : Ideal (G.level v) := Hopf.augIdeal R (G.level v)

theorem mem_augIdeal_iff (v : ℕ) (a : G.level v) : a ∈ G.augIdeal v ↔ counit (R := R) a = 0 := Iff.rfl

abbrev Cotangent (v : ℕ) : Type := (G.augIdeal v).Cotangent

theorem augIdeal_le_comap_transition (v : ℕ) :
    G.augIdeal (v + 1) ≤ (G.augIdeal v).comap (G.transitionAlgHom v) := by
  intro a ha
  rw [Ideal.mem_comap, mem_augIdeal_iff, transitionAlgHom_apply, G.counit_transition]
  exact ha

def cotangentMap (v : ℕ) : G.Cotangent (v + 1) →ₗ[R] G.Cotangent v :=
  Ideal.mapCotangent (G.augIdeal (v + 1)) (G.augIdeal v) (G.transitionAlgHom v)
    (G.augIdeal_le_comap_transition v)

@[simp] theorem cotangentMap_toCotangent (v : ℕ) (a : G.augIdeal (v + 1)) :
    G.cotangentMap v ((G.augIdeal (v + 1)).toCotangent a) =
      (G.augIdeal v).toCotangent ⟨G.transition v a, G.augIdeal_le_comap_transition v a.2⟩ := rfl

theorem cotangentMap_surjective (v : ℕ) : Function.Surjective (G.cotangentMap v) := by
  intro y
  obtain ⟨⟨b, hb⟩, rfl⟩ := (G.augIdeal v).toCotangent_surjective y
  obtain ⟨a, rfl⟩ := G.transition_surjective v b

  refine ⟨(G.augIdeal (v + 1)).toCotangent
    ⟨a - algebraMap R _ (counit (R := R) a), Hopf.sub_algebraMap_counit_mem_augIdeal R _ a⟩, ?_⟩
  rw [cotangentMap_toCotangent]
  congr 1
  ext
  change G.transition v (a - algebraMap R _ (counit (R := R) a)) = G.transition v a
  have hb' : counit (R := R) (G.transition v a) = 0 := hb
  rw [G.counit_transition] at hb'
  rw [hb', map_zero, sub_zero]

def HasDimension (n : ℕ) : Prop :=
  ∀ v : ℕ, Nonempty (G.Cotangent v ≃ₗ[R] (Fin n → R ⧸ Ideal.span {(p : R) ^ v}))

theorem hasDimension_zero_of_isIdempotentElem (hI : ∀ v, IsIdempotentElem (G.augIdeal v)) :
    G.HasDimension 0 := by
  intro v
  haveI : Subsingleton (G.Cotangent v) := (Ideal.cotangent_subsingleton_iff _).mpr (hI v)
  exact ⟨LinearEquiv.ofSubsingleton _ _⟩

theorem subsingleton_target_zero (n : ℕ) : Subsingleton (Fin n → R ⧸ Ideal.span {(p : R) ^ 0}) := by
  rw [pow_zero, Ideal.span_singleton_one]
  infer_instance

def cotangentModule : Submodule R (∀ v, G.Cotangent v) where
  carrier := {x | ∀ v, G.cotangentMap v (x (v + 1)) = x v}
  add_mem' {x y} hx hy v := by rw [Pi.add_apply, Pi.add_apply, map_add, hx v, hy v]
  zero_mem' v := by rw [Pi.zero_apply, Pi.zero_apply, map_zero]
  smul_mem' r x hx v := by rw [Pi.smul_apply, Pi.smul_apply, map_smul, hx v]

theorem mem_cotangentModule_iff (x : ∀ v, G.Cotangent v) :
    x ∈ G.cotangentModule ↔ ∀ v, G.cotangentMap v (x (v + 1)) = x v := Iff.rfl

def cotangentModuleProj (v : ℕ) : G.cotangentModule →ₗ[R] G.Cotangent v where
  toFun x := (x : ∀ v, G.Cotangent v) v
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

theorem cotangentMap_cotangentModuleProj (v : ℕ) (x : G.cotangentModule) :
    G.cotangentMap v (G.cotangentModuleProj (v + 1) x) = G.cotangentModuleProj v x := x.2 v

abbrev tangentSpace (L : Type) [CommRing L] [Algebra R L] : Type := G.cotangentModule →ₗ[R] L

end PDivisibleGroup

end

Statements phrased using this module (24)