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.

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

• toFun : R → R'
• map_one' : OneHom.toFun (↑s.toMonoidHom) 1 = 1
• map_mul' : ∀ (x y : R), OneHom.toFun (↑s.toMonoidHom) (x * y) = OneHom.toFun (↑s.toMonoidHom) x * OneHom.toFun (↑s.toMonoidHom) y
• map_nonunit' : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑s.toMonoidHom) 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.

instance funLike (R : Type u) [CommMonoid R] (R' : Type v) [CommMonoidWithZero R'] : FunLike (MulChar R R') R fun x => R'

Equations

• funLike R R' = { coe := fun χ => χ.toFun, coe_injective' := (_ : ∀ (χ₀ χ₁ : MulChar R R'), (fun χ => χ.toFun) χ₀ = (fun χ => χ.toFun) χ₁ → χ₀ = χ₁) }

class MulCharClass (F : Type u_1) (R : outParam (Type u_2)) (R' : outParam (Type u_3)) [CommMonoid R] [CommMonoidWithZero R'] extends MonoidHomClass : Type (max (max u_1 u_2) u_3)

• coe : F → R → R'
• 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}, ¬IsUnit a → ↑χ a = 0

This is the corresponding extension of MonoidHomClass.

@[simp]

theorem MulChar.trivial_apply (R : Type u) [CommMonoid R] (R' : Type v) [CommMonoidWithZero R'] (x : R) : ↑(MulChar.trivial R R') x = if IsUnit x then 1 else 0

noncomputable def MulChar.trivial (R : Type u) [CommMonoid R] (R' : Type v) [CommMonoidWithZero R'] : MulChar R R'

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MulChar.coe_mk {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (f : R →* R') (hf : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑f) a = 0) : ↑{ toMonoidHom := f, map_nonunit' := hf } = ↑f

theorem MulChar.ext' {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] {χ : 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} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] : MulCharClass (MulChar R R') R R'

Equations

• MulChar.instMulCharClassMulChar = MulCharClass.mk (_ : ∀ (χ : MulChar R R') {a : R}, ¬IsUnit a → OneHom.toFun (↑χ.toMonoidHom) a = 0)

theorem MulChar.map_nonunit {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') {a : R} (ha : ¬IsUnit a) : ↑χ a = 0

theorem MulChar.ext {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] {χ : 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} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] {χ : 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} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') : Rˣ →* R'ˣ

Turn a MulChar into a homomorphism between the unit groups.

Equations

• MulChar.toUnitHom χ = Units.map ↑χ

theorem MulChar.coe_toUnitHom {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') (a : Rˣ) : ↑(↑(MulChar.toUnitHom χ) a) = ↑χ ↑a

noncomputable def MulChar.ofUnitHom {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) : MulChar R R'

Turn a homomorphism between unit groups into a MulChar.

Equations

• One or more equations did not get rendered due to their size.

theorem MulChar.ofUnitHom_coe {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ) : ↑(MulChar.ofUnitHom f) ↑a = ↑(↑f a)

noncomputable def MulChar.equivToUnitHom {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] : MulChar R R' ≃ (Rˣ →* R'ˣ)

The equivalence between multiplicative characters and homomorphisms of unit groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MulChar.toUnitHom_eq {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') : MulChar.toUnitHom χ = ↑MulChar.equivToUnitHom χ

@[simp]

theorem MulChar.ofUnitHom_eq {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : Rˣ →* R'ˣ) : MulChar.ofUnitHom χ = ↑MulChar.equivToUnitHom.symm χ

@[simp]

theorem MulChar.coe_equivToUnitHom {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') (a : Rˣ) : ↑(↑(↑MulChar.equivToUnitHom χ) a) = ↑χ ↑a

@[simp]

theorem MulChar.equivToUnitHom_symm_coe {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ) : ↑(↑MulChar.equivToUnitHom.symm f) ↑a = ↑(↑f a)

@[simp]

theorem MulChar.coe_toMonoidHom {R : Type u} {R' : Type v} [CommMonoidWithZero R'] [CommMonoid 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} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') : ↑χ 1 = 1

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

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

theorem MulChar.map_ringChar {R' : Type v} [CommMonoidWithZero R'] {R : Type u} [CommRing 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} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] : One (MulChar R R')

Equations

• MulChar.hasOne = { one := MulChar.trivial R R' }

noncomputable instance MulChar.inhabited {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] : Inhabited (MulChar R R')

Equations

• MulChar.inhabited = { default := 1 }

@[simp]

theorem MulChar.one_apply_coe {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (a : Rˣ) : ↑1 ↑a = 1

Evaluation of the trivial character

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

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

Equations

• One or more equations did not get rendered due to their size.

instance MulChar.hasMul {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] : Mul (MulChar R R')

Equations

• MulChar.hasMul = { mul := MulChar.mul }

theorem MulChar.mul_apply {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') (χ' : MulChar R R') (a : R) : ↑(χ * χ') a = ↑χ a * ↑χ' a

@[simp]

theorem MulChar.coeToFun_mul {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') (χ' : MulChar R R') : ↑(χ * χ') = ↑χ * ↑χ'

theorem MulChar.one_mul {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') : 1 * χ = χ

theorem MulChar.mul_one {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') : χ * 1 = χ

noncomputable def MulChar.inv {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') : MulChar R R'

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance MulChar.hasInv {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] : Inv (MulChar R R')

Equations

• MulChar.hasInv = { inv := MulChar.inv }

theorem MulChar.inv_apply_eq_inv {R : Type u} [CommMonoid R] {R' : Type v} [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} [CommMonoid R] {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} [CommMonoidWithZero R'] {R : Type u} [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 v} [CommMonoidWithZero R'] {R : Type u} [Field 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} [CommMonoid R] {R' : Type v} [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} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] : CommGroup (MulChar R R')

The commutative group structure on MulChar R R'.

Equations

• MulChar.commGroup = CommGroup.mk (_ : ∀ (χ₁ χ₂ : MulChar R R'), χ₁ * χ₂ = χ₂ * χ₁)

theorem MulChar.pow_apply_coe {R : Type u} [CommMonoid R] {R' : Type v} [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} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : 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} [CommRing R] {R' : Type v} [CommRing R'] (χ : MulChar R R') : Prop

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

Equations

• MulChar.IsNontrivial χ = ∃ a, ↑χ ↑a ≠ 1

theorem MulChar.isNontrivial_iff {R : Type u} [CommRing R] {R' : Type v} [CommRing R'] (χ : MulChar R R') : MulChar.IsNontrivial χ ↔ χ ≠ 1

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

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

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

Equations

• MulChar.IsQuadratic χ = ∀ (a : R), ↑χ a = 0 ∨ ↑χ a = 1 ∨ ↑χ a = -1

theorem MulChar.IsQuadratic.eq_of_eq_coe {R : Type u} [CommRing R] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R''] {χ : MulChar R ℤ} (hχ : MulChar.IsQuadratic χ) {χ' : MulChar R' ℤ} (hχ' : MulChar.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 ℤ.

@[simp]

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

def MulChar.ringHomComp {R : Type u} [CommRing R] {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.

Equations

• One or more equations did not get rendered due to their size.

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

Composition with an injective ring homomorphism preserves nontriviality.

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

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

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

The inverse of a quadratic character is itself. →

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

The square of a quadratic character is the trivial character.

theorem MulChar.IsQuadratic.pow_char {R : Type u} [CommRing R] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : MulChar.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} [CommRing R] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : MulChar.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} [CommRing R] {R' : Type v} [CommRing R'] {χ : MulChar R R'} (hχ : MulChar.IsQuadratic χ) {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} [CommRing R] {R' : Type v} [CommRing R'] [Fintype R] [IsDomain R'] {χ : MulChar R R'} (hχ : MulChar.IsNontrivial χ) : (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} [CommRing R] {R' : Type v} [CommRing R'] [Fintype R] [DecidableEq R] : (Finset.sum Finset.univ fun a => ↑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.