Multiplicative characters of finite rings and fields

Let R and R' be 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_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.

• toFun : R → R'
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' (x y : R) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• map_nonunit' (a : R) : ¬IsUnit a → (↑self.toMonoidHom).toFun a = 0

@[instance_reducible]

instance MulChar.instFunLike (R : Type u_1) [CommMonoid R] (R' : Type u_2) [CommMonoidWithZero R'] : FunLike (MulChar R R') R R'

Equations

• MulChar.instFunLike R R' = { coe := fun (χ : MulChar R R') => (↑χ.toMonoidHom).toFun, coe_injective := ⋯ }

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

This is the corresponding extension of MonoidHomClass.

• 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

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

• MulChar.trivial R R' = { toFun := fun (x : R) => if IsUnit x then 1 else 0, map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }

@[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') : Rˣ →* R'ˣ

Turn a MulChar into a homomorphism between the unit groups.

Equations

• χ.toUnitHom = Units.map ↑χ

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

• MulChar.ofUnitHom f = { toFun := fun (x : R) => if hx : IsUnit x then ↑(f hx.unit) else 0, map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }

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

• MulChar.equivToUnitHom = { toFun := MulChar.toUnitHom, invFun := MulChar.ofUnitHom, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[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

theorem MulChar.apply_ne_zero_iff {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] [Nontrivial R'] {χ : MulChar R R'} {a : R} : χ a ≠ 0 ↔ IsUnit a

theorem MulChar.apply_eq_zero_iff {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] [Nontrivial R'] {χ : MulChar R R'} {a : R} : χ a = 0 ↔ ¬IsUnit a

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.

def MulChar.toMonoidWithZeroHom {R' : Type u_2} [CommMonoidWithZero R'] {R : Type u_3} [CommMonoidWithZero R] [Nontrivial R] (χ : MulChar R R') : R →*₀ R'

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.

@[instance_reducible]

noncomputable instance MulChar.hasOne {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] : One (MulChar R R')

Equations

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

@[instance_reducible]

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

Equations

• MulChar.inhabited = { default := 1 }

@[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_reducible]

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

Equations

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

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

• χ.inv = { toFun := fun (a : R) => MonoidWithZero.inverse (χ a), map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }

@[instance_reducible]

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

Equations

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

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.

@[instance_reducible]

noncomputable instance MulChar.commGroup {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] : CommGroup (MulChar R 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

• MulChar.mulEquivToUnitHom = { toEquiv := MulChar.equivToUnitHom, map_mul' := ⋯ }

@[simp]

theorem MulChar.mulEquivToUnitHom_apply {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (χ : MulChar R R') : mulEquivToUnitHom χ = equivToUnitHom χ

@[simp]

theorem MulChar.mulEquivToUnitHom_symm_apply {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) : mulEquivToUnitHom.symm f = equivToUnitHom.symm f

noncomputable def MulChar.restrict {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] {S : Type u_3} [SetLike S R] [SubmonoidClass S R] (T : S) (χ : MulChar R R') : MulChar (↥T) R'

The restriction of a MulChar to a submonoid.

Equations

• MulChar.restrict T χ = MulChar.ofUnitHom (χ.toUnitHom.comp (Units.map (SubmonoidClass.subtype T)))

@[simp]

theorem MulChar.restrict_apply {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] {S : Type u_3} [SetLike S R] [SubmonoidClass S R] (T : S) (χ : MulChar R R') (x : ↥T) : (restrict T χ) x = if IsUnit x then χ ↑x else 0

noncomputable def MulChar.restrictHom {R : Type u_1} [CommMonoid R] {S : Type u_3} [SetLike S R] [SubmonoidClass S R] (T : S) (R'' : Type u_4) [CommMonoidWithZero R''] : MulChar R R'' →* MulChar (↥T) R''

The restriction of a MulChar to a submonoid as an homomorphism.

Equations

• MulChar.restrictHom T R'' = { toFun := MulChar.restrict T, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulChar.restrictHom_apply {R : Type u_1} [CommMonoid R] {S : Type u_3} [SetLike S R] [SubmonoidClass S R] (T : S) (R'' : Type u_4) [CommMonoidWithZero R''] (χ : MulChar R R'') : (restrictHom T R'') χ = restrict T χ

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

theorem MulChar.restrict_eq_one_iff {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommMonoidWithZero R'] {S : Type u_3} [SetLike S R] [SubmonoidClass S R] {T : S} {χ : MulChar R R'} : restrict T χ = 1 ↔ ∀ (x : (↥T)ˣ), χ ↑↑x = 1

def MulChar.IsQuadratic {R : Type u_1} [CommMonoid R] {R' : Type u_2} [CommRing R'] (χ : MulChar R R') : Prop

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

Equations

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

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 ℤ} (hχ : χ.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'') : ringHomComp 1 f = 1

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'') : (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f

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

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

Bundled version of MulChar.ringHomComp as a MonoidHom.

Equations

• MulChar.ringHomCompHom f = { toFun := fun (χ : MulChar R R') => χ.ringHomComp f, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

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

theorem MulChar.ringHomComp_zpow {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.zpow_apply_coe {R : Type u_4} [CommGroupWithZero R] {R' : Type u_5} [CommRing 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.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'} (hχ : χ.IsQuadratic) (f : R' →+* R'') : (χ.ringHomComp f).IsQuadratic

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'} (hχ : χ.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'} (hχ : χ.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'} (hχ : χ.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'} (hχ : χ.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'} (hχ : χ.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) : χ ^ Fintype.card Mˣ = 1

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'} (hχ : χ ≠ 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) (hχ : χ ^ n = 1) : χ (-1) = 1

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