@[reducible, inline]

noncomputable abbrev Qbar : IntermediateField ℚ ℂ

The algebraic closure of ℚ inside ℂ, viewed as an intermediate field. This provides a concrete model of ℚ̄ sitting inside ℂ.

@[reducible, inline]

abbrev AbsGaloisGroupQ : Type

The absolute Galois group of ℚ, realized as the group of ℚ-algebra automorphisms of Qbar.

@[reducible, inline]

abbrev GaloisRepMod (ℓ : ℕ) : Type

A mod-ℓ Galois representation is a group homomorphism from the absolute Galois group of ℚ to GL₂(ℤ/ℓℤ).

noncomputable def complexConjugation : AbsGaloisGroupQ

A specific element of the absolute Galois group of ℚ realizing complex conjugation on Qbar ⊆ ℂ.

def GaloisRepMod.IsOdd {ℓ : ℕ} (ρ : GaloisRepMod ℓ) : Prop

A mod-ℓ Galois representation ρ is odd if det(ρ(c)) = -1, where c is complex conjugation.

def GaloisRepMod.IsIrreducible {ℓ : ℕ} (ρ : GaloisRepMod ℓ) : Prop

A mod-ℓ Galois representation is irreducible if no nonzero vector v ∈ (ℤ/ℓℤ)² is simultaneously an eigenvector of every ρ(g).

noncomputable def frobeniusElement (p : ℕ) (hp : Nat.Prime p) : AbsGaloisGroupQ

An element of the absolute Galois group realizing a Frobenius at the prime p.

def GaloisRepMod.IsModular {ℓ : ℕ} (ρ : GaloisRepMod ℓ) : Prop

A mod-ℓ Galois representation ρ is modular if there exists a cusp form f of some weight k and level Γ₁(N), with integer Fourier coefficients a(n), such that for every prime p not dividing ℓN the trace of ρ(Frob_p) equals a(p) mod ℓ.

@[reducible, inline]

abbrev FLT.EllipticCurveOverQ : Type

An elliptic curve over ℚ: a Weierstrass curve in affine form together with a proof that it satisfies the elliptic (nonsingular) condition.

noncomputable def FLT.minimalDiscriminant (E : EllipticCurveOverQ) : ℤ

The minimal discriminant of an elliptic curve over ℚ: the discriminant of a global minimal Weierstrass model.

theorem FLT.minimalDiscriminant_ne_zero (E : EllipticCurveOverQ) : minimalDiscriminant E ≠ 0

The minimal discriminant of an elliptic curve over ℚ is nonzero (consequence of nonsingularity of the global minimal model).

noncomputable def FLT.conductor (E : EllipticCurveOverQ) : ℕ

The conductor of an elliptic curve over ℚ, defined here as the radical of the absolute value of the minimal discriminant.

theorem FLT.conductor_pos (E : EllipticCurveOverQ) : 0 < conductor E

The conductor of any elliptic curve over ℚ is strictly positive.

def FLT.IsSemistable (E : EllipticCurveOverQ) : Prop

An elliptic curve over ℚ is semistable if it has no additive reduction at any prime — equivalently, all bad reduction is multiplicative.

theorem FLT.isSemistable_iff_squarefree_conductor (E : EllipticCurveOverQ) : IsSemistable E ↔ Squarefree (conductor E)

An elliptic curve over ℚ is semistable iff its conductor is squarefree.

noncomputable def FLT.AdmitsRationalCyclicIsogeny (E : EllipticCurveOverQ) (n : ℕ) : Prop

E admits a rational cyclic n-isogeny: there is a ℚ-rational isogeny from E whose kernel is cyclic of order n.

theorem FLT.conductor_not_squarefree_of_admits_15_isogeny (E : EllipticCurveOverQ) (h : AdmitsRationalCyclicIsogeny E 15) : ¬Squarefree (conductor E)

If E/ℚ admits a rational cyclic 15-isogeny then its conductor is not squarefree.

theorem FLT.not_semistable_of_admits_15_isogeny (E : EllipticCurveOverQ) (h : AdmitsRationalCyclicIsogeny E 15) : ¬IsSemistable E

An elliptic curve admitting a rational cyclic 15-isogeny cannot be semistable. This follows from squarefree-conductor characterization of semistability.

theorem FLT.no_semistable_rational_15_isogeny (E : EllipticCurveOverQ) (hss : IsSemistable E) (hiso : AdmitsRationalCyclicIsogeny E 15) : False

A semistable elliptic curve over ℚ admits no rational cyclic 15-isogeny.

noncomputable def FLT.galoisRepMod_of_EC (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : GaloisRepMod ℓ

The mod-ℓ Galois representation attached to an elliptic curve E/ℚ, obtained from the Galois action on the ℓ-torsion E[ℓ].

def FLT.ModLGaloisRepIsIrreducible (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Prop

The mod-ℓ representation attached to an elliptic curve E/ℚ is irreducible.

def FLT.ModLGaloisRepIsModular (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Prop

The mod-ℓ representation attached to an elliptic curve E/ℚ is modular.

noncomputable def FLT.LSeriesCoeff (E : EllipticCurveOverQ) : ℕ → ℤ

The Dirichlet coefficients a_n of the L-series of E/ℚ.

structure FLT.Weight2Newform (N : ℕ) : Type

A weight-2 newform of level N, specified by its Fourier coefficients: normalized so that a₁ = 1, multiplicative on coprime indices, and satisfying the standard Hecke recursion at primes p ∤ N.

• coeff : ℕ → ℤ
• coeff_one : self.coeff 1 = 1
• coeff_mult (m n : ℕ) : m.Coprime n → self.coeff (m * n) = self.coeff m * self.coeff n
• coeff_prime_power (p r : ℕ) : Nat.Prime p → ¬p ∣ N → r ≥ 1 → self.coeff (p ^ (r + 1)) = self.coeff p * self.coeff (p ^ r) - ↑p * self.coeff (p ^ (r - 1))

def FLT.ModLGaloisRepIsModularOfWeightAndLevel (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (weight : ℕ) (level : ℕ+) : Prop

The mod-ℓ representation of E/ℚ is modular of a prescribed weight and level: there is a weight-2 newform of the given level matching tr ρ(Frob_p) at primes p ∤ ℓ · level.

def FLT.LAdicGaloisRepIsModular (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Prop

The ℓ-adic Galois representation attached to E/ℚ is modular: there is a weight-2 newform of level equal to the conductor whose Fourier coefficients match a_p(E) at primes p ∤ ℓ · conductor.

def FLT.IsModularEllipticCurve (E : EllipticCurveOverQ) : Prop

E/ℚ is a modular elliptic curve: there is a weight-2 newform of level the conductor of E whose Fourier coefficients equal the L-series coefficients of E for every n ≥ 1.

theorem FLT.taylor_wiles_modularity_lifting (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hss : IsSemistable E) (hmod : ModLGaloisRepIsModular E ℓ) : LAdicGaloisRepIsModular E ℓ ∧ IsModularEllipticCurve E

Taylor–Wiles modularity lifting: if E/ℚ is semistable and its mod-ℓ representation is modular, then its ℓ-adic representation is modular and E itself is a modular elliptic curve.

noncomputable def FLT.ribetLevelDivisor (E : EllipticCurveOverQ) (ℓ : ℕ) : ℕ

Ribet's level-lowering divisor: the product over primes p ∥ N(E) of those p at which the mod-ℓ representation is unramified, i.e. ℓ ∣ v_p(Δ_E).

theorem FLT.ribetLevelDivisor_dvd (E : EllipticCurveOverQ) (ℓ : ℕ) : ribetLevelDivisor E ℓ ∣ conductor E

The Ribet level divisor divides the conductor of E.

theorem FLT.ribetLevelDivisor_pos (E : EllipticCurveOverQ) (ℓ : ℕ) : 0 < ribetLevelDivisor E ℓ

The Ribet level divisor is strictly positive.

noncomputable def FLT.ribetLoweredLevel (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : ℕ+

The level produced by Ribet's level-lowering theorem: the conductor of E divided by the Ribet level divisor, as a positive natural number.

theorem FLT.ribet_level_lowering (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hmod : IsModularEllipticCurve E) (hirr : ModLGaloisRepIsIrreducible E ℓ) : ModLGaloisRepIsModularOfWeightAndLevel E ℓ 2 (ribetLoweredLevel E ℓ)

Ribet's level-lowering theorem: if E/ℚ is modular and the mod-ℓ representation is irreducible, then the mod-ℓ representation is modular of weight 2 and level equal to the Ribet-lowered level.

theorem FLT.langlands_tunnel (E : EllipticCurveOverQ) (hirr : ModLGaloisRepIsIrreducible E 3) : ModLGaloisRepIsModular E 3

The Langlands–Tunnell theorem: if the mod-3 representation of E/ℚ is irreducible, then it is modular.

noncomputable def FLT.freyCurve (a b c : ℤ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : EllipticCurveOverQ

The Frey curve y² = x(x - aᵉ)(x + bᵉ) associated to a putative counterexample aᵉ + bᵉ = cᵉ to Fermat's Last Theorem at prime exponent ℓ.

theorem FLT.freyCurve_isSemistable (a b c : ℤ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hflt : a ^ ℓ + b ^ ℓ = c ^ ℓ) (hcoprime : a.gcd ↑(b.gcd c) = 1) : IsSemistable (freyCurve a b c ℓ)

The Frey curve attached to a coprime Fermat triple is semistable.

theorem FLT.mazur_isogeny_theorem (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hℓ : ℓ > 163) : ¬AdmitsRationalCyclicIsogeny E ℓ

Mazur's isogeny theorem: for primes ℓ > 163, no elliptic curve over ℚ admits a rational cyclic ℓ-isogeny.

theorem FLT.reducible_implies_rational_isogeny (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hred : ¬ModLGaloisRepIsIrreducible E ℓ) : AdmitsRationalCyclicIsogeny E ℓ

If the mod-ℓ Galois representation of E/ℚ is reducible, then E admits a rational cyclic ℓ-isogeny (coming from a Galois-stable line in E[ℓ]).

theorem FLT.freyCurve_modLRep_irreducible (a b c : ℤ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (_hflt : a ^ ℓ + b ^ ℓ = c ^ ℓ) (hℓ_large : ℓ > 163) : ModLGaloisRepIsIrreducible (freyCurve a b c ℓ) ℓ

The mod-ℓ representation of the Frey curve is irreducible (for ℓ > 163), combining Mazur's isogeny theorem with the reducibility–isogeny correspondence.

theorem FLT.freyCurve_ribetLoweredLevel_eq_two (a b c : ℤ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hflt : a ^ ℓ + b ^ ℓ = c ^ ℓ) (hℓ_large : ℓ > 163) : ribetLoweredLevel (freyCurve a b c ℓ) ℓ = ⟨2, ⋯⟩

For the Frey curve attached to a Fermat triple, Ribet's level-lowering produces level 2.

theorem FLT.no_weight2_level2_modular_form (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : ¬ModLGaloisRepIsModularOfWeightAndLevel E ℓ 2 ⟨2, ⋯⟩

There is no weight-2, level-2 cuspform: the space S_2(Γ₀(2)) is zero, so no elliptic curve has a mod-ℓ representation modular of weight 2 and level 2.

theorem FLT.freyCurve_not_modular (a b c : ℤ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hflt : a ^ ℓ + b ^ ℓ = c ^ ℓ) (hℓ_large : ℓ > 163) : ¬IsModularEllipticCurve (freyCurve a b c ℓ)

The Frey curve attached to a Fermat triple is not modular: combining Ribet's level-lowering with the nonexistence of weight-2, level-2 newforms.

instance FLT.instFactPrimeOfNatNat_atlas : Fact (Nat.Prime 3)

3 is a prime number. Provided as a Fact for use as a typeclass parameter.

instance FLT.instFactPrimeOfNatNat_atlas_1 : Fact (Nat.Prime 5)

5 is a prime number. Provided as a Fact for use as a typeclass parameter.

def FLT.ModLGaloisRepIsIsomorphic (E E' : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Prop

The mod-ℓ representations of two elliptic curves E, E' over ℚ are isomorphic (at the level of traces): for every g in the absolute Galois group, tr ρ_E(g) = tr ρ_{E'}(g).

theorem FLT.modLGaloisRep_modular_of_isomorphic (E E' : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hiso : ModLGaloisRepIsIsomorphic E E' ℓ) (hmod : ModLGaloisRepIsModular E ℓ) : ModLGaloisRepIsModular E' ℓ

If the mod-ℓ representations of E and E' are isomorphic and E's mod-ℓ representation is modular, then so is E''s.

theorem FLT.reducible_mod3_implies_irreducible_mod5 (E : EllipticCurveOverQ) (hss : IsSemistable E) (hred : ¬ModLGaloisRepIsIrreducible E 3) : ModLGaloisRepIsIrreducible E 5

For a semistable E/ℚ whose mod-3 representation is reducible, the mod-5 representation is irreducible. (Used in the 3-5 trick.)

theorem FLT.modular_implies_mod_rep_modular (E : EllipticCurveOverQ) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hmod : IsModularEllipticCurve E) : ModLGaloisRepIsModular E ℓ

If E/ℚ is a modular elliptic curve, then for any prime ℓ the mod-ℓ representation of E is also modular.

theorem FLT.wiles_three_five_trick (E : EllipticCurveOverQ) (hss : IsSemistable E) (hirr5 : ModLGaloisRepIsIrreducible E 5) : ∃ (E' : EllipticCurveOverQ), IsSemistable E' ∧ ModLGaloisRepIsIrreducible E' 3 ∧ ModLGaloisRepIsIsomorphic E' E 5

Wiles's 3-5 trick: given a semistable E/ℚ whose mod-5 representation is irreducible, there exists a semistable E'/ℚ whose mod-3 representation is irreducible and whose mod-5 representation is isomorphic to that of E.

theorem FLT.wiles_modularity_semistable (E : EllipticCurveOverQ) (hss : IsSemistable E) : IsModularEllipticCurve E

Wiles's modularity theorem for semistable elliptic curves: every semistable elliptic curve over ℚ is modular. Proof uses Langlands–Tunnell at the prime 3 together with Wiles's 3-5 trick when the mod-3 representation is reducible.

theorem FLT.taylor_wiles_modularity_theorem (E : EllipticCurveOverQ) (hss : IsSemistable E) : IsModularEllipticCurve E

Wiles's modularity theorem for semistable elliptic curves (Theorem 25.8), restated.

theorem FLT.freyCurve_coprimality_reduction (a b c : ℤ) (p : ℕ) [Fact (Nat.Prime p)] (heq : a ^ p + b ^ p = c ^ p) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : a.gcd ↑(b.gcd c) = 1

For a Fermat-like triple aᵖ + bᵖ = cᵖ with a, b, c all nonzero, the entries can be assumed pairwise coprime: gcd(a, gcd(b, c)) = 1.

theorem FLT.flt_for_prime_gt_163 (p : ℕ) [Fact (Nat.Prime p)] (hp_large : p > 163) : FermatLastTheoremWith ℤ p

Fermat's Last Theorem for prime exponent p > 163, deduced via the Frey curve: its semistability and Wiles's modularity contradict its non-modularity.

theorem FLT.flt_for_small_odd_primes (p : ℕ) (hp : Nat.Prime p) (hp_odd : Odd p) (hp_ge5 : p ≥ 5) (hp_le163 : p ≤ 163) : FermatLastTheoremFor p

Fermat's Last Theorem for odd primes p in the range 5 ≤ p ≤ 163, handled by the classical (pre-Wiles) techniques.

theorem FLT.flt_for_odd_prime (p : ℕ) (hp : Nat.Prime p) (hp_odd : Odd p) : FermatLastTheoremFor p

Fermat's Last Theorem for any odd prime exponent p, combining the case p = 3 (fermatLastTheoremThree), the small-prime range, and the large-prime case from Wiles/Ribet.

theorem FLT.fermats_last_theorem_cor_25_9 (n : ℕ) : n > 2 → ∀ (x y z : ℤ), x ^ n + y ^ n = z ^ n → x * y * z = 0

Corollary 25.9 (Fermat's Last Theorem): for every n > 2, the equation xⁿ + yⁿ = zⁿ has no integer solutions with xyz ≠ 0.

@[reducible, inline]

abbrev EllipticCurve.OverQ : Type

Convenience abbreviation for FLT.EllipticCurveOverQ, the type of elliptic curves over ℚ.

noncomputable def EllipticCurve.conductor (E : FLT.EllipticCurveOverQ) : ℕ

The conductor of an elliptic curve over ℚ, re-exported from the FLT namespace.

noncomputable def EllipticCurve.minimalDiscriminant (E : FLT.EllipticCurveOverQ) : ℤ

The minimal discriminant of an elliptic curve over ℚ, re-exported from FLT.

theorem EllipticCurve.conductor_pos (E : FLT.EllipticCurveOverQ) : 0 < conductor E

The conductor of any elliptic curve over ℚ is strictly positive (re-export).

def EllipticCurve.IsSemistable (E : FLT.EllipticCurveOverQ) : Prop

An elliptic curve over ℚ is semistable, re-exported from FLT.

theorem EllipticCurve.isSemistable_iff_squarefree_conductor (E : FLT.EllipticCurveOverQ) : IsSemistable E ↔ Squarefree (conductor E)

Re-export: semistability is equivalent to the conductor being squarefree.

theorem serre_modularity_conjecture (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (ρ : GaloisRepMod ℓ) (hodd : ρ.IsOdd) (hirr : ρ.IsIrreducible) : ρ.IsModular

Serre's modularity conjecture (now a theorem of Khare–Wintenberger): every odd, irreducible mod-ℓ Galois representation of Gal(ℚ̄/ℚ) arises from a modular form.