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.

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

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.

Instances For

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.

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

Multiplicative 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] :

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.

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) :

A →+ Additive 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] :

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.

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

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] :

AddChar.toMonoidHomEquiv 0 = 1

@[simp]

theorem AddChar.toMonoidHomEquiv_symm_one {A : Type u_1} {M : Type u_3} [AddMonoid A] [Monoid M] :

AddChar.toMonoidHomEquiv.symm 1 = 0

@[simp]

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

AddChar.toAddMonoidHomEquiv 0 = 0

@[simp]

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

AddChar.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) :

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

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

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) :

AddChar.toMonoidHomEquiv (ψ + φ) = AddChar.toMonoidHomEquiv ψ * AddChar.toMonoidHomEquiv φ

@[simp]

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

AddChar.toMonoidHomEquiv.symm (ψ * φ) = AddChar.toMonoidHomEquiv.symm ψ + AddChar.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' := ⋯ }

Instances For

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' := ⋯ }

Instances For

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' := ⋯ }

Instances For

@[simp]

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

(AddChar.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.

@[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) (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) :

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

Equations

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

Instances For

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