# 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 #

structure AddChar (A : Type u_1) [] (M : Type u_2) [] :
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_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.

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

The function maps 0 to 1.

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

theorem AddChar.map_add_mul' {A : Type u_1} [] {M : Type u_2} [] (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_mul.

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

Define coercion to a function.

Equations
theorem AddChar.ext {A : Type u_1} {M : Type u_2} [] [] (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} [] [] (f : AM) (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} [] [] (ψ : 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} [] [] (ψ : 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} [] [] (φ : 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_2} [] [] (ψ : AddChar A M) (a : ) :
ψ.toMonoidHom a = ψ (Multiplicative.toAdd a)
theorem AddChar.map_nsmul_pow {A : Type u_1} {M : Type u_2} [] [] (ψ : 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) [] [] :

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
def AddChar.toAddMonoidHom {A : Type u_1} {M : Type u_2} [] [] (φ : AddChar A M) :
A →+

Interpret an additive character as a monoid homomorphism.

Equations
• φ.toAddMonoidHom = { toFun := φ.toFun, map_zero' := , map_add' := }
Instances For
@[simp]
theorem AddChar.toAddMonoidHom_apply {A : Type u_1} {M : Type u_2} [] [] (ψ : AddChar A M) (a : A) :
def AddChar.toAddMonoidHomEquiv (A : Type u_1) (M : Type u_2) [] [] :
AddChar A M (A →+ )

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
instance AddChar.instOne {A : Type u_1} {M : Type u_2} [] [] :

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

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

Composing a MonoidHom with an AddChar yields another AddChar.

Equations
• f.compAddChar φ = ().symm (f.comp φ.toMonoidHom)
Instances For
@[simp]
theorem MonoidHom.coe_compAddChar {A : Type u_1} {M : Type u_2} [] [] {N : Type u_3} [] (f : M →* N) (φ : AddChar A M) :
def AddChar.compAddMonoidHom {A : Type u_1} {M : Type u_2} [] [] {B : Type u_3} [] (φ : AddChar B M) (f : A →+ B) :

Composing an AddChar with an AddMonoidHom yields another AddChar.

Equations
Instances For
@[simp]
theorem AddChar.coe_compAddMonoidHom {A : Type u_1} {M : Type u_2} [] [] {B : Type u_3} [] (φ : AddChar B M) (f : A →+ B) :
def AddChar.IsNontrivial {A : Type u_1} {M : Type u_2} [] [] (ψ : AddChar A M) :

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

Equations
• ψ.IsNontrivial = ∃ (a : A), ψ a 1
Instances For
theorem AddChar.isNontrivial_iff_ne_trivial {A : Type u_1} {M : Type u_2} [] [] (ψ : 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} [] [] :

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

Equations
@[simp]
theorem AddChar.mul_apply {A : Type u_1} {M : Type u_2} [] [] (ψ : AddChar A M) (φ : AddChar A M) (a : A) :
(ψ * φ) a = ψ a * φ a
@[simp]
theorem AddChar.pow_apply {A : Type u_1} {M : Type u_2} [] [] (ψ : AddChar A M) (n : ) (a : A) :
(ψ ^ n) a = ψ a ^ n
def AddChar.toMonoidHomMulEquiv (A : Type u_1) (M : Type u_2) [] [] :

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

Equations
• = let __src := ; { toEquiv := __src, map_mul' := }
Instances For

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

Equations
• = let __src := ; { toEquiv := __src, map_add' := }
Instances For

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

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
@[simp]
theorem AddChar.inv_apply {A : Type u_1} {M : Type u_2} [] [] (ψ : AddChar A M) (x : A) :
ψ⁻¹ x = ψ (-x)
theorem AddChar.map_neg_inv {A : Type u_1} {M : Type u_2} [] [] (ψ : 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} [] [] (ψ : 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} [] (ψ : AddChar A M) (x : A) :
ψ⁻¹ x = (ψ x)⁻¹

## Additive characters of rings #

def AddChar.mulShift {R : Type u_1} {M : Type u_2} [Ring R] [] (ψ : 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] [] {ψ : 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] [] (ψ : AddChar R M) :
ψ⁻¹ = ψ.mulShift (-1)

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

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