feat: the absolute discriminant of cyclotomic fields (#10492)

We compute the absolute discriminant of cyclotomic fields.


From flt-regular.

Author: riccardobrasca

Mathlib/NumberTheory/Cyclotomic/Rat.lean

@@ -20,6 +20,8 @@ integers of a `p ^ n`-th cyclotomic extension of `ℚ`.
   `ℤ` in `K`.
 * `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`: the integral
   closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is `CyclotomicRing (p ^ k) ℤ ℚ`.
+* `IsCyclotomicExtension.Rat.absdiscr_prime_pow` and related results: the absolute discriminant
+  of cyclotomic fields.
 -/
 
 
@@ -344,4 +346,57 @@ theorem subOneIntegralPowerBasis'_gen_prime [IsCyclotomicExtension {p} ℚ K]
 
 end IsPrimitiveRoot
 
+section absdiscr
+
+namespace IsCyclotomicExtension.Rat
+
+open nonZeroDivisors IsPrimitiveRoot
+
+variable (K p k)
+
+/-- We compute the absolute discriminant of a `p ^ k`-th cyclotomic field.
+  Beware that in the cases `p ^ k = 1` and `p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`.
+  See also the results below. -/
+theorem absdiscr_prime_pow [NumberField K] [IsCyclotomicExtension {p ^ k} ℚ K] :
+    NumberField.discr K =
+    (-1) ^ ((p ^ k : ℕ).totient / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1)) := by
+  have hζ := (IsCyclotomicExtension.zeta_spec (p ^ k) ℚ K)
+  let pB₁ := integralPowerBasis hζ
+  apply (algebraMap ℤ ℚ).injective_int
+  rw [← NumberField.discr_eq_discr _ pB₁.basis, ← Algebra.discr_localizationLocalization ℤ ℤ⁰ K]
+  convert IsCyclotomicExtension.discr_prime_pow hζ (cyclotomic.irreducible_rat (p ^ k).2) using 1
+  · have : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim := by
+      rw [← PowerBasis.finrank, ← PowerBasis.finrank]
+      exact RingOfIntegers.rank K
+    rw [← Algebra.discr_reindex _ _ (finCongr this)]
+    congr 1
+    ext i
+    simp_rw [Function.comp_apply, Basis.localizationLocalization_apply, powerBasis_dim,
+      PowerBasis.coe_basis,integralPowerBasis_gen]
+    convert ← ((IsPrimitiveRoot.powerBasis ℚ hζ).basis_eq_pow i).symm using 1
+  · simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]
+
+open Nat in
+/-- We compute the absolute discriminant of a `p ^ (k + 1)`-th cyclotomic field.
+  Beware that in the case `p ^ k = 2` the formula uses `1 / 2 = 0`. See also the results below. -/
+theorem absdiscr_prime_pow_succ [NumberField K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] :
+    NumberField.discr K =
+    (-1) ^ ((p : ℕ) ^ k * (p - 1) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) := by
+  simpa [totient_prime_pow hp.out (succ_pos k)] using absdiscr_prime_pow p (k + 1) K
+
+/-- We compute the absolute discriminant of a `p`-th cyclotomic field where `p` is prime. -/
+theorem absdiscr_prime [NumberField K] [IsCyclotomicExtension {p} ℚ K] :
+    NumberField.discr K = (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2) := by
+  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by
+    rw [zero_add, pow_one]
+    infer_instance
+  rw [absdiscr_prime_pow_succ p 0 K]
+  simp only [Int.reduceNeg, pow_zero, one_mul, zero_add, mul_one, mul_eq_mul_left_iff, gt_iff_lt,
+    Nat.cast_pos, PNat.pos, pow_eq_zero_iff', neg_eq_zero, one_ne_zero, ne_eq, false_and, or_false]
+  rfl
+
+end IsCyclotomicExtension.Rat
+
+end absdiscr
+
 end PowerBasis

Mathlib/RingTheory/PowerBasis.lean

@@ -82,7 +82,8 @@ theorem finiteDimensional [Algebra K S] (pb : PowerBasis K S) : FiniteDimensiona
   FiniteDimensional.of_fintype_basis pb.basis
 #align power_basis.finite_dimensional PowerBasis.finiteDimensional
 
-theorem finrank [Algebra K S] (pb : PowerBasis K S) : FiniteDimensional.finrank K S = pb.dim := by
+theorem finrank [StrongRankCondition R] (pb : PowerBasis R S) :
+    FiniteDimensional.finrank R S = pb.dim := by
   rw [FiniteDimensional.finrank_eq_card_basis pb.basis, Fintype.card_fin]
 #align power_basis.finrank PowerBasis.finrank