Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_ShimuraCurve.lean

definition module

Shimura curve models over and their Jacobian torsion

For a rational quaternion algebra B=\mathbb{H}[\mathbb{Q},a,b], QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt a b q q' asserts that a>0 or b>0, and that for every height-one prime v of \mathbb{Z} the completion B\otimes_{\mathbb{Q}}\mathbb{Q}_v is a division ring (every nonzero element a unit) exactly when q or q' lies in v. For a \mathbb{Z}-lattice R\subseteq B, unitGroup R is the subgroup of B^\times generated by those u satisfying the predicate IsUnitOf R, and fuchsianGroup R ι is the intersection of its image under a \mathbb{Q}-algebra map \iota\colon B\to M_2(\mathbb{R}) with the kernel of \det in \mathrm{GL}_2(\mathbb{R}).

ShimuraCurveModel R ι 𝒮, for a family \mathcal{S} of subsets of (B\otimes_{\mathbb{Q}}\mathbb{A}_f)^\times indexed by naturals, is a structure packaging a model: function fields F/\mathbb{Q}, \bar F/\overline{\mathbb{Q}}, F_{\mathbb{C}}/\mathbb{C} which are curves in the project's sense (IsCurveOver together with Algebra.EssFiniteType), with \mathbb{Q} algebraically closed in F; ring maps F\to\bar F\to F_{\mathbb{C}} over a chosen embedding \overline{\mathbb{Q}}\to\mathbb{C}, required to generate the target over the new base field and to preserve linear independence of finite subsets (base change, stated elementwise); a homomorphism from \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) to semilinear automorphisms of \bar F inducing \sigma on \overline{\mathbb{Q}} and fixing the image of F; a UniformizedHeckeCurve structure for fuchsianGroup R ι on F_{\mathbb{C}}, whose multiset of Hecke points at each prime \ell is pinned to be \iota applied to a finite set S of elements of R of reduced norm \ell lying in \mathcal{S}(\ell) adelically, S being a system of representatives for left multiplication by norm-one units of R on all such elements; a place map and divisor correspondences over \overline{\mathbb{Q}} compatible with the complex ones; induced endomorphisms heckePic0 of \mathrm{Pic}^0(\bar F), commuting with each other and with the Galois action; and finiteness of each n-torsion subgroup together with a finite field of definition for it.

Derived material turns J=\mathrm{Pic}^0(\bar F/\overline{\mathbb{Q}}) into a module over HeckeAlg =\mathbb{Z}[X_\ell]_{\ell\ \mathrm{prime}}: heckeJ is the ring map sending heckeGen ℓ to heckePic0 ℓ (the image lies in the commutative subalgebra generated by these), galJ the Galois action, and J_comm their commutation; signTwist ε rescales each generator by a unit \varepsilon(\ell)\in\mathbb{Z}^\times, giving heckeJSigned. Tors p is the p-torsion of J with its restricted Hecke and Galois actions, finite when p is prime, trivialised by a finite extension of \mathbb{Q}. GoodReductionOutside p S is the conjunction of: inertia at every prime \ell\nmid S acts trivially on elements killed by p, and the Eichler–Shimura relation \sigma^2-T_\ell\sigma+\ell=0 holds on them for Frobenius elements \sigma at \ell. Finally IsTorsionOf p T hecke gal says that an abstract Hecke–Galois module T embeds additively into J with image exactly the p-torsion, equivariantly for the Galois action and for each Hecke generator; RealizesJPrime and RealizesTwoPlace apply this to a JPrimeTorsionDatum resp. a TwoPlaceTorsionDatum, and isTorsionOf_self records that Tors p itself is such a realisation.

Relation to Mathlib

Mathlib has no Shimura curves, quaternionic Fuchsian groups or models of curves over \mathbb{Q}; this module is the project's own packaging, resting on the project's notions of function-field curve (IsCurveOver), places, divisors and \mathrm{Pic}^0, semilinear Galois actions, the reduced norm nrd on \mathbb{H}[R,a,b], and the free commutative \mathbb{Z}-algebra HeckeAlg on the primes. The quaternion algebra type itself, the finite adele ring and \mathrm{GL}_2(\mathbb{R}) are Mathlib's.

Where it is used

These definitions provide the one pinned record for the Shimura curve attached to an Eichler order in an indefinite rational quaternion algebra ramified at two primes, the curve used in the (q,q')-exchange step of level lowering. Its Jacobian's p-torsion, with the Hecke and Galois structure defined here, is what a two-place torsion datum is required to realise, so that the Čerednik–Drinfeld description at the two ramified primes and the Eichler–Shimura congruence away from the level can be stated about a single model.

References

  1. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476
  2. J.-F. Boutot and H. Carayol, Uniformisation p-adique des courbes de Shimura: les théorèmes de Čerednik et de Drinfeld, Astérisque 196–197 (1991), 45–158
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §4

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

Imports

Imported by

Declarations

Source

import Definitions.Def_QuaternionAlgebra_EichlerOrder
import Definitions.Def_QuaternionAlgebra_ReducedNorm
import Definitions.Def_ModularCurve_UniformizedHeckeCurve
import Definitions.Def_AlgebraicCurve_BaseChangeGalois
import Definitions.Def_AlgebraicCurve_IsCurveOver
import Definitions.Def_CerednikDrinfeld_TwoPlaceTorsionDatum
import Definitions.Def_Compat_Mathlib430

set_option autoImplicit false

noncomputable section

open scoped Quaternion TensorProduct MatrixGroups
open IsDedekindDomain NumberField AlgebraicCurve

namespace QuaternionAlgebra

variable (a b : ℚ)

def IsIndefiniteRamifiedExactlyAt (q q' : ℕ) : Prop :=
  (0 < a ∨ 0 < b) ∧
    ∀ v : HeightOneSpectrum (𝓞 ℚ),
      (∀ x : ℍ[ℚ, a, b] ⊗[ℚ] v.adicCompletion ℚ, x ≠ 0 → IsUnit x) ↔
        ((q : 𝓞 ℚ) ∈ v.asIdeal ∨ (q' : 𝓞 ℚ) ∈ v.asIdeal)

end QuaternionAlgebra

namespace CerednikDrinfeld

open QuaternionAlgebra ModularCurve

variable {a b : ℚ}

def unitGroup (R : Submodule ℤ ℍ[ℚ, a, b]) : Subgroup (ℍ[ℚ, a, b])ˣ :=
  Subgroup.closure {u : (ℍ[ℚ, a, b])ˣ | IsUnitOf R (u : ℍ[ℚ, a, b])}

def fuchsianGroup (R : Submodule ℤ ℍ[ℚ, a, b]) (ι : ℍ[ℚ, a, b] →ₐ[ℚ] Matrix (Fin 2) (Fin 2) ℝ) :
    Subgroup (GL (Fin 2) ℝ) :=
  (unitGroup R).map (Units.map (ι : ℍ[ℚ, a, b] →* Matrix (Fin 2) (Fin 2) ℝ)) ⊓
    (Matrix.GeneralLinearGroup.det : GL (Fin 2) ℝ →* ℝˣ).ker

structure ShimuraCurveModel (R : Submodule ℤ ℍ[ℚ, a, b])
    (ι : ℍ[ℚ, a, b] →ₐ[ℚ] Matrix (Fin 2) (Fin 2) ℝ) (𝒮 : ℕ → Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Type 1 where

  F : Type
  [instFieldF : Field F]
  [instAlgebraF : Algebra ℚ F]

  Fbar : Type
  [instFieldFbar : Field Fbar]
  [instAlgebraFbar : Algebra (AlgebraicClosure ℚ) Fbar]

  Fc : Type
  [instFieldFc : Field Fc]
  [instAlgebraFc : Algebra ℂ Fc]

  [isCurveOverF : IsCurveOver ℚ F]

  [essFiniteTypeF : Algebra.EssFiniteType ℚ F]

  [isCurveOverBar : IsCurveOver (AlgebraicClosure ℚ) Fbar]

  [essFiniteTypeBar : Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]

  [isCurveOverC : IsCurveOver ℂ Fc]

  [essFiniteTypeC : Algebra.EssFiniteType ℂ Fc]

  algebraic_mem_range : ∀ x : F, IsAlgebraic ℚ x → x ∈ Set.range (algebraMap ℚ F)

  toBar : F →+* Fbar

  toBar_algebraMap : ∀ r : ℚ,
    toBar (algebraMap ℚ F r) = algebraMap (AlgebraicClosure ℚ) Fbar (algebraMap ℚ (AlgebraicClosure ℚ) r)

  closure_toBar : Subfield.closure
      (Set.range (algebraMap (AlgebraicClosure ℚ) Fbar) ∪ Set.range toBar) = ⊤

  linearIndependent_toBar : ∀ s : Finset F,
    LinearIndependent ℚ (fun x : s => (x : F)) →
      LinearIndependent (AlgebraicClosure ℚ) (fun x : s => toBar (x : F))

  emb : AlgebraicClosure ℚ →+* ℂ

  toC : Fbar →+* Fc

  toC_algebraMap : ∀ z : AlgebraicClosure ℚ,
    toC (algebraMap (AlgebraicClosure ℚ) Fbar z) = algebraMap ℂ Fc (emb z)

  closure_toC : Subfield.closure (Set.range (algebraMap ℂ Fc) ∪ Set.range toC) = ⊤

  linearIndependent_toC : ∀ s : Finset Fbar,
    LinearIndependent (AlgebraicClosure ℚ) (fun x : s => (x : Fbar)) →
      LinearIndependent ℂ (fun x : s => toC (x : Fbar))

  gal : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* SemilinearAut (AlgebraicClosure ℚ) Fbar

  baseAut_gal : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
    SemilinearAut.baseAut (gal σ) = (σ : AlgebraicClosure ℚ ≃+* AlgebraicClosure ℚ)

  gal_smul_toBar : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : F), gal σ • toBar x = toBar x

  unif : UniformizedHeckeCurve (fuchsianGroup R ι) Fc

  heckePoints_eq : ∀ (ℓ : ℕ) (hℓ : ℓ.Prime), ∃ S : Finset ℍ[ℚ, a, b],
    (∀ x ∈ S, x ∈ R ∧ nrd x = ℓ ∧
      ∃ h ∈ 𝒮 ℓ, (h : ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ) = x ⊗ₜ[ℚ] (1 : FiniteAdeleRing (𝓞 ℚ) ℚ)) ∧
    (∀ y : ℍ[ℚ, a, b], y ∈ R → nrd y = ℓ →
      (∃ h ∈ 𝒮 ℓ, (h : ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ) = y ⊗ₜ[ℚ] (1 : FiniteAdeleRing (𝓞 ℚ) ℚ)) →
      ∃! x, x ∈ S ∧ ∃ u : ℍ[ℚ, a, b], IsUnitOf R u ∧ nrd u = 1 ∧ u * x = y) ∧
    (unif.heckePoints ℓ hℓ).map (fun g => (g : Matrix (Fin 2) (Fin 2) ℝ)) = S.val.map ι

  bcPlace : Place (AlgebraicClosure ℚ) Fbar → Place ℂ Fc

  mem_bcPlace_iff : ∀ (P : Place (AlgebraicClosure ℚ) Fbar) (x : Fbar),
    toC x ∈ (bcPlace P).toValuationSubring ↔ x ∈ P.toValuationSubring

  corrBar : ∀ ℓ : ℕ, ℓ.Prime →
    (Divisor (AlgebraicClosure ℚ) Fbar →+ Divisor (AlgebraicClosure ℚ) Fbar)

  corr_mapDomain : ∀ (ℓ : ℕ) (hℓ : ℓ.Prime) (D : Divisor (AlgebraicClosure ℚ) Fbar),
    unif.corr ℓ hℓ (Finsupp.mapDomain bcPlace D) = Finsupp.mapDomain bcPlace (corrBar ℓ hℓ D)

  heckePic0 : ∀ ℓ : ℕ, ℓ.Prime → (Pic0 (AlgebraicClosure ℚ) Fbar →+ Pic0 (AlgebraicClosure ℚ) Fbar)

  heckePic0_mk : ∀ (ℓ : ℕ) (hℓ : ℓ.Prime) (D : Divisor.degZero (K := AlgebraicClosure ℚ) (F := Fbar))
    (hD : corrBar ℓ hℓ (D : Divisor (AlgebraicClosure ℚ) Fbar) ∈
      Divisor.degZero (K := AlgebraicClosure ℚ) (F := Fbar)),
    heckePic0 ℓ hℓ (Pic0.mk D) = Pic0.mk ⟨corrBar ℓ hℓ (D : Divisor (AlgebraicClosure ℚ) Fbar), hD⟩

  heckePic0_comm : ∀ (ℓ ℓ' : ℕ) (hℓ : ℓ.Prime) (hℓ' : ℓ'.Prime),
    (heckePic0 ℓ hℓ).comp (heckePic0 ℓ' hℓ') = (heckePic0 ℓ' hℓ').comp (heckePic0 ℓ hℓ)

  gal_smul_heckePic0 : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (ℓ : ℕ) (hℓ : ℓ.Prime)
    (c : Pic0 (AlgebraicClosure ℚ) Fbar), gal σ • heckePic0 ℓ hℓ c = heckePic0 ℓ hℓ (gal σ • c)

  finite_torsion : ∀ n : ℕ, 0 < n → Finite (Pic0.torsion (AlgebraicClosure ℚ) Fbar n)

  finiteLevel_torsion : ∀ n : ℕ, 0 < n →
    ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ L ∧
      ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, (∀ y ∈ L, σ y = y) →
        ∀ c : Pic0 (AlgebraicClosure ℚ) Fbar, c ∈ Pic0.torsion (AlgebraicClosure ℚ) Fbar n → gal σ • c = c

attribute [instance] ShimuraCurveModel.instFieldF ShimuraCurveModel.instAlgebraF
  ShimuraCurveModel.instFieldFbar ShimuraCurveModel.instAlgebraFbar ShimuraCurveModel.instFieldFc
  ShimuraCurveModel.instAlgebraFc ShimuraCurveModel.isCurveOverF ShimuraCurveModel.essFiniteTypeF
  ShimuraCurveModel.isCurveOverBar ShimuraCurveModel.essFiniteTypeBar ShimuraCurveModel.isCurveOverC
  ShimuraCurveModel.essFiniteTypeC

namespace ShimuraCurveModel

variable {R : Submodule ℤ ℍ[ℚ, a, b]} {ι : ℍ[ℚ, a, b] →ₐ[ℚ] Matrix (Fin 2) (Fin 2) ℝ}
  {𝒮 : ℕ → Set (ℍ[ℚ, a, b] ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ}

abbrev J (M : ShimuraCurveModel R ι 𝒮) : Type := Pic0 (AlgebraicClosure ℚ) M.Fbar

def heckeGenJ (M : ShimuraCurveModel R ι 𝒮) (ℓ : Nat.Primes) : Module.End ℤ M.J :=
  (M.heckePic0 ℓ ℓ.prop).toIntLinearMap

@[simp] theorem heckeGenJ_apply (M : ShimuraCurveModel R ι 𝒮) (ℓ : Nat.Primes) (c : M.J) :
    M.heckeGenJ ℓ c = M.heckePic0 ℓ ℓ.prop c := rfl

theorem heckeGenJ_comm (M : ShimuraCurveModel R ι 𝒮) (ℓ ℓ' : Nat.Primes) :
    M.heckeGenJ ℓ * M.heckeGenJ ℓ' = M.heckeGenJ ℓ' * M.heckeGenJ ℓ := by
  apply LinearMap.ext
  intro c
  exact DFunLike.congr_fun (M.heckePic0_comm ℓ ℓ' ℓ.prop ℓ'.prop) c

theorem isMulCommutative_adjoin_heckeGenJ (M : ShimuraCurveModel R ι 𝒮) :
    IsMulCommutative (Algebra.adjoin ℤ (Set.range M.heckeGenJ)) :=
  Algebra.isMulCommutative_adjoin ℤ (by
    rintro _ ⟨ℓ, rfl⟩ _ ⟨ℓ', rfl⟩
    exact M.heckeGenJ_comm ℓ ℓ')

@[reducible] def commRingAdjoinJ (M : ShimuraCurveModel R ι 𝒮) :
    CommRing ↥(Algebra.adjoin ℤ (Set.range M.heckeGenJ)) :=
  { (inferInstance : Ring ↥(Algebra.adjoin ℤ (Set.range M.heckeGenJ))) with
    mul_comm := M.isMulCommutative_adjoin_heckeGenJ.is_comm.comm }

def heckeJAux (M : ShimuraCurveModel R ι 𝒮) :
    HeckeAlg →ₐ[ℤ] (Algebra.adjoin ℤ (Set.range M.heckeGenJ) : Subalgebra ℤ (Module.End ℤ M.J)) :=
  letI : CommSemiring ↥(Algebra.adjoin ℤ (Set.range M.heckeGenJ)) := M.commRingAdjoinJ.toCommSemiring
  MvPolynomial.aeval fun ℓ =>
    (⟨M.heckeGenJ ℓ, Algebra.subset_adjoin (Set.mem_range_self ℓ)⟩ : Algebra.adjoin ℤ (Set.range M.heckeGenJ))

def heckeJ (M : ShimuraCurveModel R ι 𝒮) : HeckeAlg →+* Module.End ℤ M.J :=
  ((Algebra.adjoin ℤ (Set.range M.heckeGenJ)).val.comp M.heckeJAux).toRingHom

theorem heckeJ_mem_adjoin (M : ShimuraCurveModel R ι 𝒮) (x : HeckeAlg) :
    M.heckeJ x ∈ Algebra.adjoin ℤ (Set.range M.heckeGenJ) :=
  (M.heckeJAux x).2

theorem heckeJ_heckeGen (M : ShimuraCurveModel R ι 𝒮) (ℓ : Nat.Primes) : M.heckeJ (heckeGen ℓ) = M.heckeGenJ ℓ := by
  letI : CommSemiring ↥(Algebra.adjoin ℤ (Set.range M.heckeGenJ)) := M.commRingAdjoinJ.toCommSemiring
  show ((M.heckeJAux (heckeGen ℓ) : Module.End ℤ M.J)) = _
  rw [heckeJAux, heckeGen, MvPolynomial.aeval_X]

theorem heckeJ_heckeGen_apply (M : ShimuraCurveModel R ι 𝒮) (ℓ : Nat.Primes) (c : M.J) :
    M.heckeJ (heckeGen ℓ) c = M.heckePic0 ℓ ℓ.prop c := by
  rw [heckeJ_heckeGen]
  rfl

def galJ (M : ShimuraCurveModel R ι 𝒮) : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* AddAut M.J :=
  (DistribMulAction.toAddAut' (SemilinearAut (AlgebraicClosure ℚ) M.Fbar) M.J).comp M.gal

@[simp] theorem galJ_apply (M : ShimuraCurveModel R ι 𝒮) (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (c : M.J) :
    M.galJ σ c = M.gal σ • c := rfl

theorem J_comm (M : ShimuraCurveModel R ι 𝒮) :
    ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : HeckeAlg) (c : M.J),
      M.galJ σ (M.heckeJ x c) = M.heckeJ x (M.galJ σ c) := by
  intro σ x c
  let g : Module.End ℤ M.J := (M.galJ σ).toAddMonoidHom.toIntLinearMap
  have hle : Algebra.adjoin ℤ (Set.range M.heckeGenJ) ≤ Subalgebra.centralizer ℤ {g} := by
    rw [Algebra.adjoin_le_iff]
    rintro _ ⟨ℓ, rfl⟩
    rw [SetLike.mem_coe, Subalgebra.mem_centralizer_iff]
    intro b hb
    rw [Set.mem_singleton_iff] at hb
    subst hb
    apply LinearMap.ext
    intro s
    exact M.gal_smul_heckePic0 σ ℓ ℓ.prop s
  have h := (Subalgebra.mem_centralizer_iff ℤ).1 (hle (M.heckeJ_mem_adjoin x)) g (Set.mem_singleton g)
  exact LinearMap.congr_fun h c

def signTwist (ε : Nat.Primes → ℤˣ) : HeckeAlg →+* HeckeAlg :=
  (MvPolynomial.aeval fun ℓ => ((ε ℓ : ℤ) : HeckeAlg) * MvPolynomial.X ℓ).toRingHom

@[simp] theorem signTwist_heckeGen (ε : Nat.Primes → ℤˣ) (ℓ : Nat.Primes) :
    signTwist ε (heckeGen ℓ) = ((ε ℓ : ℤ) : HeckeAlg) * heckeGen ℓ := by
  show (MvPolynomial.aeval fun ℓ => ((ε ℓ : ℤ) : HeckeAlg) * MvPolynomial.X ℓ) (MvPolynomial.X ℓ) = _
  rw [MvPolynomial.aeval_X]
  rfl

abbrev heckeJSigned (M : ShimuraCurveModel R ι 𝒮) (ε : Nat.Primes → ℤˣ) : HeckeAlg →+* Module.End ℤ M.J :=
  M.heckeJ.comp (signTwist ε)

theorem heckeJSigned_heckeGen_apply (M : ShimuraCurveModel R ι 𝒮) (ε : Nat.Primes → ℤˣ) (ℓ : Nat.Primes) (c : M.J) :
    M.heckeJSigned ε (heckeGen ℓ) c = (ε ℓ : ℤ) • M.heckePic0 ℓ ℓ.prop c := by
  rw [heckeJSigned, RingHom.comp_apply, signTwist_heckeGen, map_mul, map_intCast, Module.End.mul_apply,
    heckeJ_heckeGen_apply, Module.End.intCast_apply]

theorem J_comm_signed (M : ShimuraCurveModel R ι 𝒮) (ε : Nat.Primes → ℤˣ) :
    ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : HeckeAlg) (c : M.J),
      M.galJ σ (M.heckeJSigned ε x c) = M.heckeJSigned ε x (M.galJ σ c) :=
  fun σ x c => M.J_comm σ (signTwist ε x) c

theorem finiteLevel_J (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) (hp : 0 < p) :
    ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ L ∧
      ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, (∀ y ∈ L, σ y = y) →
        ∀ t : M.J, p • t = 0 → M.galJ σ t = t := by
  obtain ⟨L, hL, h⟩ := M.finiteLevel_torsion p hp
  refine ⟨L, hL, fun σ hσ t ht => h σ hσ t (Pic0.mem_torsion.2 ?_)⟩
  rw [natCast_zsmul]
  exact ht

def GoodReductionOutside (M : ShimuraCurveModel R ι 𝒮) (p S : ℕ) : Prop :=
  (∀ (ℓ : ℕ), ℓ.Prime → ¬ ℓ ∣ S →
    ∀ B : ValuationSubring (AlgebraicClosure ℚ), B.LiesOverPrime ℓ →
      ∀ σ ∈ B.inertiaSubgroupIn ℚ, ∀ t : M.J, p • t = 0 → M.galJ σ t = t) ∧
  (∀ (ℓ : ℕ) (hℓ : ℓ.Prime), ¬ ℓ ∣ S →
    ∀ B : ValuationSubring (AlgebraicClosure ℚ), B.LiesOverPrime ℓ →
      ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, B.IsFrobeniusAt σ ℓ →
        ∀ t : M.J, p • t = 0 →
          M.galJ σ (M.galJ σ t) - M.heckeJ (heckeGen ⟨ℓ, hℓ⟩) (M.galJ σ t) + ℓ • t = 0)

abbrev Tors (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) : Type := ↥(Pic0.torsion (AlgebraicClosure ℚ) M.Fbar p)

theorem torsion_pTorsion (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) : ∀ t : M.Tors p, p • t = 0 := by
  intro t
  have h : (p : ℤ) • (t : M.J) = 0 := Pic0.mem_torsion.1 t.2
  apply Subtype.ext
  rw [AddSubmonoidClass.coe_nsmul, ZeroMemClass.coe_zero, ← Nat.cast_smul_eq_nsmul ℤ]
  exact h

instance instFiniteTors (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) [Fact p.Prime] : Finite (M.Tors p) :=
  M.finite_torsion p (Fact.out : p.Prime).pos

def restrictTors (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) : Module.End ℤ M.J →+* Module.End ℤ (M.Tors p) where
  toFun f := f.restrict (p := (Pic0.torsion (AlgebraicClosure ℚ) M.Fbar p).toIntSubmodule)
    (q := (Pic0.torsion (AlgebraicClosure ℚ) M.Fbar p).toIntSubmodule) (fun x hx => by
      change x ∈ Pic0.torsion (AlgebraicClosure ℚ) M.Fbar p at hx
      change f x ∈ Pic0.torsion (AlgebraicClosure ℚ) M.Fbar p
      rw [Pic0.mem_torsion] at hx ⊢
      rw [← map_zsmul, hx, map_zero])
  map_one' := by apply LinearMap.ext; intro t; rfl
  map_mul' f g := by apply LinearMap.ext; intro t; rfl
  map_zero' := by apply LinearMap.ext; intro t; rfl
  map_add' f g := by apply LinearMap.ext; intro t; rfl

@[simp] theorem coe_restrictTors_apply (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) (f : Module.End ℤ M.J) (t : M.Tors p) :
    ((M.restrictTors p f t : M.Tors p) : M.J) = f t := rfl

def torsionHecke (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) : HeckeAlg →+* Module.End ℤ (M.Tors p) :=
  (M.restrictTors p).comp M.heckeJ

@[simp] theorem coe_torsionHecke_apply (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) (x : HeckeAlg) (t : M.Tors p) :
    ((M.torsionHecke p x t : M.Tors p) : M.J) = M.heckeJ x t := rfl

theorem coe_torsionHecke_heckeGen_apply (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) (ℓ : Nat.Primes) (t : M.Tors p) :
    ((M.torsionHecke p (heckeGen ℓ) t : M.Tors p) : M.J) = M.heckePic0 ℓ ℓ.prop t := by
  rw [coe_torsionHecke_apply, heckeJ_heckeGen_apply]

def torsionGal (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) :
    (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* AddAut (M.Tors p) :=
  (DistribMulAction.toAddAut' (SemilinearAut (AlgebraicClosure ℚ) M.Fbar) (M.Tors p)).comp M.gal

@[simp] theorem coe_torsionGal_apply (M : ShimuraCurveModel R ι 𝒮) (p : ℕ)
    (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (t : M.Tors p) :
    ((M.torsionGal p σ t : M.Tors p) : M.J) = M.galJ σ (t : M.J) := rfl

theorem torsion_comm (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) :
    ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : HeckeAlg) (t : M.Tors p),
      M.torsionGal p σ (M.torsionHecke p x t) = M.torsionHecke p x (M.torsionGal p σ t) := by
  intro σ x t
  apply Subtype.ext
  rw [coe_torsionGal_apply, coe_torsionHecke_apply, coe_torsionHecke_apply, coe_torsionGal_apply]
  exact M.J_comm σ x t

theorem torsion_finiteLevel (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) [Fact p.Prime] :
    ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ L ∧
      ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, (∀ y ∈ L, σ y = y) → M.torsionGal p σ = 1 := by
  obtain ⟨L, hL, h⟩ := M.finiteLevel_torsion p (Fact.out : p.Prime).pos
  refine ⟨L, hL, fun σ hσ => AddEquiv.ext fun t => Subtype.ext ?_⟩
  exact h σ hσ t t.2

def IsTorsionOf (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) (T : Type) [AddCommGroup T]
    (hecke : HeckeAlg →+* Module.End ℤ T)
    (gal : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* AddAut T) : Prop :=
  ∃ e : T →+ M.J, Function.Injective e ∧ e.range = Pic0.torsion (AlgebraicClosure ℚ) M.Fbar p ∧
    (∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (t : T), e (gal σ t) = M.gal σ • e t) ∧
    ∀ (ℓ : Nat.Primes) (t : T), e (hecke (heckeGen ℓ) t) = M.heckePic0 ℓ ℓ.prop (e t)

def RealizesJPrime (M : ShimuraCurveModel R ι 𝒮) {p : ℕ} {E V : Type} [Fintype E] [Fintype V] [DecidableEq V]
    {A : ValuationSubring (AlgebraicClosure ℚ)} (Dm : JPrimeTorsionDatum p E V A) : Prop :=
  M.IsTorsionOf p Dm.T Dm.hecke Dm.gal

def RealizesTwoPlace (M : ShimuraCurveModel R ι 𝒮) {p : ℕ} {E₁ V₁ E₂ V₂ : Type}
    [Fintype E₁] [Fintype V₁] [DecidableEq V₁] [Fintype E₂] [Fintype V₂] [DecidableEq V₂]
    {D₁ : DegeneracyData E₁ V₁} {H₁ : HeckeData D₁} {D₂ : DegeneracyData E₂ V₂} {H₂ : HeckeData D₂}
    {A₁ A₂ : ValuationSubring (AlgebraicClosure ℚ)} (𝒥 : TwoPlaceTorsionDatum p D₁ H₁ D₂ H₂ A₁ A₂) : Prop :=
  M.IsTorsionOf p 𝒥.T 𝒥.hecke 𝒥.gal

theorem isTorsionOf_self (M : ShimuraCurveModel R ι 𝒮) (p : ℕ) :
    M.IsTorsionOf p (M.Tors p) (M.torsionHecke p) (M.torsionGal p) := by
  refine ⟨(Pic0.torsion (AlgebraicClosure ℚ) M.Fbar p).subtype, Subtype.val_injective,
    AddSubgroup.range_subtype _, fun σ t => ?_, fun ℓ t => ?_⟩
  · exact M.coe_torsionGal_apply p σ t
  · exact M.coe_torsionHecke_heckeGen_apply p ℓ t

end ShimuraCurveModel

end CerednikDrinfeld

end

Statements phrased using this module (264)

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