From 669b5af64eb4af8a16feb01799054cdef439a72f Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Wed, 3 Jul 2024 14:21:09 +0200 Subject: [PATCH] remove more stuff --- FltRegular/CaseI/Statement.lean | 5 ++-- FltRegular/CaseII/InductionStep.lean | 7 ++--- FltRegular/NumberTheory/Cyclotomic/CaseI.lean | 6 +++-- .../NumberTheory/Cyclotomic/MoreLemmas.lean | 5 ++-- .../NumberTheory/Cyclotomic/UnitLemmas.lean | 27 +++++-------------- FltRegular/NumberTheory/Hilbert92.lean | 10 +------ .../NumberTheory/KummersLemma/Field.lean | 11 ++++---- 7 files changed, 26 insertions(+), 45 deletions(-) diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index 3fb65546..7e9fa51d 100644 --- a/FltRegular/CaseI/Statement.lean +++ b/FltRegular/CaseI/Statement.lean @@ -170,14 +170,13 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)] congr 2 · ext - simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe] + simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, ← h] 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] · ext - simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow, - IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe] + simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow, map_units_inv, ← h] 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] diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean index 68008436..56b39b94 100644 --- a/FltRegular/CaseII/InductionStep.lean +++ b/FltRegular/CaseII/InductionStep.lean @@ -61,8 +61,8 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := 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 [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, IsPrimitiveRoot.coe_unit'_coe, - map_one] + simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, + map_one, show hζ.unit'.1 = ζ from rfl] rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)] /- Make (x+yη)/(ζ-1) into an element of O_K -/ @@ -73,7 +73,8 @@ 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 ext - simp [div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)] + simp [show hζ.unit'.1 = ζ from rfl, + div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)] /- y is associated to (x+yη₁)/(ζ-1) - (x+yη₂)/(ζ-1) for η₁ ≠ η₂. -/ lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) : diff --git a/FltRegular/NumberTheory/Cyclotomic/CaseI.lean b/FltRegular/NumberTheory/Cyclotomic/CaseI.lean index 2cf2da5f..16d66051 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CaseI.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CaseI.lean @@ -37,8 +37,10 @@ theorem exists_int_sum_eq_zero'_aux (x y i : ℤ) : add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero] simp_rw [NumberField.Units.coe_zpow] left - push_cast - simp only [map_zpow₀, galConj_zeta_runity hζ, inv_zpow', zpow_neg] + simp only [map_zpow₀] + rw [← inv_zpow] + congr + exact galConj_zeta_runity hζ 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/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index 2b41e0c4..a00a8da5 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -31,7 +31,8 @@ lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) - letI := IsCyclotomicExtension.numberField {p} ℚ K haveI : Fact (Nat.Prime p) := hpri apply RingHom.injective_int (algebraMap ℤ ℚ) - simp [Algebra.coe_norm_int, hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp] + simpa [Algebra.coe_norm_int] + using hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp lemma surjective_of_isCyclotomicExtension_two (R S) [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [IsCyclotomicExtension {2} R S] : @@ -64,7 +65,7 @@ lemma norm_Int_zeta_sub_one' (hp : p = 2) : haveI : Fact (Nat.Prime p) := hpri apply RingHom.injective_int (algebraMap ℤ ℚ) subst hp - simp [Algebra.coe_norm_int, hζ.sub_one_norm_two'] + simpa [Algebra.coe_norm_int] using hζ.sub_one_norm_two' lemma associated_zeta_sub_one_pow_prime : Associated ((hζ.unit' - 1 : 𝓞 K) ^ (p - 1 : ℕ)) p := by letI := IsCyclotomicExtension.numberField {p} ℚ K diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean index 9fafdb15..3fc892f1 100644 --- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean @@ -27,18 +27,6 @@ def IsPrimitiveRoot.unit' {p : ℕ+} {K : Type _} [Field K] {ζ : K} (hζ : IsPr val_inv := Subtype.ext <| mul_inv_cancel <| hζ.ne_zero p.ne_zero inv_val := Subtype.ext <| inv_mul_cancel <| hζ.ne_zero p.ne_zero -@[simp, norm_cast] -theorem IsPrimitiveRoot.coe_unit'_coe {p : ℕ+} {K : Type _} [Field K] {ζ : K} - (hζ : IsPrimitiveRoot ζ p) : ↑↑(hζ.unit') = ζ := rfl - -@[simp, norm_cast] -theorem IsPrimitiveRoot.coe_inv_unit'_coe {p : ℕ+} {K : Type _} [Field K] {ζ : K} - (hζ : IsPrimitiveRoot ζ p) : ↑↑(hζ.unit'⁻¹) = ζ⁻¹ := rfl - -@[simp, norm_cast] -theorem IsPrimitiveRoot.unit'_val_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K} - (hζ : IsPrimitiveRoot ζ p) : ↑↑(IsPrimitiveRoot.unit' hζ) = ζ := rfl - set_option quotPrecheck false local notation "ζ1" => (hζ.unit' - 1 : 𝓞 K) @@ -249,11 +237,10 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K) 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 only [even_two, Even.neg_pow, one_pow, one_mul] + simp only [SubmonoidClass.coe_pow] at Hi + simp only [PNat.val_ofNat, even_two, Even.neg_pow, one_pow, one_mul] + rw [← Hi] rfl · have hone : (-1 : R) ^ (p : ℕ) = (-1 : R) := by apply Odd.neg_one_pow hpo have hxp3 : (-1 * ⟨x, hx⟩ : R) ^ (p : ℕ) = 1 := by @@ -263,10 +250,9 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K) 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, + simp only [SubmonoidClass.coe_pow, 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, _⟩ @@ -284,9 +270,10 @@ theorem IsPrimitiveRoot.isPrime_one_sub_zeta [hp : Fact (p : ℕ).Prime] : apply_fun (fun x : 𝓞 K => (x : K)) push_cast 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] + simp only [one_right_iff] + simp only [map_sub, map_one, map_zero, sub_eq_zero] at h + exact h theorem IsPrimitiveRoot.two_not_mem_one_sub_zeta [hp : Fact (p : ℕ).Prime] (h : p ≠ 2) : (2 : 𝓞 K) ∉ I := by diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index ce18ef1b..e20dd782 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -750,13 +750,6 @@ lemma unit_to_U_map (x : (𝓞 k)ˣ) : mkG (Units.map (algebraMap (𝓞 k) (𝓞 rw [ofMul_eq_zero, QuotientGroup.eq_one_iff] exact ⟨_, rfl⟩ -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) - ext - 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 lemma IsPrimitiveRoot.one_left_iff {M} [CommMonoid M] {n : ℕ} : @@ -857,8 +850,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) : toMul_ofMul, RingHom.toMonoidHom_eq_coe, zpow_neg, unit_to_U_inv, Function.comp_apply, unit_to_U_map, smul_zero, neg_zero, add_zero, add_right_eq_self, NE, η, H2, J, N, H] apply_fun mkG at NE_p_pow - simp only [RingHom.toMonoidHom_eq_coe, unit_to_U_map, - unit_to_U_neg, unit_to_U_pow] at NE_p_pow + simp only [RingHom.toMonoidHom_eq_coe, unit_to_U_map, unit_to_U_pow] at NE_p_pow rw [eq_comm, smul_eq_zero] at NE_p_pow simp only [Nat.cast_eq_zero, PNat.ne_zero, false_or] at NE_p_pow rw [NE_p_pow, smul_zero] diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index 6e74cd6b..1a45999d 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -77,20 +77,19 @@ lemma map_poly : (poly hp hζ u hcong).map (algebraMap (𝓞 K) K) = (((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_sub, Polynomial.map_mul, map_C, 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] + Polynomial.map_one] rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm] - simp + simp [show hζ.unit'.1 = ζ from rfl] 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, - IsPrimitiveRoot.coe_unit'_coe] - simp_rw [← smul_eq_mul K, ← coeff_smul] + PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe] + simp_rw [← smul_eq_mul K, ← coeff_smul, show hζ.unit'.1 = ζ from rfl] 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