Further Results on multiplicative characters

theorem MulChar.eq_iff {R : Type u_1} {R' : Type u_2} [CommMonoid R] [CommMonoidWithZero R'] {g : Rˣ} (hg : ∀ (x : Rˣ), x ∈ Subgroup.zpowers g) (χ₁ χ₂ : MulChar R R') : χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g

Two multiplicative characters on a monoid whose unit group is generated by g are equal if and only if they agree on g.

def MulChar.starComp {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [StarRing R'] (χ : MulChar R R') : MulChar R R'

Define the conjugation (star) of a multiplicative character by conjugating pointwise.

Equations

• χ.starComp = χ.ringHomComp (starRingEnd R')

@[simp]

theorem MulChar.starComp_apply {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [StarRing R'] (χ : MulChar R R') (a : R) : χ.starComp a = (starRingEnd R') (χ a)

instance MulChar.instStarMul {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [StarRing R'] : StarMul (MulChar R R')

Equations

• MulChar.instStarMul = { star := MulChar.starComp, star_involutive := ⋯, star_mul := ⋯ }

@[simp]

theorem MulChar.star_apply {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [StarRing R'] (χ : MulChar R R') (a : R) : (star χ) a = star (χ a)

theorem MulChar.apply_mem_rootsOfUnity {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Fintype Rˣ] (a : Rˣ) {χ : MulChar R R'} : (equivToUnitHom χ) a ∈ rootsOfUnity (Fintype.card Rˣ) R'

The values of a multiplicative character on R are nth roots of unity, where n = #Rˣ.

theorem MulChar.star_eq_inv {R : Type u_1} [CommRing R] [Finite Rˣ] (χ : MulChar R ℂ) : star χ = χ⁻¹

The conjugate of a multiplicative character with values in ℂ is its inverse.

theorem MulChar.star_apply' {R : Type u_1} [CommRing R] [Finite Rˣ] (χ : MulChar R ℂ) (a : R) : star (χ a) = χ⁻¹ a

Multiplicative characters on finite monoids with cyclic unit group

noncomputable def MulChar.ofRootOfUnity {M : Type u_1} [CommMonoid M] [Fintype M] [DecidableEq M] {R : Type u_2} [CommMonoidWithZero R] {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ} (hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g) : MulChar M R

Given a finite monoid M with unit group Mˣ cyclic of order n and an nth root of unity ζ in R, there is a multiplicative character M → R that sends a given generator of Mˣ to ζ.

Equations

• MulChar.ofRootOfUnity hζ hg = MulChar.ofUnitHom (monoidHomOfForallMemZpowers hg ⋯)

theorem MulChar.ofRootOfUnity_spec {M : Type u_1} [CommMonoid M] [Fintype M] [DecidableEq M] {R : Type u_2} [CommMonoidWithZero R] {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ} (hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g) : (ofRootOfUnity hζ hg) ↑g = ↑ζ

noncomputable def MulChar.equiv_rootsOfUnity (M : Type u_1) [CommMonoid M] [Fintype M] [DecidableEq M] (R : Type u_2) [CommMonoidWithZero R] [inst_cyc : IsCyclic Mˣ] : MulChar M R ≃* ↥(rootsOfUnity (Fintype.card Mˣ) R)

The group of multiplicative characters on a finite monoid M with cyclic unit group Mˣ of order n is isomorphic to the group of nth roots of unity in the target R.

Equations

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

Multiplicative characters on finite fields

theorem MulChar.exists_mulChar_orderOf (F : Type u_1) [Field F] [Fintype F] {R : Type u_2} [CommRing R] {n : ℕ} (h : n ∣ Fintype.card F - 1) {ζ : R} (hζ : IsPrimitiveRoot ζ n) : ∃ (χ : MulChar F R), orderOf χ = n

There is a character of order n on F if #F ≡ 1 mod n and the target contains a primitive nth root of unity.

theorem MulChar.orderOf_dvd_card_sub_one (F : Type u_1) [Field F] [Fintype F] {R : Type u_2} [CommRing R] (χ : MulChar F R) : orderOf χ ∣ Fintype.card F - 1

If there is a multiplicative character of order n on F, then #F ≡ 1 mod n.

theorem MulChar.exists_mulChar_orderOf_eq_card_units (F : Type u_1) [Field F] [Fintype F] {R : Type u_2} [CommRing R] [DecidableEq F] {ζ : R} (hζ : IsPrimitiveRoot ζ (Fintype.card Fˣ)) : ∃ (χ : MulChar F R), orderOf χ = Fintype.card Fˣ

There is always a character on F of order #F-1 with values in a ring that has a primitive (#F-1)th root of unity.

theorem MulChar.apply_mem_rootsOfUnity_orderOf {F : Type u_1} [Field F] [Finite F] {R : Type u_2} [CommRing R] (χ : MulChar F R) {a : F} (ha : a ≠ 0) : ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ↑ζ = χ a

theorem MulChar.apply_mem_rootsOfUnity_of_pow_eq_one {F : Type u_1} [Field F] [Finite F] {R : Type u_2} [CommRing R] {χ : MulChar F R} {n : ℕ} (hχ : χ ^ n = 1) {a : F} (ha : a ≠ 0) : ∃ ζ ∈ rootsOfUnity n R, ↑ζ = χ a

The non-zero values of a multiplicative character χ such that χ^n = 1 are nth roots of unity.

theorem MulChar.exists_apply_eq_pow {F : Type u_1} [Field F] [Finite F] {R : Type u_2} [CommRing R] [IsDomain R] {χ : MulChar F R} {n : ℕ} [NeZero n] (hχ : χ ^ n = 1) {μ : R} (hμ : IsPrimitiveRoot μ n) {a : F} (ha : a ≠ 0) : ∃ k < n, χ a = μ ^ k

If χ is a multiplicative character with χ^n = 1 and μ is a primitive nth root of unity, then, for a ≠ 0, there is some k such that χ a = μ^k.

theorem MulChar.apply_mem_algebraAdjoin_of_pow_eq_one {F : Type u_1} [Field F] [Finite F] {R : Type u_2} [CommRing R] [IsDomain R] {χ : MulChar F R} {n : ℕ} [NeZero n] (hχ : χ ^ n = 1) {μ : R} (hμ : IsPrimitiveRoot μ n) (a : F) : χ a ∈ Algebra.adjoin ℤ {μ}

The values of a multiplicative character χ such that χ^n = 1 are contained in ℤ[μ] when μ is a primitive nth root of unity.

theorem MulChar.apply_mem_algebraAdjoin {F : Type u_1} [Field F] [Finite F] {R : Type u_2} [CommRing R] [IsDomain R] {χ : MulChar F R} {μ : R} (hμ : IsPrimitiveRoot μ (orderOf χ)) (a : F) : χ a ∈ Algebra.adjoin ℤ {μ}

The values of a multiplicative character of order n are contained in ℤ[μ] when μ is a primitive nth root of unity.