Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_HeckeLocal.lean

definition module

The local Hecke coefficient ring

Fix a level N\ge 1, a set S of excluded primes, a complete discrete valuation ring \mathcal{O} and a ring homomorphism \theta from the weight-2 Hecke algebra heckeAlgebra N 2 S (the \mathbb{Z}-subalgebra of \operatorname{End}_{\mathbb{C}} of cusp forms on \Gamma_0(N) generated by the operators T_\ell for \ell prime, \ell\nmid N, \ell\notin S, and U_q for q\mid N prime, q\notin S) to the residue field of \mathcal{O}. An element of this Hecke algebra preserves intLattice N 2, the \mathbb{Z}-span of the cusp forms all of whose q-expansion coefficients are rational integers, and latticeRestrict is its restriction to that lattice; latticeActionHom assembles these restrictions into a ring homomorphism into \operatorname{End}_{\mathbb{Z}} of the lattice, and heckeLatticeAlgebra is its image, a \mathbb{Z}-subalgebra shown to be commutative and finite and free over \mathbb{Z} (the lattice itself being finitely generated and torsion-free). The induced map latticeRestrictHom onto it is surjective, and injective — hence bijective — as soon as HasIntegralStructure N 2 holds, i.e. the \mathbb{C}-span of the integral lattice is everything.

On the base algebra heckeBaseAlgebra N S 𝒪 =\mathcal{O}\otimes_{\mathbb{Z}} heckeLatticeAlgebra, latticeBaseChange is the base change of latticeRestrictHom, surjective in general and injective under an integral structure. The homomorphism residualCharacter, sending a\otimes t to the residue of a times \theta(t), is surjective, so its kernel heckeCharKernel is a maximal ideal of \mathcal{O}\otimes_{\mathbb{Z}} heckeAlgebra; heckeLocalIdeal is its image in the base algebra, maximal whenever the kernel of latticeBaseChange is contained in heckeCharKernel. The carrier heckeLocal N S 𝒪 θ is the localisation of the base algebra at heckeLocalSubmonoid, the image of the complement of heckeCharKernel; under the above containment this submonoid is exactly the complement of heckeLocalIdeal, so the localisation is the local ring at that maximal ideal. The map heckeLocal.π is the resulting homomorphism from the Hecke algebra. Registered instances make heckeLocal an \mathcal{O}-algebra which is Noetherian and finite and free over \mathcal{O} unconditionally (argued through a dichotomy: either 0 lies in the submonoid and the localisation is the zero ring, or one is at a maximal ideal and uses the splitting of a module-finite algebra over a complete local ring into its local factors at maximal ideals), and, assuming HasIntegralStructure N 2, a complete local ring with \mathcal{O}\to heckeLocal a local homomorphism.

Relation to Mathlib

The localisation apparatus (Localization, IsLocalization.AtPrime, freeness and finiteness transfer) is Mathlib's; the Hecke algebra of \Gamma_0(N) in weight 2, the lattice of cusp forms with integral q-expansion and the local Hecke ring built here are the project's own notions.

Where it is used

The ring heckeLocal is the coefficient ring on the Hecke side of the R=\mathbb{T} comparison: its registered instances (complete local Noetherian, finite and free over \mathcal{O}, with local structure map) are precisely the typeclass assumptions required of the ring T in HeckeGaloisRepDatum, the datum carrying the Galois representation attached to the residual eigensystem \theta together with the Eichler–Shimura characteristic polynomial conditions at good primes.

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
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005

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

Imports

Theorems imported by this definition module

Imported by

Declarations

Source

import Definitions.Def_CuspForm_HeckeGaloisRepDatum
import Definitions.Def_CuspForm_IntegralStructure
import Theorems.Thm_CuspForm_mem_intLattice_of_mem_heckeAlgebra
import Theorems.Thm_CuspForm_intLattice_fg
import Theorems.Thm_IsLocalRing_isAdicComplete_of_module_finite
import Theorems.Thm_Algebra_finite_maximalSpectrum_and_bijective_localization_of_module_finite

set_option autoImplicit false

noncomputable section

open scoped TensorProduct

namespace CuspForm

variable (N : ℕ) [NeZero N] (S : Set ℕ)

def latticeRestrict {t : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) 2)}
    (ht : t ∈ heckeAlgebra N 2 S) : Module.End ℤ ↥(intLattice N 2) :=
  LinearMap.restrict (t.restrictScalars ℤ)
    (fun _f hf => mem_intLattice_of_mem_heckeAlgebra one_le_two ht hf)

def latticeActionHom : ↥(heckeAlgebra N 2 S) →+* Module.End ℤ ↥(intLattice N 2) where
  toFun t := latticeRestrict N S t.2
  map_one' := LinearMap.ext fun _ => Subtype.ext rfl
  map_mul' _ _ := LinearMap.ext fun _ => Subtype.ext rfl
  map_zero' := LinearMap.ext fun _ => Subtype.ext rfl
  map_add' _ _ := LinearMap.ext fun _ => Subtype.ext rfl

def heckeLatticeAlgebra : Subalgebra ℤ (Module.End ℤ ↥(intLattice N 2)) :=
  ((latticeActionHom N S).toIntAlgHom).range

theorem intLattice.moduleFinite : Module.Finite ℤ ↥(intLattice N 2) :=
  Module.Finite.iff_fg.mpr (intLattice_fg N 2)

omit [NeZero N] in

theorem isAddTorsionFree_cuspForm : IsAddTorsionFree (CuspForm (CongruenceSubgroup.Gamma0 N) 2) :=
  .of_isTorsionFree ℂ _

theorem intLattice.moduleFree : Module.Free ℤ ↥(intLattice N 2) := by
  haveI := intLattice.moduleFinite N
  haveI := isAddTorsionFree_cuspForm N
  exact Module.free_of_finite_type_torsion_free'

omit [NeZero N] in

theorem intLattice.isAddTorsionFree_end : IsAddTorsionFree (Module.End ℤ ↥(intLattice N 2)) where
  nsmul_right_injective n hn a b hab := by
    haveI := isAddTorsionFree_cuspForm N
    refine LinearMap.ext fun f => Subtype.ext ?_
    have h : n • ((a f : ↥(intLattice N 2)) : CuspForm (CongruenceSubgroup.Gamma0 N) 2) =
        n • ((b f : ↥(intLattice N 2)) : CuspForm (CongruenceSubgroup.Gamma0 N) 2) := by
      simpa using congrArg (fun g : Module.End ℤ ↥(intLattice N 2) =>
        ((g f : ↥(intLattice N 2)) : CuspForm (CongruenceSubgroup.Gamma0 N) 2)) hab
    exact nsmul_right_injective hn h

instance heckeLatticeAlgebra.instModuleFinite : Module.Finite ℤ ↥(heckeLatticeAlgebra N S) := by
  haveI := intLattice.moduleFinite N
  haveI := intLattice.moduleFree N
  exact Module.Finite.of_injective (heckeLatticeAlgebra N S).val.toLinearMap Subtype.val_injective

theorem heckeLatticeAlgebra.isAddTorsionFree : IsAddTorsionFree ↥(heckeLatticeAlgebra N S) where
  nsmul_right_injective n hn a b hab := by
    haveI := intLattice.isAddTorsionFree_end N
    apply Subtype.ext
    have h : n • (a : Module.End ℤ ↥(intLattice N 2)) = n • (b : Module.End ℤ ↥(intLattice N 2)) :=
      congrArg Subtype.val hab
    exact nsmul_right_injective hn h

instance heckeLatticeAlgebra.instModuleFree : Module.Free ℤ ↥(heckeLatticeAlgebra N S) := by
  haveI := heckeLatticeAlgebra.isAddTorsionFree N S
  exact Module.free_of_finite_type_torsion_free'

def latticeRestrictHom : ↥(heckeAlgebra N 2 S) →ₐ[ℤ] ↥(heckeLatticeAlgebra N S) :=
  ((latticeActionHom N S).toIntAlgHom).rangeRestrict

instance heckeLatticeAlgebra.instCommRing : CommRing ↥(heckeLatticeAlgebra N S) :=
  { (inferInstance : Ring ↥(heckeLatticeAlgebra N S)) with
    mul_comm := by
      rintro ⟨_, s, rfl⟩ ⟨_, t, rfl⟩
      exact Subtype.ext ((map_mul _ s t).symm.trans ((congrArg _ (mul_comm s t)).trans (map_mul _ t s))) }

theorem latticeRestrict_injective (hint : HasIntegralStructure N 2)
    (t : ↥(heckeAlgebra N 2 S)) (h : latticeRestrict N S t.2 = 0) : t = 0 := by
  refine Subtype.ext (LinearMap.ext_on hint fun f hf => ?_)
  exact congrArg Subtype.val (LinearMap.congr_fun h ⟨f, hf⟩)

set_option synthInstance.maxHeartbeats 400000 in
theorem latticeActionHom_injective (hint : HasIntegralStructure N 2) :
    Function.Injective (latticeActionHom N S) :=
  (injective_iff_map_eq_zero _).mpr fun t ht => latticeRestrict_injective N S hint t ht

theorem latticeRestrictHom_surjective : Function.Surjective (latticeRestrictHom N S) :=
  AlgHom.rangeRestrict_surjective _

theorem latticeRestrictHom_bijective (hint : HasIntegralStructure N 2) :
    Function.Bijective (latticeRestrictHom N S) :=
  ⟨fun _ _ h => latticeActionHom_injective N S hint (congrArg Subtype.val h),
    latticeRestrictHom_surjective N S⟩

variable (𝒪 : Type) [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
  [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪]
variable (θ : heckeAlgebra N 2 S →+* IsLocalRing.ResidueField 𝒪)

def residualCharacter :
    (𝒪 ⊗[ℤ] ↥(heckeAlgebra N 2 S)) →ₐ[ℤ] IsLocalRing.ResidueField 𝒪 :=
  Algebra.TensorProduct.productMap
    (algebraMap 𝒪 (IsLocalRing.ResidueField 𝒪)).toIntAlgHom θ.toIntAlgHom

def heckeCharKernel : Ideal (𝒪 ⊗[ℤ] ↥(heckeAlgebra N 2 S)) :=
  RingHom.ker (residualCharacter N S 𝒪 θ)

instance heckeCharKernel.instIsPrime : (heckeCharKernel N S 𝒪 θ).IsPrime :=
  RingHom.ker_isPrime _

def heckeBaseAlgebra : Type := 𝒪 ⊗[ℤ] ↥(heckeLatticeAlgebra N S)

instance heckeBaseAlgebra.instCommRing : CommRing (heckeBaseAlgebra N S 𝒪) :=
  inferInstanceAs (CommRing (𝒪 ⊗[ℤ] ↥(heckeLatticeAlgebra N S)))

instance heckeBaseAlgebra.instAlgebra : Algebra 𝒪 (heckeBaseAlgebra N S 𝒪) :=
  inferInstanceAs (Algebra 𝒪 (𝒪 ⊗[ℤ] ↥(heckeLatticeAlgebra N S)))

def latticeBaseChange : (𝒪 ⊗[ℤ] ↥(heckeAlgebra N 2 S)) →+* heckeBaseAlgebra N S 𝒪 :=
  (Algebra.TensorProduct.map (AlgHom.id ℤ 𝒪) (latticeRestrictHom N S)).toRingHom

def heckeLocalSubmonoid : Submonoid (heckeBaseAlgebra N S 𝒪) :=
  (heckeCharKernel N S 𝒪 θ).primeCompl.map (latticeBaseChange N S 𝒪)

def heckeLocal : Type :=
  Localization (heckeLocalSubmonoid N S 𝒪 θ)

instance heckeLocal.instCommRing : CommRing (heckeLocal N S 𝒪 θ) :=
  inferInstanceAs (CommRing (Localization (heckeLocalSubmonoid N S 𝒪 θ)))

instance heckeLocal.instAlgebra : Algebra 𝒪 (heckeLocal N S 𝒪 θ) :=
  inferInstanceAs (Algebra 𝒪 (Localization (heckeLocalSubmonoid N S 𝒪 θ)))

instance heckeLocal.instAlgebraBase : Algebra (heckeBaseAlgebra N S 𝒪) (heckeLocal N S 𝒪 θ) :=
  inferInstanceAs (Algebra (heckeBaseAlgebra N S 𝒪) (Localization (heckeLocalSubmonoid N S 𝒪 θ)))

instance heckeLocal.instIsScalarTower :
    IsScalarTower 𝒪 (heckeBaseAlgebra N S 𝒪) (heckeLocal N S 𝒪 θ) :=
  inferInstanceAs (IsScalarTower 𝒪 (heckeBaseAlgebra N S 𝒪) (Localization (heckeLocalSubmonoid N S 𝒪 θ)))

instance heckeLocal.instIsLocalization :
    IsLocalization (heckeLocalSubmonoid N S 𝒪 θ) (heckeLocal N S 𝒪 θ) :=
  inferInstanceAs (IsLocalization (heckeLocalSubmonoid N S 𝒪 θ) (Localization (heckeLocalSubmonoid N S 𝒪 θ)))

def heckeLocal.π : ↥(heckeAlgebra N 2 S) →+* heckeLocal N S 𝒪 θ :=
  ((algebraMap (heckeBaseAlgebra N S 𝒪) (heckeLocal N S 𝒪 θ)).comp (latticeBaseChange N S 𝒪)).comp
    Algebra.TensorProduct.includeRight.toRingHom

section Structure

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 1000000

omit [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪]

theorem residualCharacter_tmul (a : 𝒪) (t : ↥(heckeAlgebra N 2 S)) :
    residualCharacter N S 𝒪 θ (a ⊗ₜ t) = IsLocalRing.residue 𝒪 a * θ t := rfl

theorem residualCharacter_algebraMap (a : 𝒪) :
    residualCharacter N S 𝒪 θ (algebraMap 𝒪 _ a) = IsLocalRing.residue 𝒪 a := by
  rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    residualCharacter_tmul, map_one, mul_one]

theorem residualCharacter_surjective : Function.Surjective (residualCharacter N S 𝒪 θ) :=
  fun x => by
    obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective x
    exact ⟨algebraMap 𝒪 _ a, residualCharacter_algebraMap N S 𝒪 θ a⟩

instance heckeCharKernel.instIsMaximal : (heckeCharKernel N S 𝒪 θ).IsMaximal :=
  RingHom.ker_isMaximal_of_surjective _ (residualCharacter_surjective N S 𝒪 θ)

theorem mem_heckeCharKernel_iff (x : 𝒪 ⊗[ℤ] ↥(heckeAlgebra N 2 S)) :
    x ∈ heckeCharKernel N S 𝒪 θ ↔ residualCharacter N S 𝒪 θ x = 0 := RingHom.mem_ker

theorem algebraMap_mem_heckeCharKernel_iff (a : 𝒪) :
    algebraMap 𝒪 (𝒪 ⊗[ℤ] ↥(heckeAlgebra N 2 S)) a ∈ heckeCharKernel N S 𝒪 θ ↔
      a ∈ IsLocalRing.maximalIdeal 𝒪 := by
  rw [mem_heckeCharKernel_iff, residualCharacter_algebraMap, IsLocalRing.residue_eq_zero_iff]

omit [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] in
theorem latticeBaseChange_tmul (a : 𝒪) (t : ↥(heckeAlgebra N 2 S)) :
    latticeBaseChange N S 𝒪 (a ⊗ₜ t) =
      (a ⊗ₜ[ℤ] latticeRestrictHom N S t : 𝒪 ⊗[ℤ] ↥(heckeLatticeAlgebra N S)) := rfl

omit [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] in
theorem latticeBaseChange_algebraMap (a : 𝒪) :
    latticeBaseChange N S 𝒪 (algebraMap 𝒪 _ a) = algebraMap 𝒪 (heckeBaseAlgebra N S 𝒪) a := by
  rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    latticeBaseChange_tmul, map_one]
  rfl

omit [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] in

theorem latticeBaseChange_surjective : Function.Surjective (latticeBaseChange N S 𝒪) :=
  Algebra.TensorProduct.map_surjective _ _ Function.surjective_id (latticeRestrictHom_surjective N S)

omit [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] in

theorem latticeBaseChange_injective (hint : HasIntegralStructure N 2) :
    Function.Injective (latticeBaseChange N S 𝒪) :=
  (Algebra.TensorProduct.congr (AlgEquiv.refl : 𝒪 ≃ₐ[ℤ] 𝒪)
    (AlgEquiv.ofBijective (latticeRestrictHom N S) (latticeRestrictHom_bijective N S hint))).injective

def heckeLocalIdeal : Ideal (heckeBaseAlgebra N S 𝒪) :=
  (heckeCharKernel N S 𝒪 θ).map (latticeBaseChange N S 𝒪)

theorem comap_heckeLocalIdeal
    (hker : RingHom.ker (latticeBaseChange N S 𝒪) ≤ heckeCharKernel N S 𝒪 θ) :
    (heckeLocalIdeal N S 𝒪 θ).comap (latticeBaseChange N S 𝒪) = heckeCharKernel N S 𝒪 θ := by
  rw [heckeLocalIdeal, Ideal.comap_map_of_surjective _ (latticeBaseChange_surjective N S 𝒪),
    sup_eq_left]
  exact hker

theorem heckeLocalIdeal_isMaximal
    (hker : RingHom.ker (latticeBaseChange N S 𝒪) ≤ heckeCharKernel N S 𝒪 θ) :
    (heckeLocalIdeal N S 𝒪 θ).IsMaximal := by
  refine (Ideal.map_eq_top_or_isMaximal_of_surjective _ (latticeBaseChange_surjective N S 𝒪)
    (heckeCharKernel.instIsMaximal N S 𝒪 θ)).resolve_left fun htop => ?_
  apply (heckeCharKernel.instIsMaximal N S 𝒪 θ).ne_top
  rw [← comap_heckeLocalIdeal N S 𝒪 θ hker, heckeLocalIdeal, htop, Ideal.comap_top]

theorem mem_heckeLocalSubmonoid_iff
    (hker : RingHom.ker (latticeBaseChange N S 𝒪) ≤ heckeCharKernel N S 𝒪 θ)
    (x : heckeBaseAlgebra N S 𝒪) :
    x ∈ heckeLocalSubmonoid N S 𝒪 θ ↔ x ∉ heckeLocalIdeal N S 𝒪 θ := by
  constructor
  · rintro ⟨a, ha, rfl⟩ hx
    refine Ideal.mem_primeCompl_iff.mp ha ?_
    rw [← comap_heckeLocalIdeal N S 𝒪 θ hker]
    exact Ideal.mem_comap.mpr hx
  · intro hx
    obtain ⟨a, rfl⟩ := latticeBaseChange_surjective N S 𝒪 x
    exact ⟨a, Ideal.mem_primeCompl_iff.mpr fun ha => hx (Ideal.mem_map_of_mem _ ha), rfl⟩

section Hint

variable [Fact (HasIntegralStructure N 2)]

theorem ker_latticeBaseChange_le_heckeCharKernel :
    RingHom.ker (latticeBaseChange N S 𝒪) ≤ heckeCharKernel N S 𝒪 θ := fun x hx => by
  rw [RingHom.mem_ker] at hx
  rw [latticeBaseChange_injective N S 𝒪 Fact.out (hx.trans (map_zero _).symm)]
  exact zero_mem _

instance heckeLocalIdeal.instIsMaximal : (heckeLocalIdeal N S 𝒪 θ).IsMaximal :=
  heckeLocalIdeal_isMaximal N S 𝒪 θ (ker_latticeBaseChange_le_heckeCharKernel N S 𝒪 θ)

theorem heckeLocalSubmonoid_eq_primeCompl :
    heckeLocalSubmonoid N S 𝒪 θ = (heckeLocalIdeal N S 𝒪 θ).primeCompl :=
  Submonoid.ext fun x =>
    (mem_heckeLocalSubmonoid_iff N S 𝒪 θ (ker_latticeBaseChange_le_heckeCharKernel N S 𝒪 θ) x).trans
      Ideal.mem_primeCompl_iff.symm

instance heckeLocal.instIsLocalizationAtPrime :
    IsLocalization.AtPrime (heckeLocal N S 𝒪 θ) (heckeLocalIdeal N S 𝒪 θ) := by
  rw [IsLocalization.AtPrime, ← heckeLocalSubmonoid_eq_primeCompl N S 𝒪 θ]
  exact heckeLocal.instIsLocalization N S 𝒪 θ

theorem heckeLocal.isLocalRing : IsLocalRing (heckeLocal N S 𝒪 θ) :=
  IsLocalization.AtPrime.isLocalRing (heckeLocal N S 𝒪 θ) (heckeLocalIdeal N S 𝒪 θ)

theorem heckeLocal.isLocalHom_algebraMap : IsLocalHom (algebraMap 𝒪 (heckeLocal N S 𝒪 θ)) := by
  constructor
  intro a ha
  rw [IsScalarTower.algebraMap_apply 𝒪 (heckeBaseAlgebra N S 𝒪) (heckeLocal N S 𝒪 θ),
    IsLocalization.AtPrime.isUnit_to_map_iff (heckeLocal N S 𝒪 θ) (heckeLocalIdeal N S 𝒪 θ),
    Ideal.mem_primeCompl_iff, ← latticeBaseChange_algebraMap, ← Ideal.mem_comap,
    comap_heckeLocalIdeal N S 𝒪 θ (ker_latticeBaseChange_le_heckeCharKernel N S 𝒪 θ),
    algebraMap_mem_heckeCharKernel_iff] at ha
  exact IsLocalRing.notMem_maximalIdeal.mp ha

end Hint

end Structure

section TrioEngines

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 1000000

private lemma trio_isTorsionFree_finsupp (R : Type) [CommRing R] (ι : Type) :
    Module.IsTorsionFree R (ι →₀ R) where
  isSMulRegular r hr f g hfg := Finsupp.ext fun a => hr.isSMulRegular (M := R) (by
    have h := congrArg (fun h => h a) hfg
    simpa [Finsupp.smul_apply] using h)

private lemma trio_isTorsionFree_of_free (R : Type) [CommRing R] (B : Type) [AddCommGroup B]
    [Module R B] [Module.Free R B] : Module.IsTorsionFree R B := by
  haveI := trio_isTorsionFree_finsupp R (Module.Free.ChooseBasisIndex R B)
  set b := Module.Free.chooseBasis R B with hb
  exact Function.Injective.moduleIsTorsionFree (⇑b.repr) b.repr.injective
    fun r m => map_smul b.repr r m

private lemma trio_surjective_atPrime {R : Type} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (B : Type) [CommRing B] [Algebra R B] [Module.Finite R B] (P : MaximalSpectrum B) :
    Function.Surjective (algebraMap B (Localization.AtPrime P.asIdeal)) := by
  classical
  obtain ⟨-, hbij, -, -⟩ := Algebra.finite_maximalSpectrum_and_bijective_localization_of_module_finite (𝒪 := R) B
  intro z
  obtain ⟨b, hb⟩ := hbij.2 (Function.update 0 P z)
  refine ⟨b, ?_⟩
  have h := congrFun hb P
  simp only [Function.update_self] at h
  exact h

private lemma trio_isTorsionFree_atPrime {R : Type} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (B : Type) [CommRing B] [Algebra R B] [Module.Finite R B] [Module.Free R B]
    (P : MaximalSpectrum B) :
    Module.IsTorsionFree R (Localization.AtPrime P.asIdeal) := by
  classical
  obtain ⟨-, hbij, -, -⟩ := Algebra.finite_maximalSpectrum_and_bijective_localization_of_module_finite (𝒪 := R) B
  haveI htfB : Module.IsTorsionFree R B := trio_isTorsionFree_of_free R B
  set Φ : B →ₗ[R] ∀ Q : MaximalSpectrum B, Localization.AtPrime Q.asIdeal :=
    { toFun := fun a Q => algebraMap B (Localization.AtPrime Q.asIdeal) a
      map_add' := fun a b => funext fun Q => map_add _ a b
      map_smul' := fun c a => funext fun Q => by
        simp only [RingHom.id_apply, Pi.smul_apply, Algebra.smul_def, map_mul,
          ← IsScalarTower.algebraMap_apply] } with hPhidef
  have hPhibij : Function.Bijective Φ := hbij
  have hsingle : Function.Injective
      (Pi.single (M := fun Q : MaximalSpectrum B => Localization.AtPrime Q.asIdeal) P) := by
    intro x y hxy
    have h := congrFun hxy P
    simpa using h
  set e := LinearEquiv.ofBijective Φ hPhibij with hedef
  set g : Localization.AtPrime P.asIdeal →ₗ[R] B :=
    e.symm.toLinearMap ∘ₗ
      LinearMap.single R (fun Q : MaximalSpectrum B => Localization.AtPrime Q.asIdeal) P
    with hgdef
  have hginj : Function.Injective g := e.symm.injective.comp hsingle
  exact Function.Injective.moduleIsTorsionFree (⇑g) hginj fun r m => map_smul g r m

private lemma trio_free_atPrime {R : Type} [CommRing R] [IsDomain R] [IsLocalRing R]
    [IsPrincipalIdealRing R] [IsNoetherianRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (B : Type) [CommRing B] [Algebra R B] [Module.Finite R B] [Module.Free R B]
    (P : MaximalSpectrum B) : Module.Free R (Localization.AtPrime P.asIdeal) := by
  obtain ⟨-, -, hfin, -⟩ := Algebra.finite_maximalSpectrum_and_bijective_localization_of_module_finite (𝒪 := R) B
  haveI := hfin P
  haveI := trio_isTorsionFree_atPrime (R := R) B P
  exact Module.free_of_finite_type_torsion_free'

omit [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] in
private lemma trio_moduleFinite_base : Module.Finite 𝒪 (heckeBaseAlgebra N S 𝒪) :=
  inferInstanceAs (Module.Finite 𝒪 (𝒪 ⊗[ℤ] ↥(heckeLatticeAlgebra N S)))

omit [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] in
private lemma trio_moduleFree_base : Module.Free 𝒪 (heckeBaseAlgebra N S 𝒪) :=
  inferInstanceAs (Module.Free 𝒪 (𝒪 ⊗[ℤ] ↥(heckeLatticeAlgebra N S)))

omit [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] in
private lemma trio_isNoetherianRing_base : IsNoetherianRing (heckeBaseAlgebra N S 𝒪) := by
  haveI := trio_moduleFinite_base N S 𝒪
  exact IsNoetherianRing.of_finite 𝒪 (heckeBaseAlgebra N S 𝒪)

omit [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] in
private lemma trio_subsingleton_or_ker_le :
    Subsingleton (heckeLocal N S 𝒪 θ) ∨
      RingHom.ker (latticeBaseChange N S 𝒪) ≤ heckeCharKernel N S 𝒪 θ := by
  by_cases hker : RingHom.ker (latticeBaseChange N S 𝒪) ≤ heckeCharKernel N S 𝒪 θ
  · exact Or.inr hker
  · refine Or.inl ?_
    obtain ⟨x, hxk, hxm⟩ := SetLike.not_le_iff_exists.mp hker
    have h0 : (0 : heckeBaseAlgebra N S 𝒪) ∈ heckeLocalSubmonoid N S 𝒪 θ :=
      ⟨x, Ideal.mem_primeCompl_iff.mpr hxm, by
        rw [RingHom.mem_ker] at hxk
        exact hxk⟩
    exact IsLocalization.subsingleton h0

omit [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] in
private lemma trio_isLocalization_atPrime
    (hker : RingHom.ker (latticeBaseChange N S 𝒪) ≤ heckeCharKernel N S 𝒪 θ) :
    haveI := (heckeLocalIdeal_isMaximal N S 𝒪 θ hker).isPrime
    IsLocalization (heckeLocalIdeal N S 𝒪 θ).primeCompl (heckeLocal N S 𝒪 θ) := by
  haveI := (heckeLocalIdeal_isMaximal N S 𝒪 θ hker).isPrime
  have hsub : heckeLocalSubmonoid N S 𝒪 θ = (heckeLocalIdeal N S 𝒪 θ).primeCompl :=
    Submonoid.ext fun x => (mem_heckeLocalSubmonoid_iff N S 𝒪 θ hker x).trans
      Ideal.mem_primeCompl_iff.symm
  rw [← hsub]
  exact heckeLocal.instIsLocalization N S 𝒪 θ

end TrioEngines

instance heckeLocal.instIsNoetherianRing : IsNoetherianRing (heckeLocal N S 𝒪 θ) := by
  haveI := trio_isNoetherianRing_base N S 𝒪
  exact IsLocalization.isNoetherianRing (heckeLocalSubmonoid N S 𝒪 θ) (heckeLocal N S 𝒪 θ)
    inferInstance

instance heckeLocal.instModuleFinite : Module.Finite 𝒪 (heckeLocal N S 𝒪 θ) := by
  rcases trio_subsingleton_or_ker_le N S 𝒪 θ with hsub | hker
  · exact Module.Finite.of_surjective (0 : 𝒪 →ₗ[𝒪] heckeLocal N S 𝒪 θ)
      fun y => ⟨0, Subsingleton.elim _ _⟩
  · haveI := trio_moduleFinite_base N S 𝒪
    haveI hPmax : (heckeLocalIdeal N S 𝒪 θ).IsMaximal := heckeLocalIdeal_isMaximal N S 𝒪 θ hker
    haveI hloc := trio_isLocalization_atPrime N S 𝒪 θ hker
    obtain ⟨-, -, hfin, -⟩ := Algebra.finite_maximalSpectrum_and_bijective_localization_of_module_finite (𝒪 := 𝒪)
      (heckeBaseAlgebra N S 𝒪)
    haveI := hfin ⟨heckeLocalIdeal N S 𝒪 θ, hPmax⟩
    have e := IsLocalization.algEquiv (heckeLocalIdeal N S 𝒪 θ).primeCompl
      (Localization.AtPrime (heckeLocalIdeal N S 𝒪 θ)) (heckeLocal N S 𝒪 θ)
    exact Module.Finite.equiv (e.toLinearEquiv.restrictScalars 𝒪)

instance heckeLocal.instModuleFree : Module.Free 𝒪 (heckeLocal N S 𝒪 θ) := by
  rcases trio_subsingleton_or_ker_le N S 𝒪 θ with hsub | hker
  · haveI := hsub
    exact Module.Free.of_subsingleton 𝒪 (heckeLocal N S 𝒪 θ)
  · haveI := trio_moduleFinite_base N S 𝒪
    haveI := trio_moduleFree_base N S 𝒪
    haveI hPmax : (heckeLocalIdeal N S 𝒪 θ).IsMaximal := heckeLocalIdeal_isMaximal N S 𝒪 θ hker
    haveI hloc := trio_isLocalization_atPrime N S 𝒪 θ hker
    haveI := trio_free_atPrime (R := 𝒪) (heckeBaseAlgebra N S 𝒪)
      ⟨heckeLocalIdeal N S 𝒪 θ, hPmax⟩
    have e := IsLocalization.algEquiv (heckeLocalIdeal N S 𝒪 θ).primeCompl
      (Localization.AtPrime (heckeLocalIdeal N S 𝒪 θ)) (heckeLocal N S 𝒪 θ)
    exact Module.Free.of_equiv (e.toLinearEquiv.restrictScalars 𝒪)

instance heckeLocal.instIsLocalRing [Fact (HasIntegralStructure N 2)] :
    IsLocalRing (heckeLocal N S 𝒪 θ) :=
  heckeLocal.isLocalRing N S 𝒪 θ

instance heckeLocal.instIsAdicComplete [Fact (HasIntegralStructure N 2)] :
    IsAdicComplete (IsLocalRing.maximalIdeal (heckeLocal N S 𝒪 θ)) (heckeLocal N S 𝒪 θ) := by
  haveI := heckeLocal.isLocalHom_algebraMap N S 𝒪 θ
  exact IsLocalRing.isAdicComplete_of_module_finite (𝒪 := 𝒪)

instance heckeLocal.instIsLocalHom [Fact (HasIntegralStructure N 2)] :
    IsLocalHom (algebraMap 𝒪 (heckeLocal N S 𝒪 θ)) :=
  heckeLocal.isLocalHom_algebraMap N S 𝒪 θ

end CuspForm

end

Statements phrased using this module (165)

… and 15 more statements (search for the module name to find them).