From fa964a61eb9c04d312a5f6e3930d33287259a99a Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Wed, 3 Jul 2024 12:07:19 +0200 Subject: [PATCH] clean more stuff --- FltRegular/CaseII/InductionStep.lean | 8 -------- .../Cyclotomic/GaloisActionOnCyclo.lean | 6 ------ .../NumberTheory/Cyclotomic/MoreLemmas.lean | 9 +-------- .../NumberTheory/Cyclotomic/UnitLemmas.lean | 20 ------------------- .../NumberTheory/KummersLemma/Field.lean | 8 -------- FltRegular/NumberTheory/SystemOfUnits.lean | 20 ------------------- FltRegular/ReadyForMathlib/PowerBasis.lean | 9 --------- 7 files changed, 1 insertion(+), 79 deletions(-) diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean index a587b87d..68008436 100644 --- a/FltRegular/CaseII/InductionStep.lean +++ b/FltRegular/CaseII/InductionStep.lean @@ -121,14 +121,6 @@ lemma div_zeta_sub_one_Bijective : Ideal.absNorm_span_singleton, norm_Int_zeta_sub_one hζ hp] rfl -/- if the image of one of the elements is zero then the corresponding x+yη is divisible by π^2-/ -lemma div_zeta_sub_one_eq_zero_iff (η) : - Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η) = 0 ↔ π ^ 2 ∣ x + y * η := by - letI := IsCyclotomicExtension.numberField {p} ℚ K - rw [Ideal.Quotient.eq_zero_iff_dvd, pow_two, - ← div_zeta_sub_one_mul_zeta_sub_one hp hζ e, - mul_dvd_mul_iff_right (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)] - /- the gcd of x y called 𝔪 is coprime to 𝔭-/ lemma gcd_zeta_sub_one_eq_one : gcd 𝔪 𝔭 = 1 := by have : Fact (Nat.Prime p) := hpri diff --git a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean index 23a9c054..14ffb1c5 100644 --- a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean +++ b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean @@ -78,12 +78,6 @@ theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K refine' Complex.norm_eq_one_of_pow_eq_one _ p.ne_zero rw [← map_pow, hζ.pow_eq_one, map_one] --- this proof makes me happy inside -theorem galConj_idempotent : (galConj K p).trans (galConj K p) = AlgEquiv.refl := - by - rw [← AlgEquiv.aut_mul, galConj, ← map_mul, neg_one_mul, neg_neg, map_one] - rfl - variable (p) --generalize this diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index 737c0b18..2b41e0c4 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -33,15 +33,12 @@ lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) - apply RingHom.injective_int (algebraMap ℤ ℚ) simp [Algebra.coe_norm_int, hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp] -@[simp] -lemma PNat.coe_two : (2 : ℕ+) = (2 : ℕ) := rfl - lemma surjective_of_isCyclotomicExtension_two (R S) [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [IsCyclotomicExtension {2} R S] : Function.Surjective (algebraMap R S) := by intro x have := IsCyclotomicExtension.adjoin_roots (S := {2}) (A := R) (B := S) x - simp only [Set.mem_singleton_iff, exists_eq_left, sq_eq_one_iff, PNat.coe_two] at this + simp only [Set.mem_singleton_iff, exists_eq_left, sq_eq_one_iff, PNat.val_ofNat] at this have H : Algebra.adjoin R {b : S | b = 1 ∨ b = -1} ≤ ⊥ := by rw [Algebra.adjoin_le_iff] rintro _ (rfl|rfl) @@ -134,10 +131,6 @@ theorem prime_isUnit_mul {a b : α} (h : IsUnit a) : Prime (a * b) ↔ Prime b : theorem prime_mul_units (a : αˣ) (b : α) : Prime (b * ↑a) ↔ Prime b := by simp [Prime] -theorem prime_mul_isUnit {a b : α} (h : IsUnit a) : Prime (b * a) ↔ Prime b := - let ⟨a, ha⟩ := h - ha ▸ prime_mul_units a b - theorem prime_neg_iff {α} [CommRing α] {a : α} : Prime (-a) ↔ Prime a := by rw [← prime_isUnit_mul isUnit_one.neg, neg_mul, one_mul, neg_neg] diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean index c7c41c20..9fafdb15 100644 --- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean @@ -67,14 +67,6 @@ theorem IsPrimitiveRoot.unit'_coe : IsPrimitiveRoot (hζ.unit' : R) p := by rw [← this] at z1 exact z1.of_map_of_injective (IsFractionRing.injective _ _) -variable (p) - -/-- `is_gal_conj_real x` means that `x` is real. -/ -def IsGalConjReal (x : K) [IsCyclotomicExtension {p} ℚ K] : Prop := - galConj K p x = x - -variable {p} - theorem contains_two_primitive_roots {p q : ℕ} {x y : K} [FiniteDimensional ℚ K] (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q) : (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K := by @@ -307,11 +299,6 @@ theorem IsPrimitiveRoot.two_not_mem_one_sub_zeta [hp : Fact (p : ℕ).Prime] (h rw [sub_eq_of_eq_add hk] at this exact hζ.isPrime_one_sub_zeta.ne_top (Ideal.eq_top_of_isUnit_mem I this isUnit_one) -lemma IsUnit.eq_mul_left_iff {S : Type*} [CommRing S] {x : S} (hx : IsUnit x) (y : S) : - x = y * x ↔ y = 1 := by - nth_rw 1 [← one_mul x] - rw [eq_comm, hx.mul_left_injective.eq_iff] - lemma map_two {S T F: Type*} [NonAssocSemiring S] [NonAssocSemiring T] [FunLike F S T] [RingHomClass F S T] (f : F) : f 2 = 2 := by rw [← one_add_one_eq_two, map_add, map_one] @@ -403,13 +390,6 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : · exact NumberField.RingOfIntegers.isIntegral_coe _ · exact unit_lemma_val_one p u -lemma inv_coe_coe {K A : Type*} [Field K] [SetLike A K] [SubsemiringClass A K] {S : A} (s : Sˣ) : - (s : K)⁻¹ = ((s⁻¹ : Sˣ) : K) := by - apply inv_eq_of_mul_eq_one_right - change ((s * s⁻¹ : Sˣ) : K) = 1 - rw [mul_inv_self] - rfl - 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/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index a8173956..6e74cd6b 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -222,14 +222,6 @@ lemma minpoly_polyRoot' {L : Type*} [Field L] [Algebra K L] (α : L) exact minpoly_polyRoot'' hp hζ u hcong hu α e i exact IsIntegral.tower_top (polyRoot hp hζ u hcong α e i).prop -lemma minpoly_polyRoot {L : Type*} [Field L] [Algebra K L] (α : L) - (e : α ^ (p : ℕ) = algebraMap K L u) (i) : - minpoly (𝓞 K) (polyRoot hp hζ u hcong α e i) = (poly hp hζ u hcong) := by - apply map_injective (algebraMap (𝓞 K) K) Subtype.coe_injective - rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L] - exact minpoly_polyRoot'' hp hζ u hcong hu α e i - exact IsIntegralClosure.isIntegral _ L (polyRoot hp hζ u hcong α e i) - lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L) (e : α ^ (p : ℕ) = algebraMap K L u) : Separable ((poly hp hζ u hcong).map (algebraMap (𝓞 K) (𝓞 L))) := by diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean index 31238c82..d6de2d14 100644 --- a/FltRegular/NumberTheory/SystemOfUnits.lean +++ b/FltRegular/NumberTheory/SystemOfUnits.lean @@ -35,29 +35,9 @@ structure systemOfUnits (r : ℕ) namespace systemOfUnits -lemma nontrivial (hr : r ≠ 0) : Nontrivial G := by - by_contra! h - rw [not_nontrivial_iff_subsingleton] at h - rw [FiniteDimensional.finrank_zero_of_subsingleton] at hf - simp only [ge_iff_le, zero_eq_mul, tsub_eq_zero_iff_le] at hf - cases hf with - | inl h => exact hr h - | inr h => simpa [Nat.lt_succ_iff, h] using not_lt.2 (Nat.prime_def_lt.1 hp).1 - lemma existence0 : Nonempty (systemOfUnits p G 0) := by exact ⟨⟨fun _ => 0, linearIndependent_empty_type⟩⟩ -lemma spanA_eq_spanZ {R : ℕ} (f : Fin R → G) : - (Submodule.span A (Set.range f)).restrictScalars ℤ = Submodule.span ℤ - (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1)) := by - letI := Fact.mk hp - rw [← Submodule.span_smul_of_span_eq_top (CyclotomicIntegers.powerBasis p).basis.span_eq, - Set.range_smul_range] - congr - ext - simp only [PowerBasis.coe_basis, CyclotomicIntegers.powerBasis_gen, Set.mem_range, Prod.exists] - rw [exists_comm, CyclotomicIntegers.powerBasis_dim] - theorem _root_.PowerBasis.finrank' {R S} [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) : FiniteDimensional.finrank R S = pb.dim := by rw [FiniteDimensional.finrank_eq_card_basis pb.basis, Fintype.card_fin] diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean index 745c2d21..0294c360 100644 --- a/FltRegular/ReadyForMathlib/PowerBasis.lean +++ b/FltRegular/ReadyForMathlib/PowerBasis.lean @@ -47,19 +47,10 @@ variable [NumberField K] {pb} variable (hpr : Prime (norm ℚ pb.gen)) -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)) - lemma SModEq.Ideal_def {R : Type*} [CommRing R] (I : Ideal R) (x y : R) : x ≡ y [SMOD I] ↔ Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := Iff.rfl -instance {K : Type*} [Field K] [NumberField K] : - Module (𝓞 ℚ) (𝓞 K) := Algebra.toModule - -instance {K : Type*} [Field K] [NumberField K] : - SMul (𝓞 ℚ) (𝓞 K) := Algebra.toSMul - lemma norm_intCast {K : Type*} [Field K] [NumberField K] (n : ℤ) : norm ℚ (n : 𝓞 K) = n ^ (finrank ℚ K) := by rw [← eq_intCast (algebraMap ℤ (𝓞 K)) n, IsScalarTower.algebraMap_apply ℤ (𝓞 ℚ) (𝓞 K)]