English
The group MulChar M R is isomorphic to the group of nth roots of unity in R when unit group is cyclic.
Русский
Группа MulChar M R изоморфна группе корней единицы, если единичная группа циклична.
LaTeX
$$MulChar M R ≃* rootsOfUnity (Fintype.card Mˣ) R$$
Lean4
/-- The group of multiplicative characters on a finite monoid `M` with cyclic unit group `Mˣ`
of order `n` is isomorphic to the group of `n`th roots of unity in the target `R`. -/
noncomputable def equiv_rootsOfUnity [inst_cyc : IsCyclic Mˣ] : MulChar M R ≃* rootsOfUnity (Fintype.card Mˣ) R
where
toFun
χ :=
⟨χ.toUnitHom <| Classical.choose inst_cyc.exists_generator, by
simp only [toUnitHom_eq, mem_rootsOfUnity, ← map_pow, pow_card_eq_one, map_one]⟩
invFun ζ := ofRootOfUnity ζ.prop <| Classical.choose_spec inst_cyc.exists_generator
left_inv
χ := by
simp only [toUnitHom_eq, eq_iff <| Classical.choose_spec inst_cyc.exists_generator, ofRootOfUnity_spec,
coe_equivToUnitHom]
right_inv
ζ := by
ext
simp only [toUnitHom_eq, coe_equivToUnitHom, ofRootOfUnity_spec]
map_mul' x y := by simp only [toUnitHom_eq, equivToUnitHom_mul_apply, MulMemClass.mk_mul_mk]
