§4 Modularity of semistable elliptic curves

4. Modularity of semistable elliptic curves

FreyPackage.frey_isModular (P : FreyPackage) : P.freyCurve.IsModular is deduced (after checking that the integral Frey model is semistable with nonzero discriminant) from

theorem WeierstrassCurve.modularity_of_semistableModel (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) : (W.map (Int.castRingHom ℚ)).IsModular

Here (Definitions/Def_FLTPrelim_Modularity.lean) IsSemistableModel says that no prime divides both $Δ$ and $c_{4}$ of the given integral equation, and IsModular E says that some integral model $W$ of $E$ and some normalised weight-2 eigenform $f$ on $Γ_{0} (N)$ , $N \geq 1$ , satisfy $a_{ℓ} (f) = ℓ + 1 - # W (F_{ℓ})$ at every prime $ℓ ∤ N Δ (W)$ ; "normalised eigenform" is expressed by the Hecke recursions on $q$ -expansion coefficients (CuspForm.IsNormalizedEigenform), and CuspForm, CongruenceSubgroup.Gamma0 and $q$ -expansions are Mathlib's. About 27,800 of the 29,511 theorems lie below this declaration. Its proof module, about 90 lines, follows Wiles's strategy and cites eight theorems:

WeierstrassCurve.modThreeOrFiveIrreducible — for a semistable model with $Δ \neq = 0$ , one of $ρ ˉ_{W, 3}$ , $ρ ˉ_{W, 5}$ is irreducible (if both were reducible the curve would give a rational point on $X_{0} (15)$ ; the child WeierstrassCurve.fifteenIsogenyClassification pins $c_{4}^{3} /Δ$ to one of four values, none semistable).
WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel — the Langlands–Tunnell input, §4.1.
Two modularity lifting theorems, §4.2.
WeierstrassCurve.threeFiveSwitchCurve — the 3–5 switch: if $ρ ˉ_{W, 5}$ is irreducible there is a second semistable model $W^{'}$ with $ρ ˉ_{W^{'}, 3}$ irreducible and $5 ∣ a_{ℓ} (W^{'}) - a_{ℓ} (W)$ at common good primes $ℓ \neq = 5$ (beneath it WeierstrassCurve.threeFiveAuxiliaryCurveExists produces $W^{'}$ with $W^{'} [5] ≅ W [5]$ as Galois modules, from an explicit family of curves with prescribed 5-torsion in the RubinSilverberg namespace, choosing a member whose mod-3 representation is irreducible by a specialization at which the 3-division polynomial criterion holds (WeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization, WeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero)); and WeierstrassCurve.isResiduallyModularOfLevel_of_switch, which turns modularity of $W^{'}$ into residual modularity of $W$ mod 5.
Two book-keeping lemmas passing from "modular of exact conductor level" to IsModular.

The assembly: if $ρ ˉ_{W, 3}$ is irreducible, apply (2) and then lifting at $p = 3$ ; otherwise $ρ ˉ_{W, 5}$ is irreducible, the switch gives $W^{'}$ , the first case makes $W^{'}$ modular, hence $W$ is residually modular mod 5 at a squarefree level, and lifting at $p = 5$ finishes.

4.1 Langlands–Tunnell, in the form Wiles uses

theorem WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel
    (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel)
    (h3 : W.ModRepIsIrreducible 3) :
    ∃ M : ℕ, 0 < M ∧ W.IsResiduallyModularOfLevel 3 M ∧
      (∀ q : ℕ, q.Prime → q ≠ 3 → ¬ q ^ 3 ∣ M) ∧
      (3 ^ 2 ∣ M →
        ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime 3 →
          ∀ x : Submodule.torsionBy ℤ
              ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point (3 : ℕ),
            (∀ σ ∈ A.inertiaSubgroupIn ℚ, σ • x = x) → x = 0)

IsResiduallyModularOfLevel W 3 M (Definitions/Def_FLTPrelim_ModularRep.lean) asks for a normalised weight-2 eigenform on $Γ_{0} (M)$ whose $a_{ℓ}$ are congruent to $a_{ℓ} (W)$ modulo a maximal ideal above 3 of the ring of all algebraic integers, at good primes $ℓ ∤ 3 M$ ; the level clauses are what the lifting theorem at 3 needs. About 7,300 theorems lie below it. The proof obtains a weight-one eigensystem from the curve, multiplies by the Eisenstein series $E_{1} (1, χ_{- 3})$ and passes to a genuine weight-2 eigenform congruent to the product (a Deligne–Serre lifting lemma); the weight-one input is LanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift: for a continuous surjective $ρ : G_{Q} \to GL_{2} (F_{3})$ with cyclotomic determinant, lifted to $GL_{2} (Z [- 2])$ through an explicit section of reduction (an odd octahedral Artin representation), there is a weight-one cusp form with nebentypus $χ_{- 3}$ whose prime-indexed coefficients are the traces of Frobenius of the lift. Surjectivity onto $GL_{2} (F_{3})$ is derived in the tree from irreducibility for semistable models. Below this lie about 6,800 theorems, essentially the whole of the LanglandsTunnell (1,543) and AutomorphicForm (2,336) namespaces: the argument is Tunnell's, organised around the quadratic, cubic and sextic subfields cut out by subgroups of $GL_{2} (F_{3})$ — monomial automorphy over those fields, cyclic base change (AutomorphicForm.CyclicBaseChangeLifting.…), a converse theorem with Rankin–Selberg integrals (LanglandsTunnell.Converse.…, LanglandsTunnell.RankinSelberg.…), and the passage from an adelic cuspidal eigensystem to a classical weight-one form (AutomorphicForm.exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion).

4.2 Modularity lifting (Taylor–Wiles patching; "R = T")

Two theorems with the same conclusion Mlc1IsModularModelOfExactConductorLevel W (Definitions/Def_WeierstrassCurve_Mlc1RowStatement.lean: $W$ is modular of some squarefree level $N > 0$ whose prime divisors are exactly the primes dividing $Δ (W)$ ) and the same shape of hypotheses — $W$ semistable with $Δ \neq = 0$ , $ρ ˉ_{W, p}$ irreducible, $W$ residually modular mod $p$ of a level $M_{0}$ with $q^{3} ∤ M_{0}$ for primes $q \neq = p$ — differing in $p$ and in the condition at $p$ :

WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd: $p = 3$ , and if $9 ∣ M_{0}$ then inertia at 3 fixes no nonzero 3-torsion point;
WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd: $p \in {3, 5}$ and $p^{2} ∤ M_{0}$ .

Each proof module cites 18 theorems and has about 23,000 theorems below it — three quarters of the tree. The architecture is the Taylor–Wiles method in Diamond's formulation, organised around three structures whose inhabitants are constructed inside the subtree: a universal deformation ring for $ρ ˉ_{W, p}$ with an ordinary or flat local condition (GaloisRep.DeformationRingData; existence WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel and …_flatCondition_…), a Galois representation over a local Hecke algebra with Eichler–Shimura characteristic polynomials (CuspForm.HeckeGaloisRepDatum), and a Taylor–Wiles patching datum (Algebra.PatchingDatum; the patching argument is Algebra.PatchingDatum.nonempty_patchingLevel_bot, one of the files that retains an Imperial College London FLT project header). The surjection $R \to T$ is GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum; the step from a patching datum to modularity of an explicit level is WeierstrassCurve.isModularModelOfLevel_of_patchingDatum; and the descent from that level to the exact conductor level (WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd) is itself substantial, using Galois representations attached to newforms and the geometry of $J_{0} (N)$ .

← §3 Irreducibility of the mod-p representation of the Frey curve · §5 Level lowering →

How the theorems of this step depend on each other

Green cards are the landmarks named in this section; dashed white cards are landmarks of neighbouring steps they connect to. Premises above conclusions; an arrow may pass through unnamed intermediate theorems. Click a card for its page.

Theorems named in this section (17; statement as in the tree, numbers from the import graph)

One of $ρ ˉ_{W, 3}$ , $ρ ˉ_{W, 5}$ is irreducible WeierstrassCurve.modThreeOrFiveIrreducible

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem WeierstrassCurve.modThreeOrFiveIrreducible (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) : W.ModRepIsIrreducible 3 ∨ W.ModRepIsIrreducible 5

25 theorems below · cites 1 · cited by 2 · depth 6 · proof 69 lines, 6 helpers

Four possible $c_{4}^{3} /Δ$ for rational $15$ -isogenies WeierstrassCurve.fifteenIsogenyClassification

open WeierstrassCurve
theorem WeierstrassCurve.fifteenIsogenyClassification (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (h3 : ¬ W.ModRepIsIrreducible 3) (h5 : ¬ W.ModRepIsIrreducible 5) : (W.c₄ : ℚ) ^ 3 / (W.Δ : ℚ) = -25 / 2 ∨ (W.c₄ : ℚ) ^ 3 / (W.Δ : ℚ) = -349938025 / 8 ∨ (W.c₄ : ℚ) ^ 3 / (W.Δ : ℚ) = -121945 / 32 ∨ (W.c₄ : ℚ) ^ 3 / (W.Δ : ℚ) = 46969655 / 32768

24 theorems below · cites 3 · cited by 1 · depth 7 · proof 13 lines, 0 helpers

Residual modularity mod $3$ at a cube-free level, with inertia condition WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel

set_option autoImplicit false
open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open scoped WeierstrassCurve.Affine
theorem WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel
    (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel)
    (h3 : W.ModRepIsIrreducible 3) :
    ∃ M : ℕ, 0 < M ∧ W.IsResiduallyModularOfLevel 3 M ∧
      (∀ q : ℕ, q.Prime → q ≠ 3 → ¬ q ^ 3 ∣ M) ∧
      (3 ^ 2 ∣ M →
        ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime 3 →
          ∀ x : Submodule.torsionBy ℤ
              ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point (3 : ℕ),
            (∀ σ ∈ A.inertiaSubgroupIn ℚ, σ • x = x) → x = 0)

7,306 theorems below · cites 2 · cited by 2 · depth 6 · proof 44 lines, 0 helpers

The 3–5 switch for semistable integral models WeierstrassCurve.threeFiveSwitchCurve

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem WeierstrassCurve.threeFiveSwitchCurve (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) (h5 : W.ModRepIsIrreducible 5) : ∃ W' : WeierstrassCurve ℤ, W'.Δ ≠ 0 ∧ W'.IsSemistableModel ∧ W'.ModRepIsIrreducible 3 ∧ ∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ → W'.IsGoodPrimeFor ℓ → ℓ ≠ 5 → (5 : ℤ) ∣ (W'.apOfModel ℓ - W.apOfModel ℓ)

124 theorems below · cites 2 · cited by 2 · depth 6 · proof 7 lines, 0 helpers

Auxiliary curve for the 3–5 switch WeierstrassCurve.threeFiveAuxiliaryCurveExists

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
theorem WeierstrassCurve.threeFiveAuxiliaryCurveExists (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) (h5 : W.ModRepIsIrreducible 5) : ∃ W' : WeierstrassCurve ℤ, W'.Δ ≠ 0 ∧ W'.IsSemistableModel ∧ W'.ModRepIsIrreducible 3 ∧ ∃ φ : Submodule.torsionBy ℤ ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point (5 : ℕ) ≃ₗ[ZMod 5] Submodule.torsionBy ℤ ((W'.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point (5 : ℕ), ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : Submodule.torsionBy ℤ ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point (5 : ℕ)), φ (σ • x) = σ • φ x

77 theorems below · cites 20 · cited by 1 · depth 7 · proof 217 lines, 2 helpers

Specialisations with rootless $3$ -division polynomial in a weighted family WeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization

open Polynomial
theorem WeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization (a b : Polynomial ℚ) (ha : a.natDegree ≤ 20) (hb : b.natDegree ≤ 30) (hinf : 4 * a.coeff 20 ^ 3 + 27 * b.coeff 30 ^ 2 ≠ 0) (hroot : ∀ g : Polynomial ℚ, (⟨0, 0, 0, a, b⟩ : WeierstrassCurve (Polynomial ℚ)).Ψ₃.eval g ≠ 0) (M : ℕ) (hM : M ≠ 0) (m₀ : ℕ) : ∃ m : ℕ, m₀ ≤ m ∧ ∀ x : ℚ, ¬ (⟨0, 0, 0, a.eval ((M : ℚ) * m), b.eval ((M : ℚ) * m)⟩ : WeierstrassCurve ℚ).Ψ₃.IsRoot x

5 theorems below · cites 2 · cited by 1 · depth 8 · proof 119 lines, 9 helpers

Mod-3 irreducibility from $Ψ_{3}$ with no rational root WeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero

open WeierstrassCurve
theorem WeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero (V : WeierstrassCurve ℚ) (hΔ : V.Δ ≠ 0) (h : ∀ x : ℚ, V.Ψ₃.eval x ≠ 0) : Affine.Point.GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ V 3

3 theorems below · cites 3 · cited by 1 · depth 8 · proof 90 lines, 1 helpers

Mod- $5$ transport of residual modularity across the $3$ – $5$ switch WeierstrassCurve.isResiduallyModularOfLevel_of_switch

theorem WeierstrassCurve.isResiduallyModularOfLevel_of_switch {W W' : WeierstrassCurve ℤ} {N : ℕ}
    (hmod : W'.IsModularModelOfLevel N)
    (hND : ∀ ℓ : ℕ, ℓ.Prime → (ℓ : ℤ) ∣ W'.Δ → ℓ ∣ N)
    (hcong : ∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ → W'.IsGoodPrimeFor ℓ → ℓ ≠ 5 →
      (5 : ℤ) ∣ (W'.apOfModel ℓ - W.apOfModel ℓ)) :
    W.IsResiduallyModularOfLevel 5 N

0 theorems below · cites 0 · cited by 2 · depth 6 · proof 27 lines, 0 helpers

Weight-one form attached to a surjective mod-3 representation LanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift

set_option autoImplicit false
open AutomorphicForm FLT.ExplicitLift EisensteinWeightOne open WeierstrassCurve hiding cusp
open scoped MatrixGroups
local notation "Γℚ" => (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
theorem LanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift
    (ρ : Γℚ →* GL (Fin 2) (ZMod 3)) (hρ : Continuous ρ) (hsurj : Function.Surjective ρ)
    (hdet : ∀ σ : Γℚ, Matrix.GeneralLinearGroup.det (ρ σ) = modThreeCyclotomicChar σ)
    (Ψ : GL (Fin 2) (ZMod 3) →* GL (Fin 2) (ℤ√(-2)))
    (hΨ : ∀ g, Matrix.GeneralLinearGroup.map red (Ψ g) = g) :
    ∃ (N : ℕ) (_ : NeZero N) (b : ℕ → ℤ√(-2)),
      FormalHecke.IsEigensystem
        (fun ℓ => if ℓ ∣ N then 0 else ((chiNegThree ℓ : ℤ) : ℤ√(-2))) b ∧
      CuspForm.IsWeightOneChiNegThreeRealized N b ∧
      ∀ p : ℕ, p.Prime → ¬ p ∣ 3 * N →
        ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime p →
          ∀ σ : Γℚ, A.IsFrobeniusAt σ p →
            b p = ((Ψ (ρ σ) : GL (Fin 2) (ℤ√(-2))) : Matrix (Fin 2) (Fin 2) (ℤ√(-2))).trace

6,804 theorems below · cites 7 · cited by 2 · depth 9 · proof 776 lines, 65 helpers

From cuspidal adelic eigensystems to classical weight-one cusp forms AutomorphicForm.exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion

open CongruenceSubgroup EisensteinWeightOne
open scoped MatrixGroups ModularForm
theorem AutomorphicForm.exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion
    (Φ : HeckeEigensystem ℚ (ℤ√(-2))) (hΦ : AutomorphicForm.viaCompactCuspNotion.IsCusp ℚ Φ)
    (T : Finset ℕ) :
    ∃ (M : ℕ) (_ : NeZero M), 3 ∣ M ∧ (∀ ℓ ∈ T, ℓ ≠ 0 → ℓ ∣ M) ∧
      ∃ (g : CuspForm (Gamma1 M) 1) (b : ℕ → ℤ√(-2)),
        (∀ γ : SL(2, ℤ), γ ∈ Gamma0 M →
          (⇑g) ∣[(1 : ℤ)] γ = ((chiNegThree (((γ 1 1 : ℤ) : ZMod 3).val) : ℤ) : ℂ) • (⇑g)) ∧
        (∀ n, ModularFormClass.qCoeff (⇑g) n =
          ((b n).re : ℂ) + ((b n).im : ℂ) * ((Real.sqrt 2 : ℂ) * Complex.I)) ∧
        b 0 = 0 ∧
        FormalHecke.IsEigensystem
          (fun ℓ => if ℓ ∣ M then (0 : ℤ√(-2)) else ((chiNegThree ℓ : ℤ) : ℤ√(-2))) b ∧
        ∀ (p : ℕ) (hp : p.Prime), ¬ p ∣ 3 * M → b p = Φ.a (AutomorphicForm.ratPrime ⟨p, hp⟩)

6 theorems below · cites 2 · cited by 1 · depth 10 · proof 9,938 lines, 467 helpers

Modularity lifting at $p = 3$ from a prescribed residual level WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd

set_option autoImplicit false
open scoped WeierstrassCurve.Affine
theorem WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd (p : ℕ) (hp : p = 3)
    (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) (hirr : W.ModRepIsIrreducible p)
    (M₀ : ℕ) [NeZero M₀] (hres₀ : W.IsResiduallyModularOfLevel p M₀)
    (hns : p ^ 2 ∣ M₀ →
      ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime p →
        ∀ x : Submodule.torsionBy ℤ ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point p,
          (∀ σ ∈ A.inertiaSubgroupIn ℚ, σ • x = x) → x = 0)

    (hM₀3 : ∀ q : ℕ, q.Prime → q ≠ p → ¬ q ^ 3 ∣ M₀) :
    Mlc1IsModularModelOfExactConductorLevel W

23,032 theorems below · cites 18 · cited by 2 · depth 6 · proof 225 lines, 10 helpers

Modularity lifting at $p \in {3, 5}$ for $p^{2} ∤ M_{0}$ WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd

set_option autoImplicit false
open scoped WeierstrassCurve.Affine
theorem WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd (p : ℕ) (hp : p = 3 ∨ p = 5)
    (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) (hirr : W.ModRepIsIrreducible p)
    (M₀ : ℕ) [NeZero M₀] (hres₀ : W.IsResiduallyModularOfLevel p M₀)
    (hM₀ : ¬ p ^ 2 ∣ M₀)
    (hM₀3 : ∀ q : ℕ, q.Prime → q ≠ p → ¬ q ^ 3 ∣ M₀) :
    Mlc1IsModularModelOfExactConductorLevel W

22,708 theorems below · cites 18 · cited by 2 · depth 6 · proof 217 lines, 10 helpers

Representability of the ordinary deformation problem for a semistable curve WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
theorem WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel (p : ℕ) [Fact p.Prime] (hp2 : p ≠ 2) (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0)
    (hW : W.IsSemistableModel)
    (hcard₁ : Nat.card (Submodule.torsionBy ℤ
      ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point p) = p ^ 2)
    (hker : GaloisFactorsThroughFiniteLevel
      (WeierstrassCurve.Affine.Point.galoisRepModuleEnd (K := AlgebraicClosure ℚ) ℚ
        (W.map (Int.castRingHom ℚ)) p))
    (S : Finset ℕ) (hS : ∀ q ∈ S, q.Prime) (hpS : p ∈ S)
    (hbadS : ∀ q : ℕ, q.Prime → (q : ℤ) ∣ W.Δ → q ∈ S)
    {𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
    [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] [Finite (IsLocalRing.ResidueField 𝒪)]
    [CharZero 𝒪] (hp𝒪 : (p : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪)
    (ι : ZMod p →+* IsLocalRing.ResidueField 𝒪)
    (habs : (((W.map (Int.castRingHom ℚ)).residualGaloisRepOf p hcard₁ hker).baseChangeAlong
      ι).IsAbsolutelyIrreducible)
    (hord : ¬ W.IsGoodPrimeFor p ∨ ¬ (p : ℤ) ∣ W.apOfModel p) :
    Nonempty (GaloisRep.DeformationRingData 𝒪
      (((W.map (Int.castRingHom ℚ)).residualGaloisRepOf p hcard₁ hker).baseChangeAlong ι)
      (GaloisRep.ordinaryCondition 𝒪 p S))

169 theorems below · cites 5 · cited by 2 · depth 7 · proof 33 lines, 0 helpers

Taylor–Wiles patching: a patched level with zero relation ideal Algebra.PatchingDatum.nonempty_patchingLevel_bot

theorem Algebra.PatchingDatum.nonempty_patchingLevel_bot
    {𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
    [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] [Finite (IsLocalRing.ResidueField 𝒪)]
    {ℓ r : ℕ} (hℓ : (ℓ : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪)
    {R : Type} [CommRing R] [Algebra 𝒪 R] {M : Type} [AddCommGroup M] [Module R M]
    (P : Algebra.PatchingDatum 𝒪 ℓ r R M) :
    Nonempty (Algebra.PatchingLevel 𝒪 r R M ⊥)

5 theorems below · cites 5 · cited by 2 · depth 8 · proof 3,138 lines, 180 helpers

Existence of a surjection $R ↠ T$ GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum

theorem GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum {𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] {ρbar : ResidualGaloisRep (IsLocalRing.ResidueField 𝒪)} {𝒟 : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop} (D : GaloisRep.DeformationRingData 𝒪 ρbar 𝒟) {N : ℕ} [NeZero N] {S : Set ℕ} {θ : CuspForm.heckeAlgebra N 2 S →+* IsLocalRing.ResidueField 𝒪} {T : Type} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] [Algebra 𝒪 T] [IsLocalHom (algebraMap 𝒪 T)] [Module.Finite 𝒪 T] [Module.Free 𝒪 T] (H : CuspForm.HeckeGaloisRepDatum N S 𝒪 θ T) (hS : ∀ q : ℕ, q.Prime → q ∣ N → q ∈ S) (h𝒟 : 𝒟 H.ρ) (hres : H.ρ.residual.IsEquiv (ρbar.baseChangeAlong (IsLocalRing.ResidueField.map (algebraMap 𝒪 T)))) : ∃ φ : D.R →ₐ[𝒪] T, Function.Surjective φ ∧ ∃ hφ : IsLocalHom (φ : D.R →+* T), (D.ρ.baseChangeAlong (φ : D.R →+* T) hφ).IsEquiv H.ρ

6 theorems below · cites 1 · cited by 5 · depth 7 · proof 4 lines, 0 helpers

From a patching datum to modularity at an explicit level WeierstrassCurve.isModularModelOfLevel_of_patchingDatum

open Polynomial
theorem WeierstrassCurve.isModularModelOfLevel_of_patchingDatum (p : ℕ) (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) {𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪] [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] [Finite (IsLocalRing.ResidueField 𝒪)] [CharZero 𝒪] (hp𝒪 : (p : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪) {ρbar : ResidualGaloisRep (IsLocalRing.ResidueField 𝒪)} {𝒟 : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop} (D : GaloisRep.DeformationRingData 𝒪 ρbar 𝒟) {N : ℕ} [NeZero N] {S : Finset ℕ} (hSprime : ∀ q ∈ S, q.Prime) (hNS : ∀ q : ℕ, q.Prime → q ∣ N → q ∈ S) (hN : CuspForm.HasIntegralStructure N 2) {θ : CuspForm.heckeAlgebra N 2 (S : Set ℕ) →+* IsLocalRing.ResidueField 𝒪} {T : Type} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] [Algebra 𝒪 T] [IsLocalHom (algebraMap 𝒪 T)] [Module.Finite 𝒪 T] [Module.Free 𝒪 T] (H : CuspForm.HeckeGaloisRepDatum N (S : Set ℕ) 𝒪 θ T) (φ : D.R →ₐ[𝒪] T) (hφ : IsLocalHom (φ : D.R →+* T)) (hφρ : (D.ρ.baseChangeAlong (φ : D.R →+* T) hφ).IsEquiv H.ρ) {M : Type} [AddCommGroup M] [Module D.R M] [Module T M] [Nontrivial M] (hcompat : ∀ (x : D.R) (m : M), φ x • m = x • m) {r : ℕ} (P : Algebra.PatchingDatum 𝒪 p r D.R M) (ρW : GaloisRepAdic 𝒪) (h𝒟W : 𝒟 ρW) (hWres : ρW.residual.IsEquiv (ρbar.baseChangeAlong (IsLocalRing.ResidueField.map (algebraMap 𝒪 𝒪)))) (hWfrob : ∀ (ℓ : ℕ), ℓ.Prime → W.IsGoodPrimeFor ℓ → ℓ ∉ S → ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime ℓ → ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, A.IsFrobeniusAt σ ℓ → LinearMap.charpoly (ρW.ρ σ) = X ^ 2 - C ((W.apOfModel ℓ : ℤ) : 𝒪) * X + C ((ℓ : 𝒪))) :
    W.IsModularModelOfLevel (N * ∏ q ∈ S.filter (fun q => ¬ q ∣ N), q)

64 theorems below · cites 10 · cited by 2 · depth 7 · proof 112 lines, 0 helpers

Descent to the conductor level when $p^{2} ∤ N$ WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd

set_option autoImplicit false
theorem
WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd
    (W : WeierstrassCurve ℤ) (hss : W.IsSemistableModel) (N : ℕ)
    (p : ℕ) [Fact p.Prime] (hp2 : p ≠ 2) (hirr : W.ModRepIsIrreducible p)
    (hp2N : ¬ p ^ 2 ∣ N)
    (hN : W.IsModularModelOfLevel N) (hbad : ∀ ℓ : ℕ, ℓ.Prime → (ℓ : ℤ) ∣ W.Δ → ℓ ∣ N)
    (hN3 : ∀ q : ℕ, q.Prime → ¬ q ^ 3 ∣ N) :
    W.IsModularModelOfLevel W.conductorLevel

11,044 theorems below · cites 2 · cited by 2 · depth 7 · proof 84 lines, 4 helpers

Definition modules named here

16,030 theorems of the tree are first reached through this step, in the sense that the first landmark met on a shortest citation path up to fermat_last_theorem is one named in this section. That is a reading aid, not a classification: the infrastructure below modularity and level lowering is largely shared.

← §3 Irreducibility of the mod-p representation of the Frey curve · §5 Level lowering →