Documentation

Mathlib.NumberTheory.MulChar.Duality

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.

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

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.

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

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 when R is a ring that has enough roots of unity.