Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_CornerPairingFamily.lean

definition module

Chosen pairings on parabolic classes at all levels

Fix a commutative ring \mathcal O. For a level M, a subgroup H\le(\mathbb Z/M)^\times and a datum h_1:\mathrm{LevelLE}\,M\,M\,\top\,H\,1, write W(M,H) for the submodule of H^1(M,H,\mathcal O)=\mathrm{Hom}(\mathrm{Additive}\,\Gamma_H(M,H),\mathcal O) obtained as the image under iDegL M M ⊀ H 1 (restriction along the inclusion \Gamma_H(M,H)\to\Gamma_H(M,\top)=\Gamma_0(M)) of ModularCurve.Period.parabolicHoms, i.e. of those additive characters of \Gamma_0(M) that vanish on every element whose matrix trace has square 4. Two predicates are defined on families B=(B_{M,H,h_1}) of \mathcal O-bilinear forms W(M,H)\times W(M,H)\to\mathcal O. LevelBlock asks, for every M\ne 0 and every H whose index [(\mathbb Z/M)^\times:H] is a unit in \mathcal O: that B_{M,H,h_1} be bijective as a map W(M,H)\to\mathrm{Hom}_{\mathcal O}(W(M,H),\mathcal O); that for each \ell\ne 0 which is prime or divides M and for elements x,y,Tx,Ty of W(M,H) whose underlying characters satisfy Tx=\mathrm{heckeT}_\ell x and Ty=\mathrm{heckeT}_\ell y one has B(Tx,y)=B(x,Ty); and that diamondL at every d\in(\mathbb Z/M)^\times fix each element of W(M,H). DegeneracyBlock asks, for h:\mathrm{LevelLE}\,M\,M'\,H\,H'\,d and h':\mathrm{LevelLE}\,M\,M'\,H\,H'\,d' with dd'=M'/M, with H' the full preimage of H under ZMod.unitsMap and both indices units, that B_{M,H,h_1}(jy,x)=B_{M',H',h_1'}(y,ix) whenever ix and jy have underlying characters \mathrm{iDegL}\,x and \mathrm{jDegL}\,y. CuspForm.Bfam π’ͺ is then a family chosen by Classical.epsilon to satisfy both blocks when such a family exists.

In the corner section, for corner data cd : H1CornerData M H π’ͺ 𝕋 (an idempotent splitting of \mathbb T, an index, and a level pairing on the corresponding corner submodule of H^1) and a hypothesis hW placing that corner submodule inside W(M,H), cornerInclusion is the resulting \mathcal O-linear inclusion, cornerRestrict is Bfam π’ͺ M H h₁ restricted along it in both arguments, and pairing_eq_cornerRestrict_iff states that the corner datum's own pairing equals this restriction exactly when the two agree on all pairs of elements. The Bfamβ‚€ section repeats the construction for H=\top on parabolicHoms itself: Bfamβ‚€.Block requires bijectivity, self-adjointness of heckeT for every \ell\ne 0 and of diamondL for every d (rather than triviality of the diamonds), together with the same degeneracy compatibility at H=H'=\top, and Bfamβ‚€ π’ͺ is a family chosen to satisfy it.

Relation to Mathlib

Mathlib has no pairing on parabolic cohomology of congruence subgroups; the carriers (CohCarrier.H1, parabolicHoms, the Hecke, diamond and degeneracy operators) and both pairing families are the project's own, built on Mathlib's congruence subgroups, transfer and LinearMap.compl₁₂, with the choice made by Mathlib's Classical.epsilon.

Where it is used

These named pairings let statements about Hecke modules at the various levels of the tower used in modularity lifting (\Gamma_0(N)\cap\Gamma_1(r), its p-level and its auxiliary Taylor–Wiles levels) refer to one and the same pairing at each level, instead of carrying a family together with its perfectness, Hecke-adjointness and degeneracy-adjointness hypotheses. The corner constructions transport such a pairing to the summand cut out by an idempotent of a Hecke algebra, which is the shape required by the Ihara-style rung data.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, Β§4.4
  2. R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572

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

Imports

Imported by

Declarations

Source

import Definitions.Def_CohCarrier_Inst
import Definitions.Def_ModularCurve_PeriodMap
import Definitions.Def_CohCarrier_LevelPairing

set_option autoImplicit false

set_option linter.unusedVariables false

noncomputable section

namespace CuspForm

open CohCarrier IharaLemma IharaTower

namespace Bfam

variable (π’ͺ : Type) [CommRing π’ͺ]

def LevelBlock
    (B : (M : β„•) β†’ (H : Subgroup (ZMod M)Λ£) β†’ (h₁ : LevelLE M M ⊀ H 1) β†’
        β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) β†’β‚—[π’ͺ]
        β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) β†’β‚—[π’ͺ] π’ͺ) :
    Prop :=
  βˆ€ (M : β„•) [NeZero M] (H : Subgroup (ZMod M)Λ£) (h₁ : LevelLE M M ⊀ H 1),
    IsUnit ((H.index : β„•) : π’ͺ) β†’
    Function.Bijective (B M H h₁) ∧
    (βˆ€ (β„“ : β„•) [NeZero β„“], (β„“.Prime ∨ β„“ ∣ M) β†’
      βˆ€ (x y Tx Ty : β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map
          (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁))),
        (Tx : H1 M H π’ͺ) = heckeT M H β„“ π’ͺ x β†’ (Ty : H1 M H π’ͺ) = heckeT M H β„“ π’ͺ y β†’
        B M H h₁ Tx y = B M H h₁ x Ty) ∧
    (βˆ€ (d : (ZMod M)Λ£) (x : β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map
          (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁))),
        diamondL M H π’ͺ d (x : H1 M H π’ͺ) = x)

def DegeneracyBlock
    (B : (M : β„•) β†’ (H : Subgroup (ZMod M)Λ£) β†’ (h₁ : LevelLE M M ⊀ H 1) β†’
        β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) β†’β‚—[π’ͺ]
        β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) β†’β‚—[π’ͺ] π’ͺ) :
    Prop :=
  βˆ€ (M M' : β„•) [NeZero M] [NeZero M'] (H : Subgroup (ZMod M)Λ£) (H' : Subgroup (ZMod M')Λ£)
      (h₁ : LevelLE M M ⊀ H 1) (h₁' : LevelLE M' M' ⊀ H' 1)
      (d d' : β„•) [NeZero d] [NeZero d'] (h : LevelLE M M' H H' d) (h' : LevelLE M M' H H' d')
      (hdd' : d * d' = M' / M)
      (hH' : βˆ€ u : (ZMod M')Λ£, u ∈ H' ↔ ZMod.unitsMap h.dvd u ∈ H),
      IsUnit ((H.index : β„•) : π’ͺ) β†’ IsUnit ((H'.index : β„•) : π’ͺ) β†’
      βˆ€ (x : β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)))
        (y : β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M' ⊀) π’ͺ).map (iDegL M' M' ⊀ H' 1 π’ͺ π’ͺ h₁')))
        (ix : β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M' ⊀) π’ͺ).map (iDegL M' M' ⊀ H' 1 π’ͺ π’ͺ h₁')))
        (jy : β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁))),
      (ix : H1 M' H' π’ͺ) = iDegL M M' H H' d π’ͺ π’ͺ h x β†’
      (jy : H1 M H π’ͺ) = jDegL M M' H H' d' π’ͺ π’ͺ h' y β†’
      B M H h₁ jy x = B M' H' h₁' y ix

end Bfam

def Bfam (π’ͺ : Type) [CommRing π’ͺ] :
    (M : β„•) β†’ (H : Subgroup (ZMod M)Λ£) β†’ (h₁ : LevelLE M M ⊀ H 1) β†’
      β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) β†’β‚—[π’ͺ]
      β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) β†’β‚—[π’ͺ] π’ͺ :=
  Classical.epsilon fun B => Bfam.LevelBlock π’ͺ B ∧ Bfam.DegeneracyBlock π’ͺ B

namespace Bfam

section Corner

variable (π’ͺ : Type) [CommRing π’ͺ] (M : β„•) (H : Subgroup (ZMod M)Λ£) (h₁ : LevelLE M M ⊀ H 1)
variable {𝕋 : Type} [CommRing 𝕋] [Algebra π’ͺ 𝕋] [Module 𝕋 (H1 M H π’ͺ)] [IsScalarTower π’ͺ 𝕋 (H1 M H π’ͺ)]

def cornerInclusion (cd : H1CornerData (π’ͺ := π’ͺ) M H π’ͺ 𝕋)
    (hW : βˆ€ v : H1 M H π’ͺ, v ∈ cornerSubmodule (M := H1 M H π’ͺ) (cd.split.e cd.idx) β†’
      v ∈ (ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) :
    cd.cornerModule β†’β‚—[π’ͺ]
      β†₯((ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) where
  toFun x := ⟨x, hW _ x.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

@[simp] theorem cornerInclusion_apply (cd : H1CornerData (π’ͺ := π’ͺ) M H π’ͺ 𝕋)
    (hW : βˆ€ v : H1 M H π’ͺ, v ∈ cornerSubmodule (M := H1 M H π’ͺ) (cd.split.e cd.idx) β†’
      v ∈ (ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁))
    (x : cd.cornerModule) :
    cornerInclusion π’ͺ M H h₁ cd hW x = ⟨x, hW _ x.2⟩ := rfl

def cornerRestrict (cd : H1CornerData (π’ͺ := π’ͺ) M H π’ͺ 𝕋)
    (hW : βˆ€ v : H1 M H π’ͺ, v ∈ cornerSubmodule (M := H1 M H π’ͺ) (cd.split.e cd.idx) β†’
      v ∈ (ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) :
    cd.cornerModule β†’β‚—[π’ͺ] cd.cornerModule β†’β‚—[π’ͺ] π’ͺ :=
  (Bfam π’ͺ M H h₁).compl₁₂ (cornerInclusion π’ͺ M H h₁ cd hW) (cornerInclusion π’ͺ M H h₁ cd hW)

@[simp] theorem cornerRestrict_apply (cd : H1CornerData (π’ͺ := π’ͺ) M H π’ͺ 𝕋)
    (hW : βˆ€ v : H1 M H π’ͺ, v ∈ cornerSubmodule (M := H1 M H π’ͺ) (cd.split.e cd.idx) β†’
      v ∈ (ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁))
    (x y : cd.cornerModule) :
    cornerRestrict π’ͺ M H h₁ cd hW x y = Bfam π’ͺ M H h₁ ⟨x, hW _ x.2⟩ ⟨y, hW _ y.2⟩ := rfl

theorem pairing_eq_cornerRestrict_iff (cd : H1CornerData (π’ͺ := π’ͺ) M H π’ͺ 𝕋)
    (hW : βˆ€ v : H1 M H π’ͺ, v ∈ cornerSubmodule (M := H1 M H π’ͺ) (cd.split.e cd.idx) β†’
      v ∈ (ModularCurve.Period.parabolicHoms π’ͺ (GammaH M ⊀) π’ͺ).map (iDegL M M ⊀ H 1 π’ͺ π’ͺ h₁)) :
    cd.pairing.B = cornerRestrict π’ͺ M H h₁ cd hW ↔
      βˆ€ x y : cd.cornerModule, cd.pairing.B x y = Bfam π’ͺ M H h₁ ⟨x, hW _ x.2⟩ ⟨y, hW _ y.2⟩ := by
  constructor
  Β· intro h x y
    rw [h]
    rfl
  Β· intro h
    exact LinearMap.extβ‚‚ fun x y => h x y

end Corner

end Bfam

namespace Bfamβ‚€

variable (π’ͺ : Type) [CommRing π’ͺ]

def Block
    (B : (M : β„•) β†’ β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ) β†’β‚—[π’ͺ]
        β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ) β†’β‚—[π’ͺ] π’ͺ) : Prop :=
  (βˆ€ (M : β„•) [NeZero M],
    Function.Bijective (B M) ∧
    (βˆ€ (β„“ : β„•) [NeZero β„“] (x y Tx Ty : β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ)),
        (Tx : CohCarrier.H1 M ⊀ π’ͺ) = CohCarrier.heckeT M ⊀ β„“ π’ͺ x β†’
        (Ty : CohCarrier.H1 M ⊀ π’ͺ) = CohCarrier.heckeT M ⊀ β„“ π’ͺ y β†’ B M Tx y = B M x Ty) ∧
    (βˆ€ (d : (ZMod M)Λ£) (x y Dx Dy : β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ)),
        (Dx : CohCarrier.H1 M ⊀ π’ͺ) = CohCarrier.diamondL M ⊀ π’ͺ d x β†’
        (Dy : CohCarrier.H1 M ⊀ π’ͺ) = CohCarrier.diamondL M ⊀ π’ͺ d y β†’ B M Dx y = B M x Dy)) ∧
  (βˆ€ (M M' : β„•) [NeZero M'] (d d' : β„•) [NeZero d] [NeZero d']
      (h : CohCarrier.LevelLE M M' ⊀ ⊀ d) (h' : CohCarrier.LevelLE M M' ⊀ ⊀ d') (hdd' : d * d' = M' / M)
      (x : β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ))
      (y : β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M' ⊀) π’ͺ))
      (ix : β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M' ⊀) π’ͺ))
      (jy : β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ)),
      (ix : CohCarrier.H1 M' ⊀ π’ͺ) = CohCarrier.iDegL M M' ⊀ ⊀ d π’ͺ π’ͺ h x β†’
      (jy : CohCarrier.H1 M ⊀ π’ͺ) = CohCarrier.jDegL M M' ⊀ ⊀ d' π’ͺ π’ͺ h' y β†’
      B M jy x = B M' y ix)

end Bfamβ‚€

def Bfamβ‚€ (π’ͺ : Type) [CommRing π’ͺ] :
    (M : β„•) β†’ β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ) β†’β‚—[π’ͺ]
      β†₯(ModularCurve.Period.parabolicHoms π’ͺ (CohCarrier.GammaH M ⊀) π’ͺ) β†’β‚—[π’ͺ] π’ͺ :=
  Classical.epsilon (Bfamβ‚€.Block π’ͺ)

end CuspForm

end

Statements phrased using this module (11)