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).

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' := ⋯ }

@[simp]

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

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

A variant of mem_rootsOfUnity using ζ : M.

@[simp]

theorem rootsOfUnity_one (M : Type u_7) [CommMonoid M] : rootsOfUnity 1 M = ⊥

@[simp]

theorem rootsOfUnity_zero (M : Type u_7) [CommMonoid M] : rootsOfUnity 0 M = ⊤

theorem rootsOfUnity.coe_injective {M : Type u_1} [CommMonoid M] {n : ℕ} : Function.Injective fun (x : ↥(rootsOfUnity n M)) => ↑↑x

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 ⋯, ⋯⟩

@[simp]

theorem rootsOfUnity.val_mkOfPowEq_coe {M : Type u_1} [CommMonoid M] (ζ : M) {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : ↑↑(rootsOfUnity.mkOfPowEq ζ h) = ζ

@[simp]

theorem rootsOfUnity.coe_mkOfPowEq {M : Type u_1} [CommMonoid M] {ζ : M} {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : ↑↑(rootsOfUnity.mkOfPowEq ζ h) = ζ

theorem rootsOfUnity_le_of_dvd {M : Type u_1} [CommMonoid M] {k : ℕ} {l : ℕ} (h : k ∣ l) : rootsOfUnity k M ≤ rootsOfUnity l M

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

theorem rootsOfUnity.coe_pow {R : Type u_4} {k : ℕ} [CommMonoid R] (ζ : ↥(rootsOfUnity k R)) (m : ℕ) : ↑↑(ζ ^ m) = ↑↑ζ ^ m

def rootsOfUnityUnitsMulEquiv (M : Type u_7) [CommMonoid M] (n : ℕ) : ↥(rootsOfUnity n Mˣ) ≃* ↥(rootsOfUnity n M)

The canonical isomorphism from the nth roots of unity in Mˣ to the nth 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' := ⋯ }

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' := ⋯ }

@[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) ζ) = σ ↑↑ζ

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' := ⋯ }

@[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) ζ) = σ ↑↑ζ

@[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

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

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.

@[simp]

theorem rootsOfUnityEquivNthRoots_apply {R : Type u_4} {k : ℕ} [NeZero k] [CommRing R] [IsDomain R] (x : ↥(rootsOfUnity k R)) : ↑((rootsOfUnityEquivNthRoots R k) x) = ↑↑x

@[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

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

instance rootsOfUnity.isCyclic (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] : IsCyclic ↥(rootsOfUnity k R)

Equations

• ⋯ = ⋯

theorem card_rootsOfUnity (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] : Fintype.card ↥(rootsOfUnity k R) ≤ k

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] [RingHomClass F R R] (σ : F) (ζ : ↥(rootsOfUnity k R)) : ∃ (m : ℕ), σ ↑↑ζ = ↑↑ζ ^ m

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

@[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 ζ ^ _.