# Documentation

Mathlib.NumberTheory.LegendreSymbol.MulCharacter

# 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

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.

structure MulChar (R : Type u) [] (R' : Type v) [] extends :
Type (max u v)

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.

Instances For
instance funLike (R : Type u) [] (R' : Type v) [] :
FunLike (MulChar R R') R fun x => R'
class MulCharClass (F : Type u_1) (R : outParam (Type u_2)) (R' : outParam (Type u_3)) [] [] extends :
Type (max (max u_1 u_2) u_3)
• coe : FRR'
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : R), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1
• map_nonunit : ∀ (χ : F) {a : R}, ¬χ a = 0

This is the corresponding extension of MonoidHomClass.

Instances
@[simp]
theorem MulChar.trivial_apply (R : Type u) [] (R' : Type v) [] (x : R) :
↑() x = if then 1 else 0
noncomputable def MulChar.trivial (R : Type u) [] (R' : Type v) [] :
MulChar R R'

The trivial multiplicative character. It takes the value 0 on non-units and the value 1 on units.

Instances For
@[simp]
theorem MulChar.coe_mk {R : Type u} [] {R' : Type v} [] (f : R →* R') (hf : ∀ (a : R), ¬OneHom.toFun (f) a = 0) :
{ toMonoidHom := f, map_nonunit' := hf } = f
theorem MulChar.ext' {R : Type u} [] {R' : Type v} [] {χ : MulChar R R'} {χ' : MulChar R R'} (h : ∀ (a : R), χ a = χ' a) :
χ = χ'

Extensionality. See ext below for the version that will actually be used.

instance MulChar.instMulCharClassMulChar {R : Type u} [] {R' : Type v} [] :
MulCharClass (MulChar R R') R R'
theorem MulChar.map_nonunit {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') {a : R} (ha : ¬) :
χ a = 0
theorem MulChar.ext {R : Type u} [] {R' : Type v} [] {χ : MulChar R R'} {χ' : MulChar R R'} (h : ∀ (a : Rˣ), χ a = χ' a) :
χ = χ'

Extensionality. Since MulChars always take the value zero on non-units, it is sufficient to compare the values on units.

theorem MulChar.ext_iff {R : Type u} [] {R' : Type v} [] {χ : MulChar R R'} {χ' : MulChar R R'} :
χ = χ' ∀ (a : Rˣ), χ a = χ' a

### 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'ˣ.

def MulChar.toUnitHom {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') :

Turn a MulChar into a homomorphism between the unit groups.

Instances For
theorem MulChar.coe_toUnitHom {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') (a : Rˣ) :
↑(↑() a) = χ a
noncomputable def MulChar.ofUnitHom {R : Type u} [] {R' : Type v} [] (f : Rˣ →* R'ˣ) :
MulChar R R'

Turn a homomorphism between unit groups into a MulChar.

Instances For
theorem MulChar.ofUnitHom_coe {R : Type u} [] {R' : Type v} [] (f : Rˣ →* R'ˣ) (a : Rˣ) :
↑() a = ↑(f a)
noncomputable def MulChar.equivToUnitHom {R : Type u} [] {R' : Type v} [] :
MulChar R R' (Rˣ →* R'ˣ)

The equivalence between multiplicative characters and homomorphisms of unit groups.

Instances For
@[simp]
theorem MulChar.toUnitHom_eq {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') :
= MulChar.equivToUnitHom χ
@[simp]
theorem MulChar.ofUnitHom_eq {R : Type u} [] {R' : Type v} [] (χ : Rˣ →* R'ˣ) :
= MulChar.equivToUnitHom.symm χ
@[simp]
theorem MulChar.coe_equivToUnitHom {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') (a : Rˣ) :
↑(↑(MulChar.equivToUnitHom χ) a) = χ a
@[simp]
theorem MulChar.equivToUnitHom_symm_coe {R : Type u} [] {R' : Type v} [] (f : Rˣ →* R'ˣ) (a : Rˣ) :
↑(MulChar.equivToUnitHom.symm f) a = ↑(f a)
@[simp]
theorem MulChar.coe_toMonoidHom {R : Type u} {R' : Type v} [] [] (χ : MulChar R R') (x : R) :
χ.toMonoidHom x = χ x

### Commutative group structure on multiplicative characters #

The multiplicative characters R → R' form a commutative group.

theorem MulChar.map_one {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') :
χ 1 = 1
theorem MulChar.map_zero {R' : Type v} [] {R : Type u} [] (χ : MulChar R R') :
χ 0 = 0

If the domain has a zero (and is nontrivial), then χ 0 = 0.

theorem MulChar.map_ringChar {R' : Type v} [] {R : Type u} [] [] (χ : MulChar R R') :
χ ↑() = 0

If the domain is a ring R, then χ (ringChar R) = 0.

noncomputable instance MulChar.hasOne {R : Type u} [] {R' : Type v} [] :
One (MulChar R R')
noncomputable instance MulChar.inhabited {R : Type u} [] {R' : Type v} [] :
@[simp]
theorem MulChar.one_apply_coe {R : Type u} [] {R' : Type v} [] (a : Rˣ) :
1 a = 1

Evaluation of the trivial character

def MulChar.mul {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') (χ' : MulChar R R') :
MulChar R R'

Multiplication of multiplicative characters. (This needs the target to be commutative.)

Instances For
instance MulChar.hasMul {R : Type u} [] {R' : Type v} [] :
Mul (MulChar R R')
theorem MulChar.mul_apply {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') (χ' : MulChar R R') (a : R) :
↑(χ * χ') a = χ a * χ' a
@[simp]
theorem MulChar.coeToFun_mul {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') (χ' : MulChar R R') :
↑(χ * χ') = χ * χ'
theorem MulChar.one_mul {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') :
1 * χ = χ
theorem MulChar.mul_one {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') :
χ * 1 = χ
noncomputable def MulChar.inv {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') :
MulChar R R'

The inverse of a multiplicative character. We define it as inverse ∘ χ.

Instances For
noncomputable instance MulChar.hasInv {R : Type u} [] {R' : Type v} [] :
Inv (MulChar R R')
theorem MulChar.inv_apply_eq_inv {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') (a : R) :
χ⁻¹ a = Ring.inverse (χ a)

The inverse of a multiplicative character χ, applied to a, is the inverse of χ a.

theorem MulChar.inv_apply_eq_inv' {R : Type u} [] {R' : Type v} [Field R'] (χ : MulChar R R') (a : R) :
χ⁻¹ a = (χ a)⁻¹

The inverse of a multiplicative character χ, applied to a, is the inverse of χ a. Variant when the target is a field

theorem MulChar.inv_apply {R' : Type v} [] {R : Type u} (χ : MulChar R R') (a : R) :
χ⁻¹ a = χ ()

When the domain has a zero, then the inverse of a multiplicative character χ, applied to a, is χ applied to the inverse of a.

theorem MulChar.inv_apply' {R' : Type v} [] {R : Type u} [] (χ : MulChar R R') (a : R) :
χ⁻¹ a = χ a⁻¹

When the domain has a zero, then the inverse of a multiplicative character χ, applied to a, is χ applied to the inverse of a.

theorem MulChar.inv_mul {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') :
χ⁻¹ * χ = 1

The product of a character with its inverse is the trivial character.

noncomputable instance MulChar.commGroup {R : Type u} [] {R' : Type v} [] :

The commutative group structure on MulChar R R'.

theorem MulChar.pow_apply_coe {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') (n : ) (a : Rˣ) :
↑(χ ^ n) a = χ a ^ n

If a is a unit and n : ℕ, then (χ ^ n) a = (χ a) ^ n.

theorem MulChar.pow_apply' {R : Type u} [] {R' : Type v} [] (χ : MulChar R R') {n : } (hn : 0 < n) (a : R) :
↑(χ ^ n) a = χ a ^ n

If n is positive, then (χ ^ n) a = (χ a) ^ n.

### Properties of multiplicative characters #

We introduce the properties of being nontrivial or quadratic and prove some basic facts about them.

We now assume that domain and target are commutative rings.

def MulChar.IsNontrivial {R : Type u} [] {R' : Type v} [CommRing R'] (χ : MulChar R R') :

A multiplicative character is nontrivial if it takes a value ≠ 1 on a unit.

Instances For
theorem MulChar.isNontrivial_iff {R : Type u} [] {R' : Type v} [CommRing R'] (χ : MulChar R R') :
χ 1

A multiplicative character is nontrivial iff it is not the trivial character.

def MulChar.IsQuadratic {R : Type u} [] {R' : Type v} [CommRing R'] (χ : MulChar R R') :

A multiplicative character is quadratic if it takes only the values 0, 1, -1.

Instances For
theorem MulChar.IsQuadratic.eq_of_eq_coe {R : Type u} [] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R''] {χ : } (hχ : ) {χ' : MulChar R' } (hχ' : ) [Nontrivial R''] (hR'' : ringChar R'' 2) {a : R} {a' : R'} (h : ↑(χ a) = ↑(χ' a')) :
χ a = χ' a'

If two values of quadratic characters with target ℤ agree after coercion into a ring of characteristic not 2, then they agree in ℤ.

@[simp]
theorem MulChar.ringHomComp_apply {R : Type u} [] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R''] (χ : MulChar R R') (f : R' →+* R'') (a : R) :
↑() a = f (χ a)
def MulChar.ringHomComp {R : Type u} [] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R''] (χ : MulChar R R') (f : R' →+* R'') :
MulChar R R''

We can post-compose a multiplicative character with a ring homomorphism.

Instances For
theorem MulChar.IsNontrivial.comp {R : Type u} [] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R''] {χ : MulChar R R'} (hχ : ) {f : R' →+* R''} (hf : ) :

Composition with an injective ring homomorphism preserves nontriviality.

theorem MulChar.IsQuadratic.comp {R : Type u} [] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R''] {χ : MulChar R R'} (hχ : ) (f : R' →+* R'') :

Composition with a ring homomorphism preserves the property of being a quadratic character.

theorem MulChar.IsQuadratic.inv {R : Type u} [] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : ) :
χ⁻¹ = χ

The inverse of a quadratic character is itself. →

theorem MulChar.IsQuadratic.sq_eq_one {R : Type u} [] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : ) :
χ ^ 2 = 1

The square of a quadratic character is the trivial character.

theorem MulChar.IsQuadratic.pow_char {R : Type u} [] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : ) (p : ) [hp : Fact ()] [CharP R' p] :
χ ^ p = χ

The pth power of a quadratic character is itself, when p is the (prime) characteristic of the target ring.

theorem MulChar.IsQuadratic.pow_even {R : Type u} [] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : ) {n : } (hn : Even n) :
χ ^ n = 1

The nth power of a quadratic character is the trivial character, when n is even.

theorem MulChar.IsQuadratic.pow_odd {R : Type u} [] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : ) {n : } (hn : Odd n) :
χ ^ n = χ

The nth power of a quadratic character is itself, when n is odd.

theorem MulChar.IsNontrivial.sum_eq_zero {R : Type u} [] {R' : Type v} [CommRing R'] [] [IsDomain R'] {χ : MulChar R R'} (hχ : ) :
(Finset.sum Finset.univ fun a => χ a) = 0

The sum over all values of a nontrivial multiplicative character on a finite ring is zero (when the target is a domain).

theorem MulChar.sum_one_eq_card_units {R : Type u} [] {R' : Type v} [CommRing R'] [] [] :
(Finset.sum Finset.univ fun a => 1 a) = ↑()

The sum over all values of the trivial multiplicative character on a finite ring is the cardinality of its unit group.