Documentation

Mathlib.NumberTheory.DirichletCharacter.Basic

Dirichlet Characters #

Let R be a commutative monoid with zero. A Dirichlet character χ of level n over R is a multiplicative character from ZMod n to R sending non-units to 0. We then obtain some properties of toUnitHom χ, the restriction of χ to a group homomorphism (ZMod n)ˣ →* Rˣ.

Main definitions:

Tags #

dirichlet character, multiplicative character

Definitions #

@[reducible, inline]
abbrev DirichletCharacter (R : Type u_1) [CommMonoidWithZero R] (n : ) :
Type (max 0 u_1)

The type of Dirichlet characters of level n.

Equations
Instances For
    theorem DirichletCharacter.toUnitHom_eq_char' {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {a : ZMod n} (ha : IsUnit a) :
    χ a = ((MulChar.toUnitHom χ) ha.unit)
    theorem DirichletCharacter.eval_modulus_sub {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) (x : ZMod n) :
    χ (n - x) = χ (-x)

    Changing levels #

    noncomputable def DirichletCharacter.changeLevel {R : Type u_1} [CommMonoidWithZero R] {n : } {m : } (hm : n m) :

    A function that modifies the level of a Dirichlet character to some multiple of its original level.

    Equations
    Instances For

      The changeLevel map is injective (except in the degenerate case m = 0).

      @[simp]
      theorem DirichletCharacter.changeLevel_eq_cast_of_dvd {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {m : } (hm : n m) (a : (ZMod m)ˣ) :
      ((DirichletCharacter.changeLevel hm) χ) a = χ (↑a).cast

      χ of level n factors through a Dirichlet character χ₀ of level d if d ∣ n and χ₀ = χ ∘ (ZMod n → ZMod d).

      Equations
      Instances For
        theorem DirichletCharacter.changeLevel_factorsThrough {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {m : } (hm : n m) :
        ((DirichletCharacter.changeLevel hm) χ).FactorsThrough n
        theorem DirichletCharacter.FactorsThrough.dvd {R : Type u_1} [CommMonoidWithZero R] {n : } {χ : DirichletCharacter R n} {d : } (h : χ.FactorsThrough d) :
        d n

        The fact that d divides n when χ factors through a Dirichlet character at level d

        noncomputable def DirichletCharacter.FactorsThrough.χ₀ {R : Type u_1} [CommMonoidWithZero R] {n : } {χ : DirichletCharacter R n} {d : } (h : χ.FactorsThrough d) :

        The Dirichlet character at level d through which χ factors

        Equations
        Instances For
          theorem DirichletCharacter.FactorsThrough.eq_changeLevel {R : Type u_1} [CommMonoidWithZero R] {n : } {χ : DirichletCharacter R n} {d : } (h : χ.FactorsThrough d) :

          The fact that χ factors through χ₀ of level d

          theorem DirichletCharacter.FactorsThrough.existsUnique {R : Type u_1} [CommMonoidWithZero R] {n : } {χ : DirichletCharacter R n} {d : } [NeZero n] (h : χ.FactorsThrough d) :

          The character of level d through which χ factors is uniquely determined.

          theorem DirichletCharacter.FactorsThrough.same_level {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
          χ.FactorsThrough n
          theorem DirichletCharacter.factorsThrough_iff_ker_unitsMap {R : Type u_1} [CommMonoidWithZero R] {n : } {χ : DirichletCharacter R n} {d : } [NeZero n] (hd : d n) :
          χ.FactorsThrough d (ZMod.unitsMap hd).ker (MulChar.toUnitHom χ).ker

          A Dirichlet character χ factors through d | n iff its associated unit-group hom is trivial on the kernel of ZMod.unitsMap.

          Edge cases #

          theorem DirichletCharacter.level_one' {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) (hn : n = 1) :
          χ = 1
          Equations
          theorem DirichletCharacter.factorsThrough_one_iff {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
          χ.FactorsThrough 1 χ = 1

          The conductor #

          The set of natural numbers d such that χ factors through a character of level d.

          Equations
          • χ.conductorSet = {d : | χ.FactorsThrough d}
          Instances For
            theorem DirichletCharacter.mem_conductorSet_iff {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {x : } :
            x χ.conductorSet χ.FactorsThrough x
            theorem DirichletCharacter.level_mem_conductorSet {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
            n χ.conductorSet
            theorem DirichletCharacter.mem_conductorSet_dvd {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {x : } (hx : x χ.conductorSet) :
            x n
            noncomputable def DirichletCharacter.conductor {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :

            The minimum natural number level n through which χ factors.

            Equations
            • χ.conductor = sInf χ.conductorSet
            Instances For
              theorem DirichletCharacter.conductor_mem_conductorSet {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
              χ.conductor χ.conductorSet
              theorem DirichletCharacter.conductor_dvd_level {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
              χ.conductor n
              theorem DirichletCharacter.factorsThrough_conductor {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
              χ.FactorsThrough χ.conductor
              theorem DirichletCharacter.conductor_ne_zero {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) (hn : n 0) :
              χ.conductor 0

              The conductor of the trivial character is 1.

              theorem DirichletCharacter.eq_one_iff_conductor_eq_one {R : Type u_1} [CommMonoidWithZero R] {n : } {χ : DirichletCharacter R n} (hn : n 0) :
              χ = 1 χ.conductor = 1
              theorem DirichletCharacter.conductor_le_conductor_mem_conductorSet {R : Type u_1} [CommMonoidWithZero R] {n : } {χ : DirichletCharacter R n} {d : } (hd : d χ.conductorSet) :
              χ.conductor (Classical.choose ).conductor

              A character is primitive if its level is equal to its conductor.

              Equations
              • χ.IsPrimitive = (χ.conductor = n)
              Instances For
                @[deprecated DirichletCharacter.IsPrimitive]

                Alias of DirichletCharacter.IsPrimitive.


                A character is primitive if its level is equal to its conductor.

                Equations
                Instances For
                  theorem DirichletCharacter.isPrimitive_def {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
                  χ.IsPrimitive χ.conductor = n
                  noncomputable def DirichletCharacter.primitiveCharacter {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
                  DirichletCharacter R χ.conductor

                  The primitive character associated to a Dirichlet character.

                  Equations
                  Instances For
                    theorem DirichletCharacter.primitiveCharacter_isPrimitive {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) :
                    χ.primitiveCharacter.IsPrimitive
                    noncomputable def DirichletCharacter.mul {R : Type u_1} [CommMonoidWithZero R] {n : } {m : } (χ₁ : DirichletCharacter R n) (χ₂ : DirichletCharacter R m) :
                    DirichletCharacter R (n.lcm m)

                    Dirichlet character associated to multiplication of Dirichlet characters, after changing both levels to the same

                    Equations
                    Instances For
                      noncomputable def DirichletCharacter.primitive_mul {R : Type u_1} [CommMonoidWithZero R] {n : } {m : } (χ₁ : DirichletCharacter R n) (χ₂ : DirichletCharacter R m) :
                      DirichletCharacter R (χ₁.mul χ₂).conductor

                      Primitive character associated to multiplication of Dirichlet characters, after changing both levels to the same

                      Equations
                      • χ₁.primitive_mul χ₂ = (χ₁.mul χ₂).primitiveCharacter
                      Instances For
                        theorem DirichletCharacter.mul_def {R : Type u_1} [CommMonoidWithZero R] {n : } {m : } {χ : DirichletCharacter R n} {ψ : DirichletCharacter R m} :
                        χ.primitive_mul ψ = (χ.mul ψ).primitiveCharacter
                        theorem DirichletCharacter.primitive_mul_isPrimitive {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {m : } (ψ : DirichletCharacter R m) :
                        (χ.primitive_mul ψ).IsPrimitive
                        @[deprecated DirichletCharacter.primitive_mul_isPrimitive]
                        theorem DirichletCharacter.isPrimitive.primitive_mul {R : Type u_1} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {m : } (ψ : DirichletCharacter R m) :
                        (χ.primitive_mul ψ).IsPrimitive

                        Alias of DirichletCharacter.primitive_mul_isPrimitive.

                        A Dirichlet character is odd if its value at -1 is -1.

                        Equations
                        • ψ.Odd = (ψ (-1) = -1)
                        Instances For

                          A Dirichlet character is even if its value at -1 is 1.

                          Equations
                          • ψ.Even = (ψ (-1) = 1)
                          Instances For
                            theorem DirichletCharacter.even_or_odd {S : Type} [CommRing S] {m : } (ψ : DirichletCharacter S m) [NoZeroDivisors S] :
                            ψ.Even ψ.Odd
                            theorem DirichletCharacter.Odd.toUnitHom_eval_neg_one {S : Type} [CommRing S] {m : } (ψ : DirichletCharacter S m) (hψ : ψ.Odd) :
                            (MulChar.toUnitHom ψ) (-1) = -1
                            theorem DirichletCharacter.Even.toUnitHom_eval_neg_one {S : Type} [CommRing S] {m : } (ψ : DirichletCharacter S m) (hψ : ψ.Even) :
                            (MulChar.toUnitHom ψ) (-1) = 1
                            theorem DirichletCharacter.Odd.eval_neg {S : Type} [CommRing S] {m : } (ψ : DirichletCharacter S m) (x : ZMod m) (hψ : ψ.Odd) :
                            ψ (-x) = -ψ x
                            theorem DirichletCharacter.Even.eval_neg {S : Type} [CommRing S] {m : } (ψ : DirichletCharacter S m) (x : ZMod m) (hψ : ψ.Even) :
                            ψ (-x) = ψ x