Documentation

Mathlib.NumberTheory.LegendreSymbol.MulCharacter

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

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)

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 : RR'
  • map_one' : self.toFun 1 = 1
  • map_mul' : ∀ (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y
  • map_nonunit' : ∀ (a : R), ¬IsUnit aself.toFun a = 0
Instances For
    instance MulChar.instFunLike (R : Type u) [CommMonoid R] (R' : Type v) [CommMonoidWithZero R'] :
    FunLike (MulChar R R') R R'
    Equations
    class MulCharClass (F : Type u_1) (R : outParam (Type u_2)) (R' : outParam (Type u_3)) [CommMonoid R] [CommMonoidWithZero R'] [FunLike F R R'] extends MonoidHomClass :

    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
    Instances
      @[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
      • MulChar.trivial R R' = { toMonoidHom := { toOneHom := { toFun := fun (x : R) => if IsUnit x then 1 else 0, map_one' := }, map_mul' := }, map_nonunit' := }
      Instances For
        @[simp]
        theorem MulChar.coe_mk {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (f : R →* R') (hf : ∀ (a : R), ¬IsUnit af.toFun 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.

        Equations
        • =
        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') :

        Turn a MulChar into a homomorphism between the unit groups.

        Equations
        Instances For
          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.
          Instances For
            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
            • MulChar.equivToUnitHom = { toFun := MulChar.toUnitHom, invFun := MulChar.ofUnitHom, left_inv := , right_inv := }
            Instances For
              @[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.

              @[simp]
              theorem MulChar.toMonoidWithZeroHom_apply {R' : Type v} [CommMonoidWithZero R'] {R : Type u_1} [CommMonoidWithZero R] [Nontrivial R] (χ : MulChar R R') :
              ∀ (a : R), χ a = χ.toFun a

              We can convert a multiplicative character into a homomorphism of monoids with zero when the source has a zero and another element.

              Equations
              • χ = { toZeroHom := { toFun := χ.toFun, map_zero' := }, map_one' := , map_mul' := }
              Instances For
                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
                noncomputable instance MulChar.inhabited {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero 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

                theorem MulChar.one_apply {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] {x : R} (hx : IsUnit x) :
                1 x = 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
                • MulChar.mul χ χ' = let __src := χ.toMonoidHom * χ'.toMonoidHom; { toMonoidHom := { toOneHom := { toFun := χ * χ', map_one' := }, map_mul' := }, map_nonunit' := }
                Instances For
                  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.
                  Instances For
                    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'] :

                    The commutative group structure on MulChar R R'.

                    Equations
                    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 : n 0) (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 (mostly) assume that the target is a commutative ring.

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

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

                    Equations
                    Instances For
                      theorem MulChar.isNontrivial_iff {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R'] (χ : MulChar R R') :

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

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

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

                      Equations
                      Instances For
                        theorem MulChar.IsQuadratic.eq_of_eq_coe {R : Type u} [CommMonoid 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} [CommMonoid 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} [CommMonoid 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.
                        Instances For
                          theorem MulChar.IsNontrivial.comp {R : Type u} [CommMonoid R] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R''] {χ : MulChar R R'} (hχ : MulChar.IsNontrivial χ) {f : R' →+* R''} (hf : Function.Injective f) :

                          Composition with an injective ring homomorphism preserves nontriviality.

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

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

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