English
For a finite cyclic group G and a ring M with enough roots of unity, there exists a nonempty monoid equivalence between G →* Mˣ and G.
Русский
Для конечной циклической группы G и кольца M с достаточным количеством корней единицы существует непустое моноидальное эквивалентство между группо-однородными гомоморфизмами G →* Mˣ и G.
LaTeX
$$IsCyclic.monoidHom_equiv_self: ∀ G M, [CommGroup G] [Finite G] [IsCyclic G] [CommMonoid M] [HasEnoughRootsOfUnity M (|G|)], Nonempty ((G →* Mˣ) ≃* G)$$
Lean4
/-- The group of group homomorphisms from a finite cyclic group `G` of order `n` into the
group of units of a ring `M` with all roots of unity is isomorphic to `G` -/
theorem monoidHom_equiv_self (G M : Type*) [CommGroup G] [Finite G] [IsCyclic G] [CommMonoid M]
[HasEnoughRootsOfUnity M (Nat.card G)] : Nonempty ((G →* Mˣ) ≃* G) :=
by
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
have hord := HasEnoughRootsOfUnity.natCard_rootsOfUnity M (Nat.card G)
let e := (IsCyclic.monoidHom_mulEquiv_rootsOfUnity G Mˣ).some
exact ⟨e.trans (rootsOfUnityUnitsMulEquiv M (Nat.card G)) |>.trans (mulEquivOfCyclicCardEq hord)⟩
