Characters of a cyclic group read off a ZMod coordinate

A group H presented as cyclic of order m by a coordinate e : H ≃* Multiplicative (ZMod m) has its characters named by the m-th roots of unity: the character attached to ζ sends the element with coordinate i to ζ ^ i. This file reads Mathlib's AddChar.zmodChar through such a coordinate to get MulEquiv.zmodCoordChar, and shows that a primitive root of unity gives a faithful character.

The coordinate is data, not merely the existence of IsCyclic H: the character depends on which generator e names, a different coordinate permuting the characters among themselves. Concrete cyclic subgroups come with a preferred coordinate -- the rotation subgroup of a dihedral or a generalized quaternion group, for instance -- and the characters used there are the specializations of this one.

Main definitions

• MulEquiv.zmodCoordChar: the character sending the element with coordinate i to ζ ^ i, for ζ an m-th root of unity.

Main results

• MulEquiv.zmodCoordChar_injective: the character attached to a primitive m-th root of unity is faithful.

def MulEquiv.zmodCoordChar {H : Type u_1} {M : Type u_2} [Group H] [CommMonoid M] {m : ℕ} [NeZero m] {ζ : M} (e : H ≃* Multiplicative (ZMod m)) (hζ : ζ ^ m = 1) : H →* M

The character of a cyclic group attached to an m-th root of unity ζ, read off a coordinate e : H ≃* Multiplicative (ZMod m): the element with coordinate i is sent to ζ ^ i, the exponent being the canonical representative of i in ZMod m. It is Mathlib's AddChar.zmodChar composed with e.

Equations

• e.zmodCoordChar hζ = (AddChar.toMonoidHomEquiv (AddChar.zmodChar m hζ)).comp e.toMonoidHom

@[simp]

theorem MulEquiv.zmodCoordChar_apply {H : Type u_1} {M : Type u_2} [Group H] [CommMonoid M] {m : ℕ} [NeZero m] {ζ : M} (e : H ≃* Multiplicative (ZMod m)) (hζ : ζ ^ m = 1) (x : H) : (e.zmodCoordChar hζ) x = ζ ^ (Multiplicative.toAdd (e x)).val

theorem MulEquiv.zmodCoordChar_injective {H : Type u_1} {M : Type u_2} [Group H] [CommMonoid M] {m : ℕ} [NeZero m] {ζ : M} (e : H ≃* Multiplicative (ZMod m)) (h : IsPrimitiveRoot ζ m) : Function.Injective ⇑(e.zmodCoordChar ⋯)

The character attached to a primitive m-th root of unity is faithful: the additive character AddChar.zmodChar it is read off is then primitive, so it takes the value 1 only at the identity.