4. Modularity

4. Modularity. FreyPackage.frey_isModular follows from WeierstrassCurve.modularity_of_semistableModel: every integral Weierstrass model with Δ ≠ 0 and no prime dividing both Δ and c₄ (IsSemistableModel) is modular (IsModular: a_ℓ matches a normalised weight-2 eigenform on some Γ₀(N) at good primes; both in Definitions/Def_FLTPrelim_Modularity.lean; cusp forms, Γ₀(N) and q-expansions are Mathlib's). The proof is Wiles's:

  • one of ρ̄_{W,3}, ρ̄_{W,5} is irreducible (WeierstrassCurve.modThreeOrFiveIrreducible: if both were reducible W would have a rational 15-isogeny, and WeierstrassCurve.fifteenIsogenyClassification pins c₄³/Δ of such a curve to one of four values, none of which a semistable model can have);
  • Langlands-Tunnell in the weight-2, level-conditioned form Wiles uses, WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel: a weight-one form for the odd octahedral representation lifting ρ̄_{W,3} (LanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift, for surjective ρ̄₃ with cyclotomic determinant, by Tunnell's argument: monomial automorphy over the subfields cut out by subgroups of GL₂(F₃), cyclic base change, a converse theorem with Rankin-Selberg integrals), then multiplication by the Eisenstein series E₁(1, χ₋₃) and a Deligne-Serre lifting lemma to reach a congruent weight-2 eigenform;
  • two modularity lifting theorems, R = T by Taylor-Wiles patching in Diamond's formulation (GaloisRep.DeformationRingData, CuspForm.HeckeGaloisRepDatum, Algebra.PatchingDatum, GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum): WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd (p = 3; a condition on inertia-fixed 3-torsion when 9 divides the residual level) and WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd (p ∈ {3, 5}; p² not dividing the residual level);
  • the 3-5 switch WeierstrassCurve.threeFiveSwitchCurve (a second semistable model W′ with ρ̄_{W′,3} irreducible and a_ℓ(W′) ≡ a_ℓ(W) (mod 5) at common good primes ℓ ≠ 5, built beneath from a curve with W′[5] ≅ W[5] taken from an explicit family in the RubinSilverberg namespace) and WeierstrassCurve.isResiduallyModularOfLevel_of_switch. If ρ̄_{W,3} is irreducible, Langlands-Tunnell and lifting at 3; otherwise the switch gives W′, the first case makes W′ modular, W is residually modular mod 5, and lifting at 5 finishes.

Quoted from the route of the proof in PROOF-PATH.md of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0.

The landmarks the repository's web pages place in this step, in the order this step names them, then by name:

TheoremModularity# 

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.frey_isModular (P : FreyPackage) : P.freyCurve.IsModular

Quoted from Theorems/Thm_FreyPackage_frey_isModular.lean, line 131 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Wiles”, “Taylor-Wiles”, “modularity of the Frey curve”.

PROOF-PATH.md names it in 4. Modularity, as the theorem that carries step 4.

Lean

FreyPackage.frey_isModular, stated in Theorems/Thm_FreyPackage_frey_isModular.lean, line 131 and proved in P2M/Sol/S_FreyPackage_frey_isModular.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanFreyPackage.frey_isModular
Uses 1 · Used by 1
Proof usesWeierstrassCurve.modularity_of_semistableModel
Used byFreyPackage.no_frey_package

TheoremWeierstrassCurve.modularity_of_semistableModel# 

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem WeierstrassCurve.modularity_of_semistableModel (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0) (hW : W.IsSemistableModel) : (W.map (Int.castRingHom ℚ)).IsModular

Quoted from Theorems/Thm_WeierstrassCurve_modularity_of_semistableModel.lean, line 131 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Wiles”, “Taylor-Wiles”, “modularity theorem”, “semistable modularity”.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.modularity_of_semistableModel, stated in Theorems/Thm_WeierstrassCurve_modularity_of_semistableModel.lean, line 131 and proved in P2M/Sol/S_WeierstrassCurve_modularity_of_semistableModel.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.modularity_of_semistableModel
Uses 6 · Used by 1
Proof usesWeierstrassCurve.isResiduallyModularOfLevel_of_switch · WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel · WeierstrassCurve.modThreeOrFiveIrreducible · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd · WeierstrassCurve.threeFiveSwitchCurve
Used byModularity

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_modThreeOrFiveIrreducible.lean, line 15 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “3-5 trick”, “X0(15)”, “15-isogeny”.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.modThreeOrFiveIrreducible, stated in Theorems/Thm_WeierstrassCurve_modThreeOrFiveIrreducible.lean, line 15 and proved in P2M/Sol/S_WeierstrassCurve_modThreeOrFiveIrreducible.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.modThreeOrFiveIrreducible
Uses 1 · Used by 2
Proof usesWeierstrassCurve.fifteenIsogenyClassification
Used byWeierstrassCurve.modularity_of_semistableModel · FreyPackage.modularRepOfConductorLevel

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_fifteenIsogenyClassification.lean, line 8 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.fifteenIsogenyClassification, stated in Theorems/Thm_WeierstrassCurve_fifteenIsogenyClassification.lean, line 8 and proved in P2M/Sol/S_WeierstrassCurve_fifteenIsogenyClassification.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.fifteenIsogenyClassification
Used by 1
Used byWeierstrassCurve.modThreeOrFiveIrreducible

TheoremWeierstrassCurve.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)

Quoted from Theorems/Thm_WeierstrassCurve_isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel.lean, line 57 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Langlands-Tunnell”, “residual modularity mod 3”.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel, stated in Theorems/Thm_WeierstrassCurve_isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel.lean, line 57 and proved in P2M/Sol/S_WeierstrassCurve_isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel
Uses 1 · Used by 2
Proof usesLanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift
Used byWeierstrassCurve.modularity_of_semistableModel · FreyPackage.modularRepOfConductorLevel

TheoremLanglandsTunnell.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

Quoted from Theorems/Thm_LanglandsTunnell_exists_isWeightOneChiNegThreeRealized_eq_trace_lift.lean, line 56 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Langlands-Tunnell”, “Tunnell”, “octahedral”, “weight one form”.

PROOF-PATH.md names it in 4. Modularity.

Lean

LanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift, stated in Theorems/Thm_LanglandsTunnell_exists_isWeightOneChiNegThreeRealized_eq_trace_lift.lean, line 56 and proved in P2M/Sol/S_LanglandsTunnell_exists_isWeightOneChiNegThreeRealized_eq_trace_lift.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanLanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift
Uses 1 · Used by 1
Proof usesAutomorphicForm.exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion
Used byWeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel

TheoremGaloisRep.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.ρ

Quoted from Theorems/Thm_GaloisRep_DeformationRingData_exists_surjective_algHom_of_heckeGaloisRepDatum.lean, line 6 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “R=T”, “R = T”, “Taylor-Wiles patching”, “Diamond”.

PROOF-PATH.md names it in 4. Modularity.

Lean

GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum, stated in Theorems/Thm_GaloisRep_DeformationRingData_exists_surjective_algHom_of_heckeGaloisRepDatum.lean, line 6 and proved in P2M/Sol/S_GaloisRep_DeformationRingData_exists_surjective_algHom_of_heckeGaloisRepDatum.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanGaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum
Used by 2
Used byWeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd.lean, line 120 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “modularity lifting”, “R=T”, “R = T”, “Taylor-Wiles”, “p = 3”.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd, stated in Theorems/Thm_WeierstrassCurve_modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd.lean, line 120 and proved in P2M/Sol/S_WeierstrassCurve_modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd
Uses 8 · Used by 2
Proof usesAlgebra.PatchingDatum.nonempty_patchingLevel_bot · CuspForm.newformBadPrimeCoeff · GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum · ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd · WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd · WeierstrassCurve.isModularModelOfLevel_of_patchingDatum · WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf · WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel
Used byWeierstrassCurve.modularity_of_semistableModel · FreyPackage.modularRepOfConductorLevel

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd.lean, line 120 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “modularity lifting”, “R=T”, “R = T”, “Taylor-Wiles”, “p = 5”.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd, stated in Theorems/Thm_WeierstrassCurve_modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd.lean, line 120 and proved in P2M/Sol/S_WeierstrassCurve_modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd
Uses 8 · Used by 2
Proof usesAlgebra.PatchingDatum.nonempty_patchingLevel_bot · CuspForm.newformBadPrimeCoeff · GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum · ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd · WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd · WeierstrassCurve.isModularModelOfLevel_of_patchingDatum · WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf · WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel
Used byWeierstrassCurve.modularity_of_semistableModel · FreyPackage.modularRepOfConductorLevel

TheoremWeierstrassCurve.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 ℓ)

Quoted from Theorems/Thm_WeierstrassCurve_threeFiveSwitchCurve.lean, line 16 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “3-5 switch”, “three-five switch”, “Wiles”.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.threeFiveSwitchCurve, stated in Theorems/Thm_WeierstrassCurve_threeFiveSwitchCurve.lean, line 16 and proved in P2M/Sol/S_WeierstrassCurve_threeFiveSwitchCurve.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.threeFiveSwitchCurve
Uses 1 · Used by 2
Proof usesWeierstrassCurve.threeFiveAuxiliaryCurveExists
Used byWeierstrassCurve.modularity_of_semistableModel · FreyPackage.modularRepOfConductorLevel

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_isResiduallyModularOfLevel_of_switch.lean, line 5 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “3-5 switch”.

PROOF-PATH.md names it in 4. Modularity.

Lean

WeierstrassCurve.isResiduallyModularOfLevel_of_switch, stated in Theorems/Thm_WeierstrassCurve_isResiduallyModularOfLevel_of_switch.lean, line 5 and proved in P2M/Sol/S_WeierstrassCurve_isResiduallyModularOfLevel_of_switch.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.isResiduallyModularOfLevel_of_switch
Used by 2
Used byWeierstrassCurve.modularity_of_semistableModel · FreyPackage.modularRepOfConductorLevel

TheoremAlgebra.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 ⊥)

Quoted from Theorems/Thm_Algebra_PatchingDatum_nonempty_patchingLevel_bot.lean, line 7 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Taylor-Wiles patching”, “patching datum”.

Lean

Algebra.PatchingDatum.nonempty_patchingLevel_bot, stated in Theorems/Thm_Algebra_PatchingDatum_nonempty_patchingLevel_bot.lean, line 7 and proved in P2M/Sol/S_Algebra_PatchingDatum_nonempty_patchingLevel_bot.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanAlgebra.PatchingDatum.nonempty_patchingLevel_bot
Used by 3
Used byWeierstrassCurve.isModularModelOfLevel_of_patchingDatum · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd

TheoremAutomorphicForm.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⟩)

Quoted from Theorems/Thm_AutomorphicForm_exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion.lean, line 9 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Lean

AutomorphicForm.exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion, stated in Theorems/Thm_AutomorphicForm_exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion.lean, line 9 and proved in P2M/Sol/S_AutomorphicForm_exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanAutomorphicForm.exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion
Used by 1
Used byLanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift

TheoremResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd# 

theorem ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd {k : Type} [Field k]
    (ρ : ResidualGaloisRep k) (h2 : (2 : k) ≠ 0) (hirr : ρ.IsIrreducible) (hodd : ρ.IsOdd) :
    ρ.IsAbsolutelyIrreducible

Quoted from Theorems/Thm_ResidualGaloisRep_isAbsolutelyIrreducible_of_isIrreducible_of_isOdd.lean, line 5 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “absolutely irreducible”, “odd”.

PROOF-PATH.md names it in Exact strength of the named steps.

Lean

ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd, stated in Theorems/Thm_ResidualGaloisRep_isAbsolutelyIrreducible_of_isIrreducible_of_isOdd.lean, line 5 and proved in P2M/Sol/S_ResidualGaloisRep_isAbsolutelyIrreducible_of_isIrreducible_of_isOdd.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd
Used by 5
Used byWeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd · FreyPackage.level_lowering_at_p_of_conductorLevel · WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_exists_forall_not_isRoot_Psi3_specialization.lean, line 6 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Lean

WeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization, stated in Theorems/Thm_WeierstrassCurve_exists_forall_not_isRoot_Psi3_specialization.lean, line 6 and proved in P2M/Sol/S_WeierstrassCurve_exists_forall_not_isRoot_Psi3_specialization.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization
Used by 1
Used byWeierstrassCurve.threeFiveAuxiliaryCurveExists

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero.lean, line 9 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Lean

WeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero, stated in Theorems/Thm_WeierstrassCurve_galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero.lean, line 9 and proved in P2M/Sol/S_WeierstrassCurve_galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero
Used by 1
Used byWeierstrassCurve.threeFiveAuxiliaryCurveExists

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd.lean, line 86 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Lean

WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd, stated in Theorems/Thm_WeierstrassCurve_isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd.lean, line 86 and proved in P2M/Sol/S_WeierstrassCurve_isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd
Uses 2 · Used by 2
Proof usesCuspForm.newformBadPrimeCoeff · ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd
Used byWeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd

TheoremWeierstrassCurve.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)

Quoted from Theorems/Thm_WeierstrassCurve_isModularModelOfLevel_of_patchingDatum.lean, line 11 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Lean

WeierstrassCurve.isModularModelOfLevel_of_patchingDatum, stated in Theorems/Thm_WeierstrassCurve_isModularModelOfLevel_of_patchingDatum.lean, line 11 and proved in P2M/Sol/S_WeierstrassCurve_isModularModelOfLevel_of_patchingDatum.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.isModularModelOfLevel_of_patchingDatum
Uses 1 · Used by 2
Proof usesAlgebra.PatchingDatum.nonempty_patchingLevel_bot
Used byWeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd

TheoremWeierstrassCurve.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))

Quoted from Theorems/Thm_WeierstrassCurve_nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel.lean, line 21 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Lean

WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel, stated in Theorems/Thm_WeierstrassCurve_nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel.lean, line 21 and proved in P2M/Sol/S_WeierstrassCurve_nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel
Used by 2
Used byWeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd · WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd

TheoremWeierstrassCurve.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

Quoted from Theorems/Thm_WeierstrassCurve_threeFiveAuxiliaryCurveExists.lean, line 8 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “3-5 switch”, “Rubin-Silverberg family”.

Lean

WeierstrassCurve.threeFiveAuxiliaryCurveExists, stated in Theorems/Thm_WeierstrassCurve_threeFiveAuxiliaryCurveExists.lean, line 8 and proved in P2M/Sol/S_WeierstrassCurve_threeFiveAuxiliaryCurveExists.lean. Read at commit 6e837e75, without running Lean.

Sources
LeanWeierstrassCurve.threeFiveAuxiliaryCurveExists
Uses 2 · Used by 1
Proof usesWeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization · WeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero
Used byWeierstrassCurve.threeFiveSwitchCurve

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.