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
IsPrimitiveRoot on commutative
monoids, expressing that an element is a primitive root of unity.
Main definitions #
rootsOfUnity n M, for
n : ℕ+is the subgroup of the units of a commutative monoid
Mconsisting of elements
x ^ n = 1.
IsPrimitiveRoot ζ k: an element
ζis a primitive
k-th root of unity if
ζ ^ k = 1, and if
ζ ^ l = 1then
k ∣ l.
primitiveRoots k R: the finset of primitive
k-th roots of unity in an integral domain
IsPrimitiveRoot.autToPow: the monoid hom that takes an automorphism of a ring to the power it sends that specific primitive root, as a member of
Main results #
rootsOfUnity.isCyclic: the roots of unity in an integral domain form a cyclic group.
ZMod kis equivalent to the subgroup generated by a primitive
k-th root of unity.
IsPrimitiveRoot.zpowers_eq: in an integral domain, the subgroup generated by a primitive
k-th root of unity is equal to the
k-th roots of unity.
IsPrimitiveRoot.card_primitiveRoots: if an integral domain has a primitive
k-th root of unity, then it has
φ kof them.
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.
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.
Equivalence between the
k-th roots of unity in
R and the
k-th roots of
This is implemented as equivalence of subtypes,
rootsOfUnity is a subgroup of the group of units,
nthRoots is a multiset.
nthRoots n as a
Finset is equal to the union of
primitiveRoots i R for
i ∣ n
if there is a primitive root of unity in
This holds for any
Nat, not just
MonoidHom that takes an automorphism to the power of μ that μ gets mapped to under it.