Duality for finite abelian groups

Let G be a finite abelian group and let M be a commutative monoid that has enough nth roots of unity, where n is the exponent of G. The main results in this file are

• CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity: Homomorphisms G →* Mˣ separate elements of G.
• CommGroup.monoidHom_mulEquiv_self_of_hasEnoughRootsOfUnity: G is isomorphic to G →* Mˣ.

theorem CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent G)] {a : G} (ha : a ≠ 1) : ∃ (φ : G →* Mˣ), φ a ≠ 1

If G is a finite commutative group of exponent n and M is a commutative monoid with enough nth roots of unity, then for each a ≠ 1 in G, there exists a group homomorphism φ : G → Mˣ such that φ a ≠ 1.

theorem CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent G)] : Nonempty ((G →* Mˣ) ≃* G)

A finite commutative group G is (noncanonically) isomorphic to the group G →* Mˣ when M is a commutative monoid with enough nth roots of unity, where n is the exponent of G.