feat(ring_theory/polynomial/cyclotomic): Möbius inversion formula for cyclotomic polynomials (#5192)

Proves Möbius inversion for functions to a `comm_group_with_zero`
Proves the Möbius inversion formula for cyclotomic polynomials

Author: awainverse

src/number_theory/arithmetic_function.lean

@@ -34,6 +34,7 @@ to form the Dirichlet ring.
  * `sum_eq_iff_sum_mul_moebius_eq` for functions to a `comm_ring`
  * `sum_eq_iff_sum_smul_moebius_eq` for functions to an `add_comm_group`
  * `prod_eq_iff_prod_pow_moebius_eq` for functions to a `comm_group`
+ * `prod_eq_iff_prod_pow_moebius_eq_of_nonzero` for functions to a `comm_group_with_zero`
 
 ## Notation
 The arithmetic functions `ζ` and `σ` have Greek letter names, which are localized notation in
@@ -845,6 +846,29 @@ theorem prod_eq_iff_prod_pow_moebius_eq [comm_group R] {f g : ℕ → R} :
     ∀ (n : ℕ), 0 < n → ∏ (x : ℕ × ℕ) in n.divisors_antidiagonal, g x.snd ^ (μ x.fst) = f n :=
 @sum_eq_iff_sum_smul_moebius_eq (additive R) _ _ _
 
+/-- Möbius inversion for functions to a `comm_group_with_zero`. -/
+theorem prod_eq_iff_prod_pow_moebius_eq_of_nonzero [comm_group_with_zero R] {f g : ℕ → R}
+  (hf : ∀ (n : ℕ), 0 < n → f n ≠ 0) (hg : ∀ (n : ℕ), 0 < n → g n ≠ 0) :
+  (∀ (n : ℕ), 0 < n → ∏ i in (n.divisors), f i = g n) ↔
+    ∀ (n : ℕ), 0 < n → ∏ (x : ℕ × ℕ) in n.divisors_antidiagonal, g x.snd ^ (μ x.fst) = f n :=
+begin
+  refine iff.trans (iff.trans (forall_congr (λ n, _)) (@prod_eq_iff_prod_pow_moebius_eq (units R) _
+    (λ n, if h : 0 < n then units.mk0 (f n) (hf n h) else 1)
+    (λ n, if h : 0 < n then units.mk0 (g n) (hg n h) else 1))) (forall_congr (λ n, _));
+  refine imp_congr_right (λ hn, _),
+  { dsimp,
+    rw [dif_pos hn, ← units.eq_iff, ← units.coe_hom_apply, monoid_hom.map_prod, units.coe_mk0,
+      prod_congr rfl _],
+    intros x hx,
+    rw [dif_pos (nat.pos_of_mem_divisors hx), units.coe_hom_apply, units.coe_mk0] },
+  { dsimp,
+    rw [dif_pos hn, ← units.eq_iff, ← units.coe_hom_apply, monoid_hom.map_prod, units.coe_mk0,
+      prod_congr rfl _],
+    intros x hx,
+    rw [dif_pos (nat.pos_of_mem_divisors (nat.snd_mem_divisors_of_mem_antidiagonal hx)),
+      units.coe_hom_apply, units.coe_gpow', units.coe_mk0] }
+end
+
 end special_functions
 end arithmetic_function
 end nat

src/ring_theory/polynomial/cyclotomic.lean

@@ -7,7 +7,7 @@ Author: Riccardo Brasca
 import field_theory.splitting_field
 import ring_theory.roots_of_unity
 import algebra.polynomial.big_operators
-import number_theory.divisors
+import number_theory.arithmetic_function
 import data.polynomial.lifts
 import analysis.complex.roots_of_unity
 
@@ -29,7 +29,9 @@ with coefficients in any ring `R`.
 * `int_coeff_of_cycl` : If there is a primitive `n`-th root of unity in `K`, then `cyclotomic' n K`
 comes from a polynomial with integer coefficients.
 * `deg_of_cyclotomic` : The degree of `cyclotomic n` is `totient n`.
-* `X_pow_sub_one_eq_prod_cycl` : `X ^ n - 1 = ∏ (cyclotomic i)`, where `i` divides `n`.
+* `prod_cyclotomic_eq_X_pow_sub_one` : `X ^ n - 1 = ∏ (cyclotomic i)`, where `i` divides `n`.
+* `cyclotomic_eq_prod_X_pow_sub_one_pow_moebius` : The Möbius inversion formula for
+  `cyclotomic n R` over an abstract fraction field for `polynomial R`.
 
 ## Implementation details
 
@@ -408,6 +410,30 @@ begin
   (λ i, cyclotomic i ℤ), integer]
 end
 
+section arithmetic_function
+open nat.arithmetic_function
+open_locale arithmetic_function
+
+/-- `cyclotomic n R` can be expressed as a product in a fraction field of `polynomial R`
+  using Möbius inversion. -/
+lemma cyclotomic_eq_prod_X_pow_sub_one_pow_moebius {n : ℕ} (hpos : 0 < n) (R : Type*) [comm_ring R]
+  [nontrivial R] {K : Type*} [field K] (f : fraction_map (polynomial R) K) :
+  f.to_map (cyclotomic n R) =
+    ∏ i in n.divisors_antidiagonal, (f.to_map (X ^ i.snd - 1)) ^ μ i.fst :=
+begin
+  have h : ∀ (n : ℕ), 0 < n →
+    ∏ i in nat.divisors n, f.to_map (cyclotomic i R) = f.to_map (X ^ n - 1),
+  { intros n hn,
+    rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, ring_hom.map_prod] },
+  rw (prod_eq_iff_prod_pow_moebius_eq_of_nonzero (λ n hn, _) (λ n hn, _)).1 h n hpos;
+  rw [ne.def, fraction_map.to_map_eq_zero_iff],
+  { apply cyclotomic_ne_zero },
+  { apply monic.ne_zero,
+    apply monic_X_pow_sub_C _ (ne_of_gt hn) }
+end
+
+end arithmetic_function
+
 /-- We have
 `cyclotomic n R = (X ^ k - 1) /ₘ (∏ i in nat.proper_divisors k, cyclotomic i K)`. -/
 lemma cyclotomic_eq_X_pow_sub_one_div {R : Type*} [comm_ring R] [nontrivial R] {n : ℕ}