Merge pull request #98 from leanprover-community/erd1/changeA

Change the definition of A

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

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