Documentation

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Additive characters of finite rings and fields #

This file collects some results on additive characters whose domain is (the additive group of) a finite ring or field.

Main definitions and results #

We define an additive character ψ to be primitive if mulShift ψ a is trivial only when a = 0.

We show that when ψ is primitive, then the map a ↦ mulShift ψ a is injective (AddChar.to_mulShift_inj_of_isPrimitive) and that ψ is primitive when R is a field and ψ is nontrivial (AddChar.IsNontrivial.isPrimitive).

We also show that there are primitive additive characters on R (with suitable target R') when R is a field or R = ZMod n (AddChar.primitiveCharFiniteField and AddChar.primitiveZModChar).

Finally, we show that the sum of all character values is zero when the character is nontrivial (and the target is a domain); see AddChar.sum_eq_zero_of_isNontrivial.

Tags #

additive character

theorem AddChar.val_mem_rootsOfUnity {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] (φ : AddChar R R') (a : R) (h : 0 < ringChar R) :
.unit rootsOfUnity (ringChar R).toPNat' R'

The values of an additive character on a ring of positive characteristic are roots of unity.

def AddChar.IsPrimitive {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] (ψ : AddChar R R') :

An additive character is primitive iff all its multiplicative shifts by nonzero elements are nontrivial.

Equations
  • ψ.IsPrimitive = ∀ ⦃a : R⦄, a 0ψ.mulShift a 1
Instances For
    theorem AddChar.IsPrimitive.compMulHom_of_isPrimitive {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] {R'' : Type u_1} [CommMonoid R''] {φ : AddChar R R'} {f : R' →* R''} (hφ : φ.IsPrimitive) (hf : Function.Injective f) :
    (f.compAddChar φ).IsPrimitive

    The composition of a primitive additive character with an injective mooid homomorphism is also primitive.

    theorem AddChar.to_mulShift_inj_of_isPrimitive {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] {ψ : AddChar R R'} (hψ : ψ.IsPrimitive) :
    Function.Injective ψ.mulShift

    The map associating to a : R the multiplicative shift of ψ by a is injective when ψ is primitive.

    theorem AddChar.IsPrimitive.of_ne_one {R' : Type v} [CommMonoid R'] {F : Type u} [Field F] {ψ : AddChar F R'} (hψ : ψ 1) :
    ψ.IsPrimitive

    When R is a field F, then a nontrivial additive character is primitive

    theorem AddChar.not_isPrimitive_mulShift {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R'] [Finite R] (e : AddChar R R') {r : R} (hr : ¬IsUnit r) :
    ¬(e.mulShift r).IsPrimitive

    If r is not a unit, then e.mulShift r is not primitive.

    structure AddChar.PrimitiveAddChar (R : Type u) [CommRing R] (R' : Type v) [Field R'] :
    Type (max u v)

    Definition for a primitive additive character on a finite ring R into a cyclotomic extension of a field R'. It records which cyclotomic extension it is, the character, and the fact that the character is primitive.

    Instances For
      theorem AddChar.PrimitiveAddChar.prim {R : Type u} [CommRing R] {R' : Type v} [Field R'] (self : AddChar.PrimitiveAddChar R R') :
      self.char.IsPrimitive

      The third projection from PrimitiveAddChar, showing that χ.char is primitive.

      Additive characters on ZMod n #

      theorem AddChar.exists_divisor_of_not_isPrimitive {N : } [NeZero N] {R : Type u_1} [CommRing R] (e : AddChar (ZMod N) R) (he : ¬e.IsPrimitive) :
      ∃ (d : ), d N d < N e.mulShift d = 1

      If e is not primitive, then e.mulShift d = 1 for some proper divisor d of N.

      def AddChar.zmodChar {C : Type v} [CommMonoid C] (n : ) [NeZero n] {ζ : C} (hζ : ζ ^ n = 1) :

      We can define an additive character on ZMod n when we have an nth root of unity ζ : C.

      Equations
      • AddChar.zmodChar n = { toFun := fun (a : ZMod n) => ζ ^ a.val, map_zero_eq_one' := , map_add_eq_mul' := }
      Instances For
        theorem AddChar.zmodChar_apply {C : Type v} [CommMonoid C] {n : } [NeZero n] {ζ : C} (hζ : ζ ^ n = 1) (a : ZMod n) :
        (AddChar.zmodChar n ) a = ζ ^ a.val

        The additive character on ZMod n defined using ζ sends a to ζ^a.

        theorem AddChar.zmodChar_apply' {C : Type v} [CommMonoid C] {n : } [NeZero n] {ζ : C} (hζ : ζ ^ n = 1) (a : ) :
        (AddChar.zmodChar n ) a = ζ ^ a
        theorem AddChar.zmod_char_ne_one_iff {C : Type v} [CommMonoid C] (n : ) [NeZero n] (ψ : AddChar (ZMod n) C) :
        ψ 1 ψ 1 1

        An additive character on ZMod n is nontrivial iff it takes a value ≠ 1 on 1.

        theorem AddChar.IsPrimitive.zmod_char_eq_one_iff {C : Type v} [CommMonoid C] (n : ) [NeZero n] {ψ : AddChar (ZMod n) C} (hψ : ψ.IsPrimitive) (a : ZMod n) :
        ψ a = 1 a = 0

        A primitive additive character on ZMod n takes the value 1 only at 0.

        theorem AddChar.zmod_char_primitive_of_eq_one_only_at_zero {C : Type v} [CommMonoid C] (n : ) (ψ : AddChar (ZMod n) C) (hψ : ∀ (a : ZMod n), ψ a = 1a = 0) :
        ψ.IsPrimitive

        The converse: if the additive character takes the value 1 only at 0, then it is primitive.

        theorem AddChar.zmodChar_primitive_of_primitive_root {C : Type v} [CommMonoid C] (n : ) [NeZero n] {ζ : C} (h : IsPrimitiveRoot ζ n) :
        (AddChar.zmodChar n ).IsPrimitive

        The additive character on ZMod n associated to a primitive nth root of unity is primitive

        noncomputable def AddChar.primitiveZModChar (n : ℕ+) (F' : Type v) [Field F'] (h : n 0) :

        There is a primitive additive character on ZMod n if the characteristic of the target does not divide n

        Equations
        Instances For

          Existence of a primitive additive character on a finite field #

          noncomputable def AddChar.FiniteField.primitiveChar (F : Type u_1) (F' : Type u_2) [Field F] [Finite F] [Field F'] (h : ringChar F' ringChar F) :

          There is a primitive additive character on the finite field F if the characteristic of the target is different from that of F.

          We obtain it as the composition of the trace from F to ZMod p with a primitive additive character on ZMod p, where p is the characteristic of F.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[deprecated AddChar.FiniteField.primitiveChar]

            Alias of AddChar.FiniteField.primitiveChar.


            There is a primitive additive character on the finite field F if the characteristic of the target is different from that of F.

            We obtain it as the composition of the trace from F to ZMod p with a primitive additive character on ZMod p, where p is the characteristic of F.

            Equations
            Instances For

              The sum of all character values #

              theorem AddChar.sum_eq_zero_of_ne_one {R : Type u_1} [AddGroup R] [Fintype R] {R' : Type u_2} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (hψ : ψ 1) :
              a : R, ψ a = 0

              The sum over the values of a nontrivial additive character vanishes if the target ring is a domain.

              theorem AddChar.sum_eq_card_of_eq_one {R : Type u_1} [AddGroup R] [Fintype R] {R' : Type u_2} [CommRing R'] {ψ : AddChar R R'} (hψ : ψ = 1) :
              a : R, ψ a = (Fintype.card R)

              The sum over the values of the trivial additive character is the cardinality of the source.

              theorem AddChar.sum_mulShift {R : Type u_1} [CommRing R] [Fintype R] [DecidableEq R] {R' : Type u_2} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (b : R) (hψ : ψ.IsPrimitive) :
              x : R, ψ (x * b) = (if b = 0 then Fintype.card R else 0)

              The sum over the values of mulShift ψ b for ψ primitive is zero when b ≠ 0 and #R otherwise.

              Complex-valued additive characters #

              theorem AddChar.starComp_eq_inv {R : Type u_1} [CommRing R] (hR : 0 < ringChar R) {φ : AddChar R } :
              (↑(starRingEnd )).compAddChar φ = φ⁻¹

              Post-composing an additive character to with complex conjugation gives the inverse character.

              theorem AddChar.starComp_apply {R : Type u_1} [CommRing R] (hR : 0 < ringChar R) {φ : AddChar R } (a : R) :
              (starRingEnd ) (φ a) = φ⁻¹ a

              A primitive additive character on the finite field F with values in .

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For