Documentation

Mathlib.NumberTheory.MulChar.Lemmas

Further Results on multiplicative characters #

source
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.

source
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
Instances For
    source
    @[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)
    source
    instance MulChar.instStarMul {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [StarRing R'] :
    StarMul (MulChar R R')
    Equations
    source
    @[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)
    source
    theorem MulChar.apply_mem_rootsOfUnity {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [Fintype Rˣ] (a : Rˣ) {χ : MulChar R R'} :
    (MulChar.equivToUnitHom χ) a ∈ rootsOfUnity (Fintype.card Rˣ) R'

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

    source
    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.

    source
    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 #

    source
    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
    Instances For
      source
      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) :
      (MulChar.ofRootOfUnity hζ hg) ↑g = ↑ζ
      source
      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.
      Instances For

        Multiplicative characters on finite fields #

        source
        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.

        source
        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.

        source
        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.

        source
        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
        source
        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.

        source
        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.

        source
        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.

        source
        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.