5. Level lowering

5. Level lowering. FreyPackage.level_lowering_to_two: E_P modular and ρ̄_{E_P,p} irreducible give a nonzero f : CuspForm (CongruenceSubgroup.Gamma0 2) 2. First FreyPackage.modularRepOfConductorLevel: the representation arises from a squarefree level supported on the primes dividing abc, "arises from" (ModularRepOfLevel, Definitions/Def_FLTPrelim_ModularRep.lean) being a congruence of traces modulo a prime above p, not an isomorphism of representations (this proof re-derives modularity itself, so the IsModular hypothesis above is formally unused). Then primes are removed one at a time (FreyPackage.level_lowering_to_two_of_conductorLevel): an odd q ≠ p, at which E_P[p] is unramified, by FreyPackage.level_lowering_odd_prime_of_conductorLevel, Ribet's theorem in the form needed (Čerednik-Drinfeld uniformisation, CerednikDrinfeld namespace); p itself by FreyPackage.level_lowering_at_p_of_conductorLevel, the Mazur-Ribet step, using that E_P[p] is finite at p (FreyCurve.isPeuRamifieeAt_odd_of_integralForm). Levels 1 and 2 are closed by ModularForm.S2_Gamma0_one_eq_zero and step 6.

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:

TheoremLevel lowering#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.level_lowering_to_two (P : FreyPackage) (hmod : P.freyCurve.IsModular) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) : ∃ f : CuspForm (CongruenceSubgroup.Gamma0 2) 2, f ≠ 0

Quoted from Theorems/Thm_FreyPackage_level_lowering_to_two.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: “Ribet”, “level lowering”, “epsilon conjecture”.

PROOF-PATH.md names it in 5. Level lowering, as the theorem that carries step 5.

Lean

FreyPackage.level_lowering_to_two, stated in Theorems/Thm_FreyPackage_level_lowering_to_two.lean, line 131 and proved in P2M/Sol/S_FreyPackage_level_lowering_to_two.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.level_lowering_to_two in Theorems/Thm_FreyPackage_level_lowering_to_two.lean
• Proof of FreyPackage.level_lowering_to_two in P2M/Sol/S_FreyPackage_level_lowering_to_two.lean
• The repository's documentation page for FreyPackage.level_lowering_to_two

LeanFreyPackage.level_lowering_to_two

Uses 2 · Used by 1

Proof usesFreyPackage.level_lowering_to_two_of_conductorLevel · FreyPackage.modularRepOfConductorLevel

Used byFreyPackage.no_frey_package

TheoremFreyPackage.modularRepOfConductorLevel#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.modularRepOfConductorLevel (P : FreyPackage) : ∃ N : ℕ, P.IsConductorLevel N ∧ P.ModularRepOfLevel N

Quoted from Theorems/Thm_FreyPackage_modularRepOfConductorLevel.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: “arises from level N”, “conductor level”.

PROOF-PATH.md names it in 5. Level lowering.

Lean

FreyPackage.modularRepOfConductorLevel, stated in Theorems/Thm_FreyPackage_modularRepOfConductorLevel.lean, line 131 and proved in P2M/Sol/S_FreyPackage_modularRepOfConductorLevel.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.modularRepOfConductorLevel in Theorems/Thm_FreyPackage_modularRepOfConductorLevel.lean
• Proof of FreyPackage.modularRepOfConductorLevel in P2M/Sol/S_FreyPackage_modularRepOfConductorLevel.lean
• The repository's documentation page for FreyPackage.modularRepOfConductorLevel

LeanFreyPackage.modularRepOfConductorLevel

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 byLevel lowering

TheoremFreyPackage.level_lowering_to_two_of_conductorLevel#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.level_lowering_to_two_of_conductorLevel (P : FreyPackage) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) {N : ℕ} (hcond : P.IsConductorLevel N) (hmod : P.ModularRepOfLevel N) : ∃ f : CuspForm (CongruenceSubgroup.Gamma0 2) 2, f ≠ 0

Quoted from Theorems/Thm_FreyPackage_level_lowering_to_two_of_conductorLevel.lean, line 91 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 5. Level lowering.

Lean

FreyPackage.level_lowering_to_two_of_conductorLevel, stated in Theorems/Thm_FreyPackage_level_lowering_to_two_of_conductorLevel.lean, line 91 and proved in P2M/Sol/S_FreyPackage_level_lowering_to_two_of_conductorLevel.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.level_lowering_to_two_of_conductorLevel in Theorems/Thm_FreyPackage_level_lowering_to_two_of_conductorLevel.lean
• Proof of FreyPackage.level_lowering_to_two_of_conductorLevel in P2M/Sol/S_FreyPackage_level_lowering_to_two_of_conductorLevel.lean
• The repository's documentation page for FreyPackage.level_lowering_to_two_of_conductorLevel

LeanFreyPackage.level_lowering_to_two_of_conductorLevel

Uses 5 · Used by 1

Proof usesFreyPackage.freyGaloisRep_isUnramifiedAt · FreyPackage.level_lowering_at_p_of_conductorLevel · FreyPackage.level_lowering_odd_prime_of_conductorLevel · S₂(Γ₀(2)) = 0 · ModularForm.S2_Gamma0_one_eq_zero

Used byLevel lowering

TheoremFreyPackage.level_lowering_odd_prime_of_conductorLevel#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.level_lowering_odd_prime_of_conductorLevel (P : FreyPackage) {N q : ℕ} (hcond : P.IsConductorLevel N) (hq : q.Prime) (hq2 : q ≠ 2) (hqp : q ≠ P.p) (hqN : q ∣ N) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) (hmod : P.ModularRepOfLevel N) (hunr : P.GaloisRepUnramifiedAt q) : ∃ M : ℕ, M ∣ N ∧ ¬ q ∣ M ∧ P.ModularRepOfLevel M

Quoted from Theorems/Thm_FreyPackage_level_lowering_odd_prime_of_conductorLevel.lean, line 90 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: “Ribet”, “Cerednik-Drinfeld”, “Čerednik-Drinfeld”.

PROOF-PATH.md names it in 5. Level lowering.

Lean

FreyPackage.level_lowering_odd_prime_of_conductorLevel, stated in Theorems/Thm_FreyPackage_level_lowering_odd_prime_of_conductorLevel.lean, line 90 and proved in P2M/Sol/S_FreyPackage_level_lowering_odd_prime_of_conductorLevel.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.level_lowering_odd_prime_of_conductorLevel in Theorems/Thm_FreyPackage_level_lowering_odd_prime_of_conductorLevel.lean
• Proof of FreyPackage.level_lowering_odd_prime_of_conductorLevel in P2M/Sol/S_FreyPackage_level_lowering_odd_prime_of_conductorLevel.lean
• The repository's documentation page for FreyPackage.level_lowering_odd_prime_of_conductorLevel

LeanFreyPackage.level_lowering_odd_prime_of_conductorLevel

Uses 2 · Used by 1

Proof usesFreyPackage.eigenformResidualAttachmentAtFamily · WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf

Used byFreyPackage.level_lowering_to_two_of_conductorLevel

TheoremFreyPackage.level_lowering_at_p_of_conductorLevel#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.level_lowering_at_p_of_conductorLevel (P : FreyPackage) {N : ℕ} (hcond : P.IsConductorLevel N) (hpN : P.p ∣ N) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) (hmod : P.ModularRepOfLevel N) : ∃ M : ℕ, M ∣ N ∧ ¬ P.p ∣ M ∧ P.ModularRepOfLevel M

Quoted from Theorems/Thm_FreyPackage_level_lowering_at_p_of_conductorLevel.lean, line 70 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: “Mazur-Ribet”, “level lowering at p”.

PROOF-PATH.md names it in 5. Level lowering.

Lean

FreyPackage.level_lowering_at_p_of_conductorLevel, stated in Theorems/Thm_FreyPackage_level_lowering_at_p_of_conductorLevel.lean, line 70 and proved in P2M/Sol/S_FreyPackage_level_lowering_at_p_of_conductorLevel.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.level_lowering_at_p_of_conductorLevel in Theorems/Thm_FreyPackage_level_lowering_at_p_of_conductorLevel.lean
• Proof of FreyPackage.level_lowering_at_p_of_conductorLevel in P2M/Sol/S_FreyPackage_level_lowering_at_p_of_conductorLevel.lean
• The repository's documentation page for FreyPackage.level_lowering_at_p_of_conductorLevel

LeanFreyPackage.level_lowering_at_p_of_conductorLevel

Uses 4 · Used by 1

Proof usesCuspForm.newformBadPrimeCoeff · FreyCurve.isPeuRamifieeAt_odd_of_integralForm · FreyPackage.eigenformResidualAttachmentAtFamily · ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd

Used byFreyPackage.level_lowering_to_two_of_conductorLevel

TheoremFreyCurve.isPeuRamifieeAt_odd_of_integralForm#

open FreyPackage
namespace FreyCurve
theorem isPeuRamifieeAt_odd_of_integralForm (P : FreyPackage) {q : ℕ} [Fact q.Prime]
    (hq2 : q ≠ 2) : P.freyCurve.IsPeuRamifieeAt P.p q

Quoted from Theorems/Thm_FreyCurve_isPeuRamifieeAt_odd_of_integralForm.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: “peu ramifiee”, “finite at p”.

PROOF-PATH.md names it in 5. Level lowering.

Lean

FreyCurve.isPeuRamifieeAt_odd_of_integralForm, stated in Theorems/Thm_FreyCurve_isPeuRamifieeAt_odd_of_integralForm.lean, line 8 and proved in P2M/Sol/S_FreyCurve_isPeuRamifieeAt_odd_of_integralForm.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyCurve.isPeuRamifieeAt_odd_of_integralForm in Theorems/Thm_FreyCurve_isPeuRamifieeAt_odd_of_integralForm.lean
• Proof of FreyCurve.isPeuRamifieeAt_odd_of_integralForm in P2M/Sol/S_FreyCurve_isPeuRamifieeAt_odd_of_integralForm.lean
• The repository's documentation page for FreyCurve.isPeuRamifieeAt_odd_of_integralForm

LeanFreyCurve.isPeuRamifieeAt_odd_of_integralForm

Used by 1

Used byFreyPackage.level_lowering_at_p_of_conductorLevel

TheoremCuspForm.newformBadPrimeCoeff#

set_option autoImplicit false
theorem CuspForm.newformBadPrimeCoeff (N : ℕ) :
    CuspForm.NewformBadPrimeCoeff N

Quoted from Theorems/Thm_CuspForm_newformBadPrimeCoeff.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 :=.

Lean

CuspForm.newformBadPrimeCoeff, stated in Theorems/Thm_CuspForm_newformBadPrimeCoeff.lean, line 7 and proved in P2M/Sol/S_CuspForm_newformBadPrimeCoeff.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of CuspForm.newformBadPrimeCoeff in Theorems/Thm_CuspForm_newformBadPrimeCoeff.lean
• Proof of CuspForm.newformBadPrimeCoeff in P2M/Sol/S_CuspForm_newformBadPrimeCoeff.lean
• The repository's documentation page for CuspForm.newformBadPrimeCoeff

LeanCuspForm.newformBadPrimeCoeff

Used by 4

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

TheoremFreyPackage.eigenformResidualAttachmentAtFamily#

theorem FreyPackage.eigenformResidualAttachmentAtFamily (P : FreyPackage) :
    ∀ M : ℕ, 0 < M → P.EigenformResidualAttachmentAt M

Quoted from Theorems/Thm_FreyPackage_eigenformResidualAttachmentAtFamily.lean, line 24 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

FreyPackage.eigenformResidualAttachmentAtFamily, stated in Theorems/Thm_FreyPackage_eigenformResidualAttachmentAtFamily.lean, line 24 and proved in P2M/Sol/S_FreyPackage_eigenformResidualAttachmentAtFamily.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.eigenformResidualAttachmentAtFamily in Theorems/Thm_FreyPackage_eigenformResidualAttachmentAtFamily.lean
• Proof of FreyPackage.eigenformResidualAttachmentAtFamily in P2M/Sol/S_FreyPackage_eigenformResidualAttachmentAtFamily.lean
• The repository's documentation page for FreyPackage.eigenformResidualAttachmentAtFamily

LeanFreyPackage.eigenformResidualAttachmentAtFamily

Used by 2

Used byFreyPackage.level_lowering_at_p_of_conductorLevel · FreyPackage.level_lowering_odd_prime_of_conductorLevel

TheoremFreyPackage.freyGaloisRep_isUnramifiedAt#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.freyGaloisRep_isUnramifiedAt (P : FreyPackage) {q : ℕ} (hq : q.Prime) (hq2 : q ≠ 2) (hqp : q ≠ P.p) : P.GaloisRepUnramifiedAt q

Quoted from Theorems/Thm_FreyPackage_freyGaloisRep_isUnramifiedAt.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 :=.

Lean

FreyPackage.freyGaloisRep_isUnramifiedAt, stated in Theorems/Thm_FreyPackage_freyGaloisRep_isUnramifiedAt.lean, line 15 and proved in P2M/Sol/S_FreyPackage_freyGaloisRep_isUnramifiedAt.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.freyGaloisRep_isUnramifiedAt in Theorems/Thm_FreyPackage_freyGaloisRep_isUnramifiedAt.lean
• Proof of FreyPackage.freyGaloisRep_isUnramifiedAt in P2M/Sol/S_FreyPackage_freyGaloisRep_isUnramifiedAt.lean
• The repository's documentation page for FreyPackage.freyGaloisRep_isUnramifiedAt

LeanFreyPackage.freyGaloisRep_isUnramifiedAt

Used by 2

Used byFreyPackage.frey_reducible_hasCofixedLine · FreyPackage.level_lowering_to_two_of_conductorLevel

TheoremWeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf#

set_option autoImplicit false

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point

theorem WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf
    (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))
    (_hirr : W.ModRepIsIrreducible p) (M q : ℕ) (hq : q.Prime) (hqp : q ≠ p)
    (hqM : q ∣ M) (hq2 : ¬ q ^ 2 ∣ M) (hM : Squarefree M)
    (hunr : ((W.map (Int.castRingHom ℚ)).residualGaloisRepOf p hcard₁ hker).IsUnramifiedAt q)
    (hres : W.IsResiduallyModularOfLevel p M) :
    W.IsResiduallyModularOfLevel p (M / q)

Quoted from Theorems/Thm_WeierstrassCurve_isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf.lean, line 87 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.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf, stated in Theorems/Thm_WeierstrassCurve_isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf.lean, line 87 and proved in P2M/Sol/S_WeierstrassCurve_isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf in Theorems/Thm_WeierstrassCurve_isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf.lean
• Proof of WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf in P2M/Sol/S_WeierstrassCurve_isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf.lean
• The repository's documentation page for WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf

LeanWeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf

Uses 1 · Used by 3

Proof usesResidualGaloisRep.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 · FreyPackage.level_lowering_odd_prime_of_conductorLevel

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.