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] [hM : 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] [hM : 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.

theorem CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] : Nat.card (G →* Mˣ) = Nat.card G

theorem MonoidHom.restrict_surjective (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) [Finite (G →* Mˣ)] [Finite (↥H →* Mˣ)] : Function.Surjective ⇑(restrictHom H Mˣ)

Let G be a finite commutative group and let H be a subgroup. If M is a commutative monoid such that G →* Mˣ and H →* Mˣ are both finite (this is the case for example if M is a commutative domain) and with enough nth roots of unity, where n is the exponent of G, then any homomorphism H →* Mˣ can be extended to an homomorphism G →* Mˣ.