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

Definitions related to and results on additive characters

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 : A → M

  The underlying function.

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

• map_zero_one' : self.toFun 0 = 1

  The function maps 0 to 1.

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

• map_add_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_mul.

instance AddChar.instFunLike {A : Type u_1} {M : Type u_2} [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_2} [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_2} [AddMonoid A] [Monoid M] (f : A → M) (map_zero_one' : f 0 = 1) (map_add_mul' : ∀ (a b : A), f (a + b) = f a * f b) : ⇑{ toFun := f, map_zero_one' := map_zero_one', map_add_mul' := map_add_mul' } = f

@[simp]

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

An additive character maps 0 to 1.

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

An additive character maps sums to products.

def AddChar.toMonoidHom {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (φ : AddChar A M) : Multiplicative A →* M

Interpret an additive character as a monoid homomorphism.

Equations

• AddChar.toMonoidHom φ = { toOneHom := { toFun := φ.toFun, map_one' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem AddChar.toMonoidHom_apply {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (a : Multiplicative A) : (AddChar.toMonoidHom ψ) a = ψ (Multiplicative.toAdd a)

theorem AddChar.map_nsmul_pow {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (n : ℕ) (x : A) : ψ (n • x) = ψ x ^ n

An additive character maps multiples by natural numbers to powers.

def AddChar.toMonoidHomEquiv (A : Type u_1) (M : Type u_2) [AddMonoid A] [Monoid M] : AddChar A M ≃ (Multiplicative A →* 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.

def AddChar.toAddMonoidHom {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (φ : AddChar A M) : A →+ Additive M

Interpret an additive character as a monoid homomorphism.

Equations

• AddChar.toAddMonoidHom φ = { toZeroHom := { toFun := φ.toFun, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem AddChar.toAddMonoidHom_apply {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (ψ : AddChar A M) (a : A) : (AddChar.toAddMonoidHom ψ) a = ψ a

def AddChar.toAddMonoidHomEquiv (A : Type u_1) (M : Type u_2) [AddMonoid A] [Monoid M] : AddChar A M ≃ (A →+ Additive 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.

instance AddChar.instOne {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] : One (AddChar A M)

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

Equations

• AddChar.instOne = Equiv.one (AddChar.toMonoidHomEquiv A M)

@[simp]

theorem AddChar.one_apply {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (a : A) : 1 a = 1

instance AddChar.instInhabited {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] : Inhabited (AddChar A M)

Equations

• AddChar.instInhabited = { default := 1 }

def MonoidHom.compAddChar {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] {N : Type u_3} [Monoid N] (f : M →* N) (φ : AddChar A M) : AddChar A N

Composing a MonoidHom with an AddChar yields another AddChar.

Equations

• MonoidHom.compAddChar f φ = (AddChar.toMonoidHomEquiv A N).symm (MonoidHom.comp f (AddChar.toMonoidHom φ))

@[simp]

theorem MonoidHom.coe_compAddChar {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] {N : Type u_3} [Monoid N] (f : M →* N) (φ : AddChar A M) : ⇑(MonoidHom.compAddChar f φ) = ⇑f ∘ ⇑φ

def AddChar.compAddMonoidHom {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] {B : Type u_3} [AddMonoid B] (φ : AddChar B M) (f : A →+ B) : AddChar A M

Composing an AddChar with an AddMonoidHom yields another AddChar.

Equations

• AddChar.compAddMonoidHom φ f = (AddChar.toAddMonoidHomEquiv A M).symm (AddMonoidHom.comp (AddChar.toAddMonoidHom φ) f)

@[simp]

theorem AddChar.coe_compAddMonoidHom {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] {B : Type u_3} [AddMonoid B] (φ : AddChar B M) (f : A →+ B) : ⇑(AddChar.compAddMonoidHom φ f) = ⇑φ ∘ ⇑f

def AddChar.IsNontrivial {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (ψ : AddChar A M) : Prop

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

Equations

• AddChar.IsNontrivial ψ = ∃ (a : A), ψ a ≠ 1

theorem AddChar.isNontrivial_iff_ne_trivial {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] (ψ : AddChar A M) : AddChar.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] : CommMonoid (AddChar A M)

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

Equations

• AddChar.instCommMonoid = Equiv.commMonoid (AddChar.toMonoidHomEquiv A M)

@[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

def AddChar.toMonoidHomMulEquiv (A : Type u_1) (M : Type u_2) [AddMonoid A] [CommMonoid M] : AddChar A M ≃* (Multiplicative A →* M)

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

Equations

• AddChar.toMonoidHomMulEquiv A M = let __src := AddChar.toMonoidHomEquiv A M; { toEquiv := __src, map_mul' := ⋯ }

def AddChar.toAddMonoidAddEquiv (A : Type u_1) (M : Type u_2) [AddMonoid A] [CommMonoid M] : Additive (AddChar A M) ≃+ (A →+ Additive M)

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

Equations

• AddChar.toAddMonoidAddEquiv A M = let __src := AddChar.toAddMonoidHomEquiv A M; { toEquiv := __src, map_add' := ⋯ }

Additive characters of additive abelian groups

instance AddChar.instCommGroup {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] : CommGroup (AddChar A 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_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.map_neg_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_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.

theorem AddChar.inv_apply' {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (ψ : AddChar A M) (x : A) : ψ⁻¹ x = (ψ x)⁻¹

Additive characters of rings

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

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

Equations

• AddChar.mulShift ψ r = AddChar.compAddMonoidHom ψ (AddMonoidHom.mulLeft r)

@[simp]

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

theorem AddChar.inv_mulShift {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) : ψ⁻¹ = AddChar.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) : (AddChar.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 = AddChar.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) : AddChar.mulShift ψ r * AddChar.mulShift ψ s = AddChar.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) : AddChar.mulShift (AddChar.mulShift ψ r) s = AddChar.mulShift ψ (r * s)

@[simp]

theorem AddChar.mulShift_zero {R : Type u_1} {M : Type u_2} [Ring R] [CommMonoid M] (ψ : AddChar R M) : AddChar.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) : AddChar.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) : AddChar.mulShift ψ u = 1 ↔ ψ = 1