Documentation

Mathlib.NumberTheory.MulChar.Lemmas

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') (χ₂ : 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.

@[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)
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
    instance MulChar.instStarMul {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [StarRing R'] :
    Equations
    @[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'} :
    (MulChar.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 #

    @[reducible, inline]

    The order of the unit group of a finite monoid as a PNat (for use in rootsOfUnity).

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

      Given a finite monoid M with unit group 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 to ζ.

      Equations
      Instances For
        theorem MulChar.ofRootOfUnity_spec {M : Type u_1} [CommMonoid M] [Fintype M] [DecidableEq M] {R : Type u_2} [CommMonoidWithZero R] {ζ : Rˣ} (hζ : ζ rootsOfUnity (MulChar.Monoid.orderUnits M) R) {g : Mˣ} (hg : ∀ (x : Mˣ), x Subgroup.zpowers g) :
        (MulChar.ofRootOfUnity 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ˣ] :

        The group of multiplicative characters on a finite monoid M with cyclic unit group 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 #

          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) :

          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 ζ (MulChar.Monoid.orderUnits 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 : } (hn : n 0) (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 : } (hn : n 0) (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 : } (hn : n 0) (hχ : χ ^ n = 1) {μ : R} (hμ : IsPrimitiveRoot μ n) (a : F) :

          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) :

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