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)

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)

This is the corresponding extension of monoid_hom_class.

Instances of this typeclass
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
@[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
@[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
@[simp]
theorem mul_char.coe_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (χ : mul_char R R') :
@[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') :
@[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) :
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]
Equations
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
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ˣ) :
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
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ˣ) :
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
@[simp]

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') :

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'] :
Equations
@[protected, instance]
noncomputable def mul_char.inhabited {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :
Equations
@[simp]
theorem mul_char.one_apply_coe {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] (a : Rˣ) :
1 a = 1

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
@[protected, instance]
def mul_char.has_mul {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :
Equations
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
@[protected, instance]
noncomputable def mul_char.has_inv {R : Type u} [comm_monoid R] {R' : Type v} [comm_monoid_with_zero R'] :
Equations
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) :

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) :

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) :

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'] :

The commutative group structure on mul_char R R'.

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

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
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'') :
mul_char R R''

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

Equations
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) :

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'') :

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.