English
Let G be a finite commutative group with exponent n and M a commutative monoid with enough n-th roots of unity. Then there exists a noncanonical multiplicative equivalence between G and the monoid of group homomorphisms G → Mˣ, i.e., G ≅ (G →* Mˣ).
Русский
Пусть G — конечная коммутативная группа с показателем n, а M — коммутативный моноид с достаточным числом n-й корней единства. Тогда существует неканоническое мультиэквивалентность между G и моноидом гомоморфизмов G →* Mˣ, то есть G ≅ (G →* Mˣ).
LaTeX
$$$\\exists \\mathcal{E} : (G \\to^* M^{\\times}) \\cong^* G$ (неканонически)$$
Lean4
/-- A finite commutative group `G` is (noncanonically) isomorphic to the group `G →* Mˣ`
when `M` is a commutative monoid with enough `n`th roots of unity, where `n` is the exponent
of `G`. -/
theorem monoidHom_mulEquiv_of_hasEnoughRootsOfUnity : Nonempty ((G →* Mˣ) ≃* G) := by
classical -- to get `DecidableEq ι`
obtain ⟨ι, _, n, ⟨h₁, h₂⟩⟩ := equiv_prod_multiplicative_zmod_of_finite G
let e := h₂.some
let e' := Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
have : ∀ i, NeZero (n i) := fun i ↦ NeZero.of_gt (h₁ i)
have inst i : HasEnoughRootsOfUnity M <| Nat.card <| Multiplicative <| ZMod (n i) :=
by
have hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G := by
simpa only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card] using dvd_exponent e i
exact HasEnoughRootsOfUnity.of_dvd M hdvd
let E i := (IsCyclic.monoidHom_equiv_self (Multiplicative (ZMod (n i))) M).some
exact ⟨e.monoidHomCongrLeft.trans <| e'.trans <| .trans (.piCongrRight E) e.symm⟩
