Roots of unity and primitive roots of unity #
We define roots of unity in the context of an arbitrary commutative monoid,
as a subgroup of the group of units. We also define a predicate is_primitive_root
on commutative
monoids, expressing that an element is a primitive root of unity.
Main definitions #
roots_of_unity n M
, forn : ℕ+
is the subgroup of the units of a commutative monoidM
consisting of elementsx
that satisfyx ^ n = 1
.is_primitive_root ζ k
: an elementζ
is a primitivek
-th root of unity ifζ ^ k = 1
, and ifl
satisfiesζ ^ l = 1
thenk ∣ l
.primitive_roots k R
: the finset of primitivek
-th roots of unity in an integral domainR
.is_primitive_root.aut_to_pow
: the monoid hom that takes an automorphism of a ring to the power it sends that specific primitive root, as a member of(zmod n)ˣ
.
Main results #
roots_of_unity.is_cyclic
: the roots of unity in an integral domain form a cyclic group.is_primitive_root.zmod_equiv_zpowers
:zmod k
is equivalent to the subgroup generated by a primitivek
-th root of unity.is_primitive_root.zpowers_eq
: in an integral domain, the subgroup generated by a primitivek
-th root of unity is equal to thek
-th roots of unity.is_primitive_root.card_primitive_roots
: if an integral domain has a primitivek
-th root of unity, then it hasφ k
of them.
Implementation details #
It is desirable that roots_of_unity
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 roots_of_unity n
for n : ℕ+
, instead of n : ℕ
,
because almost all lemmas need the positivity assumption,
and in particular the type class instances for fintype
and is_cyclic
.
On the other hand, for primitive roots of unity, it is desirable to have a predicate
not just on units, but directly on elements of the ring/field.
For example, we want to say that exp (2 * pi * I / n)
is a primitive n
-th root of unity
in the complex numbers, without having to turn that number into a unit first.
This creates a little bit of friction, but lemmas like is_primitive_root.is_unit
and
is_primitive_root.coe_units_iff
should provide the necessary glue.
roots_of_unity k M
is the subgroup of elements m : Mˣ
that satisfy m ^ k = 1
Equations
Instances for ↥roots_of_unity
Make an element of roots_of_unity
from a member of the base ring, and a proof that it has
a positive power equal to one.
Equations
- roots_of_unity.mk_of_pow_eq ζ h = ⟨units.mk_of_mul_eq_one ζ (ζ ^ n.nat_pred) _, _⟩
Restrict a ring homomorphism to the nth roots of unity
Equations
- restrict_roots_of_unity σ n = let h : ∀ (ξ : ↥(roots_of_unity n R)), ⇑σ ↑ξ ^ ↑n = 1 := _ in {to_fun := λ (ξ : ↥(roots_of_unity n R)), ⟨unit_of_invertible (⇑σ ↑ξ) (invertible_of_pow_eq_one (⇑σ ↑ξ) ↑n _ _), _⟩, map_one' := _, map_mul' := _}
Restrict a ring isomorphism to the nth roots of unity
Equations
- σ.restrict_roots_of_unity n = {to_fun := ⇑(restrict_roots_of_unity σ.to_ring_hom n), inv_fun := ⇑(restrict_roots_of_unity σ.symm.to_ring_hom n), left_inv := _, right_inv := _, map_mul' := _}
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 roots_of_unity
is a subgroup of the group of units,
whereas nth_roots
is a multiset.
Equations
- roots_of_unity.fintype R k = fintype.of_equiv {x // x ∈ polynomial.nth_roots ↑k 1} (roots_of_unity_equiv_nth_roots R k).symm
An element ζ
is a primitive k
-th root of unity if ζ ^ k = 1
,
and if l
satisfies ζ ^ l = 1
then k ∣ l
.
Turn a primitive root μ into a member of the roots_of_unity
subgroup.
Equations
primitive_roots k R
is the finset of primitive k
-th roots of unity
in the integral domain R
.
Equations
- primitive_roots k R = finset.filter (λ (ζ : R), is_primitive_root ζ k) (polynomial.nth_roots k 1).to_finset
If there is a n
-th primitive root of unity in R
and b
divides n
,
then there is a b
-th primitive root of unity in R
.
The (additive) monoid equivalence between zmod k
and the powers of a primitive root of unity ζ
.
Equations
- h.zmod_equiv_zpowers = add_equiv.of_bijective (⇑((int.cast_add_hom (zmod k)).lift_of_right_inverse coe zmod.int_cast_right_inverse) ⟨{to_fun := λ (i : ℤ), ⇑additive.of_mul ⟨ζ ^ i, _⟩, map_zero' := _, map_add' := _}, _⟩) _
The cardinality of the multiset nth_roots ↑n (1 : R)
is n
if there is a primitive root of unity in R
.
The multiset nth_roots ↑n (1 : R)
has no repeated elements
if there is a primitive root of unity in R
.
If an integral domain has a primitive k
-th root of unity, then it has φ k
of them.
The sets primitive_roots k R
are pairwise disjoint.
nth_roots n
as a finset
is equal to the union of primitive_roots i R
for i ∣ n
if there is a primitive root of unity in R
.
This holds for any nat
, not just pnat
, see nth_roots_one_eq_bUnion_primitive_roots
.
nth_roots n
as a finset
is equal to the union of primitive_roots i R
for i ∣ n
if there is a primitive root of unity in R
.
μ
is integral over ℤ
.
The minimal polynomial of a root of unity μ
divides X ^ n - 1
.
The reduction modulo p
of the minimal polynomial of a root of unity μ
is separable.
The reduction modulo p
of the minimal polynomial of a root of unity μ
is squarefree.
If p
is a prime that does not divide n
,
then the minimal polynomials of a primitive n
-th root of unity μ
and of μ ^ p
are the same.
If m : ℕ
is coprime with n
,
then the minimal polynomials of a primitive n
-th root of unity μ
and of μ ^ m
are the same.
If m : ℕ
is coprime with n
,
then the minimal polynomial of a primitive n
-th root of unity μ
has μ ^ m
as root.
primitive_roots n K
is a subset of the roots of the minimal polynomial of a primitive
n
-th root of unity μ
.
The degree of the minimal polynomial of μ
is at least totient n
.
The monoid_hom
that takes an automorphism to the power of μ that μ gets mapped to under it.
Equations
- is_primitive_root.aut_to_pow R hμ = let μ' : ↥(roots_of_unity n S) := hμ.to_roots_of_unity in have ho : order_of μ' = ↑n, from _, {to_fun := λ (σ : S ≃ₐ[R] S), ↑(_.some), map_one' := _, map_mul' := _}.to_hom_units