Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CohCarrier_HeckeData.lean

definition module

Abstract commuting Hecke operators and localisation at an eigensystem

Fix a commutative ring \mathcal{O}, an \mathcal{O}-module V and a field k that is an \mathcal{O}-algebra. A term of CohCarrier.HeckeData consists of four data: a type Gen of generator indices; a family op : Gen β†’ Module.End π’ͺ V of \mathcal{O}-linear endomorphisms of V; a proof field comm asserting that any two of these endomorphisms commute; and a function ΞΈbar : Gen β†’ k, to be thought of as the system of residual eigenvalues attached to the generators. Nothing else is assumed: no relations among the generators and no compatibility between op and ΞΈbar.

From such data the module builds the following. FreeAlg is the polynomial algebra \mathcal{O}[X_g : g \in \mathrm{Gen}] in one variable per generator; thetaTilde is the \mathcal{O}-algebra map \mathcal{O}[X_g] \to k evaluating X_g at ΞΈbar g, and mTheta is its kernel, an ideal of FreeAlg registered as prime. opSubalgebra is the \mathcal{O}-subalgebra of \mathrm{End}_{\mathcal{O}}(V) generated by the range of op; since the generators commute pairwise (op_comm_of_mem), this subalgebra is commutative, and opAlgHom : FreeAlg →ₐ[π’ͺ] Module.End π’ͺ V is the evaluation map factoring through it, characterised by X_g \mapsto op g (opAlgHom_X). Restriction of scalars along opAlgHom gives moduleFreeAlg, a FreeAlg-module structure on V, used as a file-local instance; algebraMap_freeAlg_smul records that the action of \mathcal{O} obtained through FreeAlg is the original one, whence the scalar tower instance V_isScalarTower for \mathcal{O} \to FreeAlg \to V. Finally ML is the localisation of V at the multiplicative complement of mTheta, a module over the localisation of FreeAlg at that prime as well as over FreeAlg and over \mathcal{O}; toML is the canonical FreeAlg-linear map V \to ML, and toMLβ‚’ its restriction of scalars to \mathcal{O}.

Relation to Mathlib

Mathlib has no notion of abstract Hecke data; this structure and the constructions around it are the project's own packaging, built on Mathlib's MvPolynomial, Algebra.adjoin, Module.compHom and LocalizedModule.

Where it is used

This is the shape in which Hecke modules are presented for localisation at a residual eigensystem: a commuting family of operators, a prime of the free polynomial algebra cut out by the residual eigenvalues, and the localised module with its canonical map from V. It is instantiated on the cohomological carriers occurring in the modularity-lifting argument, where the localised modules are the ones fed into the patching construction.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, Β§3

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.Algebra.Module.LocalizedModule.Basic β†—
import Mathlib.Algebra.MvPolynomial.CommRing β†—
import Mathlib.RingTheory.Ideal.Maps β†—
import Mathlib.Algebra.Algebra.Subalgebra.Lattice β†—

set_option autoImplicit false

noncomputable section

namespace CohCarrier

universe u v w

structure HeckeData (π’ͺ : Type u) [CommRing π’ͺ] (V : Type v) [AddCommGroup V] [Module π’ͺ V]
    (k : Type w) [Field k] [Algebra π’ͺ k] where

  Gen : Type

  op : Gen β†’ Module.End π’ͺ V

  comm : βˆ€ g h : Gen, op g * op h = op h * op g

  ΞΈbar : Gen β†’ k

namespace HeckeData

variable {π’ͺ : Type u} [CommRing π’ͺ] {V : Type v} [AddCommGroup V] [Module π’ͺ V]
  {k : Type w} [Field k] [Algebra π’ͺ k] (D : HeckeData π’ͺ V k)

abbrev FreeAlg : Type u := MvPolynomial D.Gen π’ͺ

noncomputable def thetaTilde : D.FreeAlg →ₐ[π’ͺ] k := MvPolynomial.aeval D.ΞΈbar

def mTheta : Ideal D.FreeAlg := RingHom.ker D.thetaTilde.toRingHom

instance mTheta_isPrime : D.mTheta.IsPrime := RingHom.ker_isPrime _

noncomputable def opSubalgebra : Subalgebra π’ͺ (Module.End π’ͺ V) := Algebra.adjoin π’ͺ (Set.range D.op)

theorem op_comm_of_mem : βˆ€ a ∈ Set.range D.op, βˆ€ b ∈ Set.range D.op, a * b = b * a := by
  rintro _ ⟨g, rfl⟩ _ ⟨h, rfl⟩
  exact D.comm g h

instance opSubalgebra_isMulCommutative : IsMulCommutative β†₯D.opSubalgebra :=
  Algebra.isMulCommutative_adjoin π’ͺ D.op_comm_of_mem

open scoped IsMulCommutative

noncomputable def opAlgHom : D.FreeAlg →ₐ[π’ͺ] Module.End π’ͺ V :=
  (D.opSubalgebra.val).comp
    (MvPolynomial.aeval fun g => (⟨D.op g, Algebra.subset_adjoin (Set.mem_range_self g)⟩ :
      β†₯D.opSubalgebra))

@[simp] theorem opAlgHom_X (g : D.Gen) : D.opAlgHom (MvPolynomial.X g) = D.op g := by
  simp [opAlgHom]

@[reducible] noncomputable def moduleFreeAlg : Module D.FreeAlg V :=
  Module.compHom V D.opAlgHom.toRingHom

attribute [local instance] moduleFreeAlg

noncomputable abbrev ML : Type (max u v) := LocalizedModule D.mTheta.primeCompl V

example : AddCommGroup D.ML := inferInstance
example : Module (Localization D.mTheta.primeCompl) D.ML := inferInstance
example : Module D.FreeAlg D.ML := inferInstance

noncomputable def toML : V β†’β‚—[D.FreeAlg] D.ML := LocalizedModule.mkLinearMap D.mTheta.primeCompl V

theorem algebraMap_freeAlg_smul (r : π’ͺ) (v : V) : (algebraMap π’ͺ D.FreeAlg r) β€’ v = r β€’ v := by
  show D.opAlgHom (algebraMap π’ͺ D.FreeAlg r) v = r β€’ v
  rw [AlgHom.commutes]
  rfl

instance V_isScalarTower : IsScalarTower π’ͺ D.FreeAlg V :=
  ⟨fun r a v => by rw [Algebra.smul_def, mul_smul, algebraMap_freeAlg_smul]⟩

example : Module π’ͺ D.ML := inferInstance

example : IsScalarTower π’ͺ (Localization D.mTheta.primeCompl) D.ML := inferInstance

example : IsScalarTower π’ͺ D.FreeAlg D.ML := inferInstance

noncomputable def toMLβ‚’ : V β†’β‚—[π’ͺ] D.ML := D.toML.restrictScalars π’ͺ

@[simp] theorem toMLβ‚’_apply (v : V) : D.toMLβ‚’ v = D.toML v := rfl

end HeckeData

end CohCarrier

end

Statements phrased using this module (9)