Documentation

Mathlib.NumberTheory.MulChar.Basic

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_1) [CommMonoid R] (R' : Type u_2) [CommMonoidWithZero R'] extends R →* R' :
Type (max u_1 u_2)

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.

instance MulChar.instFunLike (R : Type u_1) [CommMonoid R] (R' : Type u_2) [CommMonoidWithZero R'] :
FunLike (MulChar R R') R R'
Equations
class MulCharClass (F : Type u_3) (R : outParam (Type u_4)) (R' : outParam (Type u_5)) [CommMonoid R] [CommMonoidWithZero R'] [FunLike F R R'] extends MonoidHomClass F R R' :

This is the corresponding extension of MonoidHomClass.

Instances
    noncomputable def MulChar.trivial (R : Type u_1) [CommMonoid R] (R' : Type u_2) [CommMonoidWithZero R'] :
    MulChar R R'

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

    Equations
    @[simp]
    theorem MulChar.trivial_apply (R : Type u_1) [CommMonoid R] (R' : Type u_2) [CommMonoidWithZero R'] (x : R) :
    (trivial R R') x = if IsUnit x then 1 else 0
    @[simp]
    theorem MulChar.coe_mk {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (f : R →* R') (hf : ∀ (a : R), ¬IsUnit a(↑f).toFun a = 0) :
    { toMonoidHom := f, map_nonunit' := hf } = f
    theorem MulChar.ext' {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] {χ χ' : MulChar R R'} (h : ∀ (a : R), χ a = χ' a) :
    χ = χ'

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

    instance MulChar.instMulCharClass {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :
    MulCharClass (MulChar R R') R R'
    theorem MulChar.map_nonunit {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') {a : R} (ha : ¬IsUnit a) :
    χ a = 0
    theorem MulChar.ext {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero 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_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero 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_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') :

    Turn a MulChar into a homomorphism between the unit groups.

    Equations
    theorem MulChar.coe_toUnitHom {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') (a : Rˣ) :
    (χ.toUnitHom a) = χ a
    noncomputable def MulChar.ofUnitHom {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) :
    MulChar R R'

    Turn a homomorphism between unit groups into a MulChar.

    Equations
    theorem MulChar.ofUnitHom_coe {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ) :
    (ofUnitHom f) a = (f a)
    noncomputable def MulChar.equivToUnitHom {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :
    MulChar R R' (Rˣ →* R'ˣ)

    The equivalence between multiplicative characters and homomorphisms of unit groups.

    Equations
    @[simp]
    theorem MulChar.toUnitHom_eq {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') :
    @[simp]
    theorem MulChar.ofUnitHom_eq {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : Rˣ →* R'ˣ) :
    @[simp]
    theorem MulChar.coe_equivToUnitHom {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') (a : Rˣ) :
    ((equivToUnitHom χ) a) = χ a
    @[simp]
    theorem MulChar.equivToUnitHom_symm_coe {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ) :
    (equivToUnitHom.symm f) a = (f a)
    @[simp]
    theorem MulChar.coe_toMonoidHom {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : 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_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') :
    χ 1 = 1
    theorem MulChar.map_zero {R' : Type u_2} [CommMonoidWithZero R'] {R : Type u_3} [CommMonoidWithZero R] [Nontrivial R] (χ : MulChar R R') :
    χ 0 = 0

    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' := }
    @[simp]
    theorem MulChar.toMonoidWithZeroHom_apply {R' : Type u_2} [CommMonoidWithZero R'] {R : Type u_3} [CommMonoidWithZero R] [Nontrivial R] (χ : MulChar R R') (a✝ : R) :
    χ a✝ = (↑χ.toMonoidHom).toFun a✝
    theorem MulChar.map_ringChar {R' : Type u_2} [CommMonoidWithZero R'] {R : Type u_3} [CommSemiring R] [Nontrivial R] (χ : MulChar R R') :
    χ (ringChar R) = 0

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

    noncomputable instance MulChar.hasOne {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :
    One (MulChar R R')
    Equations
    noncomputable instance MulChar.inhabited {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :
    Equations
    @[simp]
    theorem MulChar.one_apply_coe {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (a : Rˣ) :
    1 a = 1

    Evaluation of the trivial character

    theorem MulChar.one_apply {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] {x : R} (hx : IsUnit x) :
    1 x = 1

    Evaluation of the trivial character

    def MulChar.mul {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ χ' : MulChar R R') :
    MulChar R R'

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

    Equations
    • χ.mul χ' = { toFun := χ * χ', map_one' := , map_mul' := , map_nonunit' := }
    instance MulChar.hasMul {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :
    Mul (MulChar R R')
    Equations
    theorem MulChar.mul_apply {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ χ' : MulChar R R') (a : R) :
    (χ * χ') a = χ a * χ' a
    @[simp]
    theorem MulChar.coeToFun_mul {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ χ' : MulChar R R') :
    ⇑(χ * χ') = χ * χ'
    theorem MulChar.one_mul {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') :
    1 * χ = χ
    theorem MulChar.mul_one {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') :
    χ * 1 = χ
    noncomputable def MulChar.inv {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') :
    MulChar R R'

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

    Equations
    noncomputable instance MulChar.hasInv {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :
    Inv (MulChar R R')
    Equations
    theorem MulChar.inv_apply_eq_inv {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : 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_1} [CommMonoid R] {R' : Type u_3} [CommGroupWithZero 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 u_2} [CommMonoidWithZero R'] {R : Type u_3} [CommMonoidWithZero R] (χ : MulChar 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 MulChar.inv_apply' {R' : Type u_2} [CommMonoidWithZero R'] {R : Type u_3} [CommGroupWithZero R] (χ : 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_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') :
    χ⁻¹ * χ = 1

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

    noncomputable instance MulChar.commGroup {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :

    The commutative group structure on MulChar R R'.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem MulChar.pow_apply_coe {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : 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_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') {n : } (hn : n 0) (a : R) :
    (χ ^ n) a = χ a ^ n

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

    theorem MulChar.equivToUnitHom_mul_apply {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ₁ χ₂ : MulChar R R') (a : Rˣ) :
    (equivToUnitHom (χ₁ * χ₂)) a = (equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a
    noncomputable def MulChar.mulEquivToUnitHom {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] :
    MulChar R R' ≃* (Rˣ →* R'ˣ)

    The equivalence between multiplicative characters and homomorphisms of unit groups as a multiplicative equivalence.

    Equations

    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.

    theorem MulChar.eq_one_iff {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] {χ : MulChar R R'} :
    χ = 1 ∀ (a : Rˣ), χ a = 1
    theorem MulChar.ne_one_iff {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] {χ : MulChar R R'} :
    χ 1 ∃ (a : Rˣ), χ a 1
    def MulChar.IsQuadratic {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] (χ : MulChar R R') :

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

    Equations
    theorem MulChar.IsQuadratic.eq_of_eq_coe {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] {χ : MulChar R } ( : χ.IsQuadratic) {χ' : MulChar R' } (hχ' : χ'.IsQuadratic) [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 .

    def MulChar.ringHomComp {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] (χ : MulChar R R') (f : R' →+* R'') :
    MulChar R R''

    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' := }
    @[simp]
    theorem MulChar.ringHomComp_apply {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] (χ : MulChar R R') (f : R' →+* R'') (a : R) :
    (χ.ringHomComp f) a = f (χ a)
    @[simp]
    theorem MulChar.ringHomComp_one {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] (f : R' →+* R'') :
    theorem MulChar.ringHomComp_inv {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] {R : Type u_4} [CommMonoidWithZero R] (χ : MulChar R R') (f : R' →+* R'') :
    theorem MulChar.ringHomComp_mul {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] (χ φ : MulChar R R') (f : R' →+* R'') :
    (χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f
    theorem MulChar.ringHomComp_pow {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] (χ : MulChar R R') (f : R' →+* R'') (n : ) :
    χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
    theorem MulChar.injective_ringHomComp {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] {f : R' →+* R''} (hf : Function.Injective f) :
    Function.Injective fun (x : MulChar R R') => x.ringHomComp f
    theorem MulChar.ringHomComp_eq_one_iff {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] {f : R' →+* R''} (hf : Function.Injective f) {χ : MulChar R R'} :
    χ.ringHomComp f = 1 χ = 1
    theorem MulChar.ringHomComp_ne_one_iff {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] {f : R' →+* R''} (hf : Function.Injective f) {χ : MulChar R R'} :
    χ.ringHomComp f 1 χ 1
    theorem MulChar.IsQuadratic.comp {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {R'' : Type u_3} [CommRing R''] {χ : MulChar R R'} ( : χ.IsQuadratic) (f : R' →+* R'') :

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

    theorem MulChar.IsQuadratic.inv {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {χ : MulChar R R'} ( : χ.IsQuadratic) :
    χ⁻¹ = χ

    The inverse of a quadratic character is itself. →

    theorem MulChar.IsQuadratic.sq_eq_one {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {χ : MulChar R R'} ( : χ.IsQuadratic) :
    χ ^ 2 = 1

    The square of a quadratic character is the trivial character.

    theorem MulChar.IsQuadratic.pow_char {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {χ : MulChar R R'} ( : χ.IsQuadratic) (p : ) [hp : Fact (Nat.Prime p)] [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_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {χ : MulChar R R'} ( : χ.IsQuadratic) {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_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] {χ : MulChar R R'} ( : χ.IsQuadratic) {n : } (hn : Odd n) :
    χ ^ n = χ

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

    theorem MulChar.isQuadratic_iff_sq_eq_one {M : Type u_4} {R : Type u_5} [CommMonoid M] [CommRing R] [NoZeroDivisors R] [Nontrivial R] {χ : MulChar M R} :
    χ.IsQuadratic χ ^ 2 = 1

    A multiplicative character χ into an integral domain is quadratic if and only if χ^2 = 1.

    Multiplicative characters with finite domain #

    theorem MulChar.pow_card_eq_one {M : Type u_1} [CommMonoid M] {R : Type u_2} [CommMonoidWithZero R] [Fintype Mˣ] (χ : MulChar M R) :

    If χ is a multiplicative character on a commutative monoid M with finitely many units, then χ ^ #Mˣ = 1.

    theorem MulChar.orderOf_pos {M : Type u_1} [CommMonoid M] {R : Type u_2} [CommMonoidWithZero R] [Finite Mˣ] (χ : MulChar M R) :
    0 < orderOf χ

    A multiplicative character on a commutative monoid with finitely many units has finite (= positive) order.

    theorem MulChar.sum_eq_zero_of_ne_one {R : Type u_1} [CommMonoid R] [Fintype R] {R' : Type u_2} [CommRing R'] [IsDomain R'] {χ : MulChar R R'} ( : χ 1) :
    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 MulChar.sum_one_eq_card_units {R : Type u_1} [CommMonoid R] [Fintype R] {R' : Type u_2} [CommRing R'] [DecidableEq R] :
    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.

    Multiplicative characters on rings #

    theorem MulChar.val_neg_one_eq_one_of_odd_order {R : Type u_1} {R' : Type u_2} [CommRing R] [CommMonoidWithZero R'] {χ : MulChar R R'} {n : } (hn : Odd n) ( : χ ^ n = 1) :
    χ (-1) = 1

    If χ is of odd order, then χ(-1) = 1