English
There is a canonical way to obtain a character from a generator to a given root of unity on a finite cyclic unit group.
Русский
Существует канонический способ получить характер из генератора к заданному корню единства на конечной циклической единичной группе.
LaTeX
$$ofRootOfUnity hζ hg : MulChar M R$$
Lean4
/-- Given a finite monoid `M` with unit group `Mˣ` cyclic of order `n` and an `n`th root of
unity `ζ` in `R`, there is a multiplicative character `M → R` that sends a given generator
of `Mˣ` to `ζ`. -/
noncomputable def ofRootOfUnity {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ}
(hg : ∀ x, x ∈ Subgroup.zpowers g) : MulChar M R :=
by
have : orderOf ζ ∣ Fintype.card Mˣ := orderOf_dvd_iff_pow_eq_one.mpr <| (mem_rootsOfUnity _ ζ).mp hζ
refine ofUnitHom <| monoidHomOfForallMemZpowers hg <| this.trans <| dvd_of_eq ?_
rw [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
