Documentation

Mathlib.RingTheory.RootsOfUnity.Basic

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 #

Main results #

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 (as the condition ζ^0 = 1 is satisfied for all units).

def rootsOfUnity (k : ) (M : Type u_7) [CommMonoid M] :

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

Equations
@[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] :
@[simp]
theorem rootsOfUnity_zero (M : Type u_7) [CommMonoid 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
@[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) :
theorem map_rootsOfUnity {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommMonoid N] (f : Mˣ →* Nˣ) (k : ) :
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 to the nth roots of unity in M.

Equations
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
@[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
@[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]
def rootsOfUnityEquivNthRoots (R : Type u_4) (k : ) [NeZero k] [CommRing R] [IsDomain R] :

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.isCyclic (R : Type u_4) (k : ) [NeZero k] [CommRing R] [IsDomain R] :
theorem card_rootsOfUnity (R : Type u_4) (k : ) [NeZero k] [CommRing R] [IsDomain R] :
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
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.

Equations
  • One or more equations did not get rendered due to their size.
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'.