Multiplicative characters of finite rings and fields #
Let R and R' be a commutative rings.
A multiplicative character of R with values in R' is a morphism of
monoids from the multiplicative monoid of R into that of R'
that sends non-units to zero.
We use the namespace MulChar for the definitions and results.
Main results #
We show that the multiplicative characters form a group (if R' is commutative);
see MulChar.commGroup. We also provide an equivalence with the
homomorphisms Rˣ →* R'ˣ; see MulChar.equivToUnitHom.
We define a multiplicative character to be quadratic if its values
are among 0, 1 and -1, and we prove some properties of quadratic characters.
Finally, we show that the sum of all values of a nontrivial multiplicative
character vanishes; see MulChar.IsNontrivial.sum_eq_zero.
Tags #
multiplicative character
Definitions related to multiplicative characters #
Even though the intended use is when domain and target of the characters are commutative rings, we define them in the more general setting when the domain is a commutative monoid and the target is a commutative monoid with zero. (We need a zero in the target, since non-units are supposed to map to zero.)
In this setting, there is an equivalence between multiplicative characters
R → R' and group homomorphisms Rˣ → R'ˣ, and the multiplicative characters
have a natural structure as a commutative group.
Define a structure for multiplicative characters.
A multiplicative character from a commutative monoid R to a commutative monoid with zero R'
is a homomorphism of (multiplicative) monoids that sends non-units to zero.
- toFun : R → R'
- map_one' : (↑self.toMonoidHom).toFun 1 = 1
Equations
- MulChar.instFunLike R R' = { coe := fun (χ : MulChar R R') => (↑χ.toMonoidHom).toFun, coe_injective' := ⋯ }
This is the corresponding extension of MonoidHomClass.
- map_one : ∀ (f : F), f 1 = 1
Instances
The trivial multiplicative character. It takes the value 0 on non-units and
the value 1 on units.
Equations
- MulChar.trivial R R' = { toFun := fun (x : R) => if IsUnit x then 1 else 0, map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }
Extensionality. See ext below for the version that will actually be used.
Equations
- ⋯ = ⋯
Extensionality. Since MulChars always take the value zero on non-units, it is sufficient
to compare the values on units.
Equivalence of multiplicative characters with homomorphisms on units #
We show that restriction / extension by zero gives an equivalence
between MulChar R R' and Rˣ →* R'ˣ.
Turn a MulChar into a homomorphism between the unit groups.
Turn a homomorphism between unit groups into a MulChar.
Equations
- MulChar.ofUnitHom f = { toFun := fun (x : R) => if hx : IsUnit x then ↑(f hx.unit) else 0, map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }
The equivalence between multiplicative characters and homomorphisms of unit groups.
Equations
- MulChar.equivToUnitHom = { toFun := MulChar.toUnitHom, invFun := MulChar.ofUnitHom, left_inv := ⋯, right_inv := ⋯ }
Commutative group structure on multiplicative characters #
The multiplicative characters R → R' form a commutative group.
If the domain has a zero (and is nontrivial), then χ 0 = 0.
We can convert a multiplicative character into a homomorphism of monoids with zero when the source has a zero and another element.
Equations
- ↑χ = { toFun := (↑χ.toMonoidHom).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
If the domain is a ring R, then χ (ringChar R) = 0.
Equations
- MulChar.hasOne = { one := MulChar.trivial R R' }
Equations
- MulChar.inhabited = { default := 1 }
Evaluation of the trivial character
Evaluation of the trivial character
Multiplication of multiplicative characters. (This needs the target to be commutative.)
Equations
- MulChar.hasMul = { mul := MulChar.mul }
The inverse of a multiplicative character. We define it as inverse ∘ χ.
Equations
- χ.inv = { toFun := fun (a : R) => MonoidWithZero.inverse (χ a), map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }
Equations
- MulChar.hasInv = { inv := MulChar.inv }
The inverse of a multiplicative character χ, applied to a, is the inverse of χ a.
The inverse of a multiplicative character χ, applied to a, is the inverse of χ a.
Variant when the target is a field
When the domain has a zero, then the inverse of a multiplicative character χ,
applied to a, is χ applied to the inverse of a.
When the domain has a zero, then the inverse of a multiplicative character χ,
applied to a, is χ applied to the inverse of a.
The product of a character with its inverse is the trivial character.
The commutative group structure on MulChar R R'.
Equations
- MulChar.commGroup = CommGroup.mk ⋯
If a is a unit and n : ℕ, then (χ ^ n) a = (χ a) ^ n.
If n is positive, then (χ ^ n) a = (χ a) ^ n.
The equivalence between multiplicative characters and homomorphisms of unit groups as a multiplicative equivalence.
Equations
- MulChar.mulEquivToUnitHom = { toEquiv := MulChar.equivToUnitHom, map_mul' := ⋯ }
Properties of multiplicative characters #
We introduce the properties of being nontrivial or quadratic and prove some basic facts about them.
We now (mostly) assume that the target is a commutative ring.
A multiplicative character is nontrivial if it takes a value ≠ 1 on a unit.
A multiplicative character is nontrivial iff it is not the trivial character.
If two values of quadratic characters with target ℤ agree after coercion into a ring
of characteristic not 2, then they agree in ℤ.
We can post-compose a multiplicative character with a ring homomorphism.
Equations
- χ.ringHomComp f = { toFun := fun (a : R) => f (χ a), map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }
Composition with an injective ring homomorphism preserves nontriviality.
Composition with a ring homomorphism preserves the property of being a quadratic character.
The inverse of a quadratic character is itself. →
The square of a quadratic character is the trivial character.
The pth power of a quadratic character is itself, when p is the (prime) characteristic
of the target ring.
Multiplicative characters with finite domain #
If χ is a multiplicative character on a commutative monoid M with finitely many units,
then χ ^ #Mˣ = 1.
A multiplicative character on a commutative monoid with finitely many units has finite (= positive) order.
The sum over all values of the trivial multiplicative character on a finite ring is the cardinality of its unit group.