From 8eece85682a82df48adefd90e90ea776b29977db Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 19 Jun 2024 11:32:22 +0200 Subject: [PATCH 01/11] Update Reductions.lean --- FLT/Basic/Reductions.lean | 38 +++++++++----------------------------- 1 file changed, 9 insertions(+), 29 deletions(-) diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean index f16477f6..769cda7f 100644 --- a/FLT/Basic/Reductions.lean +++ b/FLT/Basic/Reductions.lean @@ -108,11 +108,9 @@ lemma gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c have foo : gcd a b ∣ gcd a c := by apply dvd_gcd (gcd_dvd_left a b) rw [← Int.pow_dvd_pow_iff hp.ne', ← h] - apply dvd_add - · rw [Int.pow_dvd_pow_iff hp.ne'] - exact gcd_dvd_left a b - · rw [Int.pow_dvd_pow_iff hp.ne'] - exact gcd_dvd_right a b + apply dvd_add <;> rw [Int.pow_dvd_pow_iff hp.ne'] + · exact gcd_dvd_left a b + · exact gcd_dvd_right a b have bar : gcd a c ∣ gcd a b := by apply dvd_gcd (gcd_dvd_left a c) have h2 : b ^ p = c ^ p - a ^ p := eq_sub_of_add_eq' h @@ -120,8 +118,7 @@ lemma gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c apply dvd_add · rw [Int.pow_dvd_pow_iff hp.ne'] exact gcd_dvd_right a c - · rw [dvd_neg] - rw [Int.pow_dvd_pow_iff hp.ne'] + · rw [dvd_neg, Int.pow_dvd_pow_iff hp.ne'] exact gcd_dvd_left a c change _ ∣ (Int.gcd a c : ℤ) at foo apply Int.ofNat_dvd.1 at bar @@ -227,8 +224,7 @@ def FreyCurve (P : FreyPackage) : EllipticCurve ℚ := { simp_rw [← mul_pow] refine pow_ne_zero 2 <| pow_ne_zero P.p <| (mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0) coe_Δ' := by - simp only [Units.val_mk0] - rw [← Int.cast_pow P.c, ← P.hFLT] + simp only [Units.val_mk0, ← Int.cast_pow P.c, ← P.hFLT] field_simp [EllipticCurve.Δ', WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.b₆, WeierstrassCurve.b₈] ring } @@ -236,36 +232,27 @@ def FreyCurve (P : FreyPackage) : EllipticCurve ℚ := { lemma FreyCurve.b₂ (P : FreyPackage) : P.FreyCurve.b₂ = P.b ^ P.p - P.a ^ P.p := by simp [FreyCurve, WeierstrassCurve.b₂] - field_simp - norm_cast ring lemma FreyCurve.b₄ (P : FreyPackage) : P.FreyCurve.b₄ = - (P.a * P.b) ^ P.p / 8 := by simp [FreyCurve, WeierstrassCurve.b₄] - field_simp - norm_cast ring lemma FreyCurve.c₄ (P : FreyPackage) : P.FreyCurve.c₄ = (P.a ^ P.p) ^ 2 + P.a ^ P.p * P.b ^ P.p + (P.b ^ P.p) ^ 2 := by simp [FreyCurve.b₂, FreyCurve.b₄, WeierstrassCurve.c₄] - field_simp - norm_cast ring lemma FreyCurve.c₄' (P : FreyPackage) : P.FreyCurve.c₄ = P.c ^ (2 * P.p) - (P.a * P.b) ^ P.p := by rw [FreyCurve.c₄] - norm_cast - rw [pow_mul', ← hFLT] + rw_mod_cast [pow_mul', ← hFLT] ring lemma FreyCurve.Δ'inv (P : FreyPackage) : (↑(P.FreyCurve.Δ'⁻¹) : ℚ) = 2 ^ 8 / (P.a*P.b*P.c)^(2*P.p) := by simp [FreyCurve] - congr 1 - norm_cast ring lemma FreyCurve.j (P : FreyPackage) : @@ -283,7 +270,7 @@ private lemma j_pos_aux (a b : ℤ) (hb : b ≠ 0) : 0 < (a + b) ^ 2 - a * b := apply mul_self_pos.mpr hb | inr h => rw [sub_pos] - apply h.trans_le (sq_nonneg _) + exact h.trans_le (sq_nonneg _) /-- The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction. -/ @@ -293,8 +280,7 @@ lemma FreyCurve.j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hqPrime : have := Fact.mk hqPrime have hqPrime' := Nat.prime_iff_prime_int.mp hqPrime have h₀ : ((P.c ^ (2 * P.p) - (P.a * P.b) ^ P.p) ^ 3 : ℚ) ≠ 0 := by - norm_cast - rw [pow_mul', ← P.hFLT, mul_pow] + rw_mod_cast [pow_mul', ← P.hFLT, mul_pow] exact pow_ne_zero _ <| ne_of_gt <| j_pos_aux _ _ (pow_ne_zero _ P.hb0) have h₁ : P.a * P.b * P.c ≠ 0 := mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0 rw [FreyCurve.j, padicValRat.div (mul_ne_zero (by norm_num) h₀) (pow_ne_zero _ (mod_cast h₁)), @@ -327,10 +313,6 @@ lemma FreyCurve.j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hqPrime : end FreyPackage - - - - /-! Given an elliptic curve over `ℚ`, the p-torsion points defined over an algebraic @@ -367,9 +349,7 @@ It follows that there is no Frey package. /-- There is no Frey package. This profound result is proved using work of Mazur and Wiles/Ribet to rule out all possibilities for the $p$-torsion in the corresponding Frey curve. -/ -theorem FreyPackage.false (P : FreyPackage) : False := by - apply Wiles_Frey P - exact Mazur_Frey P +theorem FreyPackage.false (P : FreyPackage) : False := Wiles_Frey P (Mazur_Frey P) -- Fermat's Last Theorem is true theorem Wiles_Taylor_Wiles : FermatLastTheorem := by From 159c69696e9344714e09f1b439d97688508612ab Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 19 Jun 2024 11:32:28 +0200 Subject: [PATCH 02/11] Update Frobenius.lean --- FLT/for_mathlib/Frobenius.lean | 97 +++++++++++++--------------------- 1 file changed, 38 insertions(+), 59 deletions(-) diff --git a/FLT/for_mathlib/Frobenius.lean b/FLT/for_mathlib/Frobenius.lean index 2ec68326..7570659e 100644 --- a/FLT/for_mathlib/Frobenius.lean +++ b/FLT/for_mathlib/Frobenius.lean @@ -378,7 +378,7 @@ noncomputable instance : Field (A ⧸ P) := Ideal.Quotient.field P lemma is_primepow_char_A_quot_P : IsPrimePow q := Fintype.isPrimePow_card_of_field lemma ex_primepow_char_A_quot_P : ∃ p n : ℕ , Prime p ∧ 0 < n ∧ p ^ n = q := by - apply is_primepow_char_A_quot_P + exact is_primepow_char_A_quot_P _ local notation "p" => Classical.choose (CharP.exists (A ⧸ P)) local notation "p'" => Classical.choose (ex_primepow_char_A_quot_P P) @@ -401,7 +401,7 @@ lemma p_is_p' : p = p' := by have h1 : p ∣ q := charP_iff (A ⧸ P) p |>.1 (p_is_char P) q |>.1 eq0 have eq1 : p' ^ n = q := q_is_p'_pow_n P rw [← eq1] at h1 - refine Nat.dvd_prime (p'_is_prime P) |>.1 + exact Nat.dvd_prime (p'_is_prime P) |>.1 (Nat.Prime.dvd_of_dvd_pow (p_is_prime P) h1) |>.resolve_left <| Nat.Prime.ne_one <| p_is_prime P lemma q_is_p_pow_n : p ^ n = q := by @@ -415,7 +415,7 @@ theorem pow_eq_expand (a : (A ⧸ P)[X]) : have pprime : Nat.Prime p := p_is_prime P have factprime : Fact (Nat.Prime p) := { out := pprime } rw [← q_is_p_pow_n, ← map_expand_pow_char, map_expand, FiniteField.frobenius_pow] - · simp only [exists_and_left, RingHom.one_def, map_id] + · simp [exists_and_left, RingHom.one_def, map_id] · exact (q_is_p_pow_n P).symm end FreshmansDream @@ -482,11 +482,7 @@ theorem gal_smul_F_eq (σ : L ≃ₐ[K] L) : ∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B σ (galRestrict A K L B τ α))):= by - rw [Finset.smul_prod] - simp_rw [smul_sub] - ext - congr - simp only [smul_X, smul_C, AlgEquiv.smul_def] + simp [Finset.smul_prod, smul_sub, smul_X, smul_C, AlgEquiv.smul_def] /-- use `Finset.prod_bij` to show `(galRestrict A K L B σ • (∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B τ α))) = @@ -497,11 +493,11 @@ lemma F_invariant_under_finite_aut (σ : L ≃ₐ[K] L) : set i : (τ : L ≃ₐ[K] L) → τ ∈ Finset.univ → L ≃ₐ[K] L := fun τ _ => σ * τ -- needed to use `set i` instead of `have i`, in order to be able to use `i` later on, in proof have hi : ∀ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), i τ hτ ∈ Finset.univ := by - simp only [Finset.mem_univ, forall_true_left, forall_const] + simp [Finset.mem_univ, forall_true_left, forall_const] have i_inj : ∀ (τ₁ : L ≃ₐ[K] L) (hτ₁ : τ₁ ∈ Finset.univ) (τ₂ : L ≃ₐ[K] L) (hτ₂ : τ₂ ∈ Finset.univ), i τ₁ hτ₁ = i τ₂ hτ₂ → τ₁ = τ₂ := by intros τ₁ _ τ₂ _ h - simpa only [i, mul_right_inj] using h + simpa [i, mul_right_inj] using h have i_surj : ∀ σ ∈ Finset.univ, ∃ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), i τ hτ = σ := by intro τ' simp only [Finset.mem_univ, exists_true_left, forall_true_left, i] @@ -514,7 +510,7 @@ lemma F_invariant_under_finite_aut (σ : L ≃ₐ[K] L) : simp only [i, map_mul, sub_right_inj, C_inj] rw [AlgEquiv.aut_mul] rfl - apply Finset.prod_bij i hi i_inj i_surj h + exact Finset.prod_bij i hi i_inj i_surj h /-- ` L ≃ₐ[K] L` fixes `F`. -/ theorem gal_smul_F_eq_self (σ : L ≃ₐ[K] L) : @@ -526,9 +522,8 @@ theorem gal_smul_F_eq_self (σ : L ≃ₐ[K] L) : theorem gal_smul_coeff_eq (n : ℕ) (h : ∀ σ : L ≃ₐ[K] L, galRestrict A K L B σ • F = F) (σ : L ≃ₐ[K] L) : galRestrict A K L B σ • (coeff F n) = coeff F n := by - simp only [AlgEquiv.smul_def] nth_rewrite 2 [← h σ] - simp only [coeff_smul, AlgEquiv.smul_def] + simp [coeff_smul, AlgEquiv.smul_def] variable {A K L B Q} @@ -574,7 +569,7 @@ theorem coeff_lives_in_A (n : ℕ) : ∃ a : A, algebraMap B L (coeff F n) = (al exact NoZeroSMulDivisors.algebraMap_injective K L cases' h1.1 h2 with a' ha' use a' - simpa only [eq0, RingHom.coe_comp, Function.comp_apply, ha'] + simpa [eq0, RingHom.coe_comp, Function.comp_apply, ha'] /-- `α` is a root of `F`. -/ lemma isRoot_α : eval α F = 0 := by @@ -597,14 +592,12 @@ lemma isRoot_α : eval α F = 0 := by apply eq0 at evalid rwa [← eqF] -lemma quotient_isRoot_α : (eval α F) ∈ Q := by - rw [isRoot_α Q_ne_bot] - apply Ideal.zero_mem +lemma quotient_isRoot_α : (eval α F) ∈ Q := (isRoot_α Q_ne_bot) ▸ Ideal.zero_mem _ lemma conjugate_isRoot_α (σ : L ≃ₐ[K] L) : (eval (galRestrict A K L B σ α) F) = 0 := by have evalσ : eval (galRestrict A K L B σ α) (X - C (galRestrict A K L B σ α)) = 0 := by - simp only [eval_sub, eval_X, eval_C, sub_self] + simp [eval_sub, eval_X, eval_C, sub_self] have eqF : (eval (galRestrict A K L B σ α) (∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B τ α)))) = eval (galRestrict A K L B σ α) F := rfl @@ -624,9 +617,7 @@ lemma conjugate_isRoot_α (σ : L ≃ₐ[K] L) : (eval (galRestrict A K L B σ rw [← eqF, evalσ] lemma conjugate_quotient_isRoot_α (σ : L ≃ₐ[K] L) : - (eval (galRestrict A K L B σ α) F) ∈ Q := by - rw [conjugate_isRoot_α Q_ne_bot] - apply Ideal.zero_mem + (eval (galRestrict A K L B σ α) F) ∈ Q := (conjugate_isRoot_α Q_ne_bot) _ ▸ Ideal.zero_mem _ lemma F_is_root_iff_is_conjugate {x : B} : IsRoot F x ↔ (∃ σ : L ≃ₐ[K] L, x = (galRestrict A K L B σ α)) := by @@ -650,7 +641,7 @@ lemma F_is_root_iff_is_conjugate {x : B} : · intros h rcases h with ⟨σ, hσ⟩ rw [Polynomial.IsRoot.def, hσ] - apply conjugate_isRoot_α Q_ne_bot + exact conjugate_isRoot_α Q_ne_bot _ lemma F_eval_zero_is_conjugate {x : B} (h : eval x F = 0) : ∃ σ : L ≃ₐ[K] L, x = ((galRestrict A K L B σ) α) := by @@ -672,17 +663,15 @@ lemma ex_poly_in_A : ∃ m : A[X], Polynomial.map (algebraMap A B) m = F := by apply Iff.not rw [← _root_.map_eq_zero_iff (algebraMap B L), this, map_eq_zero_iff] have I : NoZeroSMulDivisors A L := NoZeroSMulDivisors.trans A K L - · apply NoZeroSMulDivisors.algebraMap_injective - · apply NoZeroSMulDivisors.algebraMap_injective + · exact NoZeroSMulDivisors.algebraMap_injective _ _ + · exact NoZeroSMulDivisors.algebraMap_injective _ _ }} use m ext n - have := Classical.choose_spec (h n) simp only [coeff_map, coeff_ofFinsupp, Finsupp.coe_mk] set s := Classical.choose (h n) apply NoZeroSMulDivisors.algebraMap_injective B L - rw [this] - exact (IsScalarTower.algebraMap_apply A B L _).symm + exact (Classical.choose_spec (h n)) ▸ (IsScalarTower.algebraMap_apply A B L _).symm /--`m' : A[X]` such that `Polynomial.map (algebraMap A B) m = F`. -/ noncomputable def m' : A[X] := Classical.choose (ex_poly_in_A Q_ne_bot) @@ -697,11 +686,11 @@ lemma m_eq_F_in_B_quot_Q : Polynomial.map (algebraMap B (B ⧸ Q)) F := by suffices h : Polynomial.map (algebraMap A B) m = F by exact congrArg (map (algebraMap B (B ⧸ Q))) h - apply m_mapsto_F + exact m_mapsto_F _ lemma m_expand_char_q : (Polynomial.map (algebraMap A (A ⧸ P)) m) ^ q = (expand _ q (Polynomial.map (algebraMap A (A ⧸ P)) m)) := by - apply pow_eq_expand + exact pow_eq_expand _ _ lemma B_m_expand_char_q : (Polynomial.map (algebraMap A (B ⧸ Q)) m) ^ q = (expand _ q (Polynomial.map (algebraMap A (B ⧸ Q)) m)) := by @@ -735,23 +724,22 @@ lemma pow_expand_A_B_scalar_tower_F : lemma F_expand_eval_eq_eval_pow : (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q α) F) ^ q = (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) := by - simp only [← Polynomial.eval_map, ← Ideal.Quotient.algebraMap_eq, ← Polynomial.coe_evalRingHom, - ← map_pow, pow_expand_A_B_scalar_tower_F] - simp only [Ideal.Quotient.algebraMap_eq, coe_evalRingHom, expand_eval, map_pow] + simp_rw [← Polynomial.eval_map, ← Ideal.Quotient.algebraMap_eq, ← Polynomial.coe_evalRingHom, + ← map_pow, pow_expand_A_B_scalar_tower_F, Ideal.Quotient.algebraMap_eq, coe_evalRingHom, + expand_eval, map_pow] lemma quotient_F_is_product_of_quot : (Polynomial.map (Ideal.Quotient.mk Q) F) = ∏ τ : L ≃ₐ[K] L, (X - C ((Ideal.Quotient.mk Q) ((galRestrict A K L B τ) α))) := by - rw [← Polynomial.coe_mapRingHom] - erw [map_prod] - simp only [map_sub, coe_mapRingHom, map_X, map_C] + erw [← Polynomial.coe_mapRingHom, map_prod] + simp [map_sub, coe_mapRingHom, map_X, map_C] lemma quotient_F_is_root_iff_is_conjugate (x : (B ⧸ Q)) : IsRoot (Polynomial.map (Ideal.Quotient.mk Q) F) x ↔ (∃ σ : L ≃ₐ[K] L, x = ((Ideal.Quotient.mk Q) ((galRestrict A K L B σ) α))) := by rw [quotient_F_is_product_of_quot, Polynomial.isRoot_prod] simp only [Finset.mem_univ, eval_sub, eval_X, eval_C, true_and, Polynomial.root_X_sub_C] - simp only [eq_comm (a := x)] + simp [eq_comm] lemma pow_eval_root_in_Q : ((eval α F) ^ q) ∈ Q := by have h : (eval α F) ∈ Q := quotient_isRoot_α Q_ne_bot @@ -761,16 +749,15 @@ lemma pow_eval_root_in_Q : ((eval α F) ^ q) ∈ Q := by lemma expand_eval_root_eq_zero : (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) = 0 := by - rw [← F_expand_eval_eq_eval_pow P Q_ne_bot] - simp only [eval₂_at_apply, ne_eq, Fintype.card_ne_zero, not_false_eq_true, pow_eq_zero_iff] + simp only [← F_expand_eval_eq_eval_pow P Q_ne_bot, eval₂_at_apply, ne_eq, Fintype.card_ne_zero, + not_false_eq_true, pow_eq_zero_iff] have h : eval α F ∈ Q := quotient_isRoot_α Q_ne_bot rwa [← Ideal.Quotient.eq_zero_iff_mem] at h -- now, want `∃ σ, α ^ q ≡ σ α mod Q` lemma pow_q_is_conjugate : ∃ σ : L ≃ₐ[K] L, (Ideal.Quotient.mk Q (α ^ q)) = (Ideal.Quotient.mk Q ((((galRestrict A K L B) σ)) α)) := by - rw [← quotient_F_is_root_iff_is_conjugate] - simp only [map_pow, IsRoot.def, Polynomial.eval_map] + rw [← quotient_F_is_root_iff_is_conjugate, map_pow, IsRoot.def, Polynomial.eval_map] exact expand_eval_root_eq_zero P Q_ne_bot -- following lemma suggested by Amelia @@ -779,7 +766,7 @@ lemma pow_quotient_IsRoot_α : (eval (α ^ q) F) ∈ Q := by have h2 : (eval₂ (Ideal.Quotient.mk Q) (Ideal.Quotient.mk Q (α ^ q)) F) = 0 := expand_eval_root_eq_zero P Q_ne_bot convert h2 - simp only [eval₂_at_apply] + rw [eval₂_at_apply] /--`α ^ q ≡ σ • α mod Q` for some `σ : L ≃ₐ[K] L` -/ lemma pow_q_conjugate : @@ -802,9 +789,8 @@ lemma inv_aut_not_mem_decomp (h : Frob ∉ decomposition_subgroup_Ideal' Q) : (F lemma gen_zero_mod_inv_aut (h1 : Frob ∉ decomposition_subgroup_Ideal' Q) : α ∈ (Frob⁻¹ • Q) := by have inv : Frob⁻¹ ∉ decomposition_subgroup_Ideal' Q := by - simpa only [inv_mem_iff] - apply generator_well_defined - exact inv + simpa [inv_mem_iff] + exact generator_well_defined _ _ inv lemma prop_Frob : (α ^ q - (galRestrict A K L B Frob) α) ∈ Q := Classical.choose_spec (pow_q_conjugate P Q_ne_bot) @@ -824,11 +810,9 @@ lemma is_zero_pow_gen_mod_Q (h : α ∈ (Frob⁻¹ • Q)) : rw [← Ideal.neg_mem_iff] at h1 have h3 : ((α ^ q - (galRestrict A K L B Frob) α) - (-(galRestrict A K L B Frob) α)) ∈ Q := by - apply Ideal.sub_mem - · exact h2 - · exact h1 + exact Ideal.sub_mem Q h2 h1 convert h3 - simp only [sub_neg_eq_add, sub_add_cancel] + simp [sub_neg_eq_add, sub_add_cancel] /-- `Frob ∈ decomposition_subgroup_Ideal' A K L B Q`. -/ theorem Frob_is_in_decompositionSubgroup : @@ -846,13 +830,12 @@ lemma γ_not_in_Q_is_pow_gen {γ : B} (h : γ ∉ Q) : ∃ (i : ℕ), γ - (α let g := Units.mk0 (((Ideal.Quotient.mk Q γ))) <| by intro h1 rw [Ideal.Quotient.eq_zero_iff_mem] at h1 - apply h - exact h1 + exact h h1 rcases generator_mem_submonoid_powers Q_ne_bot g with ⟨i, hi⟩ use i rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] - simp only [g, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec, Units.val_mk0] at hi - simp only [g, map_pow, hi] + simp [g, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec, Units.val_mk0] at hi + simp [g, map_pow, hi] /--`i' : ℕ` such that, for `(γ : B) (h : γ ∉ Q)`, `γ - (α ^ i) ∈ Q`. -/ noncomputable def i' {γ : B} (h : γ ∉ Q) : ℕ := @@ -868,12 +851,11 @@ lemma eq_pow_gen_apply {γ : B} (h: γ ∉ Q) : (galRestrict A K L B Frob) γ - galRestrict A K L B Frob (α ^ (i h)) ∈ Q := by rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] have h1 : γ - (α ^ (i h)) ∈ Q := prop_γ_not_in_Q_is_pow_gen Q_ne_bot h - rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at h1 + rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.Quotient.eq] at h1 rw [Ideal.Quotient.eq, ← map_sub] - rw [Ideal.Quotient.eq] at h1 have := Frob_is_in_decompositionSubgroup P Q_ne_bot rw [mem_decomposition_iff] at this - apply (this _).1 h1 + exact (this _).1 h1 -- γ ∈ B \ Q is α^i mod Q /-- `Frob • (α ^ i) ≡ α ^ (i * q) mod Q` -/ @@ -910,10 +892,7 @@ theorem Frob_γ_not_in_Q_is_pow {γ : B} (h : γ ∉ Q) : · exact h3 simp only [map_pow, sub_sub_sub_cancel_right] at h5 have h6 : (( (((galRestrict A K L B) Frob)) γ - α ^ (i h * q)) + - (((α ^ ((i h) * q)) - (γ ^ q)))) ∈ Q := by - apply Ideal.add_mem - · exact h5 - · exact h4 + (((α ^ ((i h) * q)) - (γ ^ q)))) ∈ Q := Ideal.add_mem _ h5 h4 simp only [sub_add_sub_cancel] at h6 rw [← Ideal.neg_mem_iff] at h6 simp only [neg_sub] at h6 From 2413d7ee2fd8db174d5f4a0a87af8a4c59c25b2c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 19 Jun 2024 11:32:30 +0200 Subject: [PATCH 03/11] Update Frobenius2.lean --- FLT/for_mathlib/Frobenius2.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/FLT/for_mathlib/Frobenius2.lean b/FLT/for_mathlib/Frobenius2.lean index e7dd534f..57f1245d 100644 --- a/FLT/for_mathlib/Frobenius2.lean +++ b/FLT/for_mathlib/Frobenius2.lean @@ -243,9 +243,7 @@ lemma F.mod_Q_y_pow_q_eq_zero : (F A Q).eval₂ (algebraMap B (B⧸Q)) ((algebra lemma exists_thing : ∃ σ : B ≃ₐ[A] B, σ (y A Q) - (y A Q) ^ (Fintype.card (A⧸P)) ∈ Q := by have := F.mod_Q_y_pow_q_eq_zero A Q isGalois P - rw [F_spec] at this - rw [eval₂_finset_prod] at this - rw [Finset.prod_eq_zero_iff] at this + rw [F_spec, eval₂_finset_prod, Finset.prod_eq_zero_iff] at this obtain ⟨σ, -, hσ⟩ := this use σ simp only [Ideal.Quotient.algebraMap_eq, AlgEquiv.smul_def, eval₂_sub, eval₂_X, eval₂_C, From 00a70eaf15b59e6acab87c4a7bc3e9bdada48130 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 19 Jun 2024 11:32:32 +0200 Subject: [PATCH 04/11] Update IsCentralSimple.lean --- FLT/for_mathlib/IsCentralSimple.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/FLT/for_mathlib/IsCentralSimple.lean b/FLT/for_mathlib/IsCentralSimple.lean index 051f4f2e..80b9e78a 100644 --- a/FLT/for_mathlib/IsCentralSimple.lean +++ b/FLT/for_mathlib/IsCentralSimple.lean @@ -45,8 +45,7 @@ theorem RingCon.sum {R : Type u} [AddCommMonoid R] [Mul R] {ι : Type v} {s : Fi apply RingCon.add · exact h j (Finset.mem_insert_self j s') · apply ih - intro i hi - exact h i (Finset.mem_insert_of_mem hi) + exact fun i hi ↦ h i (Finset.mem_insert_of_mem hi) open Matrix in theorem MatrixRing.isCentralSimple (ι : Type v) (hι : Fintype ι) [Nonempty ι] [DecidableEq ι] : From ca08f2edfeccc9fc60812f836555b13050a7c171 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 23 Jun 2024 23:52:04 +0200 Subject: [PATCH 05/11] Comment out unfinished proof in Frobenius2.lean --- FLT/for_mathlib/Frobenius2.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/FLT/for_mathlib/Frobenius2.lean b/FLT/for_mathlib/Frobenius2.lean index 9ef6627b..f30eda62 100644 --- a/FLT/for_mathlib/Frobenius2.lean +++ b/FLT/for_mathlib/Frobenius2.lean @@ -342,11 +342,11 @@ lemma Frob_Q_eq_pow_card (x : B) : Frob A Q isGalois P x - x^(Fintype.card (A⧸ change (Frob A Q isGalois P) • x - _ ∈ _ rw [← smul_sub] nth_rw 3 [ ← fact3] - suffices (x - y A Q ^ n) ∈ Q by - exact? - rw [smul_mem_smul] - simp - skip + -- suffices (x - y A Q ^ n) ∈ Q by + -- exact? + -- rw [smul_mem_smul] + -- simp + -- skip sorry /- maths proof: From 05245b78b154bdc5eb82d6f206ff394d9aa98622 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 23 Jun 2024 23:53:01 +0200 Subject: [PATCH 06/11] Update IsCentralSimple.lean --- FLT/for_mathlib/IsCentralSimple.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/FLT/for_mathlib/IsCentralSimple.lean b/FLT/for_mathlib/IsCentralSimple.lean index 80b9e78a..d96137e2 100644 --- a/FLT/for_mathlib/IsCentralSimple.lean +++ b/FLT/for_mathlib/IsCentralSimple.lean @@ -44,8 +44,7 @@ theorem RingCon.sum {R : Type u} [AddCommMonoid R] [Mul R] {ι : Type v} {s : Fi simp_rw [Finset.sum_insert hj] apply RingCon.add · exact h j (Finset.mem_insert_self j s') - · apply ih - exact fun i hi ↦ h i (Finset.mem_insert_of_mem hi) + · exact ih fun i hi ↦ h i (Finset.mem_insert_of_mem hi) open Matrix in theorem MatrixRing.isCentralSimple (ι : Type v) (hι : Fintype ι) [Nonempty ι] [DecidableEq ι] : From 4b0eb7c163320bc9c97e8bbc1415e8edf9e64e7e Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Tue, 16 Jul 2024 15:07:16 +0200 Subject: [PATCH 07/11] Update Frobenius.lean --- FLT/for_mathlib/Frobenius.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/FLT/for_mathlib/Frobenius.lean b/FLT/for_mathlib/Frobenius.lean index ec5a4a2c..b86c37c1 100644 --- a/FLT/for_mathlib/Frobenius.lean +++ b/FLT/for_mathlib/Frobenius.lean @@ -731,7 +731,8 @@ lemma F_expand_eval_eq_eval_pow : lemma quotient_F_is_product_of_quot : (Polynomial.map (Ideal.Quotient.mk Q) F) = ∏ τ : L ≃ₐ[K] L, (X - C ((Ideal.Quotient.mk Q) ((galRestrict A K L B τ) α))) := by - erw [← Polynomial.coe_mapRingHom, map_prod] + rw [← Polynomial.coe_mapRingHom] + erw [map_prod] simp [map_sub, coe_mapRingHom, map_X, map_C] lemma quotient_F_is_root_iff_is_conjugate (x : (B ⧸ Q)) : From 4180b4ca41605a53f124dfdbca711403cd968b4f Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Tue, 16 Jul 2024 15:16:34 +0200 Subject: [PATCH 08/11] Golf --- FLT/AutomorphicForm/QuaternionAlgebra.lean | 2 +- FLT/AutomorphicRepresentation/Example.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean index d82ee69c..271561a6 100644 --- a/FLT/AutomorphicForm/QuaternionAlgebra.lean +++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean @@ -60,7 +60,7 @@ instance : TopologicalRing (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := moobar (Fi namespace TotallyDefiniteQuaternionAlgebra -noncomputable example : D →+* (D ⊗[F] FiniteAdeleRing (𝓞 F) F) := by exact +noncomputable example : D →+* (D ⊗[F] FiniteAdeleRing (𝓞 F) F) := Algebra.TensorProduct.includeLeftRingHom abbrev Dfx := (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ diff --git a/FLT/AutomorphicRepresentation/Example.lean b/FLT/AutomorphicRepresentation/Example.lean index 1f244b70..57fddd7c 100644 --- a/FLT/AutomorphicRepresentation/Example.lean +++ b/FLT/AutomorphicRepresentation/Example.lean @@ -55,7 +55,7 @@ lemma ext (x y : ZHat) (h : ∀ n : ℕ+, x n = y n) : x = y := by apply h lemma ext_iff (x y : ZHat) : (∀ n : ℕ+, x n = y n) ↔ x = y := - ⟨ext x y, fun h n => by exact congrFun (congrArg DFunLike.coe h) n⟩ + ⟨ext x y, fun h n => congrFun (congrArg DFunLike.coe h) n⟩ @[simp] lemma zero_val (n : ℕ+) : (0 : ZHat) n = 0 := rfl @[simp] lemma one_val (n : ℕ+) : (1 : ZHat) n = 1 := rfl From f5b247c18c20734f5923a1604d54975043d38c7f Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Tue, 16 Jul 2024 15:22:24 +0200 Subject: [PATCH 09/11] Update Frobenius2.lean --- FLT/for_mathlib/Frobenius2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FLT/for_mathlib/Frobenius2.lean b/FLT/for_mathlib/Frobenius2.lean index 7537ac97..33cc20f9 100644 --- a/FLT/for_mathlib/Frobenius2.lean +++ b/FLT/for_mathlib/Frobenius2.lean @@ -282,7 +282,7 @@ lemma Frob_Q : Frob A Q isGalois P • Q = Q := by rwa [Ideal.map_eq_comap_symm] at hy have this := Q.sub_mem hy2 <| Frob_spec A Q isGalois P simp only [sub_sub_cancel] at this - apply y_not_in_Q A Q <| Ideal.IsPrime.mem_of_pow_mem (show Q.IsPrime by infer_instance) _ this + exact y_not_in_Q A Q <| Ideal.IsPrime.mem_of_pow_mem (show Q.IsPrime by infer_instance) _ this lemma _root_.Ideal.Quotient.coe_eq_coe_iff_sub_mem {R : Type*} [CommRing R] {I : Ideal R} (x y : R) : (x : R ⧸ I) = y ↔ x - y ∈ I := Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _ From e4f48b18b88439beb85e980468aa283a1be4ccc3 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 4 Aug 2024 23:01:17 +0200 Subject: [PATCH 10/11] Update FLT/Basic/Reductions.lean Co-authored-by: Kevin Buzzard --- FLT/Basic/Reductions.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean index 069242d6..a37d3d68 100644 --- a/FLT/Basic/Reductions.lean +++ b/FLT/Basic/Reductions.lean @@ -343,7 +343,9 @@ It follows that there is no Frey package. /-- There is no Frey package. This profound result is proved using work of Mazur and Wiles/Ribet to rule out all possibilities for the $p$-torsion in the corresponding Frey curve. -/ -theorem FreyPackage.false (P : FreyPackage) : False := Wiles_Frey P (Mazur_Frey P) +theorem FreyPackage.false (P : FreyPackage) : False := by + apply Wiles_Frey P + exact Mazur_Frey P -- Fermat's Last Theorem is true theorem Wiles_Taylor_Wiles : FermatLastTheorem := by From a39f7bd3fe8c6dd853fa4cba08e304afca77d2c5 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 5 Aug 2024 16:30:40 +0200 Subject: [PATCH 11/11] Revert `simp only` --- FLT/for_mathlib/Frobenius.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FLT/for_mathlib/Frobenius.lean b/FLT/for_mathlib/Frobenius.lean index 64febfad..5ec6e77c 100644 --- a/FLT/for_mathlib/Frobenius.lean +++ b/FLT/for_mathlib/Frobenius.lean @@ -499,7 +499,7 @@ lemma F_invariant_under_finite_aut (σ : L ≃ₐ[K] L) : set i : (τ : L ≃ₐ[K] L) → τ ∈ Finset.univ → L ≃ₐ[K] L := fun τ _ => σ * τ -- needed to use `set i` instead of `have i`, in order to be able to use `i` later on, in proof have hi : ∀ (τ : L ≃ₐ[K] L) (hτ : τ ∈ Finset.univ), i τ hτ ∈ Finset.univ := by - simp [Finset.mem_univ, forall_true_left, forall_const] + simp only [Finset.mem_univ, forall_true_left, forall_const] have i_inj : ∀ (τ₁ : L ≃ₐ[K] L) (hτ₁ : τ₁ ∈ Finset.univ) (τ₂ : L ≃ₐ[K] L) (hτ₂ : τ₂ ∈ Finset.univ), i τ₁ hτ₁ = i τ₂ hτ₂ → τ₁ = τ₂ := by intros τ₁ _ τ₂ _ h