Characters of the rotation subgroup of a dihedral group

The rotation subgroup TauCeti.dihedralRotations n of DihedralGroup n is cyclic, its coordinate TauCeti.dihedralRotationsMulEquiv identifying it with Multiplicative (ZMod n). A character of it is therefore named by a single n-th root of unity ζ: this file specializes MulEquiv.zmodCoordChar to that coordinate to get TauCeti.dihedralRotationChar, the character sending the rotation r i to ζ ^ i, and reads off that a primitive root of unity gives a faithful character.

This is separated from TauCeti.GroupTheory.SpecificGroups.Dihedral.Basic because MulEquiv.zmodCoordChar rests on AddChar.zmodChar, which lives in the number-theoretic part of Mathlib that the rotation subgroup itself does not need.

Main definitions

• TauCeti.dihedralRotationChar: the character of the rotation subgroup sending r i to ζ ^ i, for ζ an n-th root of unity.

Main results

• TauCeti.dihedralRotationChar_injective: the character attached to a primitive n-th root of unity is faithful.

def TauCeti.dihedralRotationChar {n : ℕ} {M : Type u_1} [CommMonoid M] {ζ : M} [NeZero n] (hζ : ζ ^ n = 1) : ↥(dihedralRotations n) →* M

The character of the rotation subgroup attached to an n-th root of unity ζ: the rotation r i is sent to ζ ^ i, the exponent being the canonical representative of i in ZMod n. It is MulEquiv.zmodCoordChar for the cyclic coordinate TauCeti.dihedralRotationsMulEquiv.

Equations

• TauCeti.dihedralRotationChar hζ = (TauCeti.dihedralRotationsMulEquiv n).zmodCoordChar hζ

@[simp]

theorem TauCeti.dihedralRotationChar_apply {n : ℕ} {M : Type u_1} [CommMonoid M] {ζ : M} [NeZero n] (hζ : ζ ^ n = 1) (x : ↥(dihedralRotations n)) : (dihedralRotationChar hζ) x = ζ ^ (Multiplicative.toAdd ((dihedralRotationsMulEquiv n) x)).val

theorem TauCeti.dihedralRotationChar_r {n : ℕ} {M : Type u_1} [CommMonoid M] {ζ : M} [NeZero n] (hζ : ζ ^ n = 1) (i : ZMod n) : (dihedralRotationChar hζ) ⟨DihedralGroup.r i, ⋯⟩ = ζ ^ i.val

The character sends the rotation r i to ζ ^ i.

theorem TauCeti.dihedralRotationChar_injective {n : ℕ} {M : Type u_1} [CommMonoid M] {ζ : M} [NeZero n] (h : IsPrimitiveRoot ζ n) : Function.Injective ⇑(dihedralRotationChar ⋯)

The character attached to a primitive n-th root of unity is faithful: this is MulEquiv.zmodCoordChar_injective for the rotation coordinate.