feat: the ring of integers of the p-th cyclotomic field is a PID if p…

… = 3 or p = 5 (#10683)

We prove that the ring of integers of the p-th cyclotomic field is a PID if p = 3 or p = 5.

From flt-regular

- [x] depends on: #10492 
- [x] depends on: #10502

Mathlib.lean

@@ -2896,6 +2896,7 @@ import Mathlib.NumberTheory.Cyclotomic.Basic
 import Mathlib.NumberTheory.Cyclotomic.Discriminant
 import Mathlib.NumberTheory.Cyclotomic.Embeddings
 import Mathlib.NumberTheory.Cyclotomic.Gal
+import Mathlib.NumberTheory.Cyclotomic.PID
 import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
 import Mathlib.NumberTheory.Cyclotomic.Rat
 import Mathlib.NumberTheory.Dioph

Mathlib/Data/Nat/Prime.lean

@@ -175,6 +175,8 @@ theorem prime_two : Prime 2 := by decide
 theorem prime_three : Prime 3 := by decide
 #align nat.prime_three Nat.prime_three
 
+theorem prime_five : Prime 5 := by decide
+
 theorem Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2)
     (h_three : p ≠ 3) : 5 ≤ p := by
   by_contra! h

Mathlib/Data/PNat/Basic.lean

@@ -68,6 +68,9 @@ theorem natPred_inj {m n : ℕ+} : m.natPred = n.natPred ↔ m = n :=
   natPred_injective.eq_iff
 #align pnat.nat_pred_inj PNat.natPred_inj
 
+@[simp]
+lemma val_ofNat (n : ℕ) : ((no_index (OfNat.ofNat n.succ) : ℕ+) : ℕ) = n.succ := rfl
+
 end PNat
 
 namespace Nat

Mathlib/Data/PNat/Defs.lean

@@ -194,7 +194,7 @@ theorem mk_one {h} : (⟨1, h⟩ : ℕ+) = (1 : ℕ+) :=
   rfl
 #align pnat.mk_one PNat.mk_one
 
-@[simp, norm_cast]
+@[norm_cast]
 theorem one_coe : ((1 : ℕ+) : ℕ) = 1 :=
   rfl
 #align pnat.one_coe PNat.one_coe

Mathlib/Data/PNat/Prime.lean

@@ -123,6 +123,23 @@ theorem prime_two : (2 : ℕ+).Prime :=
   Nat.prime_two
 #align pnat.prime_two PNat.prime_two
 
+instance {p : ℕ+} [h : Fact p.Prime] : Fact (p : ℕ).Prime := h
+
+instance fact_prime_two : Fact (2 : ℕ+).Prime :=
+  ⟨prime_two⟩
+
+theorem prime_three : (3 : ℕ+).Prime :=
+  Nat.prime_three
+
+instance fact_prime_three : Fact (3 : ℕ+).Prime :=
+  ⟨prime_three⟩
+
+theorem prime_five : (5 : ℕ+).Prime :=
+  Nat.prime_five
+
+instance fact_prime_five : Fact (5 : ℕ+).Prime :=
+  ⟨prime_five⟩
+
 theorem dvd_prime {p m : ℕ+} (pp : p.Prime) : m ∣ p ↔ m = 1 ∨ m = p := by
   rw [PNat.dvd_iff]
   rw [Nat.dvd_prime pp]

Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

@@ -183,7 +183,6 @@ theorem discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (
       · simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero,
           _root_.pow_zero, traceForm_apply, mul_one]
         rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]; norm_num
-        simp [← coe_two, Even.neg_pow (by decide : Even (1 / 2))]
     · exact discr_prime_pow_ne_two hζ hirr hk
 #align is_cyclotomic_extension.discr_prime_pow IsCyclotomicExtension.discr_prime_pow
 

Mathlib/NumberTheory/Cyclotomic/PID.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2024 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+-/
+
+import Mathlib.NumberTheory.NumberField.ClassNumber
+import Mathlib.NumberTheory.Cyclotomic.Rat
+import Mathlib.NumberTheory.Cyclotomic.Embeddings
+
+/-!
+# Cyclotomic fields whose ring of integers is a PID.
+We prove that `ℤ [ζₚ]` is a PID for specific values of `p`. The result holds for `p ≤ 19`,
+but the proof is more and more involved.
+
+## Main results
+* `three_pid`: If `IsCyclotomicExtension {3} ℚ K` then `𝓞 K` is a principal ideal domain.
+* `five_pid`: If `IsCyclotomicExtension {5} ℚ K` then `𝓞 K` is a principal ideal domain.
+-/
+
+universe u
+
+namespace IsCyclotomicExtension.Rat
+
+open NumberField Polynomial InfinitePlace Nat Real cyclotomic
+
+variable (K : Type u) [Field K] [NumberField K]
+
+/-- If `IsCyclotomicExtension {3} ℚ K` then `𝓞 K` is a principal ideal domain. -/
+theorem three_pid [IsCyclotomicExtension {3} ℚ K] : IsPrincipalIdealRing (𝓞 K) := by
+  apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
+  rw [absdiscr_prime 3 K, IsCyclotomicExtension.finrank (n := 3) K
+    (irreducible_rat (by norm_num)), nrComplexPlaces_eq_totient_div_two 3, totient_prime
+      PNat.prime_three]
+  simp only [Int.reduceNeg, PNat.val_ofNat, succ_sub_succ_eq_sub, tsub_zero, zero_lt_two,
+    Nat.div_self, pow_one, cast_ofNat, neg_mul, one_mul, abs_neg, Int.cast_abs, Int.int_cast_ofNat,
+    factorial_two, gt_iff_lt, abs_of_pos (show (0 : ℝ) < 3 by norm_num)]
+  suffices (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2 from
+    lt_trans (by norm_num) this
+  gcongr
+  exact pi_gt_three
+
+/-- If `IsCyclotomicExtension {5} ℚ K` then `𝓞 K` is a principal ideal domain. -/
+theorem five_pid [IsCyclotomicExtension {5} ℚ K] : IsPrincipalIdealRing (𝓞 K) := by
+  apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
+  rw [absdiscr_prime 5 K, IsCyclotomicExtension.finrank (n := 5) K
+    (irreducible_rat (by norm_num)), nrComplexPlaces_eq_totient_div_two 5, totient_prime
+      PNat.prime_five]
+  simp only [Int.reduceNeg, PNat.val_ofNat, succ_sub_succ_eq_sub, tsub_zero, reduceDiv, even_two,
+    Even.neg_pow, one_pow, cast_ofNat, Int.reducePow, one_mul, Int.cast_abs, Int.int_cast_ofNat,
+    div_pow, gt_iff_lt, show 4! = 24 by rfl, abs_of_pos (show (0 : ℝ) < 125 by norm_num)]
+  suffices (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 from
+    lt_trans (by norm_num) this
+  gcongr
+  exact pi_gt_three
+
+end IsCyclotomicExtension.Rat