3. Irreducibility

3. Irreducibility. FreyPackage.Mazur_Frey proves GaloisRepIsIrreducible ℚ P.freyCurve P.p (Definitions/Def_FLTPrelim_GaloisRep.lean: E_P[p] is nontrivial with no Galois-stable F_p-submodule besides 0 and itself). The case a ≡ 3 (mod 8) has its own argument at the prime 2 (FreyPackage.Mazur_Frey_of_a_mod_eight). Otherwise reducibility would give a Galois-stable line with trivial action on the quotient (FreyPackage.frey_reducible_hasCofixedLine, Serre's observation, using that E_P has no rational point of order p), excluded in three ranges:

• p ≥ 17: FreyPackage.frey_no_cofixed_large, Mazur's Eisenstein-ideal argument carried out for this situation (X₀(N), its Jacobian and Néron model, the cuspidal subgroup, the Eisenstein quotient; ModularCurve and AlgebraicGeometry namespaces; the global input is WeierstrassCurve.mazurStepThree_not_inZeroComponentAt). This is by far the largest part of the step.
• p = 11 (FreyPackage.frey_no_cofixed_eleven) and p ∈ {5, 7, 13} (FreyPackage.frey_no_cofixed_small) hold vacuously because those exponents are settled outright: fermatLastTheoremFive by a self-contained descent in Z[(1+√5)/2]; fermatLastTheoremSeven, …Eleven, …Thirteen by Kummer's theorem for regular primes flt_regular (a port of the flt-regular project: cases I and II, Kummer's lemma via Hilbert's theorems 90-94) plus proofs that the rings of integers of the 7th, 11th and 13th cyclotomic fields are principal (IsCyclotomicExtension.Rat.seven_pid, ….eleven_pid, ….thirteen_pid).

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:

TheoremIrreducibility#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.Mazur_Frey (P : FreyPackage) : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p

Quoted from Theorems/Thm_FreyPackage_Mazur_Frey.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”, “irreducibility of the mod-p representation”.

PROOF-PATH.md names it in 3. Irreducibility, as the theorem that carries step 3.

Lean

FreyPackage.Mazur_Frey, stated in Theorems/Thm_FreyPackage_Mazur_Frey.lean, line 70 and proved in P2M/Sol/S_FreyPackage_Mazur_Frey.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.Mazur_Frey in Theorems/Thm_FreyPackage_Mazur_Frey.lean
• Proof of FreyPackage.Mazur_Frey in P2M/Sol/S_FreyPackage_Mazur_Frey.lean
• The repository's documentation page for FreyPackage.Mazur_Frey

LeanFreyPackage.Mazur_Frey

Uses 5 · Used by 1

Proof usesFreyPackage.Mazur_Frey_of_a_mod_eight · FreyPackage.frey_no_cofixed_eleven · FreyPackage.frey_no_cofixed_large · FreyPackage.frey_no_cofixed_small · FreyPackage.frey_reducible_hasCofixedLine

Used byFreyPackage.no_frey_package

TheoremFreyPackage.Mazur_Frey_of_a_mod_eight#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
theorem FreyPackage.Mazur_Frey_of_a_mod_eight (P : FreyPackage)
    (h8 : (P.a : ZMod 8) = 3) :
    GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p

Quoted from Theorems/Thm_FreyPackage_Mazur_Frey_of_a_mod_eight.lean, line 12 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 3. Irreducibility.

Lean

FreyPackage.Mazur_Frey_of_a_mod_eight, stated in Theorems/Thm_FreyPackage_Mazur_Frey_of_a_mod_eight.lean, line 12 and proved in P2M/Sol/S_FreyPackage_Mazur_Frey_of_a_mod_eight.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.Mazur_Frey_of_a_mod_eight in Theorems/Thm_FreyPackage_Mazur_Frey_of_a_mod_eight.lean
• Proof of FreyPackage.Mazur_Frey_of_a_mod_eight in P2M/Sol/S_FreyPackage_Mazur_Frey_of_a_mod_eight.lean
• The repository's documentation page for FreyPackage.Mazur_Frey_of_a_mod_eight

LeanFreyPackage.Mazur_Frey_of_a_mod_eight

Uses 1 · Used by 1

Proof usesFreyPackage.frey_reducible_hasCofixedLine

Used byIrreducibility

TheoremFreyPackage.frey_reducible_hasCofixedLine#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.frey_reducible_hasCofixedLine (P : FreyPackage) (hred : ¬ GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) : HasGaloisStableCofixedLine (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p

Quoted from Theorems/Thm_FreyPackage_frey_reducible_hasCofixedLine.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: “Serre”, “cofixed line”.

PROOF-PATH.md names it in 3. Irreducibility.

Lean

FreyPackage.frey_reducible_hasCofixedLine, stated in Theorems/Thm_FreyPackage_frey_reducible_hasCofixedLine.lean, line 15 and proved in P2M/Sol/S_FreyPackage_frey_reducible_hasCofixedLine.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.frey_reducible_hasCofixedLine in Theorems/Thm_FreyPackage_frey_reducible_hasCofixedLine.lean
• Proof of FreyPackage.frey_reducible_hasCofixedLine in P2M/Sol/S_FreyPackage_frey_reducible_hasCofixedLine.lean
• The repository's documentation page for FreyPackage.frey_reducible_hasCofixedLine

LeanFreyPackage.frey_reducible_hasCofixedLine

Uses 1 · Used by 2

Proof usesFreyPackage.freyGaloisRep_isUnramifiedAt

Used byIrreducibility · FreyPackage.Mazur_Frey_of_a_mod_eight

TheoremFreyPackage.frey_no_cofixed_large#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.frey_no_cofixed_large (P : FreyPackage) (hp : 17 ≤ P.p) : ¬ HasGaloisStableCofixedLine (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p

Quoted from Theorems/Thm_FreyPackage_frey_no_cofixed_large.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”, “Eisenstein ideal”, “Eisenstein quotient”.

PROOF-PATH.md names it in 3. Irreducibility.

Lean

FreyPackage.frey_no_cofixed_large, stated in Theorems/Thm_FreyPackage_frey_no_cofixed_large.lean, line 70 and proved in P2M/Sol/S_FreyPackage_frey_no_cofixed_large.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.frey_no_cofixed_large in Theorems/Thm_FreyPackage_frey_no_cofixed_large.lean
• Proof of FreyPackage.frey_no_cofixed_large in P2M/Sol/S_FreyPackage_frey_no_cofixed_large.lean
• The repository's documentation page for FreyPackage.frey_no_cofixed_large

LeanFreyPackage.frey_no_cofixed_large

Uses 1 · Used by 1

Proof usesWeierstrassCurve.mazurStepThree_not_inZeroComponentAt

Used byIrreducibility

TheoremWeierstrassCurve.mazurStepThree_not_inZeroComponentAt#

open WeierstrassCurve WeierstrassCurve.Affine
theorem WeierstrassCurve.mazurStepThree_not_inZeroComponentAt
    {p : ℕ} (hp : p.Prime) (hp' : p ∉ ({2, 3, 5, 7, 13} : Finset ℕ))
    (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0)
    (Q : ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point)
    (hQfix : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, σ • Q = Q)
    (hQord : addOrderOf Q = p)
    (h2Δ : (2 : ℤ) ∣ W.Δ) (h2c₄ : ¬ (2 : ℤ) ∣ W.c₄)
    (h2 : ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime 2 → ¬ W.InZeroComponentAt A Q)
    (h3Δ : (3 : ℤ) ∣ W.Δ) (h3c₄ : ¬ (3 : ℤ) ∣ W.c₄)
    (h3 : ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime 3 → ¬ W.InZeroComponentAt A Q)
    {ℓ : ℕ} (hℓ : ℓ.Prime) (hℓp : ℓ ≠ p) (hℓΔ : (ℓ : ℤ) ∣ W.Δ) (hℓc₄ : ¬ (ℓ : ℤ) ∣ W.c₄)
    (A : ValuationSubring (AlgebraicClosure ℚ)) (hA : A.LiesOverPrime ℓ) :
    ¬ W.InZeroComponentAt A Q

Quoted from Theorems/Thm_WeierstrassCurve_mazurStepThree_not_inZeroComponentAt.lean, line 65 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 Step 3”.

PROOF-PATH.md names it in 3. Irreducibility.

Lean

WeierstrassCurve.mazurStepThree_not_inZeroComponentAt, stated in Theorems/Thm_WeierstrassCurve_mazurStepThree_not_inZeroComponentAt.lean, line 65 and proved in P2M/Sol/S_WeierstrassCurve_mazurStepThree_not_inZeroComponentAt.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of WeierstrassCurve.mazurStepThree_not_inZeroComponentAt in Theorems/Thm_WeierstrassCurve_mazurStepThree_not_inZeroComponentAt.lean
• Proof of WeierstrassCurve.mazurStepThree_not_inZeroComponentAt in P2M/Sol/S_WeierstrassCurve_mazurStepThree_not_inZeroComponentAt.lean
• The repository's documentation page for WeierstrassCurve.mazurStepThree_not_inZeroComponentAt

LeanWeierstrassCurve.mazurStepThree_not_inZeroComponentAt

Uses 2 · Used by 1

Proof usesModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar · ModularCurve.mazurQuotientSpecialization_heckeModuleBar

Used byFreyPackage.frey_no_cofixed_large

TheoremFreyPackage.frey_no_cofixed_eleven#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.frey_no_cofixed_eleven (P : FreyPackage) (hp : P.p = 11) : ¬ HasGaloisStableCofixedLine (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p

Quoted from Theorems/Thm_FreyPackage_frey_no_cofixed_eleven.lean, line 13 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 3. Irreducibility.

Lean

FreyPackage.frey_no_cofixed_eleven, stated in Theorems/Thm_FreyPackage_frey_no_cofixed_eleven.lean, line 13 and proved in P2M/Sol/S_FreyPackage_frey_no_cofixed_eleven.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.frey_no_cofixed_eleven in Theorems/Thm_FreyPackage_frey_no_cofixed_eleven.lean
• Proof of FreyPackage.frey_no_cofixed_eleven in P2M/Sol/S_FreyPackage_frey_no_cofixed_eleven.lean
• The repository's documentation page for FreyPackage.frey_no_cofixed_eleven

LeanFreyPackage.frey_no_cofixed_eleven

Uses 1 · Used by 1

Proof usesflt_regular

Used byIrreducibility

TheoremFreyPackage.frey_no_cofixed_small#

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.frey_no_cofixed_small (P : FreyPackage) (hp : P.p = 5 ∨ P.p = 7 ∨ P.p = 13) : ¬ HasGaloisStableCofixedLine (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p

Quoted from Theorems/Thm_FreyPackage_frey_no_cofixed_small.lean, line 13 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 3. Irreducibility.

Lean

FreyPackage.frey_no_cofixed_small, stated in Theorems/Thm_FreyPackage_frey_no_cofixed_small.lean, line 13 and proved in P2M/Sol/S_FreyPackage_frey_no_cofixed_small.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.frey_no_cofixed_small in Theorems/Thm_FreyPackage_frey_no_cofixed_small.lean
• Proof of FreyPackage.frey_no_cofixed_small in P2M/Sol/S_FreyPackage_frey_no_cofixed_small.lean
• The repository's documentation page for FreyPackage.frey_no_cofixed_small

LeanFreyPackage.frey_no_cofixed_small

Uses 3 · Used by 1

Proof usesfermatLastTheoremFive · fermatLastTheoremSeven · flt_regular

Used byIrreducibility

TheoremfermatLastTheoremFive#

theorem fermatLastTheoremFive : FermatLastTheoremFor 5

Quoted from Theorems/Thm_fermatLastTheoremFive.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: “descent”, “exponent 5”.

PROOF-PATH.md names it in 3. Irreducibility.

Lean

fermatLastTheoremFive, stated in Theorems/Thm_fermatLastTheoremFive.lean, line 5 and proved in P2M/Sol/S_fermatLastTheoremFive.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of fermatLastTheoremFive in Theorems/Thm_fermatLastTheoremFive.lean
• Proof of fermatLastTheoremFive in P2M/Sol/S_fermatLastTheoremFive.lean
• The repository's documentation page for fermatLastTheoremFive

LeanfermatLastTheoremFive

Used by 1

Used byFreyPackage.frey_no_cofixed_small

TheoremfermatLastTheoremSeven#

theorem fermatLastTheoremSeven : FermatLastTheoremFor 7

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

PROOF-PATH.md names it in 3. Irreducibility.

Lean

fermatLastTheoremSeven, stated in Theorems/Thm_fermatLastTheoremSeven.lean, line 5 and proved in P2M/Sol/S_fermatLastTheoremSeven.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of fermatLastTheoremSeven in Theorems/Thm_fermatLastTheoremSeven.lean
• Proof of fermatLastTheoremSeven in P2M/Sol/S_fermatLastTheoremSeven.lean
• The repository's documentation page for fermatLastTheoremSeven

LeanfermatLastTheoremSeven

Uses 2 · Used by 1

Proof usesIsCyclotomicExtension.Rat.seven_pid · flt_regular

Used byFreyPackage.frey_no_cofixed_small

Theoremflt_regular#

open scoped NumberField
theorem flt_regular {p : ℕ} [Fact p.Prime] (hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField p ℚ))))) (hodd : p ≠ 2) : FermatLastTheoremFor p

Quoted from Theorems/Thm_flt_regular.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: “Kummer”, “regular primes”, “flt-regular”.

PROOF-PATH.md names it in 3. Irreducibility.

Lean

flt_regular, stated in Theorems/Thm_flt_regular.lean, line 6 and proved in P2M/Sol/S_flt_regular.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of flt_regular in Theorems/Thm_flt_regular.lean
• Proof of flt_regular in P2M/Sol/S_flt_regular.lean
• The repository's documentation page for flt_regular

Leanflt_regular

Used by 3

Used byfermatLastTheoremSeven · FreyPackage.frey_no_cofixed_eleven · FreyPackage.frey_no_cofixed_small

TheoremIsCyclotomicExtension.Rat.seven_pid#

open scoped NumberField
theorem IsCyclotomicExtension.Rat.seven_pid (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {7} ℚ K] : IsPrincipalIdealRing (𝓞 K)

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

PROOF-PATH.md names it in 3. Irreducibility.

Lean

IsCyclotomicExtension.Rat.seven_pid, stated in Theorems/Thm_IsCyclotomicExtension_Rat_seven_pid.lean, line 6 and proved in P2M/Sol/S_IsCyclotomicExtension_Rat_seven_pid.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of IsCyclotomicExtension.Rat.seven_pid in Theorems/Thm_IsCyclotomicExtension_Rat_seven_pid.lean
• Proof of IsCyclotomicExtension.Rat.seven_pid in P2M/Sol/S_IsCyclotomicExtension_Rat_seven_pid.lean
• The repository's documentation page for IsCyclotomicExtension.Rat.seven_pid

LeanIsCyclotomicExtension.Rat.seven_pid

Used by 1

Used byfermatLastTheoremSeven

TheoremModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar#

open ModularCurve AlgebraicCurve
theorem ModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar (p : ℕ) [Fact p.Prime]
    (hcomm : HeckeOperatorsCommuteBar p) :
    EisensteinQuotientInvariantsFiniteAt p (heckeModuleBar p)

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

ModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar, stated in Theorems/Thm_ModularCurve_eisensteinQuotientInvariantsFiniteAt_heckeModuleBar.lean, line 61 and proved in P2M/Sol/S_ModularCurve_eisensteinQuotientInvariantsFiniteAt_heckeModuleBar.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of ModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar in Theorems/Thm_ModularCurve_eisensteinQuotientInvariantsFiniteAt_heckeModuleBar.lean
• Proof of ModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar in P2M/Sol/S_ModularCurve_eisensteinQuotientInvariantsFiniteAt_heckeModuleBar.lean
• The repository's documentation page for ModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar

LeanModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar

Uses 1 · Used by 1

Proof usesModularForm.S2_Gamma0_one_eq_zero

Used byWeierstrassCurve.mazurStepThree_not_inZeroComponentAt

TheoremModularCurve.mazurQuotientSpecialization_heckeModuleBar#

open ModularCurve AlgebraicCurve
theorem ModularCurve.mazurQuotientSpecialization_heckeModuleBar (p : ℕ) [Fact p.Prime]
    (hcomm : HeckeOperatorsCommuteBar p) :
    MazurQuotientSpecialization p (heckeModuleBar p)

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

ModularCurve.mazurQuotientSpecialization_heckeModuleBar, stated in Theorems/Thm_ModularCurve_mazurQuotientSpecialization_heckeModuleBar.lean, line 35 and proved in P2M/Sol/S_ModularCurve_mazurQuotientSpecialization_heckeModuleBar.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of ModularCurve.mazurQuotientSpecialization_heckeModuleBar in Theorems/Thm_ModularCurve_mazurQuotientSpecialization_heckeModuleBar.lean
• Proof of ModularCurve.mazurQuotientSpecialization_heckeModuleBar in P2M/Sol/S_ModularCurve_mazurQuotientSpecialization_heckeModuleBar.lean
• The repository's documentation page for ModularCurve.mazurQuotientSpecialization_heckeModuleBar

LeanModularCurve.mazurQuotientSpecialization_heckeModuleBar

Used by 1

Used byWeierstrassCurve.mazurStepThree_not_inZeroComponentAt

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.