[Merged by Bors] - feat: characterize roots of unity in cyclotomic extensions

Mathlib/Data/Nat/Totient.lean

@@ -276,6 +276,10 @@ theorem totient_eq_one_iff : ∀ {n : ℕ}, n.totient = 1 ↔ n = 1 ∨ n = 2
     exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩
 #align nat.totient_eq_one_iff Nat.totient_eq_one_iff
 
+theorem totient_le_one_dvd_two {a : ℕ} (han : 0 < a) (ha : a.totient ≤ 1) : a ∣ 2 := by
+  have : a.totient = 1 := by linarith [Nat.totient_pos han]
+  cases' Nat.totient_eq_one_iff.1 this with h h <;> simp [h]
+
 /-! ### Euler's product formula for the totient function
 
 We prove several different statements of this formula. -/

Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

@@ -189,6 +189,101 @@ theorem finrank (hirr : Irreducible (cyclotomic n K)) : finrank K L = (n : ℕ).
     (zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]
 #align is_cyclotomic_extension.finrank IsCyclotomicExtension.finrank
 
+variable {L} in
+/-- If `L` contains both a primitive `p`-th root of unity and `q`-th root of unity, and
+`Irreducible (cyclotomic (lcm p q) K)` (in particular for `K = ℚ`), then the `finrank K L` is at
+least `(lcm p q).totient`. -/
+theorem _root_.IsPrimitiveRoot.lcm_totient_le_finrank [FiniteDimensional K L] {p q : ℕ} {x y : L}
+    (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q)
+    (hirr : Irreducible (cyclotomic (Nat.lcm p q) K)) :
+    (Nat.lcm p q).totient ≤ FiniteDimensional.finrank K L := by
+  rcases Nat.eq_zero_or_pos p with (rfl | hppos)
+  · simp
+  rcases Nat.eq_zero_or_pos q with (rfl | hqpos)
+  · simp
+  let k := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
+  obtain ⟨xu, rfl⟩ := hx.isUnit hppos
+  let yu := (hy.isUnit hqpos).unit
+  have hxmem : xu ∈ rootsOfUnity k L :=  by
+    rw [mem_rootsOfUnity, ← Units.val_eq_one, Units.val_pow_eq_pow_val]
+    exact (hx.pow_eq_one_iff_dvd _).2 (Nat.dvd_lcm_left _ _)
+  have hymem : yu ∈ rootsOfUnity k L := by
+    rw [mem_rootsOfUnity, ← Units.val_eq_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec]
+    exact (hy.pow_eq_one_iff_dvd _).2 (Nat.dvd_lcm_right _ _)
+  have hxuord : orderOf (⟨xu, hxmem⟩ : rootsOfUnity k L) = p := by
+    rw [← orderOf_injective (rootsOfUnity k L).subtype Subtype.coe_injective,
+      Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units]
+    exact hx.eq_orderOf.symm
+  have hyuord : orderOf (⟨yu, hymem⟩ : rootsOfUnity k L) = q := by
+    rw [← orderOf_injective (rootsOfUnity k L).subtype Subtype.coe_injective,
+      Subgroup.coeSubtype, Subgroup.coe_mk, ← orderOf_units, IsUnit.unit_spec]
+    exact hy.eq_orderOf.symm
+  obtain ⟨g : rootsOfUnity k L, hg⟩ := IsCyclic.exists_monoid_generator (α := rootsOfUnity k L)
+  obtain ⟨nx, hnx⟩ := hg ⟨xu, hxmem⟩
+  obtain ⟨ny, hny⟩ := hg ⟨yu, hymem⟩
+  have H : orderOf g = k := by
+    refine' Nat.dvd_antisymm (orderOf_dvd_of_pow_eq_one _) (Nat.lcm_dvd _ _)
+    · have := (mem_rootsOfUnity _ _).1 g.2
+      simp only [PNat.mk_coe] at this
+      exact_mod_cast this
+    · simp_rw [← hxuord, ← hnx, orderOf_pow]
+      exact Nat.div_dvd_of_dvd ((orderOf g).gcd_dvd_left nx)
+    · simp_rw [← hyuord, ← hny, orderOf_pow]
+      exact Nat.div_dvd_of_dvd ((orderOf g).gcd_dvd_left ny)
+  have hroot := IsPrimitiveRoot.orderOf g
+  rw [H, ← IsPrimitiveRoot.coe_submonoidClass_iff, ← IsPrimitiveRoot.coe_units_iff] at hroot
+  haveI := IsPrimitiveRoot.adjoin_isCyclotomicExtension K hroot
+  convert Submodule.finrank_le (Subalgebra.toSubmodule (Algebra.adjoin K ({g.1.1} : Set L)))
+  replace hirr : Irreducible (cyclotomic k K) := hirr
+  simpa using (IsCyclotomicExtension.finrank (Algebra.adjoin K ({g.1.1} : Set L)) hirr).symm
+
+variable (n) in
+/-- If a `n`-th cyclotomic extension of `ℚ` contains a primitive `l`-th root of unity, then
+`l ∣ 2 * n`. -/
+theorem _root_.IsPrimitiveRoot.dvd_of_isCyclotomicExtension [NumberField K]
+    [IsCyclotomicExtension {n} ℚ K] {ζ : K} {l : ℕ} (hζ : IsPrimitiveRoot ζ l) (hl : l ≠ 0) :
+    l ∣ 2 * n := by
+  have hl : NeZero l := ⟨hl⟩
+  have hroot := IsCyclotomicExtension.zeta_spec n ℚ K
+  have key := IsPrimitiveRoot.lcm_totient_le_finrank hζ hroot (cyclotomic.irreducible_rat
+    <| Nat.lcm_pos (Nat.pos_of_ne_zero hl.1) n.2)
+  rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat n.2)] at key
+  rcases _root_.dvd_lcm_right l n with ⟨r, hr⟩
+  have ineq := Nat.totient_super_multiplicative n r
+  rw [← hr] at ineq
+  replace key := (mul_le_iff_le_one_right (Nat.totient_pos n.2)).mp (le_trans ineq key)
+  have rpos : 0 < r := by
+    refine Nat.pos_of_ne_zero (fun h ↦ ?_)
+    simp only [h, mul_zero, _root_.lcm_eq_zero_iff, PNat.ne_zero, or_false] at hr
+    exact hl.1 hr
+  replace key := (Nat.dvd_prime Nat.prime_two).1 (Nat.totient_le_one_dvd_two rpos key)
+  rcases key with (key | key)
+  · rw [key, mul_one] at hr
+    rw [← hr]
+    exact dvd_mul_of_dvd_right (_root_.dvd_lcm_left l ↑n) 2
+  · rw [key, mul_comm] at hr
+    simpa [← hr] using _root_.dvd_lcm_left _ _
+
+/-- If `x` is a `k`-th root of unity in an `n`-th cyclotomic extension, where `n` is odd, and `ζ`
+is a primitive `n`-th root of unity, then there exist `r` such that `x = (-1)^r * ζ^r`. -/
+theorem _root_.IsPrimitiveRoot.exists_neg_pow_mul_pow_of_pow_eq_one [NumberField K]
+    [IsCyclotomicExtension {n} ℚ K] (hno : Odd (n : ℕ)) {ζ x : K} {k : ℕ+}
+    (hζ : IsPrimitiveRoot ζ n) (hx : x ^ (k : ℕ) = 1) : ∃ (r : ℕ), x = (-1) ^ r * ζ ^ r :=  by
+  have hnegζ : IsPrimitiveRoot (-ζ) (2 * n) := by
+    convert IsPrimitiveRoot.orderOf (-ζ)
+    rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
+    · simp [hζ.eq_orderOf]
+    · simp [← hζ.eq_orderOf, Nat.odd_iff_not_even.1 hno]
+  obtain ⟨l, hl, hlroot⟩ := (isRoot_of_unity_iff k.2 _).1 hx
+  have hlzero : NeZero l := ⟨fun h ↦ by simp [h] at hl⟩
+  have : NeZero (l : K) := ⟨NeZero.natCast_ne l K⟩
+  rw [isRoot_cyclotomic_iff] at hlroot
+  obtain ⟨a, ha⟩ := hlroot.dvd_of_isCyclotomicExtension n hlzero.1
+  replace hlroot : x ^ (2 * (n : ℕ)) = 1 := by rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
+  obtain ⟨s, -, hs⟩ := hnegζ.eq_pow_of_pow_eq_one hlroot (by simp)
+  rw [neg_pow] at hs
+  exact ⟨s, hs.symm⟩
+
 end IsCyclotomicExtension
 
 end NoOrder