Documentation

Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

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.

source
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.

Instances
    source
    theorem HasEnoughRootsOfUnity.exists_primitiveRoot (M : Type u_1) [CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n] :
    ∃ (ζ : M), IsPrimitiveRoot ζ n
    source
    instance HasEnoughRootsOfUnity.rootsOfUnity_isCyclic (M : Type u_1) [CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n] :
    IsCyclic ↥(rootsOfUnity n M)
    source
    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.

    source
    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.

    source
    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.

    source
    theorem HasEnoughRootsOfUnity.of_card_le {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} [NeZero n] (h : n ≤ Fintype.card ↥(rootsOfUnity n R)) :
    HasEnoughRootsOfUnity R n
    source
    theorem MulEquiv.hasEnoughRootsOfUnity {n : ℕ} [NeZero n] {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommMonoid N] [hm : HasEnoughRootsOfUnity M n] (e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)) :
    HasEnoughRootsOfUnity N n
    source
    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 homomorphisms 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

    source
    instance instHasEnoughRootsOfUnityOfNatNat {M : Type u_1} [CommMonoid M] :
    HasEnoughRootsOfUnity M 1