From 3a970be81784892ba5f0556b0aaa04f1ee803bcc Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Mon, 18 Dec 2023 10:56:45 +0100 Subject: [PATCH] wip --- FltRegular/FltThree/FltThree.lean | 2 +- FltRegular/FltThree/Primes.lean | 3 +- FltRegular/FltThree/Spts.lean | 10 +- FltRegular/NumberTheory/AuxLemmas.lean | 21 -- FltRegular/NumberTheory/CyclotomicRing.lean | 5 - FltRegular/NumberTheory/Different.lean | 53 +++-- FltRegular/NumberTheory/Hilbert90.lean | 8 +- FltRegular/NumberTheory/Hilbert92.lean | 15 +- FltRegular/NumberTheory/KummerExtension.lean | 2 +- FltRegular/NumberTheory/MinpolyDiv.lean | 235 ------------------- lake-manifest.json | 4 +- 11 files changed, 49 insertions(+), 309 deletions(-) delete mode 100644 FltRegular/NumberTheory/MinpolyDiv.lean diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean index ad6122e4..198bddab 100644 --- a/FltRegular/FltThree/FltThree.lean +++ b/FltRegular/FltThree/FltThree.lean @@ -686,7 +686,7 @@ theorem descent (a b c : ℤ) (h : FltCoprime 3 a b c) : by obtain ⟨a', b', c', ha', hb', hc', hsmaller, hsolution⟩ := this refine' ⟨a', b', c', ha', hb', hc', _, hsolution⟩ - rw [← Nat.pow_lt_iff_lt_left (by norm_num : 1 ≤ 3)] + rw [← Nat.pow_lt_pow_iff_left three_ne_zero] convert lt_of_le_of_lt hsmaller haaa <;> simp [mul_pow, Int.natAbs_mul, Int.natAbs_pow] -- 4. cases' gcd1or3 p q hp hcoprime hodd with hgcd hgcd diff --git a/FltRegular/FltThree/Primes.lean b/FltRegular/FltThree/Primes.lean index b1d76053..c04455f4 100644 --- a/FltRegular/FltThree/Primes.lean +++ b/FltRegular/FltThree/Primes.lean @@ -46,8 +46,7 @@ theorem Int.factor_div (a x : ℤ) (hodd : Odd x) : exact ⟨_, heqtwomul⟩ theorem two_not_cube (r : ℕ) : r ^ 3 ≠ 2 :=by - have : 1 ≤ 3 := by norm_num - apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono this).monotone 1 <;> norm_num + apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono three_ne_zero).monotone 1 <;> norm_num namespace Mathlib open Lean hiding Rat mkRat diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean index 461561df..2698d042 100644 --- a/FltRegular/FltThree/Spts.lean +++ b/FltRegular/FltThree/Spts.lean @@ -204,11 +204,11 @@ theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) : · rw [mul_pow, ← Int.natAbs_pow_two c, ← Int.natAbs_pow_two x, ← mul_pow] norm_cast - exact Nat.pow_lt_pow_of_lt_left hc zero_lt_two + exact Nat.pow_lt_pow_left hc two_ne_zero · rw [mul_pow, ← Int.natAbs_pow_two d, ← Int.natAbs_pow_two x, ← mul_pow, mul_lt_mul_left (by norm_num : (0 : ℤ) < 3)] norm_cast - exact Nat.pow_lt_pow_of_lt_left hd zero_lt_two + exact Nat.pow_lt_pow_left hd two_ne_zero theorem Zqrtd.factor_div' (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) (h : 1 < |x|) (hcoprime : IsCoprime a.re a.im) (hfactor : x ∣ a.norm) : @@ -326,13 +326,13 @@ theorem Spts.eq_one {a : ℤ√(-3)} (h : a.norm = 1) : abs a.re = 1 ∧ a.im = · have : 1 ≤ abs a.im := by rwa [← Int.abs_lt_one_iff, not_lt] at hb have : 1 ≤ a.im ^ 2 := by rw [← sq_abs] - exact pow_le_pow_of_le_left zero_le_one this 2 + exact pow_le_pow_left zero_le_one this 2 linarith · apply ne_of_gt rw [Zsqrtd.norm_def, neg_mul, neg_mul, sub_neg_eq_add] apply lt_add_of_lt_of_nonneg · rw [← sq, ← sq_abs] - exact pow_lt_pow_of_lt_left H zero_le_one zero_lt_two + exact pow_lt_pow_left H zero_le_one two_ne_zero · rw [mul_assoc] exact mul_nonneg zero_lt_three.le (mul_self_nonneg _) @@ -371,7 +371,7 @@ theorem Spts.not_two (a : ℤ√(-3)) : a.norm ≠ 2 := obtain him | him := eq_or_ne a.im 0 · rw [him, MulZeroClass.mul_zero, sub_zero, ← Int.natAbs_mul_self, ← sq] norm_cast - apply (Nat.pow_left_strictMono one_le_two).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num + apply (Nat.pow_left_strictMono two_ne_zero).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num · apply ne_of_gt apply lt_add_of_nonneg_of_lt (mul_self_nonneg a.re) rw [← Int.add_one_le_iff] diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index 260bd795..141a75eb 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -567,27 +567,6 @@ theorem span_range_natDegree_eq_adjoin {R A} [CommRing R] [CommRing A] [Algebra rw [Finset.mem_range] exact (le_natDegree_of_mem_supp _ hkq).trans_lt this --- Mathlib/Data/Polynomial/RingDivision.lean -open Polynomial BigOperators in -lemma Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R} [CommRing R] [IsDomain R] - (p : R[X]) {ι} [Fintype ι] {f : ι → R} (hf : Function.Injective f) - (heval : ∀ i, p.eval (f i) = 0) (hcard : natDegree p < Fintype.card ι) : p = 0 := by - classical - by_contra hp - apply not_lt_of_le (le_refl (Finset.card p.roots.toFinset)) - calc - Finset.card p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _ - _ ≤ natDegree p := Polynomial.card_roots' p - _ < Fintype.card ι := hcard - _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm - _ = Finset.card (Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range] - _ ≤ Finset.card p.roots.toFinset := Finset.card_mono ?_ - intro _ - simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq, - IsRoot.def, forall_exists_index, hp, not_false_eq_true] - rintro x rfl - exact heval _ - -- Dunno. Somewhere near Mathlib/FieldTheory/Minpoly/Basic.lean. lemma aeval_derivative_minpoly_ne_zero {K L} [CommRing K] [CommRing L] [Algebra K L] (x : L) (hx : (minpoly K x).Separable) [Nontrivial L] : diff --git a/FltRegular/NumberTheory/CyclotomicRing.lean b/FltRegular/NumberTheory/CyclotomicRing.lean index 010994f6..2c9161cf 100644 --- a/FltRegular/NumberTheory/CyclotomicRing.lean +++ b/FltRegular/NumberTheory/CyclotomicRing.lean @@ -30,11 +30,6 @@ def AdjoinRoot.equivOfMinpolyEq {R S} [CommRing R] [CommRing S] [Algebra R S] (P : R[X]) (pb : PowerBasis R S) (hpb : minpoly R pb.gen = P) : AdjoinRoot P ≃ₐ[R] S := AdjoinRoot.equiv' P pb (hpb ▸ aeval_root _) (hpb ▸ minpoly.aeval _ _) -theorem map_dvd_iff {M N} [Monoid M] [Monoid N] {F : Type*} [MulEquivClass F M N] (f : F) {a b} : - f a ∣ f b ↔ a ∣ b := by - refine ⟨?_, map_dvd f⟩ - convert _root_.map_dvd (f : M ≃* N).symm <;> exact ((f : M ≃* N).symm_apply_apply _).symm - namespace CyclotomicIntegers @[simps! (config := .lemmasOnly)] diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean index 68e92c49..6df9b35c 100644 --- a/FltRegular/NumberTheory/Different.lean +++ b/FltRegular/NumberTheory/Different.lean @@ -1,7 +1,7 @@ +import Mathlib.RingTheory.DedekindDomain.Different import Mathlib.RingTheory.DedekindDomain.Ideal import Mathlib.RingTheory.Discriminant import Mathlib.RingTheory.Localization.FractionRing -import FltRegular.NumberTheory.MinpolyDiv import FltRegular.NumberTheory.QuotientTrace import Mathlib.NumberTheory.KummerDedekind /-! @@ -134,7 +134,8 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule variable (A K) -def FractionalIdeal.dual (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) : +-- TODO: merge with FractionalIdeal.dual +def FractionalIdeal.dual₂ (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) : FractionalIdeal B⁰ L := ⟨traceFormDualSubmodule A K I, by classical @@ -155,13 +156,13 @@ def FractionalIdeal.dual (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) : variable {A K} -lemma FractionalIdeal.mem_dual {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} {x} : - x ∈ dual A K I hI ↔ ∀ a ∈ I, Algebra.traceForm K L x a ∈ (algebraMap A K).range := Iff.rfl +lemma FractionalIdeal.mem_dual₂ {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} {x} : + x ∈ dual₂ A K I hI ↔ ∀ a ∈ I, Algebra.traceForm K L x a ∈ (algebraMap A K).range := Iff.rfl -lemma FractionalIdeal.dual_ne_zero {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} : - dual A K I hI ≠ 0 := by +lemma FractionalIdeal.dual₂_ne_zero {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} : + dual₂ A K I hI ≠ 0 := by obtain ⟨b, hb, hb'⟩ := I.prop - suffices algebraMap B L b ∈ dual A K I hI by + suffices algebraMap B L b ∈ dual₂ A K I hI by intro e rw [e, mem_zero_iff, ← (algebraMap B L).map_zero, (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this @@ -175,8 +176,8 @@ lemma FractionalIdeal.dual_ne_zero {I : FractionalIdeal B⁰ L} {hI : I ≠ 0} : exact IsIntegralClosure.isIntegral_iff (A := B) · exact (Algebra.smul_def _ _).symm -lemma FractionalIdeal.le_dual_inv_aux (I J: FractionalIdeal B⁰ L) (hI) (hIJ : I * J ≤ 1) : - J ≤ dual A K I hI := by +lemma FractionalIdeal.le_dual₂_inv_aux (I J: FractionalIdeal B⁰ L) (hI) (hIJ : I * J ≤ 1) : + J ≤ dual₂ A K I hI := by intro x hx y hy apply IsIntegrallyClosed.isIntegral_iff.mp apply isIntegral_trace @@ -189,16 +190,16 @@ variable [IsDedekindDomain B] [IsFractionRing B L] variable (A K) -lemma FractionalIdeal.inv_le_dual (I : FractionalIdeal B⁰ L) (hI) : - I⁻¹ ≤ dual A K I hI := - le_dual_inv_aux _ _ _ (le_of_eq (mul_inv_cancel hI)) +lemma FractionalIdeal.inv_le_dual₂ (I : FractionalIdeal B⁰ L) (hI) : + I⁻¹ ≤ dual₂ A K I hI := + le_dual₂_inv_aux _ _ _ (le_of_eq (mul_inv_cancel hI)) -lemma FractionalIdeal.dual_inv_le (I : FractionalIdeal B⁰ L) (hI) : - (dual A K I hI)⁻¹ ≤ I := by - convert mul_right_mono ((dual A K I hI)⁻¹) - (mul_left_mono I (FractionalIdeal.inv_le_dual A K I hI)) using 1 +lemma FractionalIdeal.dual₂_inv_le (I : FractionalIdeal B⁰ L) (hI) : + (dual₂ A K I hI)⁻¹ ≤ I := by + convert mul_right_mono ((dual₂ A K I hI)⁻¹) + (mul_left_mono I (FractionalIdeal.inv_le_dual₂ A K I hI)) using 1 · simp only [mul_inv_cancel hI, one_mul] - · simp only [mul_inv_cancel (FractionalIdeal.dual_ne_zero (hI := hI)), mul_assoc, mul_one] + · simp only [mul_inv_cancel (FractionalIdeal.dual₂_ne_zero (hI := hI)), mul_assoc, mul_one] variable (B) @@ -214,12 +215,12 @@ lemma coeSubmodule_differentIdeal' [NoZeroSMulDivisors A B] (hAB : Algebra.IsInt have : IsIntegralClosure B A (FractionRing B) := isIntegralClosure_of_isIntegrallyClosed _ _ _ hAB rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right] - have := FractionalIdeal.dual_inv_le A (FractionRing A) (1 : FractionalIdeal B⁰ (FractionRing B)) + have := FractionalIdeal.dual₂_inv_le A (FractionRing A) (1 : FractionalIdeal B⁰ (FractionRing B)) one_ne_zero have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this simp only [← one_div, FractionalIdeal.val_eq_coe, - FractionalIdeal.coe_div FractionalIdeal.dual_ne_zero] at this - dsimp [FractionalIdeal.dual] at this + FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero] at this + dsimp [FractionalIdeal.dual₂] at this simpa only [FractionalIdeal.coe_one] using this lemma coeSubmodule_differentIdeal [NoZeroSMulDivisors A B] : @@ -251,17 +252,17 @@ variable (L) lemma coeIdeal_different_ideal [NoZeroSMulDivisors A B] : ↑(differentIdeal A B) = - (FractionalIdeal.dual A K (1 : FractionalIdeal B⁰ L) one_ne_zero)⁻¹ := by + (FractionalIdeal.dual₂ A K (1 : FractionalIdeal B⁰ L) one_ne_zero)⁻¹ := by apply FractionalIdeal.coeToSubmodule_injective - simp only [FractionalIdeal.coe_div FractionalIdeal.dual_ne_zero, + simp only [FractionalIdeal.coe_div FractionalIdeal.dual₂_ne_zero, FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal A K, inv_eq_one_div] - simp only [FractionalIdeal.dual, FractionalIdeal.coe_mk, FractionalIdeal.coe_one] + simp only [FractionalIdeal.dual₂, FractionalIdeal.coe_mk, FractionalIdeal.coe_one] lemma differentialIdeal_le_fractionalIdeal_iff (I : FractionalIdeal B⁰ L) (hI : I ≠ 0) [NoZeroSMulDivisors A B] : differentIdeal A B ≤ I ↔ (((I⁻¹ : _) : Submodule B L).restrictScalars A).map ((Algebra.trace K L).restrictScalars A) ≤ 1 := by - rw [coeIdeal_different_ideal A K B L, FractionalIdeal.inv_le_comm FractionalIdeal.dual_ne_zero hI] + rw [coeIdeal_different_ideal A K B L, FractionalIdeal.inv_le_comm FractionalIdeal.dual₂_ne_zero hI] refine le_traceFormDualSubmodule.trans ?_ simp @@ -415,7 +416,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] apply FractionalIdeal.coeIdeal_injective (K := L) simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton] rw [coeIdeal_different_ideal A K B L, - mul_inv_eq_iff_eq_mul₀ FractionalIdeal.dual_ne_zero] + mul_inv_eq_iff_eq_mul₀ FractionalIdeal.dual₂_ne_zero] apply FractionalIdeal.coeToSubmodule_injective simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul, FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_mul] @@ -425,7 +426,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0 · rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁ - rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual, + rw [Submodule.mem_smul_iff_inv this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual₂, mem_coeIdeal_conductor] have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 · rwa [ne_eq, inv_eq_zero] diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean index 0df2fc68..aa4846bf 100644 --- a/FltRegular/NumberTheory/Hilbert90.lean +++ b/FltRegular/NumberTheory/Hilbert90.lean @@ -17,12 +17,12 @@ noncomputable def ηu : Lˣ := (Ne.isUnit (fun h ↦ by simp [h] at hη) : IsUnit η).unit noncomputable -def φ := (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm +def φ := (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm variable {σ} lemma hφ : ∀ (n : ℕ), φ σ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n ↦ by - simpa [Fin.ext_iff] using finEquivZpowers_symm_apply _ (isOfFinOrder_of_finite σ) n + simpa [Fin.ext_iff] using finEquivZPowers_symm_apply _ (isOfFinOrder_of_finite σ) n noncomputable def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ σ ⟨τ, hσ τ⟩), Units.map (σ ^ i) (ηu hη) @@ -45,8 +45,8 @@ lemma foo {a: ℕ} (h : a % orderOf σ = 0) : (fun a b ha hb hab ↦ ?_) (fun τ _ ↦ ?_) · rwa [pow_inj_mod, Nat.mod_eq_of_lt (Finset.mem_range.1 ha), Nat.mod_eq_of_lt (Finset.mem_range.1 hb)] at hab - · refine ⟨(finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩, by simp, ?_⟩ - have := Equiv.symm_apply_apply (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩ + · refine ⟨(finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩, by simp, ?_⟩ + have := Equiv.symm_apply_apply (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩ simp only [SetLike.coe_sort_coe, Equiv.symm_symm, ← Subtype.coe_inj] at this ⊢ rw [← this] simp only [SetLike.coe_sort_coe, Subtype.coe_eta, Equiv.symm_apply_apply] diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 0b0da174..a8b027e2 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -301,9 +301,10 @@ def Group.forall_mem_zpowers_iff {H} [Group H] {x : H} : rw [SetLike.ext_iff] simp only [Subgroup.mem_top, iff_true] -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) +-- TODO move +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) open Polynomial in lemma isTors' : Module.IsTorsionBySet ℤ[X] @@ -336,8 +337,8 @@ lemma isTors' : Module.IsTorsionBySet ℤ[X] 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] - simp only [pow_finEquivZpowers_symm_apply, coe_galRestrictHom_apply, AlgHom.coe_coe] + ← 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] rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i ↑x) (Subgroup.zpowers σ)] congr ext x @@ -751,8 +752,8 @@ lemma norm_eq_prod_pow_gen (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (η : K) : algebraMap k K (Algebra.norm k η) = (∏ i in Finset.range (orderOf σ), (σ ^ i) η) := by rw [Algebra.norm_eq_prod_automorphisms, ← Fin.prod_univ_eq_prod_range, - ← (finEquivZpowers σ <| isOfFinOrder_of_finite _).symm.prod_comp] - simp only [pow_finEquivZpowers_symm_apply] + ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp] + simp only [pow_finEquivZPowers_symm_apply] rw [Finset.prod_set_coe (α := K ≃ₐ[k] K) (β := K) (f := fun i ↦ i η) (Subgroup.zpowers σ)] congr; ext; simp [hσ] diff --git a/FltRegular/NumberTheory/KummerExtension.lean b/FltRegular/NumberTheory/KummerExtension.lean index 97a1d050..ae780af0 100644 --- a/FltRegular/NumberTheory/KummerExtension.lean +++ b/FltRegular/NumberTheory/KummerExtension.lean @@ -388,7 +388,7 @@ def autEquivZmod {ζ : K} (hζ : IsPrimitiveRoot ζ n) : (autEquivRootsOfUnity ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hn).trans ((MulEquiv.subgroupCongr (IsPrimitiveRoot.zpowers_eq (k := ⟨n, hn⟩) (hζ.isUnit_unit' hn)).symm).trans (AddEquiv.toMultiplicative' - (hζ.isUnit_unit' hn).zmodEquivZpowers.symm)) + (hζ.isUnit_unit' hn).zmodEquivZPowers.symm)) lemma MulEquiv.subgroupCongr_apply {G} [Group G] {H₁ H₂ : Subgroup G} (e : H₁ = H₂) (x) : (MulEquiv.subgroupCongr e x : G) = x := rfl diff --git a/FltRegular/NumberTheory/MinpolyDiv.lean b/FltRegular/NumberTheory/MinpolyDiv.lean deleted file mode 100644 index 00e5922c..00000000 --- a/FltRegular/NumberTheory/MinpolyDiv.lean +++ /dev/null @@ -1,235 +0,0 @@ -import Mathlib.RingTheory.DedekindDomain.Ideal -import Mathlib.RingTheory.Discriminant -import Mathlib.RingTheory.Localization.FractionRing -import FltRegular.NumberTheory.AuxLemmas -import FltRegular.NumberTheory.QuotientTrace -import Mathlib.NumberTheory.KummerDedekind - -/-! -# Results about `minpoly R x / (X - C x)` - -## Main definition -- `minpolyDiv`: The polynomial `minpoly R x / (X - C x)`. - -## Main result - -- `span_coeff_minpolyDiv`: The coefficients of `minpolyDiv` spans `R`. -- `traceForm_dualBasis_powerBasis_eq`: The dual basis of a powerbasis under the trace form. - --/ - -open Polynomial BigOperators FiniteDimensional - -variable (R K) {L S} [CommRing R] [Field K] [Field L] [CommRing S] [Algebra R S] [Algebra K L] -variable (x : S) - -noncomputable def minpolyDiv : S[X] := (minpoly R x).map (algebraMap R S) /ₘ (X - C x) - -lemma minpolyDiv_spec : - minpolyDiv R x * (X - C x) = (minpoly R x).map (algebraMap R S) := by - delta minpolyDiv - rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map, ← aeval_def, minpoly.aeval] - -lemma coeff_minpolyDiv (i) : coeff (minpolyDiv R x) i = - algebraMap R S (coeff (minpoly R x) (i + 1)) + coeff (minpolyDiv R x) (i + 1) * x := by - rw [← coeff_map, ← minpolyDiv_spec R x]; simp [mul_sub] - -variable (hx : IsIntegral R x) -variable {R x} - -lemma minpolyDiv_ne_zero [Nontrivial S] : minpolyDiv R x ≠ 0 := by - intro e - have := minpolyDiv_spec R x - rw [e, zero_mul] at this - exact ((minpoly.monic hx).map (algebraMap R S)).ne_zero this.symm - -lemma minpolyDiv_eq_zero (hx : ¬IsIntegral R x) : minpolyDiv R x = 0 := by - delta minpolyDiv minpoly - rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic] - -lemma minpolyDiv_monic : Monic (minpolyDiv R x) := by - nontriviality S - have := congr_arg leadingCoeff (minpolyDiv_spec R x) - rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this - · simpa using this - · simpa using minpolyDiv_ne_zero hx - -lemma eval_minpolyDiv_self : (minpolyDiv R x).eval x = aeval x (derivative <| minpoly R x) := by - rw [aeval_def, ← eval_map, ← derivative_map, ← minpolyDiv_spec R x]; simp - -lemma minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero [IsDomain S] - {y} (hxy : y ≠ x) (hy : aeval y (minpoly R x) = 0) : (minpolyDiv R x).eval y = 0 := by - rw [aeval_def, ← eval_map, ← minpolyDiv_spec R x] at hy - simp only [eval_mul, eval_sub, eval_X, eval_C, mul_eq_zero] at hy - exact hy.resolve_right (by rwa [sub_eq_zero]) - -lemma eval₂_minpolyDiv_of_eval₂_eq_zero {T} [CommRing T] - [IsDomain T] [DecidableEq T] (x : S) (y : T) - (σ : S →+* T) (hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0) : - eval₂ σ y (minpolyDiv R x) = - if σ x = y then σ (aeval x (derivative <| minpoly R x)) else 0 := by - split_ifs with h - · rw [← h, eval₂_hom, eval_minpolyDiv_self] - · rw [← eval₂_map, ← minpolyDiv_spec] at hy - simpa [sub_eq_zero, Ne.symm h] using hy - -lemma eval₂_minpolyDiv_self {T} [CommRing T] [Algebra R T] [IsDomain T] [DecidableEq T] (x : S) - (σ₁ σ₂ : S →ₐ[R] T) : - eval₂ σ₁ (σ₂ x) (minpolyDiv R x) = - if σ₁ x = σ₂ x then σ₁ (aeval x (derivative <| minpoly R x)) else 0 := by - apply eval₂_minpolyDiv_of_eval₂_eq_zero - rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom, - eval_map, ← aeval_def, minpoly.aeval, map_zero] - - -lemma eval_minpolyDiv_of_aeval_eq_zero [IsDomain S] [DecidableEq S] - {y} (hy : aeval y (minpoly R x) = 0) : - (minpolyDiv R x).eval y = if x = y then aeval x (derivative <| minpoly R x) else 0 := by - rw [eval, eval₂_minpolyDiv_of_eval₂_eq_zero]; rfl - exact hy - -lemma natDegree_minpolyDiv_succ [Nontrivial S] : - natDegree (minpolyDiv R x) + 1 = natDegree (minpoly R x) := by - rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul'] - · simp - · simpa using minpolyDiv_ne_zero hx - -lemma natDegree_minpolyDiv : - natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1 := by - nontriviality S - have := (algebraMap R S).domain_nontrivial - by_cases hx : IsIntegral R x - · rw [← natDegree_minpolyDiv_succ hx]; rfl - · rw [minpolyDiv_eq_zero hx, minpoly.eq_zero hx]; rfl - -lemma natDegree_minpolyDiv_lt [Nontrivial S] : - natDegree (minpolyDiv R x) < natDegree (minpoly R x) := by - rw [← natDegree_minpolyDiv_succ hx] - exact Nat.lt.base _ - -lemma coeff_minpolyDiv_mem_adjoin : coeff (minpolyDiv R x) i ∈ Algebra.adjoin R {x} := by - by_contra H - have : ∀ j, coeff (minpolyDiv R x) (i + j) ∉ Algebra.adjoin R {x} - · intro j; induction j with - | zero => exact H - | succ j IH => - intro H; apply IH - rw [coeff_minpolyDiv] - refine add_mem ?_ (mul_mem H (Algebra.self_mem_adjoin_singleton R x)) - exact Subalgebra.algebraMap_mem _ _ - apply this (natDegree (minpolyDiv R x) + 1) - rw [coeff_eq_zero_of_natDegree_lt] - · exact zero_mem _ - · refine (Nat.le_add_left _ i).trans_lt ?_ - rw [← add_assoc] - exact Nat.lt.base _ - -lemma minpolyDiv_eq_of_isIntegrallyClosed [IsDomain R] [IsIntegrallyClosed R] [IsDomain S] - [Algebra R K] [Algebra K S] [IsScalarTower R K S] [IsFractionRing R K] : - minpolyDiv R x = minpolyDiv K x := by - delta minpolyDiv - rw [IsScalarTower.algebraMap_eq R K S, ← map_map, - ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx] - -lemma coeff_minpolyDiv_sub_pow_mem_span (i) (hi : i ≤ natDegree (minpolyDiv R x)) : - coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i ∈ - Submodule.span R ((x ^ ·) '' Set.Iio i) := by - induction i with - | zero => simp [(minpolyDiv_monic hx).leadingCoeff] - | succ i IH => - rw [coeff_minpolyDiv, add_sub_assoc, pow_succ', ← sub_mul, Algebra.algebraMap_eq_smul_one] - refine add_mem ?_ ?_ - · apply Submodule.smul_mem - apply Submodule.subset_span - exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩ - · rw [Nat.succ_eq_add_one, ← tsub_tsub, tsub_add_cancel_of_le - (le_tsub_of_add_le_left (b := 1) hi)] - apply SetLike.le_def.mp ?_ - (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi)) - (Submodule.mem_span_singleton_self x)) - rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image] - apply Submodule.span_mono - rintro _ ⟨j, hj : j < i, rfl⟩ - exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ' x j⟩ - -open Polynomial in -lemma span_coeff_minpolyDiv : - Submodule.span R (Set.range (coeff (minpolyDiv R x))) = - Subalgebra.toSubmodule (Algebra.adjoin R {x}) := by - nontriviality S - classical - apply le_antisymm - · rw [Submodule.span_le] - rintro _ ⟨i, rfl⟩ - apply coeff_minpolyDiv_mem_adjoin - · rw [← span_range_natDegree_eq_adjoin _ hx, Submodule.span_le] - simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff] - intro i - apply Nat.strongInductionOn i - intro i hi hi' - have : coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈ - Submodule.span R (Set.range (coeff (minpolyDiv R x))) := - Submodule.subset_span (Set.mem_range_self _) - rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ this] - refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx i ?_) - · rw [Submodule.span_le, Set.image_subset_iff] - intro j (hj : j < i) - exact hi j hj (lt_trans hj hi') - · rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi' - -section PowerBasis - -variable {K} - -lemma sum_smul_minpolyDiv_eq_X_pow (E) [Field E] [IsAlgClosed E] [Algebra K E] - [FiniteDimensional K L] [IsSeparable K L] - (x : L) (hxL : Algebra.adjoin K {x} = ⊤) (r : ℕ) (hr : r < finrank K L) : - ∑ σ : L →ₐ[K] E, ((x ^ r / aeval x (derivative <| minpoly K x)) • - minpolyDiv K x).map σ = (X ^ r : E[X]) := by - classical - rw [← sub_eq_zero] - have : Function.Injective (fun σ : L →ₐ[K] E ↦ σ x) := fun _ _ h => - AlgHom.ext_of_adjoin_eq_top hxL (fun _ hx ↦ hx ▸ h) - apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this - · intro σ - simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, eval_sub, eval_finset_sum, - eval_smul, eval_map, eval₂_minpolyDiv_self, this.eq_iff, smul_eq_mul, mul_ite, mul_zero, - Finset.sum_ite_eq', Finset.mem_univ, ite_true, eval_pow, eval_X] - rw [sub_eq_zero, div_mul_cancel] - rw [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective] - exact aeval_derivative_minpoly_ne_zero _ (IsSeparable.separable _ _) - · refine (Polynomial.natDegree_sub_le _ _).trans_lt - (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_) - · simp only [AlgEquiv.toAlgHom_eq_coe, Polynomial.map_smul, - map_div₀, map_pow, RingHom.coe_coe, AlgHom.coe_coe, Function.comp_apply, - Finset.mem_univ, forall_true_left, true_and, Finset.fold_max_lt, AlgHom.card] - refine ⟨finrank_pos, ?_⟩ - intro σ - exact ((Polynomial.natDegree_smul_le _ _).trans (natDegree_map_le _ _)).trans_lt - ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.of_finite _ _ x)).trans_le - (minpoly.natDegree_le _)) - · rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card] - -lemma traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [IsSeparable K L] - (pb : PowerBasis K L) (i) : - (Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) pb.basis i = - (minpolyDiv K pb.gen).coeff i / aeval pb.gen (derivative <| minpoly K pb.gen) := by - classical - apply ((Algebra.traceForm K L).toDual (traceForm_nondegenerate K L)).injective - apply pb.basis.ext - intro j - simp only [BilinForm.toDual_def, BilinForm.apply_dualBasis_left] - apply (algebraMap K (AlgebraicClosure K)).injective - have := congr_arg (coeff · i) (sum_smul_minpolyDiv_eq_X_pow (AlgebraicClosure K) - pb.gen pb.adjoin_gen_eq_top j (pb.finrank.symm ▸ j.prop)) - simp only [AlgEquiv.toAlgHom_eq_coe, Polynomial.map_smul, map_div₀, - map_pow, RingHom.coe_coe, AlgHom.coe_coe, finset_sum_coeff, coeff_smul, coeff_map, smul_eq_mul, - coeff_X_pow, ← Fin.ext_iff, @eq_comm _ i] at this - rw [PowerBasis.coe_basis, Algebra.traceForm_apply, RingHom.map_ite_one_zero, - ← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)] - apply Finset.sum_congr rfl - intro σ _ - simp only [_root_.map_mul, map_div₀, map_pow] - ring - -end PowerBasis diff --git a/lake-manifest.json b/lake-manifest.json index 0f472e26..283c739a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "483fd2846f9fe5107011ece0cc3d8d88af1a8603", + "rev": "9dd24a3493cceefa2bede383f21e4ef548990b68", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "d85330ef0bdda6650271c95df08b6bd72a5a6459", + "rev": "d61c95e1653dffe3f92c8927a905826929f50bce", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,