Documentation

Mathlib.Algebra.Group.AddChar

Characters from additive to multiplicative monoids #

Let A be an additive monoid, and M a multiplicative one. An additive character of A with values in M is simply a map A → M which intertwines the addition operation on A with the multiplicative operation on M.

We define these objects, using the namespace AddChar, and show that if A is a commutative group under addition, then the additive characters are also a group (written multiplicatively). Note that we do not need M to be a group here.

We also include some constructions specific to the case when A = R is a ring; then we define mulShift ψ r, where ψ : AddChar R M and r : R, to be the character defined by x ↦ ψ (r * x).

For more refined results of a number-theoretic nature (primitive characters, Gauss sums, etc) see Mathlib.NumberTheory.LegendreSymbol.AddCharacter.

Tags #

additive character

structure AddChar (A : Type u_1) [AddMonoid A] (M : Type u_2) [Monoid M] :
Type (max u_1 u_2)

AddChar A M is the type of maps A → M, for A an additive monoid and M a multiplicative monoid, which intertwine addition in A with multiplication in M.

We only put the typeclasses needed for the definition, although in practice we are usually interested in much more specific cases (e.g. when A is a group and M a commutative ring).

  • toFun : AM

    The underlying function.

    Do not use this function directly. Instead use the coercion coming from the FunLike instance.

  • map_zero_eq_one' : self.toFun 0 = 1

    The function maps 0 to 1.

    Do not use this directly. Instead use AddChar.map_zero_eq_one.

  • map_add_eq_mul' : ∀ (a b : A), self.toFun (a + b) = self.toFun a * self.toFun b

    The function maps addition in A to multiplication in M.

    Do not use this directly. Instead use AddChar.map_add_eq_mul.

Instances For
    theorem AddChar.map_zero_eq_one' {A : Type u_1} [AddMonoid A] {M : Type u_2} [Monoid M] (self : AddChar A M) :
    self.toFun 0 = 1

    The function maps 0 to 1.

    Do not use this directly. Instead use AddChar.map_zero_eq_one.

    theorem AddChar.map_add_eq_mul' {A : Type u_1} [AddMonoid A] {M : Type u_2} [Monoid M] (self : AddChar A M) (a : A) (b : A) :
    self.toFun (a + b) = self.toFun a * self.toFun b

    The function maps addition in A to multiplication in M.

    Do not use this directly. Instead use AddChar.map_add_eq_mul.

    instance AddChar.instFunLike {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] :
    FunLike (AddChar A M) A M

    Define coercion to a function.

    Equations
    • AddChar.instFunLike = { coe := AddChar.toFun, coe_injective' := }
    theorem AddChar.ext {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (f : AddChar A M) (g : AddChar A M) (h : ∀ (x : A), f x = g x) :
    f = g
    @[simp]
    theorem AddChar.coe_mk {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (f : AM) (map_zero_eq_one' : f 0 = 1) (map_add_eq_mul' : ∀ (a b : A), f (a + b) = f a * f b) :
    { toFun := f, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } = f
    @[simp]
    theorem AddChar.map_zero_eq_one {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) :
    ψ 0 = 1

    An additive character maps 0 to 1.

    theorem AddChar.map_add_eq_mul {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (x : A) (y : A) :
    ψ (x + y) = ψ x * ψ y

    An additive character maps sums to products.

    @[deprecated AddChar.map_zero_eq_one]
    theorem AddChar.map_zero_one {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) :
    ψ 0 = 1

    Alias of AddChar.map_zero_eq_one.


    An additive character maps 0 to 1.

    @[deprecated AddChar.map_add_eq_mul]
    theorem AddChar.map_add_mul {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (x : A) (y : A) :
    ψ (x + y) = ψ x * ψ y

    Alias of AddChar.map_add_eq_mul.


    An additive character maps sums to products.

    def AddChar.toMonoidHom {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (φ : AddChar A M) :

    Interpret an additive character as a monoid homomorphism.

    Equations
    • φ.toMonoidHom = { toFun := φ.toFun, map_one' := , map_mul' := }
    Instances For
      @[simp]
      theorem AddChar.toMonoidHom_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (a : Multiplicative A) :
      ψ.toMonoidHom a = ψ (Multiplicative.toAdd a)
      theorem AddChar.map_nsmul_eq_pow {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (n : ) (x : A) :
      ψ (n x) = ψ x ^ n

      An additive character maps multiples by natural numbers to powers.

      @[deprecated AddChar.map_nsmul_eq_pow]
      theorem AddChar.map_nsmul_pow {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (n : ) (x : A) :
      ψ (n x) = ψ x ^ n

      Alias of AddChar.map_nsmul_eq_pow.


      An additive character maps multiples by natural numbers to powers.

      def AddChar.toMonoidHomEquiv {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] :

      Additive characters A → M are the same thing as monoid homomorphisms from Multiplicative A to M.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem AddChar.coe_toMonoidHomEquiv {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) :
        (AddChar.toMonoidHomEquiv ψ) = ψ Multiplicative.toAdd
        @[simp]
        theorem AddChar.coe_toMonoidHomEquiv_symm {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : Multiplicative A →* M) :
        (AddChar.toMonoidHomEquiv.symm ψ) = ψ Multiplicative.ofAdd
        @[simp]
        theorem AddChar.toMonoidHomEquiv_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (a : Multiplicative A) :
        (AddChar.toMonoidHomEquiv ψ) a = ψ (Multiplicative.toAdd a)
        @[simp]
        theorem AddChar.toMonoidHomEquiv_symm_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : Multiplicative A →* M) (a : A) :
        (AddChar.toMonoidHomEquiv.symm ψ) a = ψ (Multiplicative.ofAdd a)
        def AddChar.toAddMonoidHom {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (φ : AddChar A M) :

        Interpret an additive character as a monoid homomorphism.

        Equations
        • φ.toAddMonoidHom = { toFun := φ.toFun, map_zero' := , map_add' := }
        Instances For
          @[simp]
          theorem AddChar.coe_toAddMonoidHom {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) :
          ψ.toAddMonoidHom = Additive.ofMul ψ
          @[simp]
          theorem AddChar.toAddMonoidHom_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (a : A) :
          ψ.toAddMonoidHom a = Additive.ofMul (ψ a)
          def AddChar.toAddMonoidHomEquiv {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] :

          Additive characters A → M are the same thing as additive homomorphisms from A to Additive M.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem AddChar.coe_toAddMonoidHomEquiv {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) :
            (AddChar.toAddMonoidHomEquiv ψ) = Additive.ofMul ψ
            @[simp]
            theorem AddChar.coe_toAddMonoidHomEquiv_symm {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : A →+ Additive M) :
            (AddChar.toAddMonoidHomEquiv.symm ψ) = Additive.toMul ψ
            @[simp]
            theorem AddChar.toAddMonoidHomEquiv_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (a : A) :
            (AddChar.toAddMonoidHomEquiv ψ) a = Additive.ofMul (ψ a)
            @[simp]
            theorem AddChar.toAddMonoidHomEquiv_symm_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : A →+ Additive M) (a : A) :
            (AddChar.toAddMonoidHomEquiv.symm ψ) a = Additive.toMul (ψ a)
            instance AddChar.instOne {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] :
            One (AddChar A M)

            The trivial additive character (sending everything to 1) is (1 : AddChar A M).

            Equations
            • AddChar.instOne = AddChar.toMonoidHomEquiv.one
            @[simp]
            theorem AddChar.coe_one {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] :
            1 = 1
            @[simp]
            theorem AddChar.one_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (a : A) :
            1 a = 1
            instance AddChar.instInhabited {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] :
            Equations
            • AddChar.instInhabited = { default := 1 }
            def MonoidHom.compAddChar {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] {N : Type u_5} [Monoid N] (f : M →* N) (φ : AddChar A M) :

            Composing a MonoidHom with an AddChar yields another AddChar.

            Equations
            • f.compAddChar φ = AddChar.toMonoidHomEquiv.symm (f.comp φ.toMonoidHom)
            Instances For
              @[simp]
              theorem MonoidHom.coe_compAddChar {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] {N : Type u_5} [Monoid N] (f : M →* N) (φ : AddChar A M) :
              (f.compAddChar φ) = f φ
              @[simp]
              theorem MonoidHom.compAddChar_apply {A : Type u_1} {M : Type u_3} {N : Type u_4} [AddMonoid A] [Monoid M] [Monoid N] (f : M →* N) (φ : AddChar A M) :
              (f.compAddChar φ) = f φ
              theorem MonoidHom.compAddChar_injective_left {A : Type u_1} {M : Type u_3} {N : Type u_4} [AddMonoid A] [Monoid M] [Monoid N] (ψ : AddChar A M) (hψ : Function.Surjective ψ) :
              Function.Injective fun (f : M →* N) => f.compAddChar ψ
              theorem MonoidHom.compAddChar_injective_right {B : Type u_2} {M : Type u_3} {N : Type u_4} [AddMonoid B] [Monoid M] [Monoid N] (f : M →* N) (hf : Function.Injective f) :
              Function.Injective fun (ψ : AddChar B M) => f.compAddChar ψ
              def AddChar.compAddMonoidHom {A : Type u_1} {B : Type u_2} {M : Type u_3} [AddMonoid A] [AddMonoid B] [Monoid M] (φ : AddChar B M) (f : A →+ B) :

              Composing an AddChar with an AddMonoidHom yields another AddChar.

              Equations
              • φ.compAddMonoidHom f = AddChar.toAddMonoidHomEquiv.symm (φ.toAddMonoidHom.comp f)
              Instances For
                @[simp]
                theorem AddChar.coe_compAddMonoidHom {A : Type u_1} {B : Type u_2} {M : Type u_3} [AddMonoid A] [AddMonoid B] [Monoid M] (φ : AddChar B M) (f : A →+ B) :
                (φ.compAddMonoidHom f) = φ f
                @[simp]
                theorem AddChar.compAddMonoidHom_apply {A : Type u_1} {B : Type u_2} {M : Type u_3} [AddMonoid A] [AddMonoid B] [Monoid M] (ψ : AddChar B M) (f : A →+ B) (a : A) :
                (ψ.compAddMonoidHom f) a = ψ (f a)
                theorem AddChar.compAddMonoidHom_injective_left {A : Type u_1} {B : Type u_2} {M : Type u_3} [AddMonoid A] [AddMonoid B] [Monoid M] (f : A →+ B) (hf : Function.Surjective f) :
                Function.Injective fun (ψ : AddChar B M) => ψ.compAddMonoidHom f
                theorem AddChar.compAddMonoidHom_injective_right {A : Type u_1} {B : Type u_2} {M : Type u_3} [AddMonoid A] [AddMonoid B] [Monoid M] (ψ : AddChar B M) (hψ : Function.Injective ψ) :
                Function.Injective fun (f : A →+ B) => ψ.compAddMonoidHom f
                theorem AddChar.eq_one_iff {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] {ψ : AddChar A M} :
                ψ = 1 ∀ (x : A), ψ x = 1
                theorem AddChar.ne_one_iff {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] {ψ : AddChar A M} :
                ψ 1 ∃ (x : A), ψ x 1
                @[deprecated]
                def AddChar.IsNontrivial {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) :

                An additive character is nontrivial if it takes a value ≠ 1.

                Equations
                • ψ.IsNontrivial = ∃ (a : A), ψ a 1
                Instances For
                  @[deprecated AddChar.ne_one_iff]
                  theorem AddChar.isNontrivial_iff_ne_trivial {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) :
                  ψ.IsNontrivial ψ 1

                  An additive character is nontrivial iff it is not the trivial character.

                  instance AddChar.instCommMonoid {A : Type u_1} {M : Type u_2} [AddMonoid A] [CommMonoid M] :

                  When M is commutative, AddChar A M is a commutative monoid.

                  Equations
                  • AddChar.instCommMonoid = AddChar.toMonoidHomEquiv.commMonoid
                  @[simp]
                  theorem AddChar.coe_mul {A : Type u_1} {M : Type u_2} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (χ : AddChar A M) :
                  (ψ * χ) = ψ * χ
                  @[simp]
                  theorem AddChar.coe_pow {A : Type u_1} {M : Type u_2} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (n : ) :
                  (ψ ^ n) = ψ ^ n
                  @[simp]
                  theorem AddChar.mul_apply {A : Type u_1} {M : Type u_2} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (φ : AddChar A M) (a : A) :
                  (ψ * φ) a = ψ a * φ a
                  @[simp]
                  theorem AddChar.pow_apply {A : Type u_1} {M : Type u_2} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (n : ) (a : A) :
                  (ψ ^ n) a = ψ a ^ n

                  The natural equivalence to (Multiplicative A →* M) is a monoid isomorphism.

                  Equations
                  • AddChar.toMonoidHomMulEquiv = let __src := AddChar.toMonoidHomEquiv; { toEquiv := __src, map_mul' := }
                  Instances For

                    Additive characters A → M are the same thing as additive homomorphisms from A to Additive M.

                    Equations
                    • AddChar.toAddMonoidAddEquiv = let __src := AddChar.toAddMonoidHomEquiv; { toEquiv := __src, map_add' := }
                    Instances For

                      Additive characters of additive abelian groups #

                      instance AddChar.instCommGroup {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] :

                      The additive characters on a commutative additive group form a commutative group.

                      Note that the inverse is defined using negation on the domain; we do not assume M has an inversion operation for the definition (but see AddChar.map_neg_eq_inv below).

                      Equations
                      • AddChar.instCommGroup = let __src := AddChar.instCommMonoid; CommGroup.mk
                      @[simp]
                      theorem AddChar.inv_apply {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] (ψ : AddChar A M) (x : A) :
                      ψ⁻¹ x = ψ (-x)
                      theorem AddChar.val_isUnit {A : Type u_1} {M : Type u_2} [AddGroup A] [Monoid M] (φ : AddChar A M) (a : A) :
                      IsUnit (φ a)

                      The values of an additive character on an additive group are units.

                      theorem AddChar.map_neg_eq_inv {A : Type u_1} {M : Type u_2} [AddGroup A] [DivisionMonoid M] (ψ : AddChar A M) (a : A) :
                      ψ (-a) = (ψ a)⁻¹

                      An additive character maps negatives to inverses (when defined)

                      theorem AddChar.map_zsmul_eq_zpow {A : Type u_1} {M : Type u_2} [AddGroup A] [DivisionMonoid M] (ψ : AddChar A M) (n : ) (a : A) :
                      ψ (n a) = ψ a ^ n

                      An additive character maps integer scalar multiples to integer powers.

                      @[deprecated AddChar.map_neg_eq_inv]
                      theorem AddChar.map_neg_inv {A : Type u_1} {M : Type u_2} [AddGroup A] [DivisionMonoid M] (ψ : AddChar A M) (a : A) :
                      ψ (-a) = (ψ a)⁻¹

                      Alias of AddChar.map_neg_eq_inv.


                      An additive character maps negatives to inverses (when defined)

                      @[deprecated AddChar.map_zsmul_eq_zpow]
                      theorem AddChar.map_zsmul_zpow {A : Type u_1} {M : Type u_2} [AddGroup A] [DivisionMonoid M] (ψ : AddChar A M) (n : ) (a : A) :
                      ψ (n a) = ψ a ^ n

                      Alias of AddChar.map_zsmul_eq_zpow.


                      An additive character maps integer scalar multiples to integer powers.

                      theorem AddChar.inv_apply' {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (ψ : AddChar A M) (x : A) :
                      ψ⁻¹ x = (ψ x)⁻¹
                      theorem AddChar.map_sub_eq_div {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (ψ : AddChar A M) (a : A) (b : A) :
                      ψ (a - b) = ψ a / ψ b
                      theorem AddChar.injective_iff {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] {ψ : AddChar A M} :
                      Function.Injective ψ ∀ ⦃x : A⦄, ψ x = 1x = 0

                      Additive characters of rings #

                      def AddChar.mulShift {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) (r : R) :

                      Define the multiplicative shift of an additive character. This satisfies mulShift ψ a x = ψ (a * x).

                      Equations
                      Instances For
                        @[simp]
                        theorem AddChar.mulShift_apply {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] {ψ : AddChar R M} {r : R} {x : R} :
                        (ψ.mulShift r) x = ψ (r * x)
                        theorem AddChar.inv_mulShift {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) :
                        ψ⁻¹ = ψ.mulShift (-1)

                        ψ⁻¹ = mulShift ψ (-1)).

                        theorem AddChar.mulShift_spec' {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) (n : ) (x : R) :
                        (ψ.mulShift n) x = ψ x ^ n

                        If n is a natural number, then mulShift ψ n x = (ψ x) ^ n.

                        theorem AddChar.pow_mulShift {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) (n : ) :
                        ψ ^ n = ψ.mulShift n

                        If n is a natural number, then ψ ^ n = mulShift ψ n.

                        theorem AddChar.mulShift_mul {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) (r : R) (s : R) :
                        ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)

                        The product of mulShift ψ r and mulShift ψ s is mulShift ψ (r + s).

                        theorem AddChar.mulShift_mulShift {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) (r : R) (s : R) :
                        (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)
                        @[simp]
                        theorem AddChar.mulShift_zero {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) :
                        ψ.mulShift 0 = 1

                        mulShift ψ 0 is the trivial character.

                        @[simp]
                        theorem AddChar.mulShift_one {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) :
                        ψ.mulShift 1 = ψ
                        theorem AddChar.mulShift_unit_eq_one_iff {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) {u : R} (hu : IsUnit u) :
                        ψ.mulShift u = 1 ψ = 1