Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_HeckeGalois_MazurCase1Bundle.lean

definition module

Frobenius–Verschiebung pairs and the Mazur II (14.2) Case-1 bundle

Over a field k and a k-vector space M, VerFrobPair k M is the structure consisting of two k-linear endomorphisms frob and ver of M whose two composites in either order vanish; the two accompanying lemmas record the pointwise consequences V(Fx)=0 and F(Vx)=0. SelfDual D is a structure carrying a k-linear isomorphism of M with its dual \mathrm{Dual}_k M that converts F into the transpose of V and V into the transpose of F. A submodule N is Stable for D when it is carried into itself by both F and V; quotientPair is the induced pair on M/N, and kernelPair produces, from pairs D_2 on M_2 and D_3 on M_3 and a k-linear map \pi with \pi\circ V_2=V_3\circ\pi and \pi\circ F_2=F_3\circ\pi, the pair obtained by restricting F_2,V_2 to \ker\pi.

OdaDictionary 𝕋 J π”ͺ k Vrep HDR MV H0Ξ© H1O bundles: pairs D_{HDR} on HDR and D_{MV} on MV; the equality \ker F_{HDR}=\operatorname{im} V_{HDR}; isomorphisms H0Ξ© \cong\ker F_{HDR} and H1O \cong HDR/\operatorname{im}V_{HDR}; a surjection \pi\colon HDR\to MV commuting with V and with F; and two equalities of dimensions, \dim_{𝕋/π”ͺ}\,J[π”ͺ]=\dim_k HDR, where J[π”ͺ] is the π”ͺ-torsion Submodule.torsionBySet 𝕋 J π”ͺ, and \dim_{𝕋/π”ͺ} Vrep=\dim_k MV. FontaineLayer P is the proposition: if \ker\pi is nontrivial then it has a submodule N, stable for the restricted pair, together with a k-linear isomorphism (\ker\pi)/N\cong MV intertwining the induced ver with V_{MV} (the condition is imposed on ver only).

For π”ͺ a maximal ideal of 𝕋, so that 𝕋/π”ͺ is a field, Case1Geometry 𝕋 J π”ͺ is the data of five 𝕋/π”ͺ-modules Vrep, HDR, MV, H0Ξ©, H1O with HDR finite-dimensional, an OdaDictionary on them taken with k=𝕋/π”ͺ, and, as fields, self-duality of D_{MV} and the FontaineLayer clause. Case1Bundle extends this by two numerical fields: \dim_{𝕋/π”ͺ} H1O\le 1 and \dim_{𝕋/π”ͺ} Vrep=2.

Relation to Mathlib

Mathlib has no notion of DieudonnΓ© module or of a Frobenius–Verschiebung pair; these structures are the project's own, built on Mathlib's Module.Dual, LinearMap.dualMap, Submodule.mapQ, LinearMap.restrict and Submodule.torsionBySet.

Where it is used

The structures provide the abstract DieudonnΓ©-side vocabulary for Mazur's Case 1 analysis (p\nmid N) of the π”ͺ-torsion of the Jacobian of a modular curve: the carriers stand for H^1_{\mathrm{DR}}/π”ͺ, the DieudonnΓ© module of the residual representation space, and the two Hodge pieces H^0(\Omega)/π”ͺ and H^1(\mathcal O)/π”ͺ, with the rank fields tying J[π”ͺ] and the representation space to them. A Case1Bundle is the hypothesis package from which the multiplicity-one style dimension conclusions on J[π”ͺ] are drawn.

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications MathΓ©matiques de l'IHΓ‰S 47 (1977), 33–186, §§9, 14
  2. J.-M. Fontaine, Groupes p-divisibles sur les corps locaux, AstΓ©risque 47–48, SociΓ©tΓ© MathΓ©matique de France, 1977
  3. T. Oda, The first de Rham cohomology group and DieudonnΓ© modules, Ann. Sci. Γ‰cole Norm. Sup. (4) 2 (1969), 63–135

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.Algebra.Module.Torsion.Basic β†—
import Mathlib.LinearAlgebra.Quotient.Basic β†—
import Mathlib.LinearAlgebra.Dual.Defs β†—
import Mathlib.LinearAlgebra.FiniteDimensional.Defs β†—
import Mathlib.LinearAlgebra.Dimension.Finrank β†—
import Mathlib.RingTheory.Ideal.Quotient.Basic β†—

set_option autoImplicit false

noncomputable section

open Module

namespace ModularCurve

namespace MazurII142

section Carrier

variable (k : Type*) [Field k] (M : Type*) [AddCommGroup M] [Module k M]

structure VerFrobPair where

  frob : M β†’β‚—[k] M

  ver : M β†’β‚—[k] M

  ver_comp_frob : ver βˆ˜β‚— frob = 0

  frob_comp_ver : frob βˆ˜β‚— ver = 0

end Carrier

namespace VerFrobPair

section Basic

variable {k : Type*} [Field k] {M : Type*} [AddCommGroup M] [Module k M]
variable (D : VerFrobPair k M)

theorem ver_frob_apply (x : M) : D.ver (D.frob x) = 0 := by
  simpa using LinearMap.congr_fun D.ver_comp_frob x

theorem frob_ver_apply (x : M) : D.frob (D.ver x) = 0 := by
  simpa using LinearMap.congr_fun D.frob_comp_ver x

end Basic

section Duality

variable {k : Type*} [Field k] {M : Type*} [AddCommGroup M] [Module k M]

structure SelfDual (D : VerFrobPair k M) where

  equiv : M ≃ₗ[k] Module.Dual k M

  frob_comm : βˆ€ x : M, equiv (D.frob x) = D.ver.dualMap (equiv x)

  ver_comm : βˆ€ x : M, equiv (D.ver x) = D.frob.dualMap (equiv x)

end Duality

section StableQuotient

variable {k : Type*} [Field k] {M : Type*} [AddCommGroup M] [Module k M]
variable (D : VerFrobPair k M)

def Stable (N : Submodule k M) : Prop :=
  (βˆ€ x ∈ N, D.frob x ∈ N) ∧ (βˆ€ x ∈ N, D.ver x ∈ N)

def quotientPair (N : Submodule k M) (hN : D.Stable N) : VerFrobPair k (M β§Έ N) where
  frob := Submodule.mapQ N N D.frob (fun x hx => hN.1 x hx)
  ver := Submodule.mapQ N N D.ver (fun x hx => hN.2 x hx)
  ver_comp_frob := by
    apply LinearMap.ext
    intro z
    obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective N z
    simp only [LinearMap.comp_apply, Submodule.mapQ_apply, D.ver_frob_apply,
      Submodule.Quotient.mk_zero, LinearMap.zero_apply]
  frob_comp_ver := by
    apply LinearMap.ext
    intro z
    obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective N z
    simp only [LinearMap.comp_apply, Submodule.mapQ_apply, D.frob_ver_apply,
      Submodule.Quotient.mk_zero, LinearMap.zero_apply]

end StableQuotient

section Kernel

variable {k : Type*} [Field k] {Mβ‚‚ M₃ : Type*}
  [AddCommGroup Mβ‚‚] [Module k Mβ‚‚] [AddCommGroup M₃] [Module k M₃]

def kernelPair (Dβ‚‚ : VerFrobPair k Mβ‚‚) (D₃ : VerFrobPair k M₃) (Ο€ : Mβ‚‚ β†’β‚—[k] M₃)
    (hΟ€_ver : Ο€ βˆ˜β‚— Dβ‚‚.ver = D₃.ver βˆ˜β‚— Ο€) (hΟ€_frob : Ο€ βˆ˜β‚— Dβ‚‚.frob = D₃.frob βˆ˜β‚— Ο€) :
    VerFrobPair k (LinearMap.ker Ο€) where
  frob := Dβ‚‚.frob.restrict (p := LinearMap.ker Ο€) (q := LinearMap.ker Ο€) (fun x hx => by
    rw [LinearMap.mem_ker] at hx ⊒
    have h := LinearMap.congr_fun hΟ€_frob x
    simp only [LinearMap.comp_apply] at h
    rw [h, hx, map_zero])
  ver := Dβ‚‚.ver.restrict (p := LinearMap.ker Ο€) (q := LinearMap.ker Ο€) (fun x hx => by
    rw [LinearMap.mem_ker] at hx ⊒
    have h := LinearMap.congr_fun hΟ€_ver x
    simp only [LinearMap.comp_apply] at h
    rw [h, hx, map_zero])
  ver_comp_frob := by
    apply LinearMap.ext
    intro x
    apply Subtype.ext
    show Dβ‚‚.ver (Dβ‚‚.frob (x : Mβ‚‚)) = ((0 : LinearMap.ker Ο€ β†’β‚—[k] LinearMap.ker Ο€) x : Mβ‚‚)
    rw [Dβ‚‚.ver_frob_apply]
    rfl
  frob_comp_ver := by
    apply LinearMap.ext
    intro x
    apply Subtype.ext
    show Dβ‚‚.frob (Dβ‚‚.ver (x : Mβ‚‚)) = ((0 : LinearMap.ker Ο€ β†’β‚—[k] LinearMap.ker Ο€) x : Mβ‚‚)
    rw [Dβ‚‚.frob_ver_apply]
    rfl

end Kernel

end VerFrobPair

structure OdaDictionary
    (𝕋 : Type*) [CommRing 𝕋] (J : Type*) [AddCommGroup J] [Module 𝕋 J] (π”ͺ : Ideal 𝕋)
    (k : Type*) [Field k]
    (Vrep : Type*) [AddCommGroup Vrep] [Module (𝕋 β§Έ π”ͺ) Vrep]
    (HDR : Type*) [AddCommGroup HDR] [Module k HDR]
    (MV : Type*) [AddCommGroup MV] [Module k MV]
    (H0Ξ© : Type*) [AddCommGroup H0Ξ©] [Module k H0Ξ©]
    (H1O : Type*) [AddCommGroup H1O] [Module k H1O] : Type _ where

  DHDR : VerFrobPair k HDR

  DMV : VerFrobPair k MV

  frobKer_eq_verRange : LinearMap.ker DHDR.frob = LinearMap.range DHDR.ver

  hodgeSub : H0Ξ© ≃ₗ[k] LinearMap.ker DHDR.frob

  hodgeQuot : H1O ≃ₗ[k] (HDR β§Έ LinearMap.range DHDR.ver)

  pi : HDR β†’β‚—[k] MV

  pi_surjective : Function.Surjective pi

  pi_ver : pi βˆ˜β‚— DHDR.ver = DMV.ver βˆ˜β‚— pi

  pi_frob : pi βˆ˜β‚— DHDR.frob = DMV.frob βˆ˜β‚— pi

  rank_J : Module.finrank (𝕋 β§Έ π”ͺ) (Submodule.torsionBySet 𝕋 J π”ͺ) = finrank k HDR

  rank_V : Module.finrank (𝕋 β§Έ π”ͺ) Vrep = finrank k MV

namespace OdaDictionary

section Derived

variable {𝕋 : Type*} [CommRing 𝕋] {J : Type*} [AddCommGroup J] [Module 𝕋 J] {π”ͺ : Ideal 𝕋}
  {k : Type*} [Field k]
  {Vrep : Type*} [AddCommGroup Vrep] [Module (𝕋 β§Έ π”ͺ) Vrep]
  {HDR : Type*} [AddCommGroup HDR] [Module k HDR]
  {MV : Type*} [AddCommGroup MV] [Module k MV]
  {H0Ξ© : Type*} [AddCommGroup H0Ξ©] [Module k H0Ξ©]
  {H1O : Type*} [AddCommGroup H1O] [Module k H1O]
  (P : OdaDictionary 𝕋 J π”ͺ k Vrep HDR MV H0Ξ© H1O)

abbrev kernelPair : VerFrobPair k (LinearMap.ker P.pi) :=
  P.DHDR.kernelPair P.DMV P.pi P.pi_ver P.pi_frob

abbrev FontaineLayer : Prop :=
  Nontrivial (LinearMap.ker P.pi) β†’
    βˆƒ (N : Submodule k (LinearMap.ker P.pi)) (hN : P.kernelPair.Stable N)
      (e : ((LinearMap.ker P.pi) β§Έ N) ≃ₗ[k] MV),
      βˆ€ z, e ((P.kernelPair.quotientPair N hN).ver z) = P.DMV.ver (e z)

end Derived

end OdaDictionary

universe u v

attribute [local instance] Ideal.Quotient.field

structure Case1Geometry (𝕋 : Type u) [CommRing 𝕋] (J : Type v) [AddCommGroup J] [Module 𝕋 J]
    (π”ͺ : Ideal 𝕋) [π”ͺ.IsMaximal] where

  Vrep : Type u
  [hVrepACG : AddCommGroup Vrep]
  [hVrepMod : Module (𝕋 β§Έ π”ͺ) Vrep]

  HDR : Type u
  [hHDRACG : AddCommGroup HDR]
  [hHDRMod : Module (𝕋 β§Έ π”ͺ) HDR]

  MV : Type u
  [hMVACG : AddCommGroup MV]
  [hMVMod : Module (𝕋 β§Έ π”ͺ) MV]

  H0Ξ© : Type u
  [hH0ACG : AddCommGroup H0Ξ©]
  [hH0Mod : Module (𝕋 β§Έ π”ͺ) H0Ξ©]

  H1O : Type u
  [hH1ACG : AddCommGroup H1O]
  [hH1Mod : Module (𝕋 β§Έ π”ͺ) H1O]

  pkt : OdaDictionary 𝕋 J π”ͺ (𝕋 β§Έ π”ͺ) Vrep HDR MV H0Ξ© H1O
  [hFD : FiniteDimensional (𝕋 β§Έ π”ͺ) HDR]

  hsd : pkt.DMV.SelfDual

  hlayer : pkt.FontaineLayer

attribute [instance] Case1Geometry.hVrepACG Case1Geometry.hVrepMod
  Case1Geometry.hHDRACG Case1Geometry.hHDRMod Case1Geometry.hMVACG Case1Geometry.hMVMod
  Case1Geometry.hH0ACG Case1Geometry.hH0Mod Case1Geometry.hH1ACG Case1Geometry.hH1Mod
  Case1Geometry.hFD

structure Case1Bundle (𝕋 : Type u) [CommRing 𝕋] (J : Type v) [AddCommGroup J] [Module 𝕋 J]
    (π”ͺ : Ideal 𝕋) [π”ͺ.IsMaximal] extends Case1Geometry 𝕋 J π”ͺ where

  h94 : finrank (𝕋 β§Έ π”ͺ) H1O ≀ 1

  hdimV : finrank (𝕋 β§Έ π”ͺ) Vrep = 2

end MazurII142

end ModularCurve

end

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).