Commutative monoids with enough roots of unity

We define a typeclass HasEnoughRootsOfUnity M n for a commutative monoid M and a natural number n that asserts that M contains a primitive nth root of unity and that the group of nth roots of unity in M is cyclic. Such monoids are suitable targets for homomorphisms from groups of exponent (dividing) n; for example, the homomorphisms can then be used to separate elements of the source group.

class HasEnoughRootsOfUnity (M : Type u_1) [CommMonoid M] (n : ℕ) : Prop

This is a type class recording that a commutative monoid M contains primitive nth roots of unity and such that the group of nth roots of unity is cyclic.

Such monoids are suitable targets in the context of duality statements for groups of exponent n.

• prim : ∃ (m : M), IsPrimitiveRoot m n
• cyc : IsCyclic ↥(rootsOfUnity n M)

theorem HasEnoughRootsOfUnity.exists_primitiveRoot (M : Type u_1) [CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n] : ∃ (ζ : M), IsPrimitiveRoot ζ n

instance HasEnoughRootsOfUnity.rootsOfUnity_isCyclic (M : Type u_1) [CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n] : IsCyclic ↥(rootsOfUnity n M)

theorem HasEnoughRootsOfUnity.of_dvd (M : Type u_1) [CommMonoid M] {m n : ℕ} [NeZero n] (hmn : m ∣ n) [HasEnoughRootsOfUnity M n] : HasEnoughRootsOfUnity M m

If HasEnoughRootsOfUnity M n and m ∣ n, then also HasEnoughRootsOfUnity M m.

instance HasEnoughRootsOfUnity.finite_rootsOfUnity (M : Type u_1) [CommMonoid M] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity M n] : Finite ↥(rootsOfUnity n M)

If M satisfies HasEnoughRootsOfUnity, then the group of nth roots of unity in M is finite.

theorem HasEnoughRootsOfUnity.natCard_rootsOfUnity (M : Type u_1) [CommMonoid M] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity M n] : Nat.card ↥(rootsOfUnity n M) = n

If M satisfies HasEnoughRootsOfUnity, then the group of nth roots of unity in M (is cyclic and) has order n.

theorem IsCyclic.monoidHom_equiv_self (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [IsCyclic G] [CommMonoid M] [HasEnoughRootsOfUnity M (Nat.card G)] : Nonempty ((G →* Mˣ) ≃* G)

The group of group homomorphims from a finite cyclic group G of order n into the group of units of a ring M with all roots of unity is isomorphic to G