2. Roots of unity🔗

This section defines roots of unity and proves various basic facts about them. Throughout this section we assume that d ≥ 1.

Lean code

-- This instance is referred to later, needs naming
variable (d : ℕ) [hnezero : NeZero d]

Lemma2.1

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Definition 2.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Owner

Maris OzolsEffortsmall

d is invertible in ℂ.

Proof for Lemma 2.1

uses 0

The inverse of d exists since d ∈ ℕ and d ≠ 0.

Lean code for Lemma2.1

lemma d_invertible : IsUnit (d : ℂ) := byd:ℕhnezero:NeZero d⊢ IsUnit ↑d
  simp only [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]d:ℕhnezero:NeZero d⊢ ¬d = 0
  exact NeZero.ne dAll goals completed! 🐙

Define the primitive d-th root of unity.

Definition2.2

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 3

Reverse dependency previews

Preview

Definition 4.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Owner

Maris Ozols

Let ω = \exp(2πi/d) be the primitive d-th root of unity.

Some basic lemmas about \omega

Lemma2.3

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Owner

William HasleyEffortsmall

When d = 1, \omega = 1

Lean code for Lemma2.3

@[simp]
lemma omega_one : (ω 1) = 1 := by⊢ ω 1 = 1
  ext⊢ ↑(ω 1) = ↑1; unfold ω⊢ ↑{ val := Complex.exp (2 * ↑Real.pi * Complex.I / ↑1), inv := Complex.exp (-2 * ↑Real.pi * Complex.I / ↑1),
      val_inv := ⋯, inv_val := ⋯ } =
  ↑1; simpAll goals completed! 🐙;

omit [NeZero d] in
@[simp]
lemma omega_one' (hd : d = 1) : ω d = 1 := byd:ℕhd:d = 1⊢ ω d = 1
  rw[hdd:ℕhd:d = 1⊢ ω 1 = 1]d:ℕhd:d = 1⊢ ω 1 = 1; simpAll goals completed! 🐙

Lean code

omit [NeZero d] in
lemma omega_val_pow_commutes (i : ℕ) : ((ω d) ^ i).val = (ω d).val ^ i
  := byd:ℕi:ℕ⊢ ↑(ω d ^ i) = ↑(ω d) ^ i simpAll goals completed! 🐙

Lemma2.4

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Owner

Maris OzolsEffortsmall

ω^d = 1.

Proof for Lemma 2.4

uses 0

ω^d = (\exp(2πi/d))^d = \exp(d(2πi/d)) = \exp(2πi) = 1 where we could cancel d since d ≠ 0.

Lemma2.5

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Owner

William HasleyEffortsmall

Let i ∈ ℤ, then \left(\omega^{-1}\right)^i = \omega^{d - i}

Lean code for Lemma2.5

omit [NeZero d] in
lemma omega_pow_of_inv (i : ℤ) : (ω d)⁻¹ ^ i = (ω d) ^ (-i)
  := byd:ℕi:ℤ⊢ (ω d)⁻¹ ^ i = ω d ^ (-i) rw[zpow_negd:ℕi:ℤ⊢ (ω d)⁻¹ ^ i = (ω d ^ i)⁻¹]d:ℕi:ℤ⊢ (ω d)⁻¹ ^ i = (ω d ^ i)⁻¹; simpAll goals completed! 🐙

Lemma2.6

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Owner

William HasleyEffortsmall

Let i ∈ ℤ_d, then \left(\omega^{i}\right)^{-1} = \omega^{-i}

Lemma2.7

uses 0used by 0✓L∃∀N

For z ∈ \mathbb{C}, let z^* denote the usual complex conjugate of z. Then \omega^* = \omega^{-1}

This is an additional corrolary that is nice to have.

Lemma2.8

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

OwnerGina MuussEffortsmall

ω^n = ω^{n \mod d}.

Lean code

lemma omega_pow_k_mod_d_eq_pow_k_zmod :
  ∀ k : ℤ, (ω d) ^ k = (ω d) ^ (k : ZMod d).val := byd:ℕhnezero:NeZero d⊢ ∀ (k : ℤ), ω d ^ k = ω d ^ (↑k).val
    intro kd:ℕhnezero:NeZero dk:ℤ⊢ ω d ^ k = ω d ^ (↑k).val
    rw [omega_pow_k_mod_d_eq_pow_k_intd:ℕhnezero:NeZero dk:ℤ⊢ ω d ^ (k % ↑d) = ω d ^ (↑k).val]d:ℕhnezero:NeZero dk:ℤ⊢ ω d ^ (k % ↑d) = ω d ^ (↑k).val
    rw [(Eq.symm (ZMod.val_intCast k))d:ℕhnezero:NeZero dk:ℤ⊢ ω d ^ ↑(↑k).val = ω d ^ (↑k).val]d:ℕhnezero:NeZero dk:ℤ⊢ ω d ^ ↑(↑k).val = ω d ^ (↑k).val
    exact zpow_natCast (ω d) (k : ZMod d).valAll goals completed! 🐙

We will also need another root of unity which we call τ.

Definition2.9

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 3

Reverse dependency previews

Preview

Definition 5.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Owner

Maris Ozols

Let τ = -\exp(πi/d).

Some basic lemmas about \tau

Lemma2.10

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0XL∃∀N

Owner

William HasleyEffortsmall

Much like \omega, since τ lies on the Unit circle, one has \tau^* = \tau^{-1}

Lemma2.11

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 7.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Owner

Christian SchaffnerEffortsmall

τ^2 = ω.

Proof for Lemma 2.11

uses 0

τ^2 = (-\exp(πi/d))^2 = (-1)^2 · (\exp(πi/d))^2 = 1 · \exp(2πi/d) = ω.

Lemma2.12

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Owner

Carli BruinsmaEffortsmall

If d is odd then τ^d = 1.

Proof for Lemma 2.12

uses 0

τ^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.

Lemma2.13

Group: Roots of unity and their basic properties. (11)

Group member previews

Preview

Lemma 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Owner

Maris OzolsEffortsmall

τ^{d^2} = 1.

Proof for Lemma 2.13

uses 0

τ^{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 code

lemma mod_d_nonneg (a : ℤ) : 0 ≤ a % ↑d := byd:ℕhnezero:NeZero da:ℤ⊢ 0 ≤ a % ↑d
    apply Int.emod_nonnegd:ℕhnezero:NeZero da:ℤ⊢ ↑d ≠ 0
    exact Nat.cast_ne_zero.mpr (NeZero.ne d)All goals completed! 🐙

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)