From 81ebc691340e489ab1ae28d149b406dad087c3c2 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Mon, 6 May 2024 12:17:54 +0200 Subject: [PATCH] Squashed commit of the following: commit 8a6aa792e428332d768f423d802784a46e616041 Author: Riccardo Brasca Date: Mon May 6 12:17:19 2024 +0200 fix again commit 2c7f85cda743c5d60395c88b1e8f4827c74a9502 Author: Riccardo Brasca Date: Mon May 6 12:12:52 2024 +0200 bump again commit 4a97d0cd0a99db9737621a7dc789a4b6398f5563 Author: Riccardo Brasca Date: Mon May 6 12:09:43 2024 +0200 fix build commit de3819edbb9a86cf4ccf96e74c9a9671b83464bf Author: Riccardo Brasca Date: Sun May 5 14:14:26 2024 +0200 progress commit 0400baa70191d15fd363bb50d6d7a01e96679af8 Author: Riccardo Brasca Date: Sun May 5 13:24:42 2024 +0200 this is done commit 2efb0a3a704144539bb61796ed03ece2722e2213 Author: Riccardo Brasca Date: Sun May 5 12:03:10 2024 +0200 better commit 68c61b72ba2f1115c1fbfd484a56585afa443998 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri May 3 23:16:18 2024 +0200 note commit 9ab7b4fa9e4c5f96c085672c780a841cdafa527d Author: Riccardo Brasca Date: Fri May 3 22:39:38 2024 +0200 start --- FltRegular/CaseI/Statement.lean | 18 +- FltRegular/CaseII/AuxLemmas.lean | 2 - FltRegular/CaseII/InductionStep.lean | 20 +-- FltRegular/NumberTheory/Cyclotomic/CaseI.lean | 7 +- .../NumberTheory/Cyclotomic/CyclRat.lean | 17 +- .../Cyclotomic/GaloisActionOnCyclo.lean | 14 +- .../NumberTheory/Cyclotomic/MoreLemmas.lean | 3 +- .../NumberTheory/Cyclotomic/UnitLemmas.lean | 154 ++++++------------ FltRegular/NumberTheory/CyclotomicRing.lean | 4 +- FltRegular/NumberTheory/Hilbert92.lean | 73 +++++---- FltRegular/NumberTheory/Hilbert94.lean | 10 +- .../NumberTheory/KummersLemma/Field.lean | 46 +++--- .../KummersLemma/KummersLemma.lean | 3 +- FltRegular/NumberTheory/Unramified.lean | 1 - FltRegular/ReadyForMathlib/PowerBasis.lean | 7 - lake-manifest.json | 8 +- 16 files changed, 157 insertions(+), 230 deletions(-) diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index ccdfaa91..320a3fce 100644 --- a/FltRegular/CaseI/Statement.lean +++ b/FltRegular/CaseI/Statement.lean @@ -138,7 +138,6 @@ theorem is_principal {a b c : ℤ} {ζ : R} (hreg : IsRegularPrime p) (hp5 : 5 · rwa [IsRegularPrime, IsRegularNumber] at hreg · exact hI -set_option maxHeartbeats 400000 in theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime p) (hζ : IsPrimitiveRoot ζ p) (hgcd : ({a, b, c} : Finset ℤ).gcd id = 1) (caseI : ¬↑p ∣ a * b * c) (H : a ^ p + b ^ p = c ^ p) : @@ -146,7 +145,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime k₂ ≡ k₁ - 1 [ZMOD p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ (k₁ : ℕ) - ↑b * ζ ^ (k₂ : ℕ) := by let ζ' := (ζ : K) have hζ' : IsPrimitiveRoot ζ' P := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ - have h : ζ = (hζ'.unit' : R) := by simp only [IsPrimitiveRoot.unit', SetLike.eta, Units.val_mk] + have h : ζ = (hζ'.unit' : R) := by rfl have hP : P ≠ (2 : ℕ+) := by intro hP rw [← PNat.coe_inj, PNat.mk_coe] at hP @@ -170,17 +169,16 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime convert hk using 3 rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)] congr 2 - · rw [← Subtype.coe_inj] - simp only [Fin.val_mk, SubsemiringClass.coe_pow, NumberField.Units.coe_zpow, - IsPrimitiveRoot.coe_unit'_coe] - refine' eq_of_div_eq_one _ + · ext + simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe] + refine eq_of_div_eq_one ?_ rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd] simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_natCast, sub_self] - · rw [← Subtype.coe_inj] - simp only [Fin.val_mk, SubsemiringClass.coe_pow, MulMemClass.coe_mul, - NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe] - refine' eq_of_div_eq_one _ + · ext + simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow, + IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe] + refine eq_of_div_eq_one ?_ rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd] simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd, diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean index de57340f..18608782 100644 --- a/FltRegular/CaseII/AuxLemmas.lean +++ b/FltRegular/CaseII/AuxLemmas.lean @@ -13,8 +13,6 @@ variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) open scoped BigOperators nonZeroDivisors NumberField open Polynomial -instance : CharZero (𝓞 K) := SubsemiringClass.instCharZero (𝓞 K) - instance foofoo [NumberField K] : IsDomain (Ideal (𝓞 K)) := by convert Ideal.isDomain (A := 𝓞 K) instance [NumberField K] : CancelMonoidWithZero (Ideal (𝓞 K)) := diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean index d928152f..12f43c1a 100644 --- a/FltRegular/CaseII/InductionStep.lean +++ b/FltRegular/CaseII/InductionStep.lean @@ -40,8 +40,6 @@ lemma zeta_sub_one_dvd : π ∣ x ^ (p : ℕ) + y ^ (p : ℕ) := by apply dvd_pow_self simp -set_option synthInstance.maxHeartbeats 160000 in -set_option maxHeartbeats 400000 in lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by letI : Fact (Nat.Prime p) := hpri letI := IsCyclotomicExtension.numberField {p} ℚ K @@ -55,15 +53,15 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by rw [Finset.prod_const, ← map_pow, Ideal.Quotient.eq_zero_iff_dvd] at h exact hζ.zeta_sub_one_prime'.dvd_of_dvd_pow h -lemma div_one_sub_zeta_mem : (x + y * η : 𝓞 K) / (ζ - 1) ∈ 𝓞 K := by +lemma div_one_sub_zeta_mem : IsIntegral ℤ ((x + y * η : 𝓞 K) / (ζ - 1)) := by obtain ⟨⟨a, ha⟩, e⟩ := one_sub_zeta_dvd_zeta_pow_sub hp hζ e η rw [e, mul_comm] - simp only [Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, - AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, ne_eq] + simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, IsPrimitiveRoot.coe_unit'_coe, + map_one] rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)] def div_zeta_sub_one : nthRootsFinset p (𝓞 K) → 𝓞 K := -fun η ↦ ⟨(x + y * η) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩ +fun η ↦ ⟨(x + y * η.1) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩ lemma div_zeta_sub_one_mul_zeta_sub_one (η) : div_zeta_sub_one hp hζ e η * (π) = x + y * η := by @@ -83,7 +81,6 @@ lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) : rw [Ne, ← Subtype.ext_iff.not] exact hη -set_option synthInstance.maxHeartbeats 40000 in lemma div_zeta_sub_one_Injective : Function.Injective (fun η ↦ Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η)) := by letI : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance @@ -153,13 +150,11 @@ lemma m_mul_c_mul_p : 𝔪 * 𝔠 η * 𝔭 = 𝔦 η := by rw [div_zeta_sub_one_dvd_gcd_spec, Ideal.span_singleton_mul_span_singleton, div_zeta_sub_one_mul_zeta_sub_one] -set_option synthInstance.maxHeartbeats 40000 in lemma m_ne_zero : 𝔪 ≠ 0 := by simp_rw [Ne, gcd_eq_zero_iff, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] rintro ⟨rfl, rfl⟩ exact hy (dvd_zero _) -set_option synthInstance.maxHeartbeats 40000 in lemma p_ne_zero : 𝔭 ≠ 0 := by letI := IsCyclotomicExtension.numberField {p} ℚ K rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] @@ -286,7 +281,7 @@ lemma p_dvd_c_iff : 𝔭 ∣ (𝔠 η) ↔ η = η₀ := by ← Ideal.dvd_span_singleton, ← div_zeta_sub_one_dvd_gcd_spec (hy := hy), ← dvd_gcd_mul_iff_dvd_mul, gcd_comm, gcd_zeta_sub_one_eq_one hζ hy, one_mul] -lemma p_pow_dvd_c_eta_zero_aux [DecidableEq K] : +lemma p_pow_dvd_c_eta_zero_aux [DecidableEq (𝓞 K)] : gcd (𝔭 ^ (m * p)) (∏ η in Finset.attach (nthRootsFinset p (𝓞 K)) \ {η₀}, 𝔠 η) = 1 := by rw [← Ideal.isCoprime_iff_gcd] apply IsCoprime.pow_left @@ -395,7 +390,6 @@ lemma a_mul_denom_eq_a_zero_mul_num (hη : η ≠ η₀) : simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton] rw [mul_comm (𝔞₀ : FractionalIdeal (𝓞 K)⁰ K), ← div_eq_div_iff, ← a_div_a_zero_eq hp hreg hζ e hy hz η hη, FractionalIdeal.spanSingleton_div_spanSingleton] - · rfl · intro ha rw [FractionalIdeal.coeIdeal_eq_zero] at ha apply not_p_div_a_zero hp hζ e hy hz @@ -425,7 +419,6 @@ def associated_eta_zero_unit (hη : η ≠ η₀) : (𝓞 K)ˣ := local notation "ε" => associated_eta_zero_unit hp hreg hζ e hy hz -set_option synthInstance.maxHeartbeats 40000 in lemma associated_eta_zero_unit_spec (η) (hη : η ≠ η₀) : ε η hη * (x + y * η₀) * α η hη ^ (p : ℕ) = (x + y * η) * π ^ (m * p) * β η hη ^ (p : ℕ) := by rw [mul_assoc, mul_comm (ε η hη : 𝓞 K)] @@ -457,7 +450,6 @@ lemma stuff (η₁) (hη₁ : η₁ ≠ η₀) (η₂) (hη₂ : η₂ ≠ η₀ congr 1 ring -set_option maxHeartbeats 400000 in lemma exists_solution : ∃ (x' y' z' : 𝓞 K) (ε₁ ε₂ ε₃ : (𝓞 K)ˣ), ¬ π ∣ x' ∧ ¬ π ∣ y' ∧ ¬ π ∣ z' ∧ ↑ε₁ * x' ^ (p : ℕ) + ε₂ * y' ^ (p : ℕ) = ε₃ * (π ^ m * z') ^ (p : ℕ) := by @@ -524,8 +516,6 @@ lemma exists_solution'_aux {ε₁ ε₂ : (𝓞 K)ˣ} (hx : ¬ π ∣ x) rw [neg_mul, (Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow, sub_neg_eq_add, mul_sub, mul_one, mul_comm x b, add_sub_sub_cancel, add_comm] -set_option synthInstance.maxHeartbeats 160000 in -set_option maxHeartbeats 400000 in lemma exists_solution' : ∃ (x' y' z' : 𝓞 K) (ε₃ : (𝓞 K)ˣ), ¬ π ∣ y' ∧ ¬ π ∣ z' ∧ x' ^ (p : ℕ) + y' ^ (p : ℕ) = ε₃ * (π ^ m * z') ^ (p : ℕ) := by diff --git a/FltRegular/NumberTheory/Cyclotomic/CaseI.lean b/FltRegular/NumberTheory/Cyclotomic/CaseI.lean index d481d44b..2cf2da5f 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CaseI.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CaseI.lean @@ -33,11 +33,12 @@ theorem exists_int_sum_eq_zero'_aux (x y i : ℤ) : intGal (galConj K p) (x + y * ↑(hζ.unit' ^ i) : 𝓞 K) = x + y * (hζ.unit' ^ (-i) : (𝓞 K)ˣ) := by ext1 rw [intGal_apply_coe] - push_cast + simp only [_root_.map_add, map_intCast, _root_.map_mul, AlgHom.coe_coe, zpow_neg, map_units_inv, + add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero] simp_rw [NumberField.Units.coe_zpow] + left push_cast - simp only [zpow_neg, _root_.map_add, map_intCast, _root_.map_mul, map_zpow₀, AlgHom.coe_coe, - galConj_zeta_runity hζ, add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero, inv_zpow] + simp only [map_zpow₀, galConj_zeta_runity hζ, inv_zpow', zpow_neg] theorem exists_int_sum_eq_zero' (hpodd : p ≠ 2) (hp : (p : ℕ).Prime) (x y i : ℤ) {u : (𝓞 K)ˣ} {α : 𝓞 K} (h : (x : 𝓞 K) + y * (hζ.unit' ^ i : (𝓞 K)ˣ) = u * α ^ (p : ℕ)) : diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean index 5195f849..b86887c2 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean @@ -154,9 +154,8 @@ theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη : have h2 := IsPrimitiveRoot.sub_one_norm_prime this (cyclotomic.irreducible_rat p.2) h0 convert h ext - rw [RingOfIntegers.coe_algebraMap_norm] - norm_cast at h2 - rw [h2] + rw [show (η : CyclotomicField p ℚ) - 1 = (η - 1 : _) by simp] at h2 + rw [RingOfIntegers.coe_algebraMap_norm, h2] simp theorem one_sub_zeta_prime [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R) @@ -191,8 +190,6 @@ theorem diff_of_roots2 [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ : R} ( noncomputable instance : AddCommGroup R := AddCommGroupWithOne.toAddCommGroup -set_option maxHeartbeats 300000 in -set_option synthInstance.maxHeartbeats 80000 in lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R} (hη₁ : η₁ ∈ nthRootsFinset p R) (hη₂ : η₂ ∈ nthRootsFinset p R) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y) @@ -345,7 +342,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} ⟨x, lt_trans x.2 (pred_lt hp.out.ne_zero)⟩ := fun x => Fin.ext rfl let ζ' := (ζ : L) have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ - have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by simp + have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by rfl set b := hζ'.integralPowerBasis' with hb have hdim : b.dim = (p : ℕ).pred := by rw [hζ'.power_basis_int'_dim, totient_prime hp.out, pred_eq_sub_one] @@ -371,8 +368,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb] conv_lhs at hy => congr; rfl; ext x - rw [← SubsemiringClass.coe_pow, ← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, - ← sub_eq_add_neg] + rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg] norm_cast at hy rw [sum_sub_distrib] at hy replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨i, hi⟩)) hy @@ -392,7 +388,7 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri let ζ' := (ζ : L) have : Fact (p : ℕ).Prime := ⟨hp⟩ have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ - have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by simp + have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by rfl have hlast : (Fin.castIso (succ_pred_prime hp)) (Fin.last (p : ℕ).pred) = ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩ := Fin.ext rfl have h : ∀ x, (Fin.castIso (succ_pred_prime hp)) (Fin.castSuccEmb x) = @@ -424,8 +420,7 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb] conv_lhs at hy => congr; rfl; ext x - rw [← SubsemiringClass.coe_pow, ← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, - ← sub_eq_add_neg] + rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg] norm_cast at hy rw [sum_sub_distrib] at hy replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨j, hj⟩)) hy diff --git a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean index 269b60eb..cb352da7 100644 --- a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean +++ b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean @@ -88,14 +88,16 @@ theorem galConj_idempotent : (galConj K p).trans (galConj K p) = AlgEquiv.refl : variable (p) --generalize this -theorem gal_map_mem {x : K} (hx : x ∈ RR) (σ : K →ₐ[ℚ] K) : σ x ∈ RR := +theorem gal_map_mem {x : K} (hx : IsIntegral ℤ x) (σ : K →ₐ[ℚ] K) : IsIntegral ℤ (σ x) := map_isIntegral_int (σ.restrictScalars ℤ) hx -theorem gal_map_mem_subtype (σ : K →ₐ[ℚ] K) (x : RR) : σ x ∈ RR := by simp [gal_map_mem] +theorem gal_map_mem_subtype (σ : K →ₐ[ℚ] K) (x : RR) : IsIntegral ℤ (σ x) := + gal_map_mem x.2 _ /-- Restriction of `σ : K →ₐ[ℚ] K` to the ring of integers. -/ def intGal (σ : K →ₐ[ℚ] K) : RR →ₐ[ℤ] RR := - ((σ.restrictScalars ℤ).restrictDomain RR).codRestrict RR (gal_map_mem_subtype σ) + ((σ.restrictScalars ℤ).restrictDomain RR).codRestrict (integralClosure ℤ K) + (gal_map_mem_subtype σ) @[simp] theorem intGal_apply_coe (σ : K →ₐ[ℚ] K) (x : RR) : (intGal σ x : K) = σ x := @@ -111,7 +113,7 @@ variable (K) def unitGalConj : RRˣ →* RRˣ := unitsGal (galConj K p) -theorem unitGalConj_spec (u : RRˣ) : galConj K p (u : 𝓞 K) = ↑(unitGalConj K p u : 𝓞 K) := rfl +theorem unitGalConj_spec (u : RRˣ) : galConj K p u = unitGalConj K p u := rfl variable {K} @@ -123,6 +125,4 @@ theorem unit_lemma_val_one (u : RRˣ) (φ : K →+* ℂ) : simp only [map_inv₀, Complex.abs_conj] rw [mul_inv_eq_one₀] intro h - simp only [_root_.map_eq_zero] at h - rw [← Subalgebra.coe_zero (𝓞 K), Subtype.coe_inj] at h - exact Units.ne_zero _ h + simp at h diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index b48862aa..4de92c71 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -179,6 +179,7 @@ lemma quotient_zero_sub_one_comp_aut (σ : 𝓞 K →+* 𝓞 K) : · rw [mem_nthRootsFinset p.pos, ← map_pow, hζ.unit'_coe.pow_eq_one, map_one] · rw [mem_nthRootsFinset p.pos, hζ.unit'_coe.pow_eq_one] +set_option synthInstance.maxHeartbeats 80000 in lemma zeta_sub_one_dvd_trace_sub_smul (x : 𝓞 K) : (hζ.unit' - 1 : 𝓞 K) ∣ Algebra.trace ℤ _ x - (p - 1 : ℕ) • x := by letI := IsCyclotomicExtension.numberField {p} ℚ K @@ -226,7 +227,7 @@ lemma norm_add_one_smul_of_isUnit {K} [Field K] [NumberField K] {p : ℕ} (hpri apply Int.natAbs_eq_iff.mp apply (Int.cast_injective (α := ℚ)).comp Nat.cast_injective simp only [Int.cast_abs, Function.comp_apply, Nat.cast_one, Int.cast_one, ← Int.abs_eq_natAbs, - Algebra.coe_norm_int, ← NumberField.isUnit_iff_norm.mp hx, RingOfIntegers.norm_apply_coe] + Algebra.coe_norm_int, ← NumberField.isUnit_iff_norm.mp hx, RingOfIntegers.coe_norm] have : Algebra.norm ℤ (1 + (p : ℕ) • x) ≠ -1 := by intro e; apply hp obtain ⟨r, hr⟩ := Algebra.norm_one_add_smul (p : ℤ) x diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean index c6b55514..84a06d07 100644 --- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean @@ -45,8 +45,8 @@ local notation "ζ1" => (hζ.unit' - 1 : 𝓞 K) set_option quotPrecheck false local notation "I" => (Ideal.span ({(hζ.unit' - 1 : 𝓞 K)} : Set (𝓞 K)) : Ideal (𝓞 K)) -theorem IsPrimitiveRoot.unit'_pow : hζ.unit' ^ (p : ℕ) = 1 := - Units.ext <| Subtype.ext <| by simpa using hζ.pow_eq_one +theorem IsPrimitiveRoot.unit'_pow : hζ.unit' ^ (p : ℕ) = 1 := by + ext; simpa using hζ.pow_eq_one theorem zeta_runity_pow_even (hpo : Odd (p : ℕ)) (n : ℕ) : ∃ m : ℕ, hζ.unit' ^ n = hζ.unit' ^ (2 * m) := by @@ -129,7 +129,7 @@ theorem contains_two_primitive_roots {p q : ℕ} {x y : K} [FiniteDimensional (cyclotomic.irreducible_rat (PNat.pos ⟨k, hkpos⟩))).symm theorem totient_le_one_dvd_two {a : ℕ} (han : 0 < a) (ha : a.totient ≤ 1) : a ∣ 2 := by - cases' Nat.totient_eq_one_iff.1 (show a.totient = 1 by linarith [Nat.totient_pos han]) with h + cases' Nat.totient_eq_one_iff.1 (show a.totient = 1 by linarith [Nat.totient_pos.2 han]) with h h <;> simp [h] @@ -143,14 +143,11 @@ theorem eq_one_mod_one_sub {A : Type _} [CommRing A] {t : A} : theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type _} [CommRing A] [IsDomain A] {ζ : A} (hζ : IsPrimitiveRoot ζ p) {μ : A} (hμ : μ ^ (p : ℕ) = 1) : - (@DFunLike.coe _ A (fun _ => A ⧸ Ideal.span {ζ - 1}) _ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ) = 1 := by + (@DFunLike.coe _ A (fun _ => A ⧸ Ideal.span {ζ - 1}) _ + (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ) = 1 := by obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos rw [map_pow, eq_one_mod_one_sub, one_pow] -instance : Algebra (𝓞 K) (𝓞 K ⧸ I) := Ideal.Quotient.algebra _ -instance : AddCommMonoid (𝓞 K) := inferInstance -instance : AddCommMonoid (𝓞 K ⧸ I) := inferInstance - set_option synthInstance.maxHeartbeats 40000 in theorem aux {t} {l : 𝓞 K} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot μ p) (h : ∑ x : Fin t, f x • (⟨μ, hμ.isIntegral p.pos⟩ : 𝓞 K) ^ (x : ℕ) = l) : @@ -181,7 +178,7 @@ theorem IsPrimitiveRoot.p_mem_one_sub_zeta [hp : Fact (p : ℕ).Prime] : (p : variable [IsCyclotomicExtension {p} ℚ K] -theorem roots_of_unity_in_cyclo_aux {x : K} {n l : ℕ} (hl : l ∈ n.divisors) (hx : x ∈ R) +theorem roots_of_unity_in_cyclo_aux {x : K} {n l : ℕ} (hl : l ∈ n.divisors) (hx : IsIntegral ℤ x) (hhl : (cyclotomic l R).IsRoot ⟨x, hx⟩) {ζ : K} (hζ : IsPrimitiveRoot ζ p) : l ∣ 2 * p := by by_contra h have hpl' : IsPrimitiveRoot (⟨x, hx⟩ : R) l := by @@ -204,7 +201,7 @@ theorem roots_of_unity_in_cyclo_aux {x : K} {n l : ℕ} (hl : l ∈ n.divisors) cases' pdivlcm with pdivlcm_w pdivlcm_h have ineq1 := Nat.totient_super_multiplicative (p : ℕ) pdivlcm_w rw [← pdivlcm_h] at ineq1 - have KEY3 := (mul_le_iff_le_one_right (Nat.totient_pos p.prop)).mp (le_trans ineq1 KEY) + have KEY3 := (mul_le_iff_le_one_right (Nat.totient_pos.2 p.prop)).mp (le_trans ineq1 KEY) have pdiv_ne_zero : 0 < pdivlcm_w := by by_contra h simp only [not_lt, le_zero_iff] at h @@ -230,8 +227,7 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K) (h : ∃ (n : ℕ) (_ : 0 < n), x ^ (n : ℕ) = 1) : ∃ (m : ℕ) (k : ℕ+), x = (-1) ^ (k : ℕ) * (hζ.unit' : K) ^ (m : ℕ) := by obtain ⟨n, hn0, hn⟩ := h - have hx : x ∈ R := by - rw [mem_ringOfIntegers] + have hx : IsIntegral ℤ x := by refine' ⟨X ^ n - 1, _⟩ constructor · exact monic_X_pow_sub_C 1 (ne_of_lt hn0).symm @@ -258,26 +254,27 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K) simp only [one_pow] apply hxp' cases' hxp'' with hxp'' hxp'' - obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp'' p.prop - refine' ⟨i, 2, _⟩ - simp only [IsPrimitiveRoot.unit'_val_coe] - rw [← Subtype.val_inj] at Hi - simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe] at Hi - rw [← Hi, show ((2 : ℕ+) : ℕ) = 2 by decide] - simp - have hone : (-1 : R) ^ (p : ℕ) = (-1 : R) := by apply Odd.neg_one_pow hpo - have hxp3 : (-1 * ⟨x, hx⟩ : R) ^ (p : ℕ) = 1 := by - rw [mul_pow, hone, hxp''] - ring - obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp3 p.prop - refine' ⟨i, 1, _⟩ - simp only [PNat.one_coe, pow_one, neg_mul, one_mul, neg_neg] - rw [← Subtype.val_inj] at Hi - simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe, Submonoid.coe_mul, - Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, InvMemClass.coe_inv, - OneMemClass.coe_one, neg_mul, one_mul] at Hi - simp only [IsPrimitiveRoot.unit'_val_coe] - exact Iff.mp neg_eq_iff_eq_neg (id (Eq.symm (by simpa using Hi))) + · obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp'' p.prop + refine' ⟨i, 2, _⟩ + simp only [IsPrimitiveRoot.unit'_val_coe] + rw [← Subtype.val_inj] at Hi + simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe] at Hi + rw [← Hi, show ((2 : ℕ+) : ℕ) = 2 by decide] + simp only [even_two, Even.neg_pow, one_pow, one_mul] + rfl + · have hone : (-1 : R) ^ (p : ℕ) = (-1 : R) := by apply Odd.neg_one_pow hpo + have hxp3 : (-1 * ⟨x, hx⟩ : R) ^ (p : ℕ) = 1 := by + rw [mul_pow, hone, hxp''] + ring + obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp3 p.prop + refine' ⟨i, 1, _⟩ + simp only [PNat.one_coe, pow_one, neg_mul, one_mul, neg_neg] + rw [← Subtype.val_inj] at Hi + simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe, Submonoid.coe_mul, + Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, InvMemClass.coe_inv, + OneMemClass.coe_one, neg_mul, one_mul] at Hi + simp only [IsPrimitiveRoot.unit'_val_coe] + exact Iff.mp neg_eq_iff_eq_neg (id (Eq.symm (by simpa using Hi))) obtain ⟨m, k, hmk⟩ := H refine' ⟨m, k, _⟩ have eq : ((⟨x, hx⟩ : R) : K) = x := rfl @@ -293,9 +290,10 @@ theorem IsPrimitiveRoot.isPrime_one_sub_zeta [hp : Fact (p : ℕ).Prime] : · exact hζ.zeta_sub_one_prime' apply_fun (fun x : 𝓞 K => (x : K)) push_cast - rw [Ne, sub_eq_zero] - rintro rfl - exact hp.1.ne_one (hζ.unique IsPrimitiveRoot.one) + intro h + simp only [map_sub, coe_unit'_coe, map_one, map_zero, sub_eq_zero] at h + refine hp.1.ne_one (hζ.unique ?_) + simp [h] theorem IsPrimitiveRoot.two_not_mem_one_sub_zeta [hp : Fact (p : ℕ).Prime] (h : p ≠ 2) : (2 : 𝓞 K) ∉ I := by @@ -346,12 +344,12 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : Rˣ) (hp : (p : ℕ).Prime) : congr 1 rw [map_zsmul] -- todo: probably swap `is_primitive_root.inv` and `is_primitive_root.inv'`. - have : ∀ x : Fin φn, intGal (↑(galConj K p)) (⟨ζ, hζ.isIntegral p.pos⟩ ^ (x : ℕ)) = + have : ∀ x : Fin φn, intGal ((galConj K p)) (⟨ζ, hζ.isIntegral p.pos⟩ ^ (x : ℕ)) = ⟨ζ⁻¹, hζ.inv.isIntegral p.pos⟩ ^ (x : ℕ) := by intro x ext - simp only [intGal_apply_coe, map_pow, SubsemiringClass.coe_pow, Subtype.coe_mk] - rw [← map_pow, AlgHom.coe_coe, galConj_zeta_runity_pow hζ] + simp only [map_pow, intGal_apply_coe, RingOfIntegers.map_mk, AlgHom.coe_coe, inv_pow] + rw [← map_pow, galConj_zeta_runity_pow hζ, inv_pow] conv_lhs at hu' => congr congr @@ -359,7 +357,7 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : Rˣ) (hp : (p : ℕ).Prime) : rw [this a] exact (aux hζ hζ hu).trans (aux hζ hζ.inv hu').symm -set_option synthInstance.maxHeartbeats 40000 in +set_option synthInstance.maxHeartbeats 80000 in theorem unit_inv_conj_not_neg_zeta_runity (h : p ≠ 2) (u : Rˣ) (n : ℕ) (hp : (p : ℕ).Prime) : u * (unitGalConj K p u)⁻¹ ≠ -hζ.unit' ^ n := by by_contra H @@ -373,6 +371,15 @@ theorem unit_inv_conj_not_neg_zeta_runity (h : p ≠ 2) (u : Rˣ) (n : ℕ) (hp apply hζ.two_not_mem_one_sub_zeta h rw [← Ideal.Quotient.eq_zero_iff_mem, map_two, ← neg_one_eq_one_iff_two_eq_zero, ← hμ', hμ] +-- Add to mathlib +@[norm_cast] +lemma NumberField.RingOfIntegers.eq_iff {K : Type*} [Field K] {x y : 𝓞 K} : + (x : K) = (y : K) ↔ x = y := + NumberField.RingOfIntegers.ext_iff.symm +instance {K L : Type*} [Field K] [Ring L] [Algebra K L] : Algebra (𝓞 K) L := + inferInstanceAs (Algebra (integralClosure _ _) L) +instance {K L : Type*} [Field K] [Ring L] [Algebra K L] : IsScalarTower (𝓞 K) K L := + inferInstanceAs (IsScalarTower (integralClosure _ _) K L) -- this proof has mild coe annoyances rn theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : Rˣ) : @@ -388,16 +395,14 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : have hk := Nat.even_or_odd k cases' hk with hk hk · simp only [hk.neg_one_pow, one_mul] at hz - rw [← Subalgebra.coe_mul, ← Units.val_mul, ← Subalgebra.coe_pow, - ← Units.val_pow_eq_pow_val] at hz + rw [← map_mul, ← Units.val_mul, ← map_pow, ← Units.val_pow_eq_pow_val] at hz norm_cast at hz rw [hz] refine' (exists_congr fun a => _).mp (zeta_runity_pow_even hζ hpo n) · rw [mul_comm] · by_contra simp only [hk.neg_one_pow, neg_mul, one_mul] at hz - rw [← Subalgebra.coe_mul, ← Units.val_mul, ← Subalgebra.coe_pow, ← - Units.val_pow_eq_pow_val] at hz + rw [← map_mul, ← Units.val_mul, ← map_pow, ← Units.val_pow_eq_pow_val, ← map_neg] at hz norm_cast at hz simpa [hz] using unit_inv_conj_not_neg_zeta_runity hζ h u n hp · apply RingHom.IsIntegralElem.mul @@ -412,69 +417,6 @@ lemma inv_coe_coe {K A : Type*} [Field K] [SetLike A K] [SubsemiringClass A K] { rw [mul_inv_self] rfl --- This is now not used? --- Failed when updating to leanprover/lean4:v4.3.0-rc2 (coercion / power issues) --- theorem unit_lemma_gal_conj (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : Rˣ) : --- ∃ (x : Rˣ) (n : ℕ), IsGalConjReal p (x : K) ∧ u = x * (hζ.unit' ^ n : (𝓞 K)ˣ) := by --- obtain ⟨m, hm⟩ := unit_inv_conj_is_root_of_unity hζ h hp u --- use u * hζ.unit'⁻¹ ^ m, m --- rw [IsGalConjReal] --- have hy : u * (hζ.unit' ^ m)⁻¹ = unitGalConj K p u * hζ.unit' ^ m := by --- rw [pow_two] at hm --- have := auxil u (unitGalConj K p u) (hζ.unit' ^ m) (hζ.unit' ^ m) --- apply this hm --- dsimp --- simp only [inv_pow, AlgHom.map_mul] --- have hz : galConj K p (hζ.unit' ^ m)⁻¹ = hζ.unit' ^ m := by --- simp only [Units.val_pow_eq_pow_val, SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe, --- map_inv₀, galConj_zeta_runity_pow hζ m, inv_pow, inv_inv] --- constructor --- · rw [map_mul, ← zpow_neg_one, NumberField.Units.coe_zpow, zpow_neg_one, hz, --- unitGalConj_spec K p u, ← Subalgebra.coe_mul, ← Units.val_mul, ← hy, Units.val_mul, --- Subalgebra.coe_mul, inv_coe_coe] --- · rw [inv_mul_cancel_right] - -/- -lemma unit_lemma (u : RRˣ) : - ∃ (x : RRˣ) (n : ℤ), element_is_real (x : KK) ∧ (u : KK) = x * (zeta_runity p ℚ) ^ n := -begin - have := mem_roots_of_unity_of_abs_eq_one (u * (unit_gal_conj p u)⁻¹ : KK) _ _, - { have : ∃ m : ℕ, u * (unit_gal_conj p u)⁻¹ = (zeta_runity p ℚ) ^ (2 * m), - admit, --follows from above with some work - -- what we have shows its +- a power of zeta_runity - obtain ⟨m, hm⟩ := this, - use [u * (zeta_runity p ℚ)⁻¹ ^ m, m], - split, - { rw element_is_real, - intro φ, - have := congr_arg (conj ∘ φ ∘ coe) hm, - simp at this, - simp [alg_hom.map_inv], - rw ← coe_coe, - rw ← coe_coe, -- TODO this is annoying - rw (_ : (↑(zeta_runity p ℚ ^ m)⁻¹ : KK) = (zeta_runity p ℚ ^ m : KK)⁻¹), - rw alg_hom.map_inv, - rw ring_hom.map_inv, - rw mul_inv_eq_iff_eq_mul₀, - simp, - admit, -- wow we should really have some more structure and simp lemmas to tame this beast - admit, -- similar silly goal to below - admit, - }, - { simp only [mul_assoc, inv_pow, subalgebra.coe_mul, coe_coe, units.coe_mul, zpow_coe_nat], - norm_cast, - simp, }, }, - { exact unit_lemma_val_one p u, }, - { apply is_integral_mul, - exact number_field.ring_of_integers.is_integral_coe (coe_b u), - rw (_ : ((unit_gal_conj p u)⁻¹ : KK) = (↑(unit_gal_conj p u⁻¹))), - exact number_field.ring_of_integers.is_integral_coe (coe_b _), - simp, - admit, -- tis a silly goal - }, -end --/ - lemma IsPrimitiveRoot.eq_one_mod_one_sub' {A : Type*} [CommRing A] [IsDomain A] {n : ℕ+} {ζ : A} (hζ : IsPrimitiveRoot ζ n) {η : A} (hη : η ∈ nthRootsFinset n A) : Ideal.Quotient.mk (Ideal.span ({ζ - 1} : Set A)) η = 1 := by diff --git a/FltRegular/NumberTheory/CyclotomicRing.lean b/FltRegular/NumberTheory/CyclotomicRing.lean index 099433ec..bd600d8e 100644 --- a/FltRegular/NumberTheory/CyclotomicRing.lean +++ b/FltRegular/NumberTheory/CyclotomicRing.lean @@ -73,7 +73,6 @@ lemma one_sub_zeta_mem_nonZeroDivisors : lemma not_isUnit_one_sub_zeta : ¬ IsUnit (1 - zeta p) := (prime_one_sub_zeta p).irreducible.1 -set_option synthInstance.maxHeartbeats 40000 in lemma one_sub_zeta_dvd_int_iff (n : ℤ) : 1 - zeta p ∣ n ↔ ↑p ∣ n := by letI p' : ℕ+ := ⟨p, hpri.out.pos⟩ letI : Fact (PNat.Prime p') := hpri @@ -91,7 +90,6 @@ lemma isCoprime_one_sub_zeta (n : ℤ) (hn : ¬ (p : ℤ) ∣ n) : IsCoprime (1 (algebraMap ℤ <| CyclotomicIntegers p)).of_isCoprime_of_dvd_left exact one_sub_zeta_dvd p -set_option synthInstance.maxHeartbeats 80000 in lemma exists_dvd_int (n : CyclotomicIntegers p) (hn : n ≠ 0) : ∃ m : ℤ, m ≠ 0 ∧ n ∣ m := by refine ⟨Algebra.norm ℤ ((equiv p) n), by simpa, ?_⟩ rw [← map_dvd_iff (equiv p), map_intCast] @@ -135,7 +133,7 @@ lemma nontrivial {p} (hp : p ≠ 0) : Nontrivial (CyclotomicIntegers p) := by intro h have := natDegree_eq_zero_of_isUnit h rw [natDegree_cyclotomic] at this - exact this.not_gt (p.totient_pos (Nat.pos_iff_ne_zero.mpr hp)) + exact this.not_gt (Nat.totient_pos.2 <| Nat.zero_lt_of_ne_zero hp) lemma charZero {p} (hp : p ≠ 0) : CharZero (CyclotomicIntegers p) := letI := nontrivial hp diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 126aeb12..7477a252 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -234,7 +234,7 @@ variable (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) def RelativeUnits (k K : Type*) [Field k] [Field K] [Algebra k K] := - ((𝓞 K)ˣ ⧸ (MonoidHom.range <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K)))) + ((𝓞 K)ˣ ⧸ (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K)))) instance : CommGroup (RelativeUnits k K) := by delta RelativeUnits; infer_instance @@ -242,8 +242,8 @@ attribute [local instance] IsCyclic.commGroup attribute [local instance 2000] inst_ringOfIntegersAlgebra Algebra.toSMul Algebra.toModule -instance : IsScalarTower ↥(𝓞 k) ↥(𝓞 K) K := IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl) -instance : IsIntegralClosure ↥(𝓞 K) ↥(𝓞 k) K := IsIntegralClosure.of_isIntegrallyClosed _ _ _ +instance : IsScalarTower (𝓞 k) (𝓞 K) K := IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl) +instance : IsIntegralClosure (𝓞 K) (𝓞 k) K := IsIntegralClosure.of_isIntegrallyClosed _ _ _ (fun x ↦ IsIntegral.tower_top (IsIntegralClosure.isIntegral ℤ K x)) lemma coe_galRestrictHom_apply (σ : K →ₐ[k] K) (x) : @@ -298,8 +298,6 @@ lemma pow_finEquivZPowers_symm_apply {M} [Group M] (x : M) (hx) (a) : x ^ ((finEquivZPowers x hx).symm a : ℕ) = a := congr_arg Subtype.val ((finEquivZPowers x hx).apply_symm_apply a) -set_option synthInstance.maxHeartbeats 160000 in -set_option maxHeartbeats 400000 in open Polynomial in lemma isTors' : Module.IsTorsionBySet ℤ[X] (Module.AEval' (addMonoidEndRingEquivInt _ @@ -328,7 +326,7 @@ lemma isTors' : Module.IsTorsionBySet ℤ[X] 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] - simp only [pow_finEquivZPowers_symm_apply, coe_galRestrictHom_apply, AlgHom.coe_coe] + 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 ext x @@ -406,7 +404,7 @@ lemma NumberField.Units.finrank_eq : finrank ℤ (Additive (𝓞 k)ˣ) = NumberF local instance : Module.Finite ℤ (Additive <| RelativeUnits k K) := by delta RelativeUnits show Module.Finite ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup - (MonoidHom.range <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K))))) + (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))))) infer_instance local instance : Module.Finite ℤ (Additive <| relativeUnitsWithGenerator p hp hKL σ hσ) := by @@ -432,10 +430,10 @@ lemma finrank_G : finrank ℤ G = (Units.rank k + 1) * (↑p - 1) := by rw [← Submodule.torsion_int] refine (FiniteDimensional.finrank_quotient_of_le_torsion _ le_rfl).trans ?_ show finrank ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup - (MonoidHom.range <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K))))) = _ + (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))))) = _ rw [FiniteDimensional.finrank_quotient] show _ - finrank ℤ (LinearMap.range <| AddMonoidHom.toIntLinearMap <| - MonoidHom.toAdditive <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K))) = _ + MonoidHom.toAdditive <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))) = _ rw [LinearMap.finrank_range_of_inj, NumberField.Units.finrank_eq, NumberField.Units.finrank_eq, NumberField.Units.rank_of_isUnramified (k := k), add_mul, one_mul, mul_tsub, mul_one, mul_comm, add_tsub_assoc_of_le, tsub_add_eq_add_tsub, hKL] @@ -470,16 +468,13 @@ lemma unitlifts_spec (S : systemOfUnits p G (NumberField.Units.rank k + 1)) (i) simp only [toMul_ofMul, Quotient.out_eq', ofMul_toMul] exact Quotient.out_eq' _ -set_option synthInstance.maxHeartbeats 80000 in lemma u_lemma2 (u v : (𝓞 K)ˣ) (hu : u = v / (σ v : K)) : (mkG u) = (1 - zeta p : A) • (mkG v) := by rw [sub_smul, one_smul, relativeUnitsModule_zeta_smul, ← unit_to_U_div] congr rw [eq_div_iff_mul_eq'] ext - simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, Submonoid.coe_mul, - Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, coe_galRestrictHom_apply, hu] - refine div_mul_cancel₀ _ ?_ - simp only [ne_eq, map_eq_zero, ZeroMemClass.coe_eq_zero, Units.ne_zero, not_false_eq_true] + simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, map_mul, coe_galRestrictHom_apply, hu] + exact div_mul_cancel₀ _ (by simp) open multiplicity in theorem padicValNat_dvd_iff_le' {p : ℕ} (hp : p ≠ 1) {a n : ℕ} (ha : a ≠ 0) : @@ -701,18 +696,26 @@ lemma Hilbert92ish_aux1 (n : ℕ) (H : Fin n → Additive (𝓞 K)ˣ) (ζ : ( letI J : (𝓞 K)ˣ := (Additive.toMul (∑ i : Fin n, ι i • H i)) * (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom ζ) ^ (-a) Algebra.norm k (S := K) ((J : (𝓞 K)ˣ) : K) = 1 := by - simp only [toMul_sum, toMul_zsmul, RingHom.toMonoidHom_eq_coe, zpow_neg, Units.val_mul, - Units.coe_prod, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, - Submonoid.coe_finset_prod, Units.coe_zpow, map_mul, map_prod, ← Units.coe_val_inv, - norm_map_inv, norm_map_zpow, hKL, Units.coe_map, MonoidHom.coe_coe, - RingOfInteger.coe_algebraMap_apply, Algebra.norm_algebraMap] + have hcoe : ((algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ((ζ ^ a)⁻¹).1)) = + algebraMap (𝓞 k) (𝓞 K) ((ζ ^ a)⁻¹).1 := rfl + simp only [toMul_sum, toMul_zsmul, zpow_neg, Units.val_mul, Units.coe_prod, map_mul, map_prod, + Units.coe_zpow, map_mul, map_prod, ← Units.coe_val_inv, norm_map_inv, norm_map_zpow, + Units.coe_map] + rw [← map_zpow, Units.coe_map_inv] + simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe] + have hcoe1 : + algebraMap (𝓞 k) k (((ζ ^ (p : ℕ)) ^ a)⁻¹).1 = ((((ζ : 𝓞 k) : k) ^ (p : ℕ)) ^ a)⁻¹ := by + convert (Units.coe_map_inv ((algebraMap (𝓞 k) k) : (𝓞 k) →* k) ((ζ ^ (p : ℕ)) ^ a)).symm + simp + rw [hcoe, RingOfInteger.coe_algebraMap_apply, Algebra.norm_algebraMap, hKL, ← map_pow, + ← Units.val_pow_eq_pow_val, inv_pow, ← zpow_natCast, ← zpow_mul, mul_comm a, zpow_mul, + zpow_natCast, hcoe1] apply_fun Additive.toMul at ha apply_fun ((↑) : (𝓞 k)ˣ → k) at ha - simp only [toMul_sum, toMul_zsmul, Units.coe_prod, Submonoid.coe_finset_prod, hη, - Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, Units.coe_zpow, toMul_ofMul] at ha + simp only [toMul_sum, toMul_zsmul, Units.coe_prod, map_prod, hη, + Units.coe_zpow, toMul_ofMul] at ha rwa [← zpow_natCast, ← zpow_mul, mul_comm _ a, mul_inv_eq_one₀] - rw [← Units.coe_zpow] - simp only [ne_eq, ZeroMemClass.coe_eq_zero, Units.ne_zero, not_false_eq_true] + simp [← Units.coe_zpow] lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E / σ E) (hζ : (ζ : k) ^ (p : ℕ) = 1) (hpodd : (p : ℕ) ≠ 2) : @@ -760,7 +763,6 @@ lemma unit_to_U_map (x : (𝓞 k)ˣ) : mkG (Units.map (algebraMap (𝓞 k) (𝓞 rw [ofMul_eq_zero, QuotientGroup.eq_one_iff] exact ⟨_, rfl⟩ -set_option synthInstance.maxHeartbeats 160000 in lemma unit_to_U_neg (x) : mkG (-x) = mkG x := by rw [← one_mul x, ← neg_mul, unit_to_U_mul, one_mul, add_left_eq_self] convert unit_to_U_map p hp hKL σ hσ (-1) @@ -768,7 +770,7 @@ lemma unit_to_U_neg (x) : mkG (-x) = mkG x := by simp only [Units.val_neg, Units.val_one, OneMemClass.coe_one, Units.coe_map, MonoidHom.coe_coe, map_neg, map_one] -instance : CommGroup (↥(𝓞 k))ˣ := inferInstance +instance : CommGroup ((𝓞 k))ˣ := inferInstance lemma IsPrimitiveRoot.one_left_iff {M} [CommMonoid M] {n : ℕ} : IsPrimitiveRoot (1 : M) n ↔ n = 1 := @@ -781,8 +783,6 @@ lemma Algebra.norm_of_finrank_eq_two (hKL : finrank k K = 2) (x : K) : rfl -- TODO : remove `p ≠ 2`. The offending case is when `K = k[i]`. -set_option synthInstance.maxHeartbeats 160000 in -set_option maxHeartbeats 400000 in lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := by classical @@ -797,7 +797,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : have NE_p_pow : (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom NE) = E ^ (p : ℕ) · ext simp only [RingHom.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, - RingOfInteger.coe_algebraMap_apply, RingOfIntegers.norm_apply_coe, Units.val_pow_eq_pow_val, SubmonoidClass.coe_pow, Units.val_neg] + RingOfInteger.coe_algebraMap_apply, Units.val_pow_eq_pow_val, map_pow] rw [← map_pow] at hE refine Hilbert92ish_aux2 p hp hKL σ hσ E _ hE ?_ hpodd rw [← pow_mul, ← pow_succ] @@ -819,9 +819,9 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : intro i induction i using Fin.lastCases with | last => - simp only [Fin.snoc_last, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe, NE, η, H2] + simp only [Fin.snoc_last, toMul_ofMul, Units.coe_map, RingOfIntegers.coe_norm, NE, η, H2] | cast i => - simp only [Fin.snoc_castSucc, toMul_ofMul, Units.coe_map, RingOfIntegers.norm_apply_coe, NE, + simp only [Fin.snoc_castSucc, toMul_ofMul, Units.coe_map, RingOfIntegers.coe_norm, NE, η, H2, J, N, H] · intro ε hε refine hS.corollary p hp _ _ (finrank_G p hp hKL σ hσ) _ (ι ∘ Fin.castSucc) ?_ (mkG ε) ?_ @@ -832,7 +832,9 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : Set.mem_singleton_iff, not_not] at this rw [this] at ha' cases' h with h - · exact ha'' (by simpa using hζ) this + · refine ha'' ?_ this + ext + simpa using hζ obtain ⟨ε', hε'⟩ : ∃ ε' : (𝓞 k)ˣ, ε' ^ (p : ℕ) = NE · rw [← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at ha' obtain ⟨α, β, hαβ⟩ := ha' @@ -859,10 +861,11 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : rw [map_mul, ← mul_inv_eq_iff_eq_mul] ext simpa using e.symm - simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero, hε'', - RingHom.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_pow, - RingOfInteger.coe_algebraMap_apply, AlgEquiv.commutes, ne_eq, map_eq_zero, - ZeroMemClass.coe_eq_zero, Units.ne_zero, not_false_eq_true, div_self] at hE + simp only [Nat.succ_sub_succ_eq_sub, tsub_zero, ← map_pow, hε'', RingHom.toMonoidHom_eq_coe, + Units.coe_map, MonoidHom.coe_coe, RingOfInteger.coe_algebraMap_apply, + AlgEquiv.commutes] at hE + replace hE : (algebraMap k K) (((ζ : 𝓞 k) : k) ^ (p : ℕ) ^ h) = 1 := by + rwa [div_self (by simp)] at hE erw [hE] at hζ'' --why? rw [IsPrimitiveRoot.one_left_iff] at hζ'' exact hp.one_lt.ne.symm hζ'' diff --git a/FltRegular/NumberTheory/Hilbert94.lean b/FltRegular/NumberTheory/Hilbert94.lean index 0f4d2fe7..bb0ffb7f 100644 --- a/FltRegular/NumberTheory/Hilbert94.lean +++ b/FltRegular/NumberTheory/Hilbert94.lean @@ -114,23 +114,23 @@ theorem Ideal.isPrincipal_pow_finrank_of_isPrincipal_map [IsDedekindDomain A] (I then there is an ideal that capitulates in `K`. -/ theorem exists_not_isPrincipal_and_isPrincipal_map (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] - [FiniteDimensional K L] [IsGalois K L] [IsUnramified ↥(𝓞 K) ↥(𝓞 L)] [IsCyclic (L ≃ₐ[K] L)] + [FiniteDimensional K L] [IsGalois K L] [IsUnramified (𝓞 K) (𝓞 L)] [IsCyclic (L ≃ₐ[K] L)] (hKL : Nat.Prime (finrank K L)) (hKL' : finrank K L ≠ 2) : - ∃ I : Ideal (𝓞 K), ¬I.IsPrincipal ∧ (I.map (algebraMap ↥(𝓞 K) ↥(𝓞 L))).IsPrincipal := by + ∃ I : Ideal (𝓞 K), ¬I.IsPrincipal ∧ (I.map (algebraMap (𝓞 K) (𝓞 L))).IsPrincipal := by obtain ⟨⟨σ, hσ⟩⟩ := ‹IsCyclic (L ≃ₐ[K] L)› obtain ⟨η, hη, hη'⟩ := Hilbert92 hKL hKL' σ hσ - exact exists_not_isPrincipal_and_isPrincipal_map_aux (A := ↥(𝓞 K)) σ hσ η hη (not_exists.mpr hη') + exact exists_not_isPrincipal_and_isPrincipal_map_aux (A := (𝓞 K)) σ hσ η hη (not_exists.mpr hη') /-- This is the second part of **Hilbert Theorem 94**, which states that if `L/K` is an unramified cyclic finite extension of number fields of odd prime degree, then the degree divides the class number of `K`. -/ theorem dvd_card_classGroup_of_isUnramified_isCyclic (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] - [FiniteDimensional K L] [IsGalois K L] [IsUnramified ↥(𝓞 K) ↥(𝓞 L)] [IsCyclic (L ≃ₐ[K] L)] + [FiniteDimensional K L] [IsGalois K L] [IsUnramified (𝓞 K) (𝓞 L)] [IsCyclic (L ≃ₐ[K] L)] (hKL : Nat.Prime (finrank K L)) (hKL' : finrank K L ≠ 2) : - finrank K L ∣ Fintype.card (ClassGroup ↥(𝓞 K)) := by + finrank K L ∣ Fintype.card (ClassGroup (𝓞 K)) := by obtain ⟨I, hI, hI'⟩ := exists_not_isPrincipal_and_isPrincipal_map K L hKL hKL' letI := Fact.mk hKL rw [← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hKL).irreducible.dvd_iff_not_coprime, diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index 19c70a81..2ff25ada 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -12,8 +12,6 @@ variable (hp : p ≠ 2) variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (𝓞 K)ˣ) (hcong : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑u : 𝓞 K) - 1) (hu : ∀ v : K, v ^ (p : ℕ) ≠ u) --- attribute [-instance] instCoeOut - open Polynomial lemma zeta_sub_one_pow_dvd_poly : @@ -75,20 +73,28 @@ lemma map_poly : (poly hp hζ u hcong).map (algebraMap (𝓞 K) K) = have := congr_arg (fun P : (𝓞 K)[X] ↦ (↑(coeff P i) : K)) (poly_spec hp hζ u hcong) change _ = algebraMap (𝓞 K) K _ at this rw [← coeff_map] at this - simp only [coeff_C_mul, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, - Subalgebra.coe_toSubsemiring, SubmonoidClass.coe_pow, AddSubgroupClass.coe_sub, - IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, Polynomial.map_add, Polynomial.map_pow, - Polynomial.map_sub, Polynomial.map_mul, map_C, map_sub, map_one, map_X, Polynomial.map_one, - coeff_add] at this + replace this : (ζ - 1) ^ (p : ℕ) * ↑((poly hp hζ u hcong).coeff i) = + (((C ((algebraMap ((𝓞 K)) K) ↑hζ.unit') - 1) * X - 1) ^ (p : ℕ)).coeff i + + (C ((algebraMap ((𝓞 K)) K) ↑u)).coeff i := by + simp only [map_pow, map_sub, map_one, Polynomial.map_add, Polynomial.map_pow, + Polynomial.map_sub, Polynomial.map_mul, map_C, IsPrimitiveRoot.coe_unit'_coe, + Polynomial.map_one, map_X, coeff_add] at this + convert this + simp only [NumberField.RingOfIntegers.coe_eq_algebraMap, ← Polynomial.coeff_map] + simp only [coeff_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_C, + IsPrimitiveRoot.coe_unit'_coe, Polynomial.map_one] + rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm] + simp apply mul_right_injective₀ (pow_ne_zero p (hζ.sub_one_ne_zero hpri.out.one_lt)) simp only [Subalgebra.algebraMap_eq, Algebra.id.map_eq_id, RingHomCompTriple.comp_eq, coeff_map, RingHom.coe_coe, Subalgebra.coe_val, one_div, map_sub, map_one, coeff_add, coeff_sub, - PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe] + PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe, + IsPrimitiveRoot.coe_unit'_coe] simp_rw [← smul_eq_mul K, ← coeff_smul] rw [smul_C, smul_eq_mul, ← smul_pow, ← mul_div_assoc, mul_div_cancel_left₀, smul_sub, smul_C, smul_eq_mul, mul_inv_cancel, map_one, Algebra.smul_def, ← C_eq_algebraMap, map_sub, map_one] - exact hζ.sub_one_ne_zero hpri.out.one_lt - exact pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt) + · exact hζ.sub_one_ne_zero hpri.out.one_lt + · exact pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt) lemma irreducible_map_poly : Irreducible ((poly hp hζ u hcong).map (algebraMap (𝓞 K) K)) := by @@ -110,8 +116,11 @@ theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L) rw [map_sub, map_one] have := congr_arg (aeval ((1 - ζ ^ m • α) / (algebraMap K L (ζ - 1)))) (poly_spec hp hζ u hcong) + -- also add to mathlib + have hcoe : (algebraMap (𝓞 K) L) (↑hζ.unit') = algebraMap K L ζ := rfl + have hcoe1 : (algebraMap (𝓞 K) L) ↑u = algebraMap K L ↑↑u := rfl simp only [map_sub, map_one, map_pow, map_mul, aeval_C, Subalgebra.algebraMap_eq, smul_pow, - RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e, + hcoe, RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e, hcoe1, IsPrimitiveRoot.val_unit'_coe, map_add, aeval_X, ← mul_div_assoc, mul_div_cancel_left₀ _ hζ', sub_sub_cancel_left, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow] at this rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul, add_left_neg, @@ -236,10 +245,9 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L) · rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow] · rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow] · exact mt (hζ.unit'_coe.injOn_pow hj hi) hij.symm - apply_fun Subtype.val at hv - simp only [Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, - AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, - SubmonoidClass.coe_pow] at hv + rw [NumberField.RingOfIntegers.ext_iff] at hv + have hcoe : (algebraMap (𝓞 K) K) (↑hζ.unit') = ζ := rfl + simp only [map_mul, map_sub, IsPrimitiveRoot.val_unit'_coe, map_one, map_pow, hcoe] at hv have hα : IsIntegral (𝓞 K) α := by apply IsIntegral.of_pow p.pos; rw [e]; exact isIntegral_algebraMap have : IsUnit (⟨α, isIntegral_trans (IsIntegralClosure.isIntegral_algebra ℤ K) _ hα⟩ : 𝓞 L) := by @@ -248,9 +256,8 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L) ext; simp only [SubmonoidClass.coe_pow, e]; rfl convert ((algebraMap (𝓞 K) (𝓞 L)).isUnit_map v.isUnit).mul this using 1 ext - simp only [polyRoot, map_sub, map_one, sub_div, one_div, AddSubgroupClass.coe_sub, - sub_sub_sub_cancel_left, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, - Subalgebra.coe_toSubsemiring] + simp only [polyRoot, map_sub, map_one, sub_div, one_div, map_sub, + sub_sub_sub_cancel_left, map_mul, NumberField.RingOfIntegers.map_mk] rw [← sub_div, ← sub_smul, ← hv, Algebra.smul_def, map_mul, map_sub, map_one, mul_assoc, mul_div_cancel_left₀ _ hζ'] rfl @@ -281,7 +288,8 @@ lemma polyRoot_spec {L : Type*} [Field L] [Algebra K L] (α : L) (e : α ^ (p : ℕ) = algebraMap K L u) (i) : α = (ζ ^ i)⁻¹ • (1 - (ζ - 1) • (polyRoot hp hζ u hcong α e i : L)) := by apply smul_right_injective (M := L) (c := ζ ^ i) (pow_ne_zero _ <| hζ.ne_zero p.pos.ne.symm) - simp only [polyRoot, map_sub, map_one, Algebra.smul_def (ζ - 1), ← mul_div_assoc, + simp only [polyRoot, map_sub, map_one, NumberField.RingOfIntegers.map_mk, + Algebra.smul_def (ζ - 1), ← mul_div_assoc, mul_div_cancel_left₀ _ ((hζ.map_of_injective (algebraMap K L).injective).sub_one_ne_zero hpri.out.one_lt), sub_sub_cancel, smul_smul, inv_mul_cancel (pow_ne_zero _ <| hζ.ne_zero p.pos.ne.symm), one_smul] diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean index 26466502..c1ac34fc 100644 --- a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean +++ b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean @@ -80,7 +80,8 @@ theorem eq_pow_prime_of_unit_of_congruent (u : (𝓞 K)ˣ) obtain ⟨v, hv⟩ := this have hv' : IsIntegral ℤ v · apply IsIntegral.of_pow p.pos; rw [hv]; exact NumberField.RingOfIntegers.isIntegral_coe _ - have : IsUnit (⟨v, hv'⟩ : 𝓞 K) + set w : 𝓞 K := ⟨v, hv'⟩ + have : IsUnit w · rw [← isUnit_pow_iff p.pos.ne.symm]; convert (u ^ (p - 1 : ℕ) : (𝓞 K)ˣ).isUnit; ext; exact hv have hv'' : this.unit ^ (p : ℕ) = u ^ (p - 1 : ℕ) · ext; simpa only [Units.val_pow_eq_pow_val, IsUnit.unit_spec, SubmonoidClass.coe_pow] using hv diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean index 5b48bba5..381f9f75 100644 --- a/FltRegular/NumberTheory/Unramified.lean +++ b/FltRegular/NumberTheory/Unramified.lean @@ -164,7 +164,6 @@ lemma isUnramifiedAt_iff_SquareFree_minpoly_powerBasis [NoZeroSMulDivisors R S] open nonZeroDivisors Polynomial -set_option synthInstance.maxHeartbeats 40000 in attribute [local instance] Ideal.Quotient.field in lemma isUnramifiedAt_of_Separable_minpoly' [IsSeparable K L] (p : Ideal R) [hp : p.IsPrime] (hpbot : p ≠ ⊥) (x : S) diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean index 2be44e54..9271cefc 100644 --- a/FltRegular/ReadyForMathlib/PowerBasis.lean +++ b/FltRegular/ReadyForMathlib/PowerBasis.lean @@ -47,13 +47,6 @@ variable [NumberField K] {pb} variable (hpr : Prime (norm ℚ pb.gen)) -theorem gen_ne_zero : pb.gen ≠ 0 := by - intro h - simp only [norm, MonoidHom.restrict_apply, MonoidHom.codRestrict_apply, - Algebra.norm_eq_zero_iff.2 (show (pb.gen : K) = 0 by exact_mod_cast h)] at hpr - apply Prime.ne_zero hpr - rfl - theorem quotient_not_trivial : Nontrivial ((𝓞 K) ⧸ span ({pb.gen} : Set (𝓞 K))) := Quotient.nontrivial fun h => hpr.not_unit ((isUnit_norm ℚ).2 (span_singleton_eq_top.1 h)) diff --git a/lake-manifest.json b/lake-manifest.json index 648a1159..ea156e1b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "3025cb124492b423070f20cf0a70636f757d117f", + "rev": "789020bc2f7fbc330e33818075a94381da04de4e", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,16 +49,16 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "188eb34fcf1125e89d651ad462d02598219718ca", + "rev": "7cec59317b9e4f2abbacb986c904614a113e8507", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "4e159e0ef38e6e7894342429440ec9b4f5011bfd", + "rev": "e5ecd7db552e15fba586004770f6b280bbb77e65", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,