From 6c9696a9f81879dd7a2f93a6e253bbdd59b2a0d1 Mon Sep 17 00:00:00 2001 From: erd1 Date: Fri, 1 Dec 2023 03:55:40 +0800 Subject: [PATCH] first commit --- .../NumberTheory/Cyclotomic/MoreLemmas.lean | 78 ++++++++++ FltRegular/NumberTheory/CyclotomicRing.lean | 106 +++++++++++++ FltRegular/NumberTheory/Hilbert92.lean | 139 +++++++----------- FltRegular/NumberTheory/SystemOfUnits.lean | 109 +++++++------- 4 files changed, 295 insertions(+), 137 deletions(-) create mode 100644 FltRegular/NumberTheory/CyclotomicRing.lean diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index 9448ea94..625b8f55 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -31,6 +31,42 @@ lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) - apply RingHom.injective_int (algebraMap ℤ ℚ) simp [Algebra.coe_norm_int, hζ.sub_one_norm_prime (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 + have H : Algebra.adjoin R {b : S | b = 1 ∨ b = -1} ≤ ⊥ + · rw [Algebra.adjoin_le_iff] + rintro _ (rfl|rfl) + · exact one_mem _ + · exact neg_mem (one_mem _) + exact H this + +theorem IsPrimitiveRoot.sub_one_norm_two' {K L} [Field K] [Field L] [Algebra K L] {ζ : L} + (hζ : IsPrimitiveRoot ζ 2) + [IsCyclotomicExtension {2} K L] : Algebra.norm K (ζ - 1) = -2 := by + rw [hζ.eq_neg_one_of_two_right] + suffices : Algebra.norm K (algebraMap K L (-2)) = -2 + · simpa only [sub_eq_add_neg, ← one_add_one_eq_two, + neg_add_rev, map_add, map_neg, map_one] using this + rw [Algebra.norm_algebraMap, finrank_eq_one_iff'.mpr, pow_one] + refine ⟨1, one_ne_zero, fun w ↦ ?_⟩ + simpa only [Algebra.algebraMap_eq_smul_one] using surjective_of_isCyclotomicExtension_two K L w + +lemma norm_Int_zeta_sub_one' (hp : p = 2) : + Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) - 1 : 𝓞 K) = -p := by + clear ‹p ≠ 2› + letI := IsCyclotomicExtension.numberField {p} ℚ K + haveI : Fact (Nat.Prime p) := hpri + apply RingHom.injective_int (algebraMap ℤ ℚ) + subst hp + simp [Algebra.coe_norm_int, 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 haveI : Fact (Nat.Prime p) := hpri @@ -83,8 +119,50 @@ lemma norm_dvd_iff {R : Type*} [CommRing R] [IsDomain R] [IsDedekindDomain R] Int.natAbs_dvd] rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime] +section + +variable {α} [CommMonoidWithZero α] + +theorem prime_units_mul (a : αˣ) (b : α) : Prime (↑a * b) ↔ Prime b := by simp [Prime] + +theorem prime_isUnit_mul {a b : α} (h : IsUnit a) : Prime (a * b) ↔ Prime b := + let ⟨a, ha⟩ := h + ha ▸ prime_units_mul a 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] + +theorem prime_mul_iff {α} [CancelCommMonoidWithZero α] {a b : α} : + Prime (a * b) ↔ Prime a ∧ IsUnit b ∨ Prime b ∧ IsUnit a := by + constructor + · intro h + have ha : a ≠ 0 := fun ha ↦ by simp [ha] at h + have hb : b ≠ 0 := fun hb ↦ by simp [hb] at h + have : a * b ∣ a * 1 ∨ a * b ∣ 1 * b := by simpa using h.2.2 _ _ dvd_rfl + rw [mul_dvd_mul_iff_left ha, mul_dvd_mul_iff_right hb, + ← isUnit_iff_dvd_one, ← isUnit_iff_dvd_one] at this + refine this.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) + · rwa [prime_mul_isUnit h'] at h + · rwa [prime_isUnit_mul h'] at h + · rintro (⟨ha, hb⟩ | ⟨hb, ha⟩) + · rwa [prime_mul_isUnit hb] + · rwa [prime_isUnit_mul ha] +end + lemma zeta_sub_one_dvd_Int_iff {n : ℤ} : (hζ.unit' : 𝓞 K) - 1 ∣ n ↔ ↑p ∣ n := by + clear hp letI := IsCyclotomicExtension.numberField {p} ℚ K + by_cases hp : p = 2 + · rw [← neg_dvd (a := (p : ℤ))] + rw [← norm_Int_zeta_sub_one' hζ hp, norm_dvd_iff] + rw [norm_Int_zeta_sub_one' hζ hp, prime_neg_iff, ← Nat.prime_iff_prime_int] + exact hpri.out rw [← norm_Int_zeta_sub_one hζ hp, norm_dvd_iff] rw [norm_Int_zeta_sub_one hζ hp, ← Nat.prime_iff_prime_int] exact hpri.out diff --git a/FltRegular/NumberTheory/CyclotomicRing.lean b/FltRegular/NumberTheory/CyclotomicRing.lean new file mode 100644 index 00000000..07fc1b46 --- /dev/null +++ b/FltRegular/NumberTheory/CyclotomicRing.lean @@ -0,0 +1,106 @@ +import Mathlib.NumberTheory.Cyclotomic.Rat +import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots +import FltRegular.NumberTheory.Cyclotomic.MoreLemmas + +noncomputable section + +open Polynomial NumberField + +variable (p : ℕ) [hpri : Fact p.Prime] + +def CyclotomicIntegers : Type := AdjoinRoot (cyclotomic p ℤ) + +instance : CommRing (CyclotomicIntegers p) := by delta CyclotomicIntegers; infer_instance + +open Polynomial in +lemma IsPrimitiveRoot.cyclotomic_eq_minpoly + (x : 𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) (hx : IsPrimitiveRoot x.1 p) : + minpoly ℤ x = cyclotomic p ℤ := by + apply Polynomial.map_injective (algebraMap ℤ ℚ) (RingHom.injective_int (algebraMap ℤ ℚ)) + rw [← minpoly.isIntegrallyClosed_eq_field_fractions ℚ (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ), + ← cyclotomic_eq_minpoly_rat (n := p), map_cyclotomic] + · exact hx + · exact hpri.out.pos + · exact IsIntegralClosure.isIntegral _ (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ) _ + +def AdjoinRoot.aeval_root {R} [CommRing R] (P : R[X]) : aeval (root P) P = 0 := by simp + +@[simps!] +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)] +def equiv : + CyclotomicIntegers p ≃+* 𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ) := by + letI p' : ℕ+ := ⟨p, hpri.out.pos⟩ + letI : Fact (Nat.Prime p') := hpri + letI H := IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ) + exact (AdjoinRoot.equivOfMinpolyEq (cyclotomic p ℤ) H.integralPowerBasis' + (H.integralPowerBasis'_gen ▸ IsPrimitiveRoot.cyclotomic_eq_minpoly p H.toInteger H)).toRingEquiv + +instance : IsDomain (CyclotomicIntegers p) := + AdjoinRoot.isDomain_of_prime (UniqueFactorizationMonoid.irreducible_iff_prime.mp + (cyclotomic.irreducible hpri.out.pos)) + +def zeta : CyclotomicIntegers p := AdjoinRoot.root _ + +lemma equiv_zeta : equiv p (zeta p) = (IsCyclotomicExtension.zeta_spec + ⟨p, hpri.out.pos⟩ ℚ (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)).toInteger := by + letI p' : ℕ+ := ⟨p, hpri.out.pos⟩ + letI : Fact (Nat.Prime p') := hpri + rw [equiv_apply, zeta] + simp only [AdjoinRoot.liftHom_root, IsPrimitiveRoot.integralPowerBasis'_gen] + +lemma prime_one_sub_zeta : + Prime (1 - zeta p) := by + rw [← prime_units_mul (a := -1), Units.val_neg, Units.val_one, neg_mul, one_mul, neg_sub] + apply (equiv p).toMulEquiv.prime_iff.mpr + simp only [RingEquiv.toMulEquiv_eq_coe, RingEquiv.coe_toMulEquiv, + (equiv p).map_sub, (equiv p).map_one, equiv_zeta] + letI p' : ℕ+ := ⟨p, hpri.out.pos⟩ + letI : Fact (Nat.Prime p') := hpri + letI H := IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ) + exact H.zeta_sub_one_prime' + +lemma one_sub_zeta_mem_nonZeroDivisors : + 1 - zeta p ∈ nonZeroDivisors (CyclotomicIntegers p) := by + rw [mem_nonZeroDivisors_iff_ne_zero] + exact (prime_one_sub_zeta p).1 + +lemma not_isUnit_one_sub_zeta : + ¬ IsUnit (1 - zeta p) := (prime_one_sub_zeta p).irreducible.1 + +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 + letI H := IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ) + rw [← map_dvd_iff (equiv p), map_sub, map_one, equiv_zeta, map_intCast, + ← neg_dvd, neg_sub] + exact zeta_sub_one_dvd_Int_iff H + +lemma one_sub_zeta_dvd : 1 - zeta p ∣ p := by + show 1 - zeta p ∣ (p : ℤ) + rw [one_sub_zeta_dvd_int_iff] + +lemma isCoprime_one_sub_zeta (n : ℤ) (hn : ¬ (p : ℤ) ∣ n) : IsCoprime (1 - zeta p) n := by + apply (((Nat.prime_iff_prime_int.mp hpri.out).coprime_iff_not_dvd.mpr hn).map + (algebraMap ℤ <| CyclotomicIntegers p)).of_isCoprime_of_dvd_left + exact one_sub_zeta_dvd p + +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] + convert RingOfIntegers.dvd_norm ℚ (equiv p n) using 1 + ext1 + exact FunLike.congr_arg (algebraMap ℚ _) (Algebra.coe_norm_int (equiv p n)) + +end CyclotomicIntegers +end diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 385d651b..1c87df31 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -13,6 +13,7 @@ variable (p : ℕ+) {K : Type*} [Field K] [NumberField K] [IsCyclotomicExtension variable {k : Type*} [Field k] [NumberField k] (hp : Nat.Prime p) open FiniteDimensional BigOperators Finset +open CyclotomicIntegers (zeta) -- Z[H] module M (rank L) submodule N (rank l) H-stable -- H cyclic order p -- M / N is free up to torsion rank r (as an ab group free rank r p) @@ -26,21 +27,21 @@ variable [DistribMulAction H G] [Module.Free ℤ G] (hf : finrank ℤ G = r * (p - 1)) -- TODO maybe abbrev -local notation3 "A" => - MonoidAlgebra ℤ H ⧸ Ideal.span {∑ i in Finset.range p, (MonoidAlgebra.of ℤ H σ) ^ i} +local notation3 "A" => CyclotomicIntegers p + -- MonoidAlgebra ℤ H ⧸ Ideal.span {∑ i in Finset.range p, (MonoidAlgebra.of ℤ H σ) ^ i} instance systemOfUnits.instFintype {r} [Module A G] -- [IsScalarTower ℤ A G] - (sys : systemOfUnits (G := G) p σ r) : Fintype (G ⧸ Submodule.span A (Set.range sys.units)) := sorry + (sys : systemOfUnits (G := G) p r) : Fintype (G ⧸ Submodule.span A (Set.range sys.units)) := sorry -def systemOfUnits.index [Module A G] (sys : systemOfUnits p G σ r) := +def systemOfUnits.index [Module A G] (sys : systemOfUnits p G r) := Fintype.card (G ⧸ Submodule.span A (Set.range sys.units)) -def systemOfUnits.IsFundamental [Module A G] (h : systemOfUnits p G σ r) := - ∀ s : systemOfUnits p G σ r, h.index ≤ s.index +def systemOfUnits.IsFundamental [Module A G] (h : systemOfUnits p G r) := + ∀ s : systemOfUnits p G r, h.index ≤ s.index -lemma systemOfUnits.IsFundamental.maximal' [Module A G] (S : systemOfUnits p G σ r) - (hs : S.IsFundamental) (a : systemOfUnits p G σ r) : +lemma systemOfUnits.IsFundamental.maximal' [Module A G] (S : systemOfUnits p G r) + (hs : S.IsFundamental) (a : systemOfUnits p G r) : (Submodule.span A (Set.range S.units)).toAddSubgroup.index ≤ (Submodule.span A (Set.range a.units)).toAddSubgroup.index := by convert hs a <;> symm <;> exact Nat.card_eq_fintype_card.symm @@ -91,52 +92,10 @@ lemma Subgroup.index_mono {G : Type*} [Group G] {H₁ H₂ : Subgroup G} (h : H rw [←mul_one H₂.index, ←relindex_mul_index h.le, mul_comm, Ne, eq_comm] simp [-one_mul, -Nat.one_mul, hn, h.not_le] -lemma isPrimitiveroot : IsPrimitiveRoot (σA p σ) p := sorry - -instance : IsDomain A := sorry - -lemma one_sub_σA_mem : 1 - σA p σ ∈ A⁰ := by - rw [mem_nonZeroDivisors_iff_ne_zero, ne_eq, sub_eq_zero, eq_comm] - exact (isPrimitiveroot p σ).ne_one hp.one_lt - -lemma one_sub_σA_mem_nonunit : ¬ IsUnit (1 - σA p σ) := sorry - -open Polynomial in -lemma IsPrimitiveRoot.cyclotomic_eq_minpoly - (x : 𝓞 (CyclotomicField p ℚ)) (hx : IsPrimitiveRoot x.1 p) : minpoly ℤ x = cyclotomic p ℤ := by - apply Polynomial.map_injective (algebraMap ℤ ℚ) (RingHom.injective_int (algebraMap ℤ ℚ)) - rw [← minpoly.isIntegrallyClosed_eq_field_fractions ℚ (CyclotomicField p ℚ), - ← cyclotomic_eq_minpoly_rat (n := p), map_cyclotomic] - · exact hx - · exact hp.pos - · exact IsIntegralClosure.isIntegral _ (CyclotomicField p ℚ) _ - -open Polynomial in -noncomputable -def TheEquiv : ℤ[X] ⧸ Ideal.span (singleton (cyclotomic p ℤ)) ≃+* 𝓞 (CyclotomicField p ℚ) := by - letI := Fact.mk hp - have : IsCyclotomicExtension {p ^ 1} ℚ (CyclotomicField p ℚ) - · rw [pow_one] - infer_instance - refine (AdjoinRoot.equiv' (cyclotomic p ℤ) (IsPrimitiveRoot.integralPowerBasis - (IsCyclotomicExtension.zeta_spec (p ^ 1) ℚ (CyclotomicField p ℚ))) ?_ ?_).toRingEquiv - · simp only [pow_one, IsPrimitiveRoot.integralPowerBasis_gen, AdjoinRoot.aeval_eq, - AdjoinRoot.mk_eq_zero] - rw [IsPrimitiveRoot.cyclotomic_eq_minpoly p hp - (IsCyclotomicExtension.zeta_spec p ℚ (CyclotomicField p ℚ)).toInteger - (IsCyclotomicExtension.zeta_spec p ℚ (CyclotomicField p ℚ))] - · rw [← IsPrimitiveRoot.cyclotomic_eq_minpoly p hp - (IsCyclotomicExtension.zeta_spec p ℚ (CyclotomicField p ℚ)).toInteger - (IsCyclotomicExtension.zeta_spec p ℚ (CyclotomicField p ℚ))] - simp - - -lemma isCoprime_one_sub_σA (n : ℤ) (hn : ¬ (p : ℤ) ∣ n): IsCoprime (1 - σA p σ) n := sorry - namespace fundamentalSystemOfUnits -lemma existence [Module A G] : ∃ S : systemOfUnits p G σ r, S.IsFundamental := by - obtain ⟨S⟩ := systemOfUnits.existence p G σ r - have : { a | ∃ S : systemOfUnits p G σ r, a = S.index}.Nonempty := ⟨S.index, S, rfl⟩ +lemma existence [Module A G] : ∃ S : systemOfUnits p G r, S.IsFundamental := by + obtain ⟨S⟩ := systemOfUnits.existence p hp G r + have : { a | ∃ S : systemOfUnits p G r, a = S.index}.Nonempty := ⟨S.index, S, rfl⟩ obtain ⟨S', ha⟩ := Nat.sInf_mem this use S' intro a' @@ -144,11 +103,13 @@ lemma existence [Module A G] : ∃ S : systemOfUnits p G σ r, S.IsFundamental : apply csInf_le (OrderBot.bddBelow _) use a' -lemma lemma2 [Module A G] (S : systemOfUnits p G σ r) (hs : S.IsFundamental) (i : Fin r) : - ∀ g : G, (1 - σA p σ) • g ≠ S.units i := by +lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (i : Fin r) : + ∀ g : G, (1 - zeta p) • g ≠ S.units i := by intro g hg - let S' : systemOfUnits p G σ r := ⟨Function.update S.units i g, - LinearIndependent.update (hσ := one_sub_σA_mem p hp σ) (hg := hg) S.linearIndependent⟩ + letI := Fact.mk hp + let S' : systemOfUnits p G r := ⟨Function.update S.units i g, + LinearIndependent.update (hσ := CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors p) + (hg := hg) S.linearIndependent⟩ suffices : Submodule.span A (Set.range S.units) < Submodule.span A (Set.range S'.units) · exact (hs.maximal' S').not_lt (AddSubgroup.index_mono (h₁ := S.instFintype) this) rw [SetLike.lt_iff_le_and_exists] @@ -170,19 +131,21 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G σ r) (hs : S.IsFundamental) (i ← (Finsupp.total (Fin r) G A S.units).map_sub] at hg have := FunLike.congr_fun (linearIndependent_iff.mp S.linearIndependent _ hg) i simp only [Finsupp.coe_sub, Pi.sub_apply, Finsupp.single_eq_same] at this - exact one_sub_σA_mem_nonunit p σ (isUnit_of_mul_eq_one _ _ (sub_eq_zero.mp this)) + exact CyclotomicIntegers.not_isUnit_one_sub_zeta p + (isUnit_of_mul_eq_one _ _ (sub_eq_zero.mp this)) -lemma lemma2' [Module A G] (S : systemOfUnits p G σ r) (hs : S.IsFundamental) (i : Fin r) (a : ℤ) - (ha : ¬ (p : ℤ) ∣ a) : ∀ g : G, (1 - σA p σ) • g ≠ a • (S.units i) := by +lemma lemma2' [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (i : Fin r) (a : ℤ) + (ha : ¬ (p : ℤ) ∣ a) : ∀ g : G, (1 - zeta p) • g ≠ a • (S.units i) := by intro g hg - obtain ⟨x, y, e⟩ := isCoprime_one_sub_σA p σ a ha - apply lemma2 p hp G σ r S hs i (x • (S.units i) + y • g) + letI := Fact.mk hp + obtain ⟨x, y, e⟩ := CyclotomicIntegers.isCoprime_one_sub_zeta p a ha + apply lemma2 p hp G r S hs i (x • (S.units i) + y • g) conv_rhs => rw [← one_smul A (S.units i), ← e, add_smul, ← smul_smul y, intCast_smul, ← hg] rw [smul_add, smul_smul, smul_smul, smul_smul, mul_comm x, mul_comm y] -lemma corollary [Module A G] (S : systemOfUnits p G σ r) (hs : S.IsFundamental) (a : Fin r → ℤ) +lemma corollary [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (a : Fin r → ℤ) (ha : ∃ i , ¬ (p : ℤ) ∣ a i) : - ∀ g : G, (1 - σA p σ) • g ≠ ∑ i, a i • S.units i := sorry + ∀ g : G, (1 - zeta p) • g ≠ ∑ i, a i • S.units i := sorry end fundamentalSystemOfUnits section application @@ -198,7 +161,13 @@ variable -- have : IsCyclic (K ≃ₐ[k] K) := isCyclic_of_prime_card (hp := ⟨hp⟩) this -- use IsCyclic.commGroup.mul_comm -local notation3 "G" => (𝓞 K)ˣ ⧸ (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : 𝓞 k →* 𝓞 K)) +def RelativeUnits (k K : Type*) [Field k] [Field K] [Algebra k K] := + ((𝓞 K)ˣ ⧸ (MonoidHom.range <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K)))) + + +local notation "G" => RelativeUnits k K + +instance : CommGroup G := by delta RelativeUnits; infer_instance attribute [local instance] IsCyclic.commGroup @@ -276,21 +245,21 @@ local instance : Module Ideal.span {∑ i in Finset.range p, (MonoidAlgebra.of ℤ (K ≃ₐ[k] K) σ) ^ i}) (Additive G) := (isTors (k := k) (K := K) p σ).module -def tors : Submodule - (MonoidAlgebra ℤ (K ≃ₐ[k] K) ⧸ - Ideal.span {∑ i in Finset.range p, (MonoidAlgebra.of ℤ (K ≃ₐ[k] K) σ) ^ i}) (Additive G) := sorry +instance : Module A (Additive G) := sorry + +def tors : Submodule A (Additive G) := sorry -- local instance : Module A (Additive G ⧸ AddCommGroup.torsion (Additive G)) := Submodule.Quotient.module _ -#synth CommGroup G -#synth AddCommGroup (Additive G) +-- #synth CommGroup G +-- #synth AddCommGroup (Additive G) -- #check Submodule.Quotient.module (tors (k := k) (K := K) p σ) -local instance : Module A (Additive G ⧸ tors (k := k) (K := K) p σ) := by - -- apply Submodule.Quotient.modue _ - sorry +-- local instance : Module A (Additive G ⧸ tors) := by +-- -- apply Submodule.Quotient.modue _ +-- sorry local instance : Module.Free ℤ (Additive <| G ⧸ torsion G) := sorry -- #exit lemma Hilbert91ish : - ∃ S : systemOfUnits p (Additive G ⧸ tors (k := k) (K := K) p σ) σ (NumberField.Units.rank k + 1), S.IsFundamental := - fundamentalSystemOfUnits.existence p (Additive G ⧸ tors (k := k) (K := K) p σ) σ (NumberField.Units.rank k + 1) + ∃ S : systemOfUnits p (Additive G ⧸ tors (k := k) (K := K) p) (NumberField.Units.rank k + 1), S.IsFundamental := + fundamentalSystemOfUnits.existence p hp (Additive G ⧸ tors (k := k) (K := K) p) (NumberField.Units.rank k + 1) @@ -300,7 +269,7 @@ lemma Hilbert91ish : noncomputable def unitlifts - (S : systemOfUnits p (Additive G ⧸ tors (k := k) (K := K) p σ) σ (NumberField.Units.rank k + 1)) : + (S : systemOfUnits p (Additive G ⧸ tors (k := k) (K := K) p) (NumberField.Units.rank k + 1)) : Fin (NumberField.Units.rank k + 1) → Additive (𝓞 K)ˣ := by let U := S.units intro i @@ -321,16 +290,18 @@ lemma torsion_free_lin_system [Algebra k K] (h : Monoid.IsTorsionFree (𝓞 K)ˣ sorry +variable (k) -def unit_to_U (u : (𝓞 K)ˣ) : (Additive G ⧸ tors (k := k) (K := K) p σ) := by - have u1 := (Additive.ofMul u : Additive G) +def unit_to_U (u : (𝓞 K)ˣ) : (Additive G ⧸ tors (k := k) (K := K) p) := by + have u1 := (Additive.ofMul (QuotientGroup.mk u) : Additive G) use Quot.mk _ u1 +variable {k} lemma u_lemma2 [Algebra k K] [IsGalois k K] [FiniteDimensional k K] [IsCyclic (K ≃ₐ[k] K)] - (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (u v: (𝓞 K)ˣ) - (hu : u = v / (σ v : K)) : (unit_to_U p σ u) = (1 - σA p σ) • (unit_to_U p σ v):= by - simp [unit_to_U] + (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (u v : (𝓞 K)ˣ) + (hu : u = v / (σ v : K)) : (unit_to_U p k u) = (1 - zeta p : A) • (unit_to_U p k v):= by + -- simp [unit_to_U] sorry @@ -341,16 +312,16 @@ lemma Hilbert92ish (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) : ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := by - have S := @Hilbert91ish p K _ k _ _ _ _ σ + have S := Hilbert91ish p (K := K) (k := k) hp obtain ⟨S, hS⟩ := S - let H := @unitlifts p K _ k _ _ _ _ σ S + let H := @unitlifts p K _ k _ _ _ S let N : Fin (NumberField.Units.rank k + 1) → Additive (𝓞 k)ˣ := fun e => Additive.ofMul (Units.map (RingOfIntegers.norm k )) (Additive.toMul (H e)) by_cases T : Monoid.IsTorsionFree (𝓞 K)ˣ obtain ⟨a, i, ha⟩ := torsion_free_lin_system p T N - have C := fundamentalSystemOfUnits.corollary p (Additive G ⧸ tors (k := k) (K := K) p σ) σ + have C := fundamentalSystemOfUnits.corollary p (Additive G ⧸ tors (k := k) (K := K) p) (NumberField.Units.rank k + 1) S hS a ⟨i, ha.1⟩ let J := Additive.toMul (∑ i in ⊤, a i • H i) use J diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean index 82e27483..491b3035 100644 --- a/FltRegular/NumberTheory/SystemOfUnits.lean +++ b/FltRegular/NumberTheory/SystemOfUnits.lean @@ -1,5 +1,6 @@ import FltRegular.NumberTheory.Cyclotomic.UnitLemmas import FltRegular.NumberTheory.GaloisPrime +import FltRegular.NumberTheory.CyclotomicRing import Mathlib set_option autoImplicit false @@ -11,18 +12,17 @@ variable (p : ℕ+) {K : Type*} [Field K] [NumberField K] [IsCyclotomicExtension variable {k : Type*} [Field k] [NumberField k] (hp : Nat.Prime p) open FiniteDimensional BigOperators Finset +open CyclotomicIntegers(zeta) variable - (G : Type*) {H : Type*} [AddCommGroup G] [CommGroup H] [Fintype H] (hCard : Fintype.card H = p) - (σ : H) (hσ : Subgroup.zpowers σ = ⊤) (r : ℕ) - [DistribMulAction H G] [Module.Free ℤ G] (hf : finrank ℤ G = r * (p - 1)) + (G : Type*) {H : Type*} [AddCommGroup G] -- [CommGroup H] [Fintype H] (hCard : Fintype.card H = p) + -- (σ : H) (hσ : Subgroup.zpowers σ = ⊤) + (r : ℕ) + -- [DistribMulAction H G] + [Module.Free ℤ G] (hf : finrank ℤ G = r * (p - 1)) -- TODO maybe abbrev -local notation3 "A" => - MonoidAlgebra ℤ H ⧸ Ideal.span {∑ i in Finset.range p, (MonoidAlgebra.of ℤ H σ) ^ i} - -noncomputable -abbrev σA : A := MonoidAlgebra.of ℤ H σ +local notation3 "A" => CyclotomicIntegers p structure systemOfUnits (r : ℕ) [Module A G] where @@ -43,12 +43,12 @@ lemma nontrivial (hr : r ≠ 0) : Nontrivial G := by lemma bezout [Module A G] {a : A} (ha : a ≠ 0) : ∃ (f : A) (n : ℤ), f * a = n := sorry -lemma existence0 [Module A G] : Nonempty (systemOfUnits p G σ 0) := by +lemma existence0 [Module A G] : Nonempty (systemOfUnits p G 0) := by exact ⟨⟨fun _ => 0, linearIndependent_empty_type⟩⟩ lemma spanA_eq_spanA [Module A G] {R : ℕ} (f : Fin R → G) : Submodule.span A (Set.range f) = - Submodule.span A (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (σA p σ)^e.2.1 • f e.1)) := by + Submodule.span A (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1)) := by refine le_antisymm (Submodule.span_mono (fun x hx ↦ ?_)) ?_ · obtain ⟨a, ha⟩ := hx refine ⟨⟨a, ⟨0, hp.pred_pos⟩⟩, ?_⟩ @@ -64,39 +64,40 @@ lemma spanA_eq_spanA [Module A G] {R : ℕ} (f : Fin R → G) : set_option synthInstance.maxHeartbeats 0 in lemma mem_spanS [Module A G] {R : ℕ} {g : G} (a : A) (f : Fin R → G) (hg : g ∈ Submodule.span ℤ - (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (σA p σ)^e.2.1 • f e.1))) : + (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1))) : a • g ∈ Submodule.span ℤ - (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (σA p σ)^e.2.1 • f e.1)) := by + (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1)) := by rcases a with ⟨x⟩ revert hg - apply MonoidAlgebra.induction_on x - · intro h hg - refine Submodule.span_induction hg ?_ ?_ ?_ ?_ - · intro g₁ ⟨⟨n, m⟩, key⟩ - simp only at key - - - sorry - · rw [smul_zero] - apply Submodule.zero_mem - · intro g₁ g₂ hg₁ hg₂ - rw [smul_add] - exact Submodule.add_mem _ hg₁ hg₂ - · intro n g hg - rw [smul_algebra_smul_comm] - apply Submodule.smul_mem - exact hg - · intro f₁ f₂ hf₁ hf₂ hg - simp only [MonoidAlgebra.of_apply, Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, - map_add] - rw [add_smul (R := A)] - exact Submodule.add_mem _ (hf₁ hg) (hf₂ hg) - · intro n f₁ hf₁ hg - rw [Submodule.Quotient.quot_mk_eq_mk, ← intCast_smul (k := MonoidAlgebra ℤ H), - Submodule.Quotient.mk_smul, intCast_smul, smul_assoc] - apply Submodule.smul_mem - specialize hf₁ hg - rwa [Submodule.Quotient.quot_mk_eq_mk] at hf₁ + sorry + -- apply MonoidAlgebra.induction_on x + -- · intro h hg + -- refine Submodule.span_induction hg ?_ ?_ ?_ ?_ + -- · intro g₁ ⟨⟨n, m⟩, key⟩ + -- simp only at key + + + -- sorry + -- · rw [smul_zero] + -- apply Submodule.zero_mem + -- · intro g₁ g₂ hg₁ hg₂ + -- rw [smul_add] + -- exact Submodule.add_mem _ hg₁ hg₂ + -- · intro n g hg + -- rw [smul_algebra_smul_comm] + -- apply Submodule.smul_mem + -- exact hg + -- · intro f₁ f₂ hf₁ hf₂ hg + -- simp only [MonoidAlgebra.of_apply, Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, + -- map_add] + -- rw [add_smul (R := A)] + -- exact Submodule.add_mem _ (hf₁ hg) (hf₂ hg) + -- · intro n f₁ hf₁ hg + -- rw [Submodule.Quotient.quot_mk_eq_mk, ← intCast_smul (k := MonoidAlgebra ℤ H), + -- Submodule.Quotient.mk_smul, intCast_smul, smul_assoc] + -- apply Submodule.smul_mem + -- specialize hf₁ hg + -- rwa [Submodule.Quotient.quot_mk_eq_mk] at hf₁ -- · intro h hg -- have : h ∈ Subgroup.zpowers σ := by simp [hσ] -- rw [Subgroup.mem_zpowers_iff] at this @@ -106,8 +107,8 @@ lemma mem_spanS [Module A G] {R : ℕ} {g : G} (a : A) (f : Fin R → G) lemma spanA_eq_spanZ [Module A G] {R : ℕ} (f : Fin R → G) : (Submodule.span A (Set.range f) : Set G) = - Submodule.span ℤ (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (σA p σ)^e.2.1 • f e.1)) := by - let S := Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (σA p σ)^e.2.1 • f e.1) + Submodule.span ℤ (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1)) := by + let S := Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1) have := Submodule.span_le_restrictScalars ℤ A S rw [← spanA_eq_spanA p hp] at this refine le_antisymm ?_ this @@ -122,36 +123,38 @@ lemma spanA_eq_spanZ [Module A G] {R : ℕ} (f : Fin R → G) : · intro z w hz hw exact Submodule.add_mem _ hz hw · intro a _ hx - exact mem_spanS p G σ a f hx + exact mem_spanS p G a f hx -lemma ex_not_mem [Module A G] {R : ℕ} (S : systemOfUnits p G σ R) (hR : R < r) : +lemma ex_not_mem [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) : ∃ g, ∀ (k : ℤ), ¬(k • g ∈ Submodule.span A (Set.range S.units)) := by by_contra' h sorry set_option synthInstance.maxHeartbeats 0 in -lemma existence' [Module A G] {R : ℕ} (S : systemOfUnits p G σ R) (hR : R < r) : - Nonempty (systemOfUnits p G σ (R + 1)) := by - obtain ⟨g, hg⟩ := ex_not_mem p G σ r S hR +lemma existence' [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) : + Nonempty (systemOfUnits p G (R + 1)) := by + obtain ⟨g, hg⟩ := ex_not_mem p G r S hR refine ⟨⟨Fin.cases g S.units, ?_⟩⟩ refine LinearIndependent.fin_cons' g S.units S.linearIndependent (fun a y hy ↦ ?_) by_contra' ha - obtain ⟨f, n, Hf⟩ := bezout p G σ ha + letI := Fact.mk hp + obtain ⟨n, hn, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha replace hy := congr_arg (f • ·) hy simp only at hy let mon : Monoid A := inferInstance - rw [smul_zero, smul_add, smul_smul, Hf, ← eq_neg_iff_add_eq_zero, intCast_smul] at hy + rw [smul_zero, smul_add, smul_smul, mul_comm f, + ← Hf, ← eq_neg_iff_add_eq_zero, intCast_smul] at hy apply hg n rw [hy] exact Submodule.neg_mem _ (Submodule.smul_mem _ _ y.2) -lemma existence'' [Module A G] {R : ℕ} (hR : R ≤ r) : Nonempty (systemOfUnits p G σ R) := by +lemma existence'' [Module A G] {R : ℕ} (hR : R ≤ r) : Nonempty (systemOfUnits p G R) := by induction R with - | zero => exact existence0 p G σ + | zero => exact existence0 p G | succ n ih => obtain ⟨S⟩ := ih (le_trans (Nat.le_succ n) hR) - exact existence' p G σ r S (lt_of_lt_of_le (Nat.lt.base n) hR) + exact existence' p hp G r S (lt_of_lt_of_le (Nat.lt.base n) hR) -lemma existence (r) [Module A G] : Nonempty (systemOfUnits p G σ r) := existence'' p G σ r rfl.le +lemma existence (r) [Module A G] : Nonempty (systemOfUnits p G r) := existence'' p hp G r rfl.le end systemOfUnits