Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CohCarrier_LevelPairing.lean

definition module

Corner data, degeneracy descents and leg data

Throughout, \mathcal{O} is a commutative ring, \mathbb{T} a commutative \mathcal{O}-algebra and V an \mathcal{O}-module with a compatible \mathbb{T}-action. A CornerData on (\mathbb{T},V) consists of three pieces: an IdempotentSplitting of \mathbb{T}, i.e. a finite family of idempotents e_0,\dots,e_{n-1} forming a complete orthogonal system together with maximal ideals \mathfrak{m}_i exhausting all maximal ideals of \mathbb{T} and satisfying e_i \in \mathfrak{m}_j \iff i \neq j; a chosen index idx; and a LevelPairing over the corner ring e_{\mathrm{idx}}\mathbb{T}e_{\mathrm{idx}} on the corner submodule e_{\mathrm{idx}} \cdot V, that is an \mathcal{O}-bilinear form B with values in \mathcal{O} which is self-adjoint for the corner-ring action and perfect in the sense that m \mapsto B(m,-) is bijective. The abbreviations cornerRing and cornerModule name the corner ring and corner submodule attached to the chosen index.

Given corner data cd on (\mathbb{T},V) and cd' on (\mathbb{T}',V'), a DegeneracyDescent of length n is a pair of families of \mathcal{O}-linear maps \mathrm{iRaw}_k : V \to V' and \mathrm{jRaw}_k : V' \to V, k \in \mathrm{Fin}\,n, each carrying the chosen corner submodule into the chosen corner submodule; iLeg and jLeg are the resulting maps between the corner modules, with the evident compatibility of underlying elements recorded. The map toLegDatum converts such a descent, together with a table \mathbb{T}-valued matrix (t_{k,k'}) in the corner ring, a proof that each \mathrm{jLeg}_k is adjoint to \mathrm{iLeg}_k for the two pairings, and a proof that \mathrm{jLeg}_k \circ \mathrm{iLeg}_{k'} = t_{k,k'}\cdot(-), into a RungAssembly.LegDatum between the two level pairings; three lemmas identify its components with the given data.

Finally H1CornerData specialises CornerData to V = the \mathcal{O}-module \mathrm{Hom}(\Gamma_H(M)^{\mathrm{ab,add}}, A) of additive characters of \Gamma_H(M), the subgroup of \mathrm{SL}_2(\mathbb{Z}) of matrices in \Gamma_0(M) whose lower-right entry reduces into H \leq (\mathbb{Z}/M)^\times.

Relation to Mathlib

The structures CornerData, DegeneracyDescent and the target LegDatum are the project's own; they are built on Mathlib's CompleteOrthogonalIdempotents and corner ring IsIdempotentElem.Corner, and on Mathlib's congruence subgroups \Gamma_0(M), \Gamma(M).

Where it is used

Corner data localise a Hecke algebra at a maximal ideal and equip the corresponding direct summand of degree-one group cohomology with a perfect self-adjoint pairing; degeneracy descents record the level-changing maps between two such summands. Feeding a descent through toLegDatum and then through the rung assembly produces the RungDatum whose Ihara and eta clauses are the inputs to the level-changing step of the modularity argument.

References

  1. K. A. Ribet, Congruence relations between modular forms, Proceedings of the International Congress of Mathematicians (Warsaw, 1983), PWN, Warsaw, 1984, 503–514

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

Imports

Imported by

Declarations

Source

import Definitions.Def_CohCarrier_Level
import Definitions.Def_HeckeModule_IharaRungDatum
import Definitions.Def_HeckeModule_IharaDataAt

set_option autoImplicit false

namespace IharaTower

open IharaLemma

variable {π’ͺ : Type} [CommRing π’ͺ]

structure CornerData (𝕋 : Type) [CommRing 𝕋] [Algebra π’ͺ 𝕋]
    (V : Type) [AddCommGroup V] [Module π’ͺ V] [Module 𝕋 V] [IsScalarTower π’ͺ 𝕋 V] : Type where
  split : IdempotentSplitting 𝕋
  idx : Fin split.n
  pairing : LevelPairing (π’ͺ := π’ͺ) (split.CornerRing idx)
    β†₯(cornerSubmodule (M := V) (split.e idx))

namespace CornerData

variable {𝕋 : Type} [CommRing 𝕋] [Algebra π’ͺ 𝕋]
variable {V : Type} [AddCommGroup V] [Module π’ͺ V] [Module 𝕋 V] [IsScalarTower π’ͺ 𝕋 V]

abbrev cornerRing (cd : CornerData (π’ͺ := π’ͺ) 𝕋 V) : Type := cd.split.CornerRing cd.idx

abbrev cornerModule (cd : CornerData (π’ͺ := π’ͺ) 𝕋 V) : Type :=
  β†₯(cornerSubmodule (M := V) (cd.split.e cd.idx))

end CornerData

variable {𝕋 : Type} [CommRing 𝕋] [Algebra π’ͺ 𝕋]
variable {V : Type} [AddCommGroup V] [Module π’ͺ V] [Module 𝕋 V] [IsScalarTower π’ͺ 𝕋 V]
variable {𝕋' : Type} [CommRing 𝕋'] [Algebra π’ͺ 𝕋']
variable {V' : Type} [AddCommGroup V'] [Module π’ͺ V'] [Module 𝕋' V'] [IsScalarTower π’ͺ 𝕋' V']

structure DegeneracyDescent (cd : CornerData (π’ͺ := π’ͺ) 𝕋 V)
    (cd' : CornerData (π’ͺ := π’ͺ) 𝕋' V') (n : β„•) : Type where
  iRaw : Fin n β†’ V β†’β‚—[π’ͺ] V'
  jRaw : Fin n β†’ V' β†’β‚—[π’ͺ] V
  corner_i : βˆ€ (k : Fin n) (v : V), v ∈ cornerSubmodule (M := V) (cd.split.e cd.idx) β†’
    iRaw k v ∈ cornerSubmodule (M := V') (cd'.split.e cd'.idx)
  corner_j : βˆ€ (k : Fin n) (v' : V'), v' ∈ cornerSubmodule (M := V') (cd'.split.e cd'.idx) β†’
    jRaw k v' ∈ cornerSubmodule (M := V) (cd.split.e cd.idx)

namespace DegeneracyDescent

variable {cd : CornerData (π’ͺ := π’ͺ) 𝕋 V} {cd' : CornerData (π’ͺ := π’ͺ) 𝕋' V'} {n : β„•}

noncomputable def iLeg (D : DegeneracyDescent cd cd' n) (k : Fin n) :
    cd.cornerModule β†’β‚—[π’ͺ] cd'.cornerModule where
  toFun v := ⟨D.iRaw k v, D.corner_i k v v.2⟩
  map_add' := by intro a b; apply Subtype.ext; simp
  map_smul' := by intro r a; apply Subtype.ext; simp

noncomputable def jLeg (D : DegeneracyDescent cd cd' n) (k : Fin n) :
    cd'.cornerModule β†’β‚—[π’ͺ] cd.cornerModule where
  toFun v' := ⟨D.jRaw k v', D.corner_j k v' v'.2⟩
  map_add' := by intro a b; apply Subtype.ext; simp
  map_smul' := by intro r a; apply Subtype.ext; simp

@[simp] theorem iLeg_apply (D : DegeneracyDescent cd cd' n) (k : Fin n)
    (v : cd.cornerModule) : (↑(D.iLeg k v) : V') = D.iRaw k ↑v := rfl

@[simp] theorem jLeg_apply (D : DegeneracyDescent cd cd' n) (k : Fin n)
    (v' : cd'.cornerModule) : (↑(D.jLeg k v') : V) = D.jRaw k ↑v' := rfl

noncomputable def toLegDatum (D : DegeneracyDescent cd cd' n)
    (table : Fin n β†’ Fin n β†’ cd.cornerRing)
    (adjoint_leg : βˆ€ (k : Fin n) (m' : cd'.cornerModule) (m : cd.cornerModule),
      cd.pairing.B (D.jLeg k m') m = cd'.pairing.B m' (D.iLeg k m))
    (htable : βˆ€ (k k' : Fin n) (m : cd.cornerModule),
      D.jLeg k (D.iLeg k' m) = table k k' β€’ m) :
    RungAssembly.LegDatum (π’ͺ := π’ͺ) cd.pairing cd'.pairing n :=
  ⟨D.iLeg, D.jLeg, adjoint_leg, table, htable⟩

theorem toLegDatum_iLeg (D : DegeneracyDescent cd cd' n) (table : Fin n β†’ Fin n β†’ cd.cornerRing)
    (adjoint_leg : βˆ€ (k : Fin n) (m' : cd'.cornerModule) (m : cd.cornerModule),
      cd.pairing.B (D.jLeg k m') m = cd'.pairing.B m' (D.iLeg k m))
    (htable : βˆ€ (k k' : Fin n) (m : cd.cornerModule),
      D.jLeg k (D.iLeg k' m) = table k k' β€’ m) :
    (D.toLegDatum table adjoint_leg htable).iLeg = D.iLeg := rfl

theorem toLegDatum_jLeg (D : DegeneracyDescent cd cd' n) (table : Fin n β†’ Fin n β†’ cd.cornerRing)
    (adjoint_leg : βˆ€ (k : Fin n) (m' : cd'.cornerModule) (m : cd.cornerModule),
      cd.pairing.B (D.jLeg k m') m = cd'.pairing.B m' (D.iLeg k m))
    (htable : βˆ€ (k k' : Fin n) (m : cd.cornerModule),
      D.jLeg k (D.iLeg k' m) = table k k' β€’ m) :
    (D.toLegDatum table adjoint_leg htable).jLeg = D.jLeg := rfl

theorem toLegDatum_table (D : DegeneracyDescent cd cd' n) (table : Fin n β†’ Fin n β†’ cd.cornerRing)
    (adjoint_leg : βˆ€ (k : Fin n) (m' : cd'.cornerModule) (m : cd.cornerModule),
      cd.pairing.B (D.jLeg k m') m = cd'.pairing.B m' (D.iLeg k m))
    (htable : βˆ€ (k k' : Fin n) (m : cd.cornerModule),
      D.jLeg k (D.iLeg k' m) = table k k' β€’ m) :
    (D.toLegDatum table adjoint_leg htable).table = table := rfl

end DegeneracyDescent

open CohCarrier in

abbrev H1CornerData (M : β„•) (H : Subgroup (ZMod M)Λ£) (A : Type) [AddCommGroup A] [Module π’ͺ A]
    (𝕋 : Type) [CommRing 𝕋] [Algebra π’ͺ 𝕋] [Module 𝕋 (H1 M H A)]
    [IsScalarTower π’ͺ 𝕋 (H1 M H A)] : Type :=
  CornerData (π’ͺ := π’ͺ) 𝕋 (H1 M H A)

end IharaTower

Statements phrased using this module (35)