# Roots of unity #

We define roots of unity in the context of an arbitrary commutative monoid, as a subgroup of the group of units.

## Main definitions #

- `rootsOfUnity n M`, for `n : ℕ` is the subgroup of the units of a commutative monoid `M` consisting of elements `x` that satisfy `x ^ n = 1`.

## Main results #

- `rootsOfUnity.isCyclic`: the roots of unity in an integral domain form a cyclic group.

## Implementation details #

It is desirable that `rootsOfUnity` is a subgroup, and it will mainly be applied to rings (e.g. the ring of integers in a number field) and fields. We therefore implement it as a subgroup of the units of a commutative monoid.

We have chosen to define `rootsOfUnity n` for `n : ℕ` and add a `[NeZero n]` typeclass assumption when we need `n` to be non-zero (which is the case for most interesting statements). Note that `rootsOfUnity 0 M` is the top subgroup of `Mˣ` (as the condition `ζ^0 = 1` is satisfied for all units).

source
def rootsOfUnity (k : ℕ) (M : Type u_7) [CommMonoid M] :
Subgroup M ˣ

`rootsOfUnity k M` is the subgroup of elements `m : Mˣ` that satisfy `m ^ k = 1`.

Equations

- rootsOfUnity k M = { carrier := {ζ : M ˣ | ζ ^ k = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source
@[simp]
theorem mem_rootsOfUnity {M : Type u_1} [CommMonoid M] (k : ℕ) (ζ : M ˣ) :
ζ ∈ rootsOfUnity k M ↔ ζ ^ k = 1
source
theorem mem_rootsOfUnity' {M : Type u_1} [CommMonoid M] (k : ℕ) (ζ : M ˣ) :
ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ k = 1

A variant of `mem_rootsOfUnity` using `ζ : Mˣ`.

source
@[simp]
theorem rootsOfUnity_one (M : Type u_7) [CommMonoid M] :
rootsOfUnity 1 M = ⊥
source
@[simp]
theorem rootsOfUnity_zero (M : Type u_7) [CommMonoid M] :
rootsOfUnity 0 M = ⊤
source
theorem rootsOfUnity.coe_injective {M : Type u_1} [CommMonoid M] {n : ℕ} :
Function.Injective fun (x : ↥(rootsOfUnity n M)) => ↑↑x
source
def rootsOfUnity.mkOfPowEq {M : Type u_1} [CommMonoid M] (ζ : M) {n : ℕ} [NeZero n] (h : ζ ^ n = 1) :
↥(rootsOfUnity n M)

Make an element of `rootsOfUnity` from a member of the base ring, and a proof that it has a positive power equal to one.

Equations

- rootsOfUnity.mkOfPowEq ζ h = ⟨Units.ofPowEqOne ζ n h ⋯, ⋯⟩

Instances For

source
@[simp]
theorem rootsOfUnity.val_mkOfPowEq_coe {M : Type u_1} [CommMonoid M] (ζ : M) {n : ℕ} [NeZero n] (h : ζ ^ n = 1) :
↑↑(mkOfPowEq ζ h) = ζ
source
@[simp]
theorem rootsOfUnity.coe_mkOfPowEq {M : Type u_1} [CommMonoid M] {ζ : M} {n : ℕ} [NeZero n] (h : ζ ^ n = 1) :
↑↑(mkOfPowEq ζ h) = ζ
source
theorem rootsOfUnity_le_of_dvd {M : Type u_1} [CommMonoid M] {k l : ℕ} (h : k ∣ l) :
rootsOfUnity k M ≤ rootsOfUnity l M
source
theorem map_rootsOfUnity {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommMonoid N] (f : M ˣ →* N ˣ) (k : ℕ) :
Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N
source
instance instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat {M : Type u_1} [CommMonoid M] :
Subsingleton ↥(rootsOfUnity 1 M)
source
theorem rootsOfUnity_inf_rootsOfUnity {M : Type u_1} [CommMonoid M] {m n : ℕ} :
rootsOfUnity m M ⊓ rootsOfUnity n M = rootsOfUnity (m.gcd n) M
source
theorem disjoint_rootsOfUnity_of_coprime {M : Type u_1} [CommMonoid M] {m n : ℕ} (h : m.Coprime n) :
Disjoint (rootsOfUnity m M) (rootsOfUnity n M)
source
theorem rootsOfUnity.coe_pow {R : Type u_4} {k : ℕ} [CommMonoid R] (ζ : ↥(rootsOfUnity k R)) (m : ℕ) :
↑↑(ζ ^ m) = ↑↑ζ ^ m
source
def rootsOfUnityUnitsMulEquiv (M : Type u_7) [CommMonoid M] (n : ℕ) :
↥(rootsOfUnity n M ˣ) ≃* ↥(rootsOfUnity n M)

The canonical isomorphism from the `n`th roots of unity in `Mˣ` to the `n`th roots of unity in `M`.

Equations

- rootsOfUnityUnitsMulEquiv M n = { toFun := fun (ζ : ↥(rootsOfUnity n M ˣ)) => ⟨↑↑ζ, ⋯⟩, invFun := fun (ζ : ↥(rootsOfUnity n M)) => ⟨toUnits ↑ζ, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
def restrictRootsOfUnity {R : Type u_4} {S : Type u_5} {F : Type u_6} [CommMonoid R] [CommMonoid S] [FunLike F R S] [MonoidHomClass F R S] (σ : F) (n : ℕ) :
↥(rootsOfUnity n R) →* ↥(rootsOfUnity n S)

Restrict a ring homomorphism to the nth roots of unity.

Equations

- restrictRootsOfUnity σ n = { toFun := fun (ξ : ↥(rootsOfUnity n R)) => ⟨(Units.map ↑σ) ↑ξ, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem restrictRootsOfUnity_coe_apply {R : Type u_4} {S : Type u_5} {F : Type u_6} {k : ℕ} [CommMonoid R] [CommMonoid S] [FunLike F R S] [MonoidHomClass F R S] (σ : F) (ζ : ↥(rootsOfUnity k R)) :
↑↑((restrictRootsOfUnity σ k) ζ) = σ ↑↑ζ
source
def MulEquiv.restrictRootsOfUnity {R : Type u_4} {S : Type u_5} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) (n : ℕ) :
↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n S)

Restrict a monoid isomorphism to the nth roots of unity.

Equations

- σ.restrictRootsOfUnity n = { toFun := ⇑(restrictRootsOfUnity σ n), invFun := ⇑(restrictRootsOfUnity σ.symm n), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem MulEquiv.restrictRootsOfUnity_coe_apply {R : Type u_4} {S : Type u_5} {k : ℕ} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) (ζ : ↥(rootsOfUnity k R)) :
↑↑((σ.restrictRootsOfUnity k) ζ) = σ ↑↑ζ
source
@[simp]
theorem MulEquiv.restrictRootsOfUnity_symm {R : Type u_4} {S : Type u_5} {k : ℕ} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) :
(σ.restrictRootsOfUnity k).symm = σ.symm.restrictRootsOfUnity k
source
@[simp]
theorem Units.val_set_image_rootsOfUnity {R : Type u_4} {k : ℕ} [CommMonoid R] [NeZero k] :
val '' ↑(rootsOfUnity k R) = {z : R | z ^ k = 1}
source
theorem Units.val_set_image_rootsOfUnity_one {R : Type u_4} [CommMonoid R] :
val '' ↑(rootsOfUnity 1 R) = {1}
source
theorem Units.val_set_image_rootsOfUnity_two {R : Type u_4} [CommRing R] [NoZeroDivisors R] :
val '' ↑(rootsOfUnity 2 R) = {1, -1}
source
theorem mem_rootsOfUnity_iff_mem_nthRoots {R : Type u_4} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] {ζ : R ˣ} :
ζ ∈ rootsOfUnity k R ↔ ↑ζ ∈ Polynomial.nthRoots k 1
source
def rootsOfUnityEquivNthRoots (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] :
↥(rootsOfUnity k R) ≃ { x : R // x ∈ Polynomial.nthRoots k 1 }

Equivalence between the `k`-th roots of unity in `R` and the `k`-th roots of `1`.

This is implemented as equivalence of subtypes, because `rootsOfUnity` is a subgroup of the group of units, whereas `nthRoots` is a multiset.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem rootsOfUnityEquivNthRoots_apply {R : Type u_4} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] (x : ↥(rootsOfUnity k R)) :
↑((rootsOfUnityEquivNthRoots R k) x) = ↑↑x
source
@[simp]
theorem rootsOfUnityEquivNthRoots_symm_apply {R : Type u_4} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] (x : { x : R // x ∈ Polynomial.nthRoots k 1 }) :
↑↑((rootsOfUnityEquivNthRoots R k).symm x) = ↑x
source
instance rootsOfUnity.fintype (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] :
Fintype ↥(rootsOfUnity k R)
Equations

- rootsOfUnity.fintype R k = Fintype.ofEquiv { x : R // x ∈ Polynomial.nthRoots k 1 } (rootsOfUnityEquivNthRoots R k).symm

source
instance rootsOfUnity.isCyclic (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] :
IsCyclic ↥(rootsOfUnity k R)
source
theorem card_rootsOfUnity (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] :
Fintype.card ↥(rootsOfUnity k R) ≤ k
source
theorem map_rootsOfUnity_eq_pow_self {R : Type u_4} {F : Type u_6} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] [FunLike F R R] [MonoidHomClass F R R] (σ : F) (ζ : ↥(rootsOfUnity k R)) :
∃ (m : ℕ), σ ↑↑ζ = ↑↑ζ ^ m
source
theorem mem_rootsOfUnity_prime_pow_mul_iff (R : Type u_4) [CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] {ζ : R ˣ} :
ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R
source
@[simp]
theorem mem_rootsOfUnity_prime_pow_mul_iff' (R : Type u_4) [CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] {ζ : R ˣ} :
ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R

A variant of `mem_rootsOfUnity_prime_pow_mul_iff` in terms of `ζ ^ _`

source
noncomputable def IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator {G : Type u_7} [CommGroup G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (G' : Type u_8) [CommGroup G'] :
(G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G')

The isomorphism from the group of group homomorphisms from a finite cyclic group `G` of order `n` into another group `G'` to the group of `n`th roots of unity in `G'` determined by a generator `g` of `G`. It sends `φ : G →* G'` to `φ g`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem IsCyclic.monoidHom_mulEquiv_rootsOfUnity (G : Type u_7) [CommGroup G] [IsCyclic G] (G' : Type u_8) [CommGroup G'] :
Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

The group of group homomorphisms from a finite cyclic group `G` of order `n` into another group `G'` is (noncanonically) isomorphic to the group of `n`th roots of unity in `G'`.