Duality for multiplicative characters

Let M be a finite commutative monoid and R a ring that has enough nth roots of unity, where n is the exponent of M. Then the main results of this file are as follows.

• MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity: multiplicative characters M → R separate elements of Mˣ.

• MulChar.mulEquiv_units: the group of multiplicative characters M → R is (noncanonically) isomorphic to Mˣ.

instance MulChar.finite {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite Mˣ] [IsDomain R] : Finite (MulChar M R)

theorem MulChar.exists_apply_ne_one_iff_exists_monoidHom {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] (a : Mˣ) : (∃ (χ : MulChar M R), χ ↑a ≠ 1) ↔ ∃ (φ : Mˣ →* Rˣ), φ a ≠ 1

theorem MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] [Nontrivial R] {a : M} (ha : a ≠ 1) : ∃ (χ : MulChar M R), χ a ≠ 1

If M is a finite commutative monoid and R is a ring that has enough roots of unity, then for each a ≠ 1 in M, there exists a multiplicative character χ : M → R such that χ a ≠ 1.

theorem MulChar.mulEquiv_units (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nonempty (MulChar M R ≃* Mˣ)

The group of R-valued multiplicative characters on a finite commutative monoid M is (noncanonically) isomorphic to its unit group Mˣ when R is a ring that has enough roots of unity.

theorem MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nat.card (MulChar M R) = Nat.card Mˣ

The cardinality of the group of R-valued multiplicative characters on a finite commutative monoid M is the same as that of its unit group Mˣ when R is a ring that has enough roots of unity.