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.

Implementation notes

Due to their role as the dual of an additive group, additive characters must themselves be an additive group. This contrasts to their pointwise operations which make them a multiplicative group. We simply define both the additive and multiplicative group structures and prove them equal.

For more information on this design decision, see the following zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Additive.20characters

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_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.

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 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 : A → M) (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 y : A) : ψ (x + y) = ψ x * ψ y

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

Interpret an additive character as a monoid homomorphism.

Equations

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

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

def AddChar.toMonoidHomEquiv {A : Type u_1} {M : Type u_3} [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.

@[simp]

theorem AddChar.coe_toMonoidHomEquiv {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) : ⇑(toMonoidHomEquiv ψ) = ⇑ψ ∘ ⇑Multiplicative.toAdd

@[simp]

theorem AddChar.coe_toMonoidHomEquiv_symm {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : Multiplicative A →* M) : ⇑(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) : (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) : (toMonoidHomEquiv.symm ψ) a = ψ (Multiplicative.ofAdd a)

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

Interpret an additive character as a monoid homomorphism.

Equations

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

@[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] : 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.

@[simp]

theorem AddChar.coe_toAddMonoidHomEquiv {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : AddChar A M) : ⇑(toAddMonoidHomEquiv ψ) = ⇑Additive.ofMul ∘ ⇑ψ

@[simp]

theorem AddChar.coe_toAddMonoidHomEquiv_symm {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (ψ : A →+ Additive M) : ⇑(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) : (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) : (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).

Equations

• AddChar.instOne = AddChar.toMonoidHomEquiv.one

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

The trivial additive character (sending everything to 1).

Equations

• AddChar.instZero = { zero := 1 }

@[simp]

theorem AddChar.coe_one {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : ⇑1 = 1

@[simp]

theorem AddChar.coe_zero {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : ⇑0 = 1

@[simp]

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

@[simp]

theorem AddChar.zero_apply {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] (a : A) : 0 a = 1

theorem AddChar.one_eq_zero {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : 1 = 0

@[simp]

theorem AddChar.coe_eq_one {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] {ψ : AddChar A M} : ⇑ψ = 1 ↔ ψ = 0

@[simp]

theorem AddChar.toMonoidHomEquiv_zero {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : toMonoidHomEquiv 0 = 1

@[simp]

theorem AddChar.toMonoidHomEquiv_symm_one {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : toMonoidHomEquiv.symm 1 = 0

@[simp]

theorem AddChar.toAddMonoidHomEquiv_zero {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : toAddMonoidHomEquiv 0 = 0

@[simp]

theorem AddChar.toAddMonoidHomEquiv_symm_zero {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : toAddMonoidHomEquiv.symm 0 = 0

instance AddChar.instInhabited {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : Inhabited (AddChar A 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) : AddChar A N

Composing a MonoidHom with an AddChar yields another AddChar.

Equations

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

@[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) : AddChar A M

Composing an AddChar with an AddMonoidHom yields another AddChar.

Equations

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

@[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.eq_zero_iff {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] {ψ : AddChar A M} : ψ = 0 ↔ ∀ (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

theorem AddChar.ne_zero_iff {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] {ψ : AddChar A M} : ψ ≠ 0 ↔ ∃ (x : A), ψ x ≠ 1

noncomputable instance AddChar.instDecidableEq {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] : DecidableEq (AddChar A M)

Equations

• AddChar.instDecidableEq = Classical.decEq (AddChar A M)

instance AddChar.instCommMonoid {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] : CommMonoid (AddChar A M)

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

Equations

• AddChar.instCommMonoid = AddChar.toMonoidHomEquiv.commMonoid

instance AddChar.instAddCommMonoid {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] : AddCommMonoid (AddChar A M)

When M is commutative, AddChar A M is an additive commutative monoid.

Equations

• AddChar.instAddCommMonoid = Additive.addCommMonoid

@[simp]

theorem AddChar.coe_mul {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ χ : AddChar A M) : ⇑(ψ * χ) = ⇑ψ * ⇑χ

@[simp]

theorem AddChar.coe_add {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ χ : AddChar A M) : ⇑(ψ + χ) = ⇑ψ * ⇑χ

@[simp]

theorem AddChar.coe_pow {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (n : ℕ) : ⇑(ψ ^ n) = ⇑ψ ^ n

@[simp]

theorem AddChar.coe_nsmul {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (n : ℕ) (ψ : AddChar A M) : ⇑(n • ψ) = ⇑ψ ^ n

@[simp]

theorem AddChar.coe_prod {ι : Type u_1} {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (s : Finset ι) (ψ : ι → AddChar A M) : ⇑(∏ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

@[simp]

theorem AddChar.coe_sum {ι : Type u_1} {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (s : Finset ι) (ψ : ι → AddChar A M) : ⇑(∑ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

@[simp]

theorem AddChar.mul_apply {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a

@[simp]

theorem AddChar.add_apply {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ φ : AddChar A M) (a : A) : (ψ + φ) a = ψ a * φ a

@[simp]

theorem AddChar.pow_apply {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (n : ℕ) (a : A) : (ψ ^ n) a = ψ a ^ n

@[simp]

theorem AddChar.nsmul_apply {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (n : ℕ) (a : A) : (n • ψ) a = ψ a ^ n

theorem AddChar.prod_apply {ι : Type u_1} {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (s : Finset ι) (ψ : ι → AddChar A M) (a : A) : (∏ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

theorem AddChar.sum_apply {ι : Type u_1} {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (s : Finset ι) (ψ : ι → AddChar A M) (a : A) : (∑ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

theorem AddChar.mul_eq_add {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ χ : AddChar A M) : ψ * χ = ψ + χ

theorem AddChar.pow_eq_nsmul {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ : AddChar A M) (n : ℕ) : ψ ^ n = n • ψ

theorem AddChar.prod_eq_sum {ι : Type u_1} {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∑ i ∈ s, ψ i

@[simp]

theorem AddChar.toMonoidHomEquiv_add {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ φ : AddChar A M) : toMonoidHomEquiv (ψ + φ) = toMonoidHomEquiv ψ * toMonoidHomEquiv φ

@[simp]

theorem AddChar.toMonoidHomEquiv_symm_mul {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (ψ φ : Multiplicative A →* M) : toMonoidHomEquiv.symm (ψ * φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ

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

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

Equations

• AddChar.toMonoidHomMulEquiv = { toEquiv := AddChar.toMonoidHomEquiv, map_mul' := ⋯ }

def AddChar.toAddMonoidAddEquiv {A : Type u_2} {M : Type u_3} [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 = { toEquiv := AddChar.toAddMonoidHomEquiv, map_add' := ⋯ }

def AddChar.doubleDualEmb {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] : A →+ AddChar (AddChar A M) M

The double dual embedding.

Equations

• AddChar.doubleDualEmb = { toFun := fun (a : A) => { toFun := fun (ψ : AddChar A M) => ψ a, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddChar.doubleDualEmb_apply {A : Type u_2} {M : Type u_3} [AddMonoid A] [CommMonoid M] (a : A) (ψ : AddChar A M) : (doubleDualEmb a) ψ = ψ a

theorem AddChar.sum_eq_ite {A : Type u_1} {R : Type u_2} [AddGroup A] [Fintype A] [CommSemiring R] [IsDomain R] (ψ : AddChar A R) [Decidable (ψ = 0)] : ∑ a : A, ψ a = if ψ = 0 then ↑(Fintype.card A) else 0

theorem AddChar.sum_eq_zero_iff_ne_zero {A : Type u_1} {R : Type u_2} [AddGroup A] [Fintype A] [CommSemiring R] [IsDomain R] {ψ : AddChar A R} [CharZero R] : ∑ x : A, ψ x = 0 ↔ ψ ≠ 0

theorem AddChar.sum_ne_zero_iff_eq_zero {A : Type u_1} {R : Type u_2} [AddGroup A] [Fintype A] [CommSemiring R] [IsDomain R] {ψ : AddChar A R} [CharZero R] : ∑ x : A, ψ x ≠ 0 ↔ ψ = 0

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_eq_inv below).

Equations

• AddChar.instCommGroup = CommGroup.mk ⋯

instance AddChar.instAddCommGroup {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] : AddCommGroup (AddChar A M)

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

Equations

• AddChar.instAddCommGroup = Additive.addCommGroup

@[simp]

theorem AddChar.inv_apply {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] (ψ : AddChar A M) (a : A) : ψ⁻¹ a = ψ (-a)

@[simp]

theorem AddChar.neg_apply {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] (ψ : AddChar A M) (a : A) : (-ψ) a = ψ (-a)

theorem AddChar.div_apply {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] (ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a * χ (-a)

theorem AddChar.sub_apply {A : Type u_1} {M : Type u_2} [AddCommGroup A] [CommMonoid M] (ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a * χ (-a)

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.

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

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

theorem AddChar.div_apply' {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a / χ a

theorem AddChar.sub_apply' {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a / χ a

@[simp]

theorem AddChar.zsmul_apply {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (n : ℤ) (ψ : AddChar A M) (a : A) : (n • ψ) a = ψ a ^ n

@[simp]

theorem AddChar.zpow_apply {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (ψ : AddChar A M) (n : ℤ) (a : A) : (ψ ^ n) a = ψ a ^ n

theorem AddChar.map_sub_eq_div {A : Type u_1} {M : Type u_2} [AddCommGroup A] [DivisionCommMonoid M] (ψ : AddChar A M) (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 = 1 → x = 0

@[simp]

theorem AddChar.coe_ne_zero {A : Type u_1} {M₀ : Type u_2} [AddGroup A] [MonoidWithZero M₀] [Nontrivial M₀] (ψ : AddChar A M₀) : ⇑ψ ≠ 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) : AddChar R M

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

Equations

• ψ.mulShift r = ψ.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 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 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 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