diff --git a/FltRegular.lean b/FltRegular.lean index 84a24aa9..86775379 100644 --- a/FltRegular.lean +++ b/FltRegular.lean @@ -9,7 +9,6 @@ import FltRegular.MayAssume.Lemmas import FltRegular.NumberTheory.Cyclotomic.CaseI import FltRegular.NumberTheory.Cyclotomic.CyclRat import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits -import FltRegular.NumberTheory.Cyclotomic.Factoring import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo import FltRegular.NumberTheory.Cyclotomic.MoreLemmas import FltRegular.NumberTheory.Cyclotomic.UnitLemmas diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index 6ab6f975..a92098b4 100644 --- a/FltRegular/CaseI/Statement.lean +++ b/FltRegular/CaseI/Statement.lean @@ -1,5 +1,4 @@ import FltRegular.MayAssume.Lemmas -import FltRegular.NumberTheory.Cyclotomic.Factoring import FltRegular.NumberTheory.Cyclotomic.CaseI import FltRegular.CaseI.AuxLemmas import FltRegular.NumberTheory.RegularPrimes @@ -140,8 +139,8 @@ theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) have H₁ := congr_arg (algebraMap ℤ R) H simp only [eq_intCast, Int.cast_add, Int.cast_pow] at H₁ have hζ' := (zeta_spec P ℚ K).unit'_coe - rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _ - (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p) hζ'] at H₁ + rw [hζ'.pow_add_pow_eq_prod_add_mul _ _ <| + odd_iff.2 <| hpri.1.eq_two_or_odd.resolve_left fun h ↦ by simp [h] at h5p] at H₁ replace H₁ := congr_arg (fun x => span ({ x } : Set R)) H₁ simp only [← prod_span_singleton, ← span_singleton_pow] at H₁ refine exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean index 73a09dc6..e206e7c2 100644 --- a/FltRegular/CaseII/InductionStep.lean +++ b/FltRegular/CaseII/InductionStep.lean @@ -1,6 +1,5 @@ import FltRegular.CaseII.AuxLemmas import FltRegular.NumberTheory.KummersLemma.KummersLemma -import FltRegular.NumberTheory.Cyclotomic.Factoring open scoped BigOperators nonZeroDivisors NumberField open Polynomial @@ -70,8 +69,8 @@ include hp hζ e hz in lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by intro hη have : x + y * η ∣ x ^ (p : ℕ) + y ^ (p : ℕ) := by - rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _ - (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe] + rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <| + hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)] simp_rw [mul_comm _ y] exact Finset.dvd_prod_of_mem _ η.prop rw [hη, zero_dvd_iff, e] at this @@ -90,8 +89,9 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by letI := IsCyclotomicExtension.numberField {p} ℚ K have h := zeta_sub_one_dvd hζ e replace h : ∏ _η in nthRootsFinset p (𝓞 K), Ideal.Quotient.mk 𝔭 (x + y * η : 𝓞 K) = 0 := by - rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _ (hpri.out.eq_two_or_odd.resolve_left - (PNat.coe_injective.ne hp)) hζ.unit'_coe, ← Ideal.Quotient.eq_zero_iff_dvd, map_prod] at h + rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <| + hpri.out.eq_two_or_odd.resolve_left + (PNat.coe_injective.ne hp), ← Ideal.Quotient.eq_zero_iff_dvd, map_prod] at h convert h using 2 with η' hη' rw [map_add, map_add, map_mul, map_mul, IsPrimitiveRoot.eq_one_mod_one_sub' hζ.unit'_coe hη', IsPrimitiveRoot.eq_one_mod_one_sub' hζ.unit'_coe η.prop, one_mul, mul_one] @@ -249,8 +249,8 @@ lemma exists_ideal_pow_eq_c_aux : /- The ∏_η, 𝔠 η = (𝔷' 𝔭^m)^p with 𝔷 = 𝔪 𝔷' -/ lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (𝔷' * 𝔭 ^ m) ^ (p : ℕ) := by have e' := span_pow_add_pow_eq hζ e - rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _ - (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe] at e' + rw [hζ.unit'_coe.pow_add_pow_eq_prod_add_mul _ _ <| Nat.odd_iff.2 <| + hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)] at e' rw [← Ideal.prod_span_singleton, ← Finset.prod_attach] at e' simp_rw [mul_comm _ y, ← m_mul_c_mul_p hp hζ e hy, Finset.prod_mul_distrib, Finset.prod_const, Finset.card_attach, diff --git a/FltRegular/NumberTheory/Cyclotomic/Factoring.lean b/FltRegular/NumberTheory/Cyclotomic/Factoring.lean deleted file mode 100644 index aeb4b74b..00000000 --- a/FltRegular/NumberTheory/Cyclotomic/Factoring.lean +++ /dev/null @@ -1,62 +0,0 @@ -/- -Copyright (c) 2021 Alex J. Best. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex J. Best - --/ -import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic - -open Polynomial Finset - -variable {R : Type*} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (x y : R) - -/-- If there is a primitive `n`th root of unity in `K`, then `X ^ n - Y ^ n = ∏ (X - μ Y)`, -where `μ` varies over the `n`-th roots of unity. -/ -theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul_field {K : Type*} [Field K] {ζ : K} (x y : K) - (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : - x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y) := by - by_cases hy : y = 0 - · simp only [hy, zero_pow (Nat.not_eq_zero_of_lt hpos), sub_zero, mul_zero, prod_const] - congr - rw [h.card_nthRootsFinset] - have := congr_arg (eval (x/y)) <| X_pow_sub_one_eq_prod hpos h - rw [eval_sub, eval_pow, eval_one, eval_X, eval_prod] at this - simp_rw [eval_sub, eval_X, eval_C] at this - apply_fun (· * y ^ n) at this - rw [sub_mul, one_mul, div_pow, div_mul_cancel₀ _ (pow_ne_zero n hy)] at this - nth_rw 4 [← h.card_nthRootsFinset] at this - rw [mul_comm, pow_card_mul_prod] at this - convert this using 2 - field_simp [hy] - rw [mul_comm] - -/-- If there is a primitive `n`th root of unity in `R`, then `X ^ n - Y ^ n = ∏ (X - μ Y)`, -where `μ` varies over the `n`-th roots of unity. -/ -theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : - x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x - ζ * y) := by - let K := FractionRing R - apply NoZeroSMulDivisors.algebraMap_injective R K - rw [map_sub, map_pow, map_pow, map_prod] - simp_rw [map_sub, map_mul] - have h' : IsPrimitiveRoot (algebraMap R K ζ) n := - h.map_of_injective <| NoZeroSMulDivisors.algebraMap_injective R K - rw [pow_sub_pow_eq_prod_sub_zeta_runity_mul_field _ _ hpos h'] - symm - refine prod_nbij (algebraMap R K) (fun a ha ↦ ?_) (fun a _ b _ H ↦ - NoZeroSMulDivisors.algebraMap_injective R K H) (fun a ha ↦ ?_) (fun _ _ ↦ rfl) - · rw [mem_nthRootsFinset hpos, ← map_pow, (mem_nthRootsFinset hpos).1 ha, map_one] - · rw [mem_coe, mem_nthRootsFinset hpos] at ha - simp only [Set.mem_image, mem_coe] - have : NeZero n := ⟨hpos.ne'⟩ - obtain ⟨i, -, hζ⟩ := h'.eq_pow_of_pow_eq_one ha - refine ⟨ζ ^ i, ?_, by rwa [map_pow]⟩ - rw [mem_nthRootsFinset hpos, ← pow_mul, mul_comm, pow_mul, h.pow_eq_one, one_pow] - -/-- If there is a primitive `n`th root of unity in `K` and `n` is odd, then -`X ^ n + Y ^ n = ∏ (X + μ Y)`, where `μ` varies over the `n`-th roots of unity. -/ -theorem pow_add_pow_eq_prod_add_zeta_runity_mul (hodd : n % 2 = 1) (h : IsPrimitiveRoot ζ n) : - x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x + ζ * y) := by - have := pow_sub_pow_eq_prod_sub_zeta_runity_mul x (-y) (Nat.odd_iff.mpr hodd).pos h - simp only [mul_neg, sub_neg_eq_add] at this - rw [neg_pow, neg_one_pow_eq_pow_mod_two] at this - simpa [hodd] using this diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index c8bc940e..8456675a 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -341,8 +341,9 @@ lemma isTors' [IsGalois k K] : Module.IsTorsionBySet ℤ[X] simp only [Units.coe_map, MonoidHom.coe_coe, RingOfIntegers.coe_algebraMap_norm, map_pow, Units.coe_prod, Submonoid.coe_finset_prod, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, Algebra.norm_eq_prod_automorphisms] - rw [← hKL, ← IsGalois.card_aut_eq_finrank, ← orderOf_eq_card_of_forall_mem_zpowers hσ, - ← Fin.prod_univ_eq_prod_range, ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp] + rw [← hKL, ← IsGalois.card_aut_eq_finrank, Fintype.card_eq_nat_card, + ← orderOf_eq_card_of_forall_mem_zpowers hσ, ← Fin.prod_univ_eq_prod_range, + ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp] simp only [pow_finEquivZPowers_symm_apply, coe_galRestrictHom_apply, AlgHom.coe_coe, map_prod] rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i ↑x) (Subgroup.zpowers σ)] congr @@ -660,7 +661,7 @@ lemma Hilbert92_aux2 (E : (𝓞 K)ˣ) (ν : k) (hE : algebraMap k K ν = E / σ rw [hE] field_simp rw [norm_eq_prod_pow_gen σ hσ, orderOf_eq_card_of_forall_mem_zpowers hσ, - IsGalois.card_aut_eq_finrank, hKL] + ← Fintype.card_eq_nat_card, IsGalois.card_aut_eq_finrank, hKL] conv => enter [1, 2, i] rw [h1 i, mul_comm] diff --git a/lake-manifest.json b/lake-manifest.json index b22788c6..16255923 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6d297a4172e6c37d3bf82e68924c45d72621ac5d", + "rev": "2c6450e45a0b2b45662a8289c3d0fbf09883939f", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,