import Verso import VersoManual import VersoBlueprint import Mathlib.Analysis.SpecialFunctions.Complex.Circle import Mathlib.RingTheory.RootsOfUnity.Complex import CliffordProject.LaTeXMacros import CliffordProject.Authors import CliffordProject.Bibliography open Verso.Genre open Verso.Genre.Manual hiding citep citet citehere open Informal #doc (Manual) "Roots of unity" => :::group "roots_of_unity" Roots of unity and their basic properties. ::: This section defines roots of unity and proves various basic facts about them. Throughout this section we assume that $`d ≥ 1`. ```lean "non_zero_dimension" variable (d : ℕ) [NeZero d] ``` :::lemma_ "d_invertible" (parent := "roots_of_unity") (effort := "small") (owner := "Maris_Ozols") $`d` is invertible in $`ℂ`. ::: :::proof "d_invertible" The inverse of $`d` exists since $`d ∈ ℕ` and $`d ≠ 0`. ::: ```lean "d_invertible" lemma d_invertible : IsUnit (d : ℂ) := by simp only [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero] exact NeZero.ne d ``` Define the primitive $`d`-th root of unity. :::definition "omega" (parent := "roots_of_unity") (owner := "Maris_Ozols") Let $`ω = \exp(2πi/d)` be the primitive $`d`-th root of unity. ::: ```lean "omega" noncomputable def ω : ℂ := Complex.exp (2 * Real.pi * Complex.I / d) ``` :::lemma_ "omega_ne_zero" (parent := "roots_of_unity") (effort := "small") (owner := "Carli_Bruinsma") $`ω ≠ 0`. ::: ```lean "omega_ne_zero" omit [NeZero d] in lemma omega_ne_zero : ω d ≠ 0 := by exact Complex.exp_ne_zero (2 * ↑Real.pi * Complex.I / ↑d) ``` :::lemma_ "omega_pow_d_eq_one" (parent := "roots_of_unity") (effort := "small") (owner := "Maris_Ozols") $`ω^d = 1`. ::: :::proof "omega_pow_d_eq_one" $`ω^d = (\exp(2πi/d))^d = \exp(d(2πi/d)) = \exp(2πi) = 1` where we could cancel $`d` since $`d ≠ 0`. ::: ```lean "omega_pow_d_eq_one" lemma omega_pow_d_eq_one : (ω d)^d = 1 := by unfold ω rw [← Complex.exp_nat_mul] rw [IsUnit.mul_div_cancel] · exact Complex.exp_two_pi_mul_I · exact d_invertible d ``` ```lean "order_omega" lemma order_omega : orderOf (ω d) = d := by refine orderOf_eq_of_pow_and_pow_div_prime ?_ ?_ ?_ exact Nat.pos_of_neZero d exact omega_pow_d_eq_one d intro p hp hpdivd unfold ω rw [← Complex.exp_nat_mul] rw [(Nat.cast_div hpdivd (Nat.cast_ne_zero.2 (Nat.Prime.ne_zero hp)))] rw [div_mul_div_comm] nth_rw 4 [mul_comm] rw [← div_mul_div_comm] --#check div_self (Nat.cast_ne_zero.2 (NeZero.ne d)) --rw [div_self, one_mul] rw [← (Nat.cast_div (dvd_refl d) (Nat.cast_ne_zero.2 (NeZero.ne d)))] simp only [dvd_refl, Nat.cast_div_charZero, div_self_of_invertible, one_mul, ne_eq] rw [← mul_one (2*Real.pi*Complex.I)] nth_rw 1 [← (Nat.cast_one (R:= ℂ )) ] by_contra hfalse exact ((Nat.Prime.not_dvd_one hp) (((Complex.exp_two_pi_mul_I_mul_div_eq_one_iff (Nat.Prime.ne_zero hp)).1 ) hfalse)) ``` This is an additional corrolary that is nice to have. :::lemma_ "omega_pow_n_mod_d" (parent := "roots_of_unity") (effort := "small") (owner := "Gina_Muuss") $`ω^n = ω^{n \mod d}`. ::: ```lean "omega_pow_n_mod_d" lemma omega_pow_n_mod_d : ∀ n : Nat, (ω d) ^ n = (ω d) ^ (n % d) := by intro n nth_rw 1 [←(Nat.mod_add_div n d)] rw [pow_add, pow_mul, omega_pow_d_eq_one, one_pow, mul_one] ``` ```lean "omega_pow_k_mod_d_eq_pow_k_int" lemma omega_pow_k_mod_d_eq_pow_k_int : ∀ k : Int, (ω d) ^ k = (ω d) ^ (k % d) := by intro k nth_rw 1 [← (Int.emod_add_ediv_mul k d)] rw [zpow_add'] nth_rw 2 [mul_comm] rw [zpow_mul] rw [zpow_natCast] rw [omega_pow_d_eq_one, one_zpow, mul_one] apply Or.inl unfold ω apply Complex.exp_ne_zero ``` ```lean "omega_pow_k_mod_d_eq_pow_k_zmod" lemma omega_pow_k_mod_d_eq_pow_k_zmod : ∀ k : Int, (ω d) ^ k = (ω d) ^ (k : ZMod d).val := by intro k rw [omega_pow_k_mod_d_eq_pow_k_int] rw [(Eq.symm (ZMod.val_intCast k))] exact zpow_natCast (ω d) (k : ZMod d).val ``` We will also need another root of unity which we call $`τ`. :::definition "tau" (parent := "roots_of_unity") (owner := "Maris_Ozols") Let $`τ = -\exp(πi/d)`. ::: ```lean "tau" noncomputable def τ : ℂ := - Complex.exp (Real.pi * Complex.I / d) ``` :::lemma_ "tau_sq_eq_omega" (parent := "roots_of_unity") (effort := "small") (owner := "Christian_Schaffner") $`τ^2 = ω`. ::: :::proof "tau_sq_eq_omega" $`τ^2 = (-\exp(πi/d))^2 = (-1)^2 · (\exp(πi/d))^2 = 1 · \exp(2πi/d) = ω`. ::: ```lean "tau_sq_eq_omega" omit [NeZero d] in lemma tau_sq_eq_omega : (τ d)^2 = ω d := by unfold τ ω rw [neg_sq, ← Complex.exp_nat_mul] congr 1 push_cast ring ``` :::lemma_ "tau_pow_d_eq_one_of_odd" (parent := "roots_of_unity") (effort := "small") (owner := "Carli_Bruinsma") If $`d` is odd then $`τ^d = 1`. ::: :::proof "tau_pow_d_eq_one_of_odd" $`τ^d = (-\exp(πi/d))^d = (-1)^d · (\exp(πi/d))^d = (-1)^d · \exp(πi) = (-1)^d · (-1) = (-1)^{d+1} = 1` when $`d` is odd. ::: ```lean "tau_pow_d_eq_one_of_odd" lemma tau_pow_d_eq_one_of_odd (hodd : Odd d) : (τ d)^d = 1 := by unfold τ have C : (-1 : ℂ) ≠ 1 := by norm_num rw [neg_eq_neg_one_mul, mul_pow, (neg_one_pow_eq_neg_one_iff_odd C).mpr hodd, ← Complex.exp_nat_mul, ← mul_div_assoc, mul_comm (↑d : ℂ), mul_div_assoc, div_self (Nat.cast_ne_zero.mpr (NeZero.ne d)), mul_one, Complex.exp_pi_mul_I, neg_one_mul, neg_neg] ``` ```lean "tau_pow_d_eq_neg_one_of_even" lemma tau_pow_d_eq_neg_one_of_even (heven : Even d) : (τ d)^d = -1 := by unfold τ have C : (-1 : ℂ) ≠ 1 := by norm_num rw [neg_eq_neg_one_mul, mul_pow, (neg_one_pow_eq_one_iff_even C).mpr heven, one_mul, ← Complex.exp_nat_mul, ← mul_div_assoc, mul_comm, mul_div_assoc, div_self (Nat.cast_ne_zero.mpr (NeZero.ne d)), mul_one, Complex.exp_pi_mul_I] lemma tau_pow_d : τ d ^ d = (-1)^(d + 1) := by have C : (-1 : ℂ) ≠ 1 := by norm_num by_cases heven : Even d · rw [tau_pow_d_eq_neg_one_of_even d heven, (neg_one_pow_eq_neg_one_iff_odd C).mpr (Even.add_one heven)] · have hodd := Nat.not_even_iff_odd.mp heven rw [tau_pow_d_eq_one_of_odd d hodd, (neg_one_pow_eq_one_iff_even C).mpr (Odd.add_one hodd)] ``` :::lemma_ "tau_pow_d_sq_eq_one" (parent := "roots_of_unity") (effort := "small") (owner := "Maris_Ozols") $`τ^{d^2} = 1`. ::: :::proof "tau_pow_d_sq_eq_one" $`τ^{d^2} = (-\exp(πi/d))^{d^2} = (-1)^{d^2} · (-1)^d = (-1)^{d(d+1)} = 1` since either $`d` or $`d+1` is even. ::: ```lean "tau_pow_d_sq_eq_one" lemma tau_pow_d2_one : (τ d) ^ (d ^ 2) = 1 := by unfold τ rw [← neg_one_mul] rw [pow_two] rw [mul_pow] rw [← Complex.exp_nat_mul] rw [Nat.cast_mul] rw [mul_assoc] rw [IsUnit.mul_div_cancel] rw [Complex.exp_nat_mul] rw [Complex.exp_pi_mul_I] rw [← pow_add] rw [← mul_add_one] rw [neg_one_pow_eq_one_iff_even] exact Nat.even_mul_succ_self d · norm_num · exact d_invertible d ``` :::lemma_ "tau_ne_zero" (parent := "roots_of_unity") (effort := "small") (owner := "Carli_Bruinsma") $`τ ≠ 0`. ::: ```lean "tau_ne_zero" omit [NeZero d] in lemma tau_ne_zero : τ d ≠ 0 := by unfold τ apply neg_ne_zero.mp rw [neg_neg] exact Complex.exp_ne_zero (↑Real.pi * Complex.I / ↑d) ``` ```lean "zero_le_c_mod_d" lemma mod_d_nonneg (a : ℤ) : 0 ≤ a % ↑d := by apply Int.emod_nonneg exact Nat.cast_ne_zero.mpr (NeZero.ne d) ``` :::lemma_ "tau_pow_n_mod_d_odd" (parent := "roots_of_unity") (effort := "small") (owner := "Carli_Bruinsma") If $`d` is odd then $`τ^{n} = τ^{n \mod d}`. ::: ```lean "tau_pow_n_mod_d_odd" theorem tau_pow_n_mod_d_of_d_odd (n d : ℕ) (hodd : Odd d) [NeZero d] : τ d ^ n = τ d ^ (n % ↑d) := pow_eq_pow_mod n (tau_pow_d_eq_one_of_odd d hodd) ``` ```lean "tau_star" theorem tau_star (d : ℕ) (n : ℤ) [NeZero d] : star (τ d ^ n) = τ d ^ (-n) := by unfold τ rw [star_zpow₀, star_neg, RCLike.star_def, ← Complex.exp_conj] simp only [map_div₀, map_mul, Complex.conj_ofReal, Complex.conj_I, mul_neg, map_natCast, neg_inj] by_cases h : Even n . rw [h.neg_zpow, (even_neg.2 h).neg_zpow] rw [← Complex.exp_int_mul, ← Complex.exp_int_mul] rw [Int.cast_neg] ring_nf apply Int.not_even_iff_odd.1 at h rw [h.neg_zpow, (odd_neg.2 h).neg_zpow] rw [← Complex.exp_int_mul, ← Complex.exp_int_mul] rw [Int.cast_neg] ring_nf ```