English
The group of multiplicative characters on a finite monoid with cyclic unit group is isomorphic to the group of nth roots of unity in the target ring.
Русский
Группа муль chap на конечном моноиде с циклической единичной группой изоморфна группе n-ых корней единицы в кольце-цели.
LaTeX
$$MulChar M R ≃* rootsOfUnity (Fintype.card Mˣ) R$$
Lean4
/-- If `M` is a finite commutative monoid and `R` is a ring that has enough roots of unity,
then for each `a ≠ 1` in `M`, there exists a multiplicative character `χ : M → R` such that
`χ a ≠ 1`. -/
theorem exists_apply_ne_one_of_hasEnoughRootsOfUnity [Nontrivial R] {a : M} (ha : a ≠ 1) : ∃ χ : MulChar M R, χ a ≠ 1 :=
by
by_cases hu : IsUnit a
· refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_
refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_
contrapose! ha
rw [← hu.unit_spec, ha, Units.val_eq_one]
· exact ⟨1, by simpa only [map_nonunit _ hu] using zero_ne_one⟩
