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.

@[simp]

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

theorem rootsOfUnity_eq_ker {M : Type u_1} [CommMonoid M] {k : ℕ} : rootsOfUnity k M = (powMonoidHom k).ker

theorem ker_zpowGroupHom_eq_rootsOfUnity {M : Type u_1} [CommMonoid M] {k : ℤ} : (zpowGroupHom k).ker = rootsOfUnity k.natAbs M

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.

@[simp]

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

@[simp]

theorem rootsOfUnity.coe_mkOfPowEq {M : Type u_1} [CommMonoid M] {ζ : M} {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : ↑↑(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

instance instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat {M : Type u_1} [CommMonoid M] : Subsingleton ↥(rootsOfUnity 1 M)

theorem rootsOfUnity_inf_rootsOfUnity {M : Type u_1} [CommMonoid M] {m n : ℕ} : rootsOfUnity m M ⊓ rootsOfUnity n M = rootsOfUnity (m.gcd n) M

theorem disjoint_rootsOfUnity_of_coprime {M : Type u_1} [CommMonoid M] {m n : ℕ} (h : m.Coprime n) : Disjoint (rootsOfUnity m M) (rootsOfUnity n M)

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.

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.

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

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

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

theorem Units.val_set_image_rootsOfUnity_one {R : Type u_4} [CommMonoid R] : val '' ↑(rootsOfUnity 1 R) = {1}

theorem Units.val_set_image_rootsOfUnity_two {R : Type u_4} [CommRing R] [NoZeroDivisors R] : val '' ↑(rootsOfUnity 2 R) = {1, -1}

theorem mem_rootsOfUnity_iff_isRoot {R : Type u_4} [CommRing R] (k : ℕ) (ζ : Rˣ) : ζ ∈ rootsOfUnity k R ↔ (Polynomial.X ^ k - 1).IsRoot ↑ζ

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.

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

@[implicit_reducible]

noncomputable instance rootsOfUnity.fintype (R : Type u_4) (k : ℕ) [NeZero k] [CommRing R] [IsDomain R] : Fintype ↥(rootsOfUnity k R)

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

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

instance instFiniteMonoidHomUnits {R : Type u_4} [CommRing R] [IsDomain R] {L : Type u_7} [LeftCancelMonoid L] [Finite L] : Finite (L →* Rˣ)

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 ζ ^ _

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 nth roots of unity in G' determined by a generator g of G. It sends φ : G →* G' to φ g.

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 nth roots of unity in G'.