mathlib3 documentation

number_theory.legendre_symbol.mul_character

Multiplicative characters of finite rings and fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 mul_char for the definitions and results.

Main results #

We show that the multiplicative characters form a group (if R' is commutative); see mul_char.comm_group. We also provide an equivalence with the homomorphisms Rˣ →* R'ˣ; see mul_char.equiv_to_unit_hom.

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 mul_char.is_nontrivial.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 mul_char (R : Type u) [comm_monoid R] (R' : Type v) [comm_monoid_with_zero R'] :

Type (max u v)

to_monoid_hom : R →* R'
map_nonunit' : ∀ (a : R), ¬is_unit a → self.to_monoid_hom.to_fun a = 0

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 mul_char

@[class]

structure mul_char_class (F : Type u_1) (R : out_param (Type u_2)) (R' : out_param (Type u_3)) [comm_monoid R] [comm_monoid_with_zero R'] :

Type (max u_1 u_2 u_3)

to_monoid_hom_class : monoid_hom_class F R R'
map_nonunit : ∀ (χ : F) {a : R}, ¬is_unit a → ⇑χ a = 0

This is the corresponding extension of monoid_hom_class.

Instances of this typeclass

mul_char.mul_char_class

Instances of other typeclasses for mul_char_class

mul_char_class.has_sizeof_inst

@[protected, instance]

def mul_char.coe_to_fun {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

has_coe_to_fun (mul_char R R') (λ (_x : mul_char R R'), R → R')

Equations

mul_char.coe_to_fun = {coe := λ (χ : mul_char R R'), χ.to_monoid_hom.to_fun}

@[protected]

def mul_char.simps.apply {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

R → R'

See note [custom simps projection]

Equations

mul_char.simps.apply χ = ⇑χ

@[simp]

theorem mul_char.trivial_apply (R : Type u) [comm_monoid R] (R' : Type v) [comm_monoid_with_zero R'] (x : R) :

⇑(mul_char.trivial R R') x = ite (is_unit x) 1 0

noncomputable def mul_char.trivial (R : Type u) [comm_monoid R] (R' : Type v) [comm_monoid_with_zero R'] :

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

Equations

mul_char.trivial R R' = {to_monoid_hom := {to_fun := λ (x : R), ite (is_unit x) 1 0, map_one' := _, map_mul' := _}, map_nonunit' := _}

@[simp]

theorem mul_char.coe_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

⇑(χ.to_monoid_hom) = ⇑χ

@[simp]

theorem mul_char.to_fun_eq_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

χ.to_monoid_hom.to_fun = ⇑χ

@[simp]

theorem mul_char.coe_mk {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (f : R →* R') (hf : ∀ (a : R), ¬is_unit a → f.to_fun a = 0) :

⇑{to_monoid_hom := f, map_nonunit' := hf} = ⇑f

theorem mul_char.ext' {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] {χ χ' : mul_char R R'} (h : ∀ (a : R), ⇑χ a = ⇑χ' a) :

χ = χ'

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

@[protected, instance]

def mul_char.mul_char_class {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

mul_char_class (mul_char R R') R R'

Equations

mul_char.mul_char_class = {to_monoid_hom_class := {coe := λ (χ : mul_char R R'), χ.to_monoid_hom.to_fun, coe_injective' := _, map_mul := _, map_one := _}, map_nonunit := _}

theorem mul_char.map_nonunit {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') {a : R} (ha : ¬is_unit a) :

⇑χ a = 0

@[ext]

theorem mul_char.ext {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] {χ χ' : mul_char R R'} (h : ∀ (a : Rˣ), ⇑χ ↑a = ⇑χ' ↑a) :

χ = χ'

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

theorem mul_char.ext_iff {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] {χ χ' : mul_char 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 mul_char R R' and Rˣ →* R'ˣ.

def mul_char.to_unit_hom {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

Turn a mul_char into a homomorphism between the unit groups.

Equations

χ.to_unit_hom = units.map ↑χ

theorem mul_char.coe_to_unit_hom {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') (a : Rˣ) :

↑(⇑(χ.to_unit_hom) a) = ⇑χ ↑a

noncomputable def mul_char.of_unit_hom {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (f : Rˣ →* R'ˣ) :

Turn a homomorphism between unit groups into a mul_char.

Equations

mul_char.of_unit_hom f = {to_monoid_hom := {to_fun := λ (x : R), dite (is_unit x) (λ (hx : is_unit x), ↑(⇑f hx.unit)) (λ (hx : ¬is_unit x), 0), map_one' := _, map_mul' := _}, map_nonunit' := _}

theorem mul_char.of_unit_hom_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (f : Rˣ →* R'ˣ) (a : Rˣ) :

⇑(mul_char.of_unit_hom f) ↑a = ↑(⇑f a)

noncomputable def mul_char.equiv_to_unit_hom {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

mul_char R R' ≃ (Rˣ →* R'ˣ)

The equivalence between multiplicative characters and homomorphisms of unit groups.

Equations

mul_char.equiv_to_unit_hom = {to_fun := mul_char.to_unit_hom _inst_2, inv_fun := mul_char.of_unit_hom _inst_2, left_inv := _, right_inv := _}

@[simp]

theorem mul_char.to_unit_hom_eq {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

χ.to_unit_hom = ⇑mul_char.equiv_to_unit_hom χ

@[simp]

theorem mul_char.of_unit_hom_eq {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : Rˣ →* R'ˣ) :

mul_char.of_unit_hom χ = ⇑(mul_char.equiv_to_unit_hom.symm) χ

@[simp]

theorem mul_char.coe_equiv_to_unit_hom {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') (a : Rˣ) :

↑(⇑(⇑mul_char.equiv_to_unit_hom χ) a) = ⇑χ ↑a

@[simp]

theorem mul_char.equiv_unit_hom_symm_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (f : Rˣ →* R'ˣ) (a : Rˣ) :

⇑(⇑(mul_char.equiv_to_unit_hom.symm) f) ↑a = ↑(⇑f a)

Commutative group structure on multiplicative characters #

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

@[protected]

theorem mul_char.map_one {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

⇑χ 1 = 1

@[protected]

theorem mul_char.map_zero {R' : Type v} [comm_monoid_with_zero R'] {R : Type u} [comm_monoid_with_zero R] [nontrivial R] (χ : mul_char R R') :

⇑χ 0 = 0

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

theorem mul_char.map_ring_char {R' : Type v} [comm_monoid_with_zero R'] {R : Type u} [comm_ring R] [nontrivial R] (χ : mul_char R R') :

⇑χ ↑(ring_char R) = 0

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

@[protected, instance]

noncomputable def mul_char.has_one {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

has_one (mul_char R R')

Equations

mul_char.has_one = {one := mul_char.trivial R R' _inst_2}

@[protected, instance]

noncomputable def mul_char.inhabited {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

inhabited (mul_char R R')

Equations

mul_char.inhabited = {default := 1}

@[simp]

theorem mul_char.one_apply_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (a : Rˣ) :

Evaluation of the trivial character

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

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

Equations

χ.mul χ' = {to_monoid_hom := {to_fun := ⇑χ * ⇑χ', map_one' := _, map_mul' := _}, map_nonunit' := _}

@[protected, instance]

def mul_char.has_mul {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

has_mul (mul_char R R')

Equations

mul_char.has_mul = {mul := mul_char.mul _inst_2}

theorem mul_char.mul_apply {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ χ' : mul_char R R') (a : R) :

⇑(χ * χ') a = ⇑χ a * ⇑χ' a

@[simp]

theorem mul_char.coe_to_fun_mul {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ χ' : mul_char R R') :

⇑(χ * χ') = ⇑χ * ⇑χ'

@[protected]

theorem mul_char.one_mul {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

1 * χ = χ

@[protected]

theorem mul_char.mul_one {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

χ * 1 = χ

noncomputable def mul_char.inv {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

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

Equations

χ.inv = {to_monoid_hom := {to_fun := λ (a : R), ⇑monoid_with_zero.inverse (⇑χ a), map_one' := _, map_mul' := _}, map_nonunit' := _}

@[protected, instance]

noncomputable def mul_char.has_inv {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

has_inv (mul_char R R')

Equations

mul_char.has_inv = {inv := mul_char.inv _inst_2}

theorem mul_char.inv_apply_eq_inv {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') (a : R) :

⇑χ⁻¹ a = ring.inverse (⇑χ a)

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

theorem mul_char.inv_apply_eq_inv' {R : Type u} [comm_monoid R] {R' : Type v} [field R'] (χ : mul_char 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 mul_char.inv_apply {R' : Type v} [comm_monoid_with_zero R'] {R : Type u} [comm_monoid_with_zero R] (χ : mul_char R R') (a : R) :

⇑χ⁻¹ a = ⇑χ (ring.inverse 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 mul_char.inv_apply' {R' : Type v} [comm_monoid_with_zero R'] {R : Type u} [field R] (χ : mul_char 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.

@[simp]

theorem mul_char.inv_mul {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :

χ⁻¹ * χ = 1

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

@[protected, instance]

noncomputable def mul_char.comm_group {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :

comm_group (mul_char R R')

The commutative group structure on mul_char R R'.

Equations

mul_char.comm_group = {mul := has_mul.mul mul_char.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := group.npow._default 1 has_mul.mul mul_char.one_mul mul_char.mul_one, npow_zero' := _, npow_succ' := _, inv := has_inv.inv mul_char.has_inv, div := group.div._default has_mul.mul mul_char.comm_group._proof_4 1 mul_char.one_mul mul_char.mul_one (group.npow._default 1 has_mul.mul mul_char.one_mul mul_char.mul_one) mul_char.comm_group._proof_5 mul_char.comm_group._proof_6 has_inv.inv, div_eq_mul_inv := _, zpow := group.zpow._default has_mul.mul mul_char.comm_group._proof_8 1 mul_char.one_mul mul_char.mul_one (group.npow._default 1 has_mul.mul mul_char.one_mul mul_char.mul_one) mul_char.comm_group._proof_9 mul_char.comm_group._proof_10 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

theorem mul_char.pow_apply_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') (n : ℕ) (a : Rˣ) :

⇑(χ ^ n) ↑a = ⇑χ ↑a ^ n

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

theorem mul_char.pow_apply' {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char 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 mul_char.is_nontrivial {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (χ : mul_char R R') :

Prop

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

Equations

χ.is_nontrivial = ∃ (a : Rˣ), ⇑χ ↑a ≠ 1

theorem mul_char.is_nontrivial_iff {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (χ : mul_char R R') :

χ.is_nontrivial ↔ χ ≠ 1

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

def mul_char.is_quadratic {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] (χ : mul_char R R') :

Prop

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

Equations

χ.is_quadratic = ∀ (a : R), ⇑χ a = 0 ∨ ⇑χ a = 1 ∨ ⇑χ a = -1

theorem mul_char.is_quadratic.eq_of_eq_coe {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {R'' : Type w} [comm_ring R''] {χ : mul_char R ℤ} (hχ : χ.is_quadratic) {χ' : mul_char R' ℤ} (hχ' : χ'.is_quadratic) [nontrivial R''] (hR'' : ring_char 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 mul_char.ring_hom_comp_apply {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {R'' : Type w} [comm_ring R''] (χ : mul_char R R') (f : R' →+* R'') (a : R) :

⇑(χ.ring_hom_comp f) a = ⇑f (⇑χ a)

def mul_char.ring_hom_comp {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {R'' : Type w} [comm_ring R''] (χ : mul_char R R') (f : R' →+* R'') :

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

Equations

χ.ring_hom_comp f = {to_monoid_hom := {to_fun := λ (a : R), ⇑f (⇑χ a), map_one' := _, map_mul' := _}, map_nonunit' := _}

theorem mul_char.is_nontrivial.comp {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {R'' : Type w} [comm_ring R''] {χ : mul_char R R'} (hχ : χ.is_nontrivial) {f : R' →+* R''} (hf : function.injective ⇑f) :

(χ.ring_hom_comp f).is_nontrivial

Composition with an injective ring homomorphism preserves nontriviality.

theorem mul_char.is_quadratic.comp {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {R'' : Type w} [comm_ring R''] {χ : mul_char R R'} (hχ : χ.is_quadratic) (f : R' →+* R'') :

(χ.ring_hom_comp f).is_quadratic

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

theorem mul_char.is_quadratic.inv {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {χ : mul_char R R'} (hχ : χ.is_quadratic) :

χ⁻¹ = χ

The inverse of a quadratic character is itself. →

theorem mul_char.is_quadratic.sq_eq_one {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {χ : mul_char R R'} (hχ : χ.is_quadratic) :

χ ^ 2 = 1

The square of a quadratic character is the trivial character.

theorem mul_char.is_quadratic.pow_char {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {χ : mul_char R R'} (hχ : χ.is_quadratic) (p : ℕ) [hp : fact (nat.prime p)] [char_p R' p] :

χ ^ p = χ

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

theorem mul_char.is_quadratic.pow_even {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {χ : mul_char R R'} (hχ : χ.is_quadratic) {n : ℕ} (hn : even n) :

χ ^ n = 1

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

theorem mul_char.is_quadratic.pow_odd {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] {χ : mul_char R R'} (hχ : χ.is_quadratic) {n : ℕ} (hn : odd n) :

χ ^ n = χ

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

theorem mul_char.is_nontrivial.sum_eq_zero {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] [fintype R] [is_domain R'] {χ : mul_char R R'} (hχ : χ.is_nontrivial) :

finset.univ.sum (λ (a : R), ⇑χ 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 mul_char.sum_one_eq_card_units {R : Type u} [comm_ring R] {R' : Type v} [comm_ring R'] [fintype R] [decidable_eq R] :

finset.univ.sum (λ (a : R), ⇑1 a) = ↑(fintype.card Rˣ)

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