Documentation

Mathlib.GroupTheory.FiniteAbelian.Duality

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

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.

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.