doc-next-gen

Mathlib.Algebra.Group.AddChar

Module docstring

{"# 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 ","## Additive characters of additive abelian groups ","## Additive characters of rings "}

AddChar structure
Full source 
/-- `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).
-/
structure AddChar where
  /-- The underlying function.

  Do not use this function directly. Instead use the coercion coming from the `FunLike`
  instance. -/
  toFun : A → M
  /-- The function maps `0` to `1`.

  Do not use this directly. Instead use `AddChar.map_zero_eq_one`. -/
  map_zero_eq_one' : toFun 0 = 1
  /-- The function maps addition in `A` to multiplication in `M`.

  Do not use this directly. Instead use `AddChar.map_add_eq_mul`. -/
  map_add_eq_mul' : ∀ a b : A, toFun (a + b) = toFun a * toFun b
Additive character
Informal description
An additive character from an additive monoid $A$ to a multiplicative monoid $M$ is a function $\psi: A \to M$ that satisfies $\psi(x + y) = \psi(x) \cdot \psi(y)$ for all $x, y \in A$.
AddChar.instFunLike instance
: FunLike (AddChar A M) A M
Full source 
/-- Define coercion to a function. -/
instance instFunLike : FunLike (AddChar A M) A M where
  coe := AddChar.toFun
  coe_injective' φ ψ h := by cases φ; cases ψ; congr
Function-Like Structure of Additive Characters
Informal description
For any additive monoid $A$ and multiplicative monoid $M$, the additive characters $\psi: A \to M$ form a function-like class, where each character can be viewed as a function from $A$ to $M$ that preserves the additive structure of $A$ in the multiplicative structure of $M$.
AddChar.ext theorem
(f g : AddChar A M) (h : ∀ x : A, f x = g x) : f = g
Full source 
@[ext] lemma ext (f g : AddChar A M) (h : ∀ x : A, f x = g x) : f = g :=
  DFunLike.ext f g h
Extensionality of Additive Characters
Informal description
For any two additive characters $\psi_1, \psi_2: A \to M$, if $\psi_1(x) = \psi_2(x)$ for all $x \in A$, then $\psi_1 = \psi_2$.
AddChar.coe_mk theorem
(f : A → M) (map_zero_eq_one' : f 0 = 1) (map_add_eq_mul' : ∀ a b : A, f (a + b) = f a * f b) : AddChar.mk f map_zero_eq_one' map_add_eq_mul' = f
Full source 
@[simp] lemma coe_mk (f : A → M)
    (map_zero_eq_one' : f 0 = 1) (map_add_eq_mul' : ∀ a b : A, f (a + b) = f a * f b) :
    AddChar.mk f map_zero_eq_one' map_add_eq_mul' = f := by
  rfl
Construction of Additive Character from Homomorphic Function
Informal description
Let $A$ be an additive monoid and $M$ a multiplicative monoid. Given a function $f: A \to M$ satisfying $f(0) = 1$ and $f(a + b) = f(a) \cdot f(b)$ for all $a, b \in A$, the construction of the corresponding additive character $\psi$ via `AddChar.mk` yields $\psi = f$.
AddChar.map_zero_eq_one theorem
(ψ : AddChar A M) : ψ 0 = 1
Full source 
/-- An additive character maps `0` to `1`. -/
@[simp] lemma map_zero_eq_one (ψ : AddChar A M) : ψ 0 = 1 := ψ.map_zero_eq_one'
Additive Character Preserves Identities: $\psi(0) = 1$
Informal description
For any additive character $\psi$ from an additive monoid $A$ to a multiplicative monoid $M$, the character maps the additive identity $0 \in A$ to the multiplicative identity $1 \in M$, i.e., $\psi(0) = 1$.
AddChar.map_add_eq_mul theorem
(ψ : AddChar A M) (x y : A) : ψ (x + y) = ψ x * ψ y
Full source 
/-- An additive character maps sums to products. -/
lemma map_add_eq_mul (ψ : AddChar A M) (x y : A) : ψ (x + y) = ψ x * ψ y := ψ.map_add_eq_mul' x y
Additive Character Homomorphism Property: $\psi(x + y) = \psi(x)\psi(y)$
Informal description
For any additive character $\psi$ from an additive monoid $A$ to a multiplicative monoid $M$, and for any elements $x, y \in A$, the character satisfies $\psi(x + y) = \psi(x) \cdot \psi(y)$.
AddChar.toMonoidHom definition
(φ : AddChar A M) : Multiplicative A →* M
Full source 
/-- Interpret an additive character as a monoid homomorphism. -/
def toMonoidHom (φ : AddChar A M) : MultiplicativeMultiplicative A →* M where
  toFun := φ.toFun
  map_one' := φ.map_zero_eq_one'
  map_mul' := φ.map_add_eq_mul'
Additive character as monoid homomorphism
Informal description
Given an additive character $\varphi \colon A \to M$ from an additive monoid $A$ to a multiplicative monoid $M$, the function $\varphi$ can be interpreted as a monoid homomorphism from the multiplicative monoid of $A$ (denoted $\text{Multiplicative}\, A$) to $M$. This homomorphism satisfies $\varphi(0) = 1$ and $\varphi(x + y) = \varphi(x) \cdot \varphi(y)$ for all $x, y \in A$.
AddChar.toMonoidHom_apply theorem
(ψ : AddChar A M) (a : Multiplicative A) : ψ.toMonoidHom a = ψ a.toAdd
Full source 
@[simp] lemma toMonoidHom_apply (ψ : AddChar A M) (a : Multiplicative A) :
  ψ.toMonoidHom a = ψ a.toAdd :=
  rfl
Equality of Monoid Homomorphism and Additive Character Evaluations: $\psi.\text{toMonoidHom}(a) = \psi(a.\text{toAdd})$
Informal description
For any additive character $\psi \colon A \to M$ and any element $a$ in the multiplicative monoid of $A$ (i.e., $a \in \text{Multiplicative}\, A$), the evaluation of the monoid homomorphism $\psi.\text{toMonoidHom}$ at $a$ equals the evaluation of $\psi$ at the additive version of $a$ (i.e., $\psi(a.\text{toAdd})$).
AddChar.map_nsmul_eq_pow theorem
(ψ : AddChar A M) (n : ℕ) (x : A) : ψ (n • x) = ψ x ^ n
Full source 
/-- An additive character maps multiples by natural numbers to powers. -/
lemma map_nsmul_eq_pow (ψ : AddChar A M) (n : ℕ) (x : A) : ψ (n • x) = ψ x ^ n :=
  ψ.toMonoidHom.map_pow x n
Additive character maps scalar multiples to powers: $\psi(n \cdot x) = \psi(x)^n$
Informal description
For any additive character $\psi \colon A \to M$ from an additive monoid $A$ to a multiplicative monoid $M$, any natural number $n$, and any element $x \in A$, we have $\psi(n \cdot x) = (\psi(x))^n$, where $n \cdot x$ denotes the $n$-fold sum $x + \cdots + x$ and $(\psi(x))^n$ denotes the $n$-fold product $\psi(x) \cdots \psi(x)$.
AddChar.toMonoidHomEquiv definition
: AddChar A M ≃ (Multiplicative A →* M)
Full source 
/-- Additive characters `A → M` are the same thing as monoid homomorphisms from `Multiplicative A`
to `M`. -/
def toMonoidHomEquiv : AddCharAddChar A M ≃ (Multiplicative A →* M) where
  toFun φ := φ.toMonoidHom
  invFun f :=
  { toFun := f.toFun
    map_zero_eq_one' := f.map_one'
    map_add_eq_mul' := f.map_mul' }
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between additive characters and monoid homomorphisms
Informal description
The equivalence between additive characters $\text{AddChar}\, A\, M$ and monoid homomorphisms $\text{Multiplicative}\, A \to^* M$. Specifically, an additive character $\varphi \colon A \to M$ corresponds to a monoid homomorphism $\text{Multiplicative}\, A \to^* M$ via $\varphi \mapsto \varphi \circ \text{Multiplicative.toAdd}$, and conversely, a monoid homomorphism $f \colon \text{Multiplicative}\, A \to^* M$ corresponds to an additive character $f \circ \text{Multiplicative.ofAdd}$.
AddChar.coe_toMonoidHomEquiv theorem
(ψ : AddChar A M) : ⇑(toMonoidHomEquiv ψ) = ψ ∘ Multiplicative.toAdd
Full source 
@[simp, norm_cast] lemma coe_toMonoidHomEquiv (ψ : AddChar A M) :
    ⇑(toMonoidHomEquiv ψ) = ψ ∘ Multiplicative.toAdd := rfl
Equivalence of Additive Characters and Monoid Homomorphisms Preserves Function Application
Informal description
For any additive character $\psi \colon A \to M$, the underlying function of the corresponding monoid homomorphism under the equivalence $\text{AddChar}\, A\, M \simeq (\text{Multiplicative}\, A \to^* M)$ is equal to the composition $\psi \circ \text{Multiplicative.toAdd}$.
AddChar.coe_toMonoidHomEquiv_symm theorem
(ψ : Multiplicative A →* M) : ⇑(toMonoidHomEquiv.symm ψ) = ψ ∘ Multiplicative.ofAdd
Full source 
@[simp, norm_cast] lemma coe_toMonoidHomEquiv_symm (ψ : MultiplicativeMultiplicative A →* M) :
    ⇑(toMonoidHomEquiv.symm ψ) = ψ ∘ Multiplicative.ofAdd := rfl
Characterization of the Inverse Equivalence for Additive Characters
Informal description
For any monoid homomorphism $\psi \colon \text{Multiplicative}\, A \to^* M$, the underlying function of the corresponding additive character (obtained via the inverse of the equivalence $\text{AddChar}\, A\, M \simeq (\text{Multiplicative}\, A \to^* M)$) is equal to the composition $\psi \circ \text{Multiplicative.ofAdd}$.
AddChar.toMonoidHomEquiv_apply theorem
(ψ : AddChar A M) (a : Multiplicative A) : toMonoidHomEquiv ψ a = ψ a.toAdd
Full source 
@[simp] lemma toMonoidHomEquiv_apply (ψ : AddChar A M) (a : Multiplicative A) :
    toMonoidHomEquiv ψ a = ψ a.toAdd := rfl
Evaluation of Additive Character via Monoid Homomorphism Equivalence
Informal description
For any additive character $\psi \colon A \to M$ and any element $a$ in the multiplicative monoid $\text{Multiplicative}\, A$, the evaluation of the corresponding monoid homomorphism $\text{toMonoidHomEquiv}(\psi)$ at $a$ is equal to $\psi$ evaluated at the additive counterpart of $a$, i.e., \[ \text{toMonoidHomEquiv}(\psi)(a) = \psi(a.\text{toAdd}). \]
AddChar.toMonoidHomEquiv_symm_apply theorem
(ψ : Multiplicative A →* M) (a : A) : toMonoidHomEquiv.symm ψ a = ψ (Multiplicative.ofAdd a)
Full source 
@[simp] lemma toMonoidHomEquiv_symm_apply (ψ : MultiplicativeMultiplicative A →* M) (a : A) :
    toMonoidHomEquiv.symm ψ a = ψ (Multiplicative.ofAdd a) := rfl
Inverse Equivalence of Additive Characters and Monoid Homomorphisms Evaluated at Additive Elements
Informal description
For any monoid homomorphism $\psi \colon \text{Multiplicative}\, A \to^* M$ and any element $a \in A$, the application of the inverse equivalence $\text{toMonoidHomEquiv}^{-1}$ to $\psi$ at $a$ is equal to $\psi$ evaluated at the multiplicative version of $a$, i.e., \[ \text{toMonoidHomEquiv}^{-1}(\psi)(a) = \psi(\text{Multiplicative.ofAdd}\, a). \]
AddChar.toAddMonoidHom definition
(φ : AddChar A M) : A →+ Additive M
Full source 
/-- Interpret an additive character as a monoid homomorphism. -/
def toAddMonoidHom (φ : AddChar A M) : A →+ Additive M where
  toFun := φ.toFun
  map_zero' := φ.map_zero_eq_one'
  map_add' := φ.map_add_eq_mul'
Conversion of additive character to additive monoid homomorphism
Informal description
Given an additive character $\varphi : A \to M$ from an additive monoid $A$ to a multiplicative monoid $M$, the function $\text{toAddMonoidHom}$ converts $\varphi$ into an additive monoid homomorphism from $A$ to the additive version of $M$, denoted $\text{Additive } M$. This homomorphism satisfies: 1. $\text{toAddMonoidHom}(\varphi)(0) = 0$ (the additive identity in $\text{Additive } M$) 2. $\text{toAddMonoidHom}(\varphi)(x + y) = \text{toAddMonoidHom}(\varphi)(x) + \text{toAddMonoidHom}(\varphi)(y)$ for all $x, y \in A$ The underlying function is given by $\text{toAddMonoidHom}(\varphi)(a) = \text{Additive.ofMul}(\varphi(a))$, where $\text{Additive.ofMul}$ converts from the multiplicative structure of $M$ to its additive counterpart.
AddChar.coe_toAddMonoidHom theorem
(ψ : AddChar A M) : ⇑ψ.toAddMonoidHom = Additive.ofMul ∘ ψ
Full source 
@[simp] lemma coe_toAddMonoidHom (ψ : AddChar A M) : ⇑ψ.toAddMonoidHom = Additive.ofMulAdditive.ofMul ∘ ψ := rfl
Coefficient Extraction of Additive Character to Additive Monoid Homomorphism
Informal description
For any additive character $\psi : A \to M$ from an additive monoid $A$ to a multiplicative monoid $M$, the underlying function of the associated additive monoid homomorphism $\psi.\text{toAddMonoidHom}$ is equal to the composition of $\psi$ with the conversion from multiplicative to additive structure, i.e., $\text{Additive.ofMul} \circ \psi$.
AddChar.toAddMonoidHom_apply theorem
(ψ : AddChar A M) (a : A) : ψ.toAddMonoidHom a = Additive.ofMul (ψ a)
Full source 
@[simp] lemma toAddMonoidHom_apply (ψ : AddChar A M) (a : A) :
    ψ.toAddMonoidHom a = Additive.ofMul (ψ a) := rfl
Evaluation of Additive Character as Additive Monoid Homomorphism
Informal description
For any additive character $\psi : A \to M$ from an additive monoid $A$ to a multiplicative monoid $M$, and for any element $a \in A$, the evaluation of the associated additive monoid homomorphism $\psi.\text{toAddMonoidHom}$ at $a$ is equal to the additive version of $\psi(a)$, i.e., $\psi.\text{toAddMonoidHom}(a) = \text{Additive.ofMul}(\psi(a))$.
AddChar.toAddMonoidHomEquiv definition
: AddChar A M ≃ (A →+ Additive M)
Full source 
/-- Additive characters `A → M` are the same thing as additive homomorphisms from `A` to
`Additive M`. -/
def toAddMonoidHomEquiv : AddCharAddChar A M ≃ (A →+ Additive M) where
  toFun φ := φ.toAddMonoidHom
  invFun f :=
  { toFun := f.toFun
    map_zero_eq_one' := f.map_zero'
    map_add_eq_mul' := f.map_add' }
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between additive characters and additive monoid homomorphisms
Informal description
The equivalence between additive characters $\text{AddChar } A M$ and additive monoid homomorphisms $A \to \text{Additive } M$. Specifically, this establishes a bijection where: 1. Given an additive character $\varphi : A \to M$, the corresponding additive monoid homomorphism is $\varphi.\text{toAddMonoidHom} : A \to \text{Additive } M$. 2. Conversely, given an additive monoid homomorphism $f : A \to \text{Additive } M$, the corresponding additive character is obtained by composing with $\text{Additive.toMul} : \text{Additive } M \to M$. The bijection satisfies: - For any $\varphi \in \text{AddChar } A M$, the inverse applied to $\varphi.\text{toAddMonoidHom}$ returns $\varphi$. - For any $f \in A \to \text{Additive } M$, applying the forward map to the inverse image of $f$ returns $f$.
AddChar.coe_toAddMonoidHomEquiv theorem
(ψ : AddChar A M) : ⇑(toAddMonoidHomEquiv ψ) = Additive.ofMul ∘ ψ
Full source 
@[simp, norm_cast]
lemma coe_toAddMonoidHomEquiv (ψ : AddChar A M) :
    ⇑(toAddMonoidHomEquiv ψ) = Additive.ofMulAdditive.ofMul ∘ ψ := rfl
Equivalence of Additive Character and Additive Monoid Homomorphism via $\text{Additive.ofMul}$
Informal description
For any additive character $\psi : A \to M$ from an additive monoid $A$ to a multiplicative monoid $M$, the underlying function of the equivalence $\text{toAddMonoidHomEquiv}(\psi)$ is equal to the composition of $\text{Additive.ofMul}$ with $\psi$, i.e., $\text{toAddMonoidHomEquiv}(\psi)(a) = \text{Additive.ofMul}(\psi(a))$ for all $a \in A$.
AddChar.coe_toAddMonoidHomEquiv_symm theorem
(ψ : A →+ Additive M) : ⇑(toAddMonoidHomEquiv.symm ψ) = Additive.toMul ∘ ψ
Full source 
@[simp, norm_cast] lemma coe_toAddMonoidHomEquiv_symm (ψ : A →+ Additive M) :
    ⇑(toAddMonoidHomEquiv.symm ψ) = Additive.toMulAdditive.toMul ∘ ψ := rfl
Characterization of the inverse equivalence for additive characters
Informal description
For any additive monoid homomorphism $\psi: A \to \text{Additive } M$, the corresponding additive character $\text{toAddMonoidHomEquiv.symm } \psi$ is equal to the composition of $\psi$ with the multiplicative conversion map $\text{Additive.toMul}: \text{Additive } M \to M$. In other words, for all $a \in A$, we have $(\text{toAddMonoidHomEquiv.symm } \psi)(a) = \text{Additive.toMul}(\psi(a))$.
AddChar.toAddMonoidHomEquiv_apply theorem
(ψ : AddChar A M) (a : A) : toAddMonoidHomEquiv ψ a = Additive.ofMul (ψ a)
Full source 
@[simp] lemma toAddMonoidHomEquiv_apply (ψ : AddChar A M) (a : A) :
    toAddMonoidHomEquiv ψ a = Additive.ofMul (ψ a) := rfl
Equivalence Application of Additive Character to Monoid Homomorphism
Informal description
For any additive character $\psi \colon A \to M$ and any element $a \in A$, the application of the equivalence $\text{toAddMonoidHomEquiv}$ to $\psi$ at $a$ is equal to the additive version of $\psi(a)$, i.e., \[ \text{toAddMonoidHomEquiv}(\psi)(a) = \text{Additive.ofMul}(\psi(a)). \]
AddChar.toAddMonoidHomEquiv_symm_apply theorem
(ψ : A →+ Additive M) (a : A) : toAddMonoidHomEquiv.symm ψ a = (ψ a).toMul
Full source 
@[simp] lemma toAddMonoidHomEquiv_symm_apply (ψ : A →+ Additive M) (a : A) :
    toAddMonoidHomEquiv.symm ψ a = (ψ a).toMul  := rfl
Inverse Equivalence of Additive Character to Monoid Homomorphism Applied to Element
Informal description
For any additive monoid homomorphism $\psi \colon A \to \text{Additive } M$ and any element $a \in A$, the application of the inverse equivalence $\text{toAddMonoidHomEquiv.symm}$ to $\psi$ at $a$ is equal to the multiplicative version of $\psi(a)$, i.e., \[ \text{toAddMonoidHomEquiv.symm}(\psi)(a) = \psi(a).\text{toMul}. \]
AddChar.instOne instance
: One (AddChar A M)
Full source 
/-- The trivial additive character (sending everything to `1`). -/
instance instOne : One (AddChar A M) := toMonoidHomEquiv.one
The Trivial Additive Character
Informal description
For any additive monoid $A$ and multiplicative monoid $M$, there is a trivial additive character $\mathbf{1} \colon A \to M$ that sends every element of $A$ to the multiplicative identity $1$ in $M$.
AddChar.instZero instance
: Zero (AddChar A M)
Full source 
/-- The trivial additive character (sending everything to `1`). -/
instance instZero : Zero (AddChar A M) := ⟨1⟩
The Zero Additive Character
Informal description
For any additive monoid $A$ and multiplicative monoid $M$, there is a zero additive character $0 \colon A \to M$ that sends every element of $A$ to the multiplicative identity $1$ in $M$.
AddChar.coe_one theorem
: ⇑(1 : AddChar A M) = 1
Full source 
@[simp, norm_cast] lemma coe_one : ⇑(1 : AddChar A M) = 1 := rfl
Trivial Additive Character Maps All Elements to One
Informal description
The trivial additive character $\mathbf{1} \colon A \to M$ satisfies $\mathbf{1}(x) = 1$ for all $x \in A$, where $1$ is the multiplicative identity in $M$.
AddChar.coe_zero theorem
: ⇑(0 : AddChar A M) = 1
Full source 
@[simp, norm_cast] lemma coe_zero : ⇑(0 : AddChar A M) = 1 := rfl
Zero Additive Character Maps All Elements to One
Informal description
The zero additive character $0 \colon A \to M$ satisfies $0(x) = 1$ for all $x \in A$, where $1$ is the multiplicative identity in $M$.
AddChar.one_apply theorem
(a : A) : (1 : AddChar A M) a = 1
Full source 
@[simp] lemma one_apply (a : A) : (1 : AddChar A M) a = 1 := rfl
Trivial Additive Character Evaluates to Identity
Informal description
For any element $a$ in an additive monoid $A$ and any multiplicative monoid $M$, the trivial additive character $\mathbf{1} \colon A \to M$ satisfies $\mathbf{1}(a) = 1_M$, where $1_M$ is the multiplicative identity in $M$.
AddChar.zero_apply theorem
(a : A) : (0 : AddChar A M) a = 1
Full source 
@[simp] lemma zero_apply (a : A) : (0 : AddChar A M) a = 1 := rfl
Zero Additive Character Evaluates to Identity
Informal description
For any element $a$ in an additive monoid $A$, the zero additive character $0 \colon A \to M$ satisfies $0(a) = 1$, where $1$ is the multiplicative identity in $M$.
AddChar.one_eq_zero theorem
: (1 : AddChar A M) = (0 : AddChar A M)
Full source 
lemma one_eq_zero : (1 : AddChar A M) = (0 : AddChar A M) := rfl
Trivial and Zero Additive Characters Coincide
Informal description
The trivial additive character $\mathbf{1} \colon A \to M$ is equal to the zero additive character $0 \colon A \to M$, where both characters send every element of the additive monoid $A$ to the multiplicative identity $1$ in $M$.
AddChar.coe_eq_one theorem
: ⇑ψ = 1 ↔ ψ = 0
Full source 
@[simp, norm_cast] lemma coe_eq_one : ⇑ψ = 1 ↔ ψ = 0 := by rw [← coe_zero, DFunLike.coe_fn_eq]
Character is Trivial if and only if it is Zero
Informal description
For an additive character $\psi : A \to M$, the function $\psi$ is identically equal to the multiplicative identity $1$ (i.e., $\psi(x) = 1$ for all $x \in A$) if and only if $\psi$ is the zero additive character.
AddChar.toMonoidHomEquiv_zero theorem
: toMonoidHomEquiv (0 : AddChar A M) = 1
Full source 
@[simp] lemma toMonoidHomEquiv_zero : toMonoidHomEquiv (0 : AddChar A M) = 1 := rfl
Zero Additive Character Corresponds to Trivial Monoid Homomorphism
Informal description
The equivalence between additive characters and monoid homomorphisms maps the zero additive character $0 \colon A \to M$ (which sends every element to $1 \in M$) to the trivial monoid homomorphism $1 \colon \text{Multiplicative}\, A \to M$ (which also sends every element to $1 \in M$).
AddChar.toMonoidHomEquiv_symm_one theorem
: toMonoidHomEquiv.symm (1 : Multiplicative A →* M) = 0
Full source 
@[simp] lemma toMonoidHomEquiv_symm_one :
    toMonoidHomEquiv.symm (1 : MultiplicativeMultiplicative A →* M) = 0 := rfl
Correspondence of Trivial Monoid Homomorphism and Zero Additive Character
Informal description
The inverse of the equivalence `toMonoidHomEquiv` applied to the trivial monoid homomorphism $1 \colon \text{Multiplicative}\, A \to M$ is equal to the zero additive character $0 \colon A \to M$. In other words, under the bijection between additive characters $\text{AddChar}\, A\, M$ and monoid homomorphisms $\text{Multiplicative}\, A \to^* M$, the trivial monoid homomorphism corresponds to the zero additive character.
AddChar.toAddMonoidHomEquiv_zero theorem
: toAddMonoidHomEquiv (0 : AddChar A M) = 0
Full source 
@[simp] lemma toAddMonoidHomEquiv_zero : toAddMonoidHomEquiv (0 : AddChar A M) = 0 := rfl
Zero Additive Character Corresponds to Zero Homomorphism
Informal description
The additive monoid homomorphism corresponding to the zero additive character $0 \colon A \to M$ is the zero homomorphism $0 \colon A \to \text{Additive } M$.
AddChar.toAddMonoidHomEquiv_symm_zero theorem
: toAddMonoidHomEquiv.symm (0 : A →+ Additive M) = 0
Full source 
@[simp] lemma toAddMonoidHomEquiv_symm_zero :
    toAddMonoidHomEquiv.symm (0 : A →+ Additive M) = 0 := rfl
Inverse Equivalence Maps Zero Homomorphism to Zero Character
Informal description
The inverse of the equivalence between additive characters and additive monoid homomorphisms, when applied to the zero homomorphism $0 \colon A \to \text{Additive } M$, yields the zero additive character $0 \colon A \to M$.
AddChar.instInhabited instance
: Inhabited (AddChar A M)
Full source 
instance instInhabited : Inhabited (AddChar A M) := ⟨1⟩
Inhabitedness of Additive Characters
Informal description
For any additive monoid $A$ and multiplicative monoid $M$, the type of additive characters $\text{AddChar}(A, M)$ is inhabited.
MonoidHom.compAddChar definition
{N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) : AddChar A N
Full source 
/-- Composing a `MonoidHom` with an `AddChar` yields another `AddChar`. -/
def _root_.MonoidHom.compAddChar {N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) :
    AddChar A N := toMonoidHomEquiv.symm (f.comp φ.toMonoidHom)
Composition of monoid homomorphism with additive character
Informal description
Given a monoid homomorphism \( f \colon M \to N \) and an additive character \( \varphi \colon A \to M \), the composition \( f \circ \varphi \) is an additive character from \( A \) to \( N \). This defines a new additive character \( f \circ \varphi \) that maps each \( x \in A \) to \( f(\varphi(x)) \in N \).
MonoidHom.coe_compAddChar theorem
{N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) : f.compAddChar φ = f ∘ φ
Full source 
@[simp, norm_cast]
lemma _root_.MonoidHom.coe_compAddChar {N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) :
    f.compAddChar φ = f ∘ φ :=
  rfl
Composition of Monoid Homomorphism with Additive Character as Pointwise Composition
Informal description
Given a monoid homomorphism $f \colon M \to N$ and an additive character $\varphi \colon A \to M$, the composition of $f$ with $\varphi$ as an additive character is equal to the pointwise composition of $f$ and $\varphi$, i.e., $(f \circ \varphi)(x) = f(\varphi(x))$ for all $x \in A$.
MonoidHom.compAddChar_apply theorem
(f : M →* N) (φ : AddChar A M) : f.compAddChar φ = f ∘ φ
Full source 
@[simp, norm_cast]
lemma _root_.MonoidHom.compAddChar_apply (f : M →* N) (φ : AddChar A M) : f.compAddChar φ = f ∘ φ :=
  rfl
Composition of Monoid Homomorphism with Additive Character Preserves Application
Informal description
For any monoid homomorphism $f \colon M \to N$ and additive character $\varphi \colon A \to M$, the composition $f \circ \varphi$ is equal to the additive character obtained by applying $f$ to $\varphi$, i.e., $(f \circ \varphi)(x) = f(\varphi(x))$ for all $x \in A$.
MonoidHom.compAddChar_injective_left theorem
(ψ : AddChar A M) (hψ : Surjective ψ) : Injective fun f : M →* N ↦ f.compAddChar ψ
Full source 
lemma _root_.MonoidHom.compAddChar_injective_left (ψ : AddChar A M) (hψ : Surjective ψ) :
    Injective fun f : M →* N ↦ f.compAddChar ψ := by
  rintro f g h; rw [DFunLike.ext'_iff] at h ⊢; exact hψ.injective_comp_right h
Injectivity of Monoid Homomorphism Composition with Surjective Additive Character
Informal description
Let $\psi \colon A \to M$ be a surjective additive character. Then the map $f \mapsto f \circ \psi$ from monoid homomorphisms $M \to^* N$ to additive characters $A \to N$ is injective.
MonoidHom.compAddChar_injective_right theorem
(f : M →* N) (hf : Injective f) : Injective fun ψ : AddChar B M ↦ f.compAddChar ψ
Full source 
lemma _root_.MonoidHom.compAddChar_injective_right (f : M →* N) (hf : Injective f) :
    Injective fun ψ : AddChar B M ↦ f.compAddChar ψ := by
  rintro ψ χ h; rw [DFunLike.ext'_iff] at h ⊢; exact hf.comp_left h
Injectivity of Right Composition with Injective Monoid Homomorphism on Additive Characters
Informal description
Let $f \colon M \to N$ be an injective monoid homomorphism. Then the map $\psi \mapsto f \circ \psi$ from additive characters of $B$ with values in $M$ to additive characters of $B$ with values in $N$ is injective.
AddChar.compAddMonoidHom definition
(φ : AddChar B M) (f : A →+ B) : AddChar A M
Full source 
/-- Composing an `AddChar` with an `AddMonoidHom` yields another `AddChar`. -/
def compAddMonoidHom (φ : AddChar B M) (f : A →+ B) : AddChar A M :=
  toAddMonoidHomEquiv.symm (φ.toAddMonoidHom.comp f)
Composition of additive character with additive monoid homomorphism
Informal description
Given an additive character $\varphi: B \to M$ and an additive monoid homomorphism $f: A \to B$, the composition $\varphi \circ f$ defines an additive character from $A$ to $M$. More precisely, for any $x, y \in A$, this composition satisfies: $$(\varphi \circ f)(x + y) = \varphi(f(x) + f(y)) = \varphi(f(x)) \cdot \varphi(f(y)) = (\varphi \circ f)(x) \cdot (\varphi \circ f)(y)$$
AddChar.coe_compAddMonoidHom theorem
(φ : AddChar B M) (f : A →+ B) : φ.compAddMonoidHom f = φ ∘ f
Full source 
@[simp, norm_cast]
lemma coe_compAddMonoidHom (φ : AddChar B M) (f : A →+ B) : φ.compAddMonoidHom f = φ ∘ f := rfl
Composition of Additive Character with Homomorphism Equals Pointwise Composition
Informal description
For any additive character $\varphi: B \to M$ and additive monoid homomorphism $f: A \to B$, the composition $\varphi \circ f$ as an additive character equals the pointwise composition of $\varphi$ and $f$ as functions. That is, $(\varphi \circ f)(a) = \varphi(f(a))$ for all $a \in A$.
AddChar.compAddMonoidHom_apply theorem
(ψ : AddChar B M) (f : A →+ B) (a : A) : ψ.compAddMonoidHom f a = ψ (f a)
Full source 
@[simp] lemma compAddMonoidHom_apply (ψ : AddChar B M) (f : A →+ B)
    (a : A) : ψ.compAddMonoidHom f a = ψ (f a) := rfl
Evaluation of Composition of Additive Character with Homomorphism
Informal description
For any additive character $\psi: B \to M$, additive monoid homomorphism $f: A \to B$, and element $a \in A$, the composition $\psi \circ f$ evaluated at $a$ equals $\psi$ evaluated at $f(a)$, i.e., $$(\psi \circ f)(a) = \psi(f(a)).$$
AddChar.compAddMonoidHom_injective_left theorem
(f : A →+ B) (hf : Surjective f) : Injective fun ψ : AddChar B M ↦ ψ.compAddMonoidHom f
Full source 
lemma compAddMonoidHom_injective_left (f : A →+ B) (hf : Surjective f) :
    Injective fun ψ : AddChar B M ↦ ψ.compAddMonoidHom f := by
  rintro ψ χ h; rw [DFunLike.ext'_iff] at h ⊢; exact hf.injective_comp_right h
Injectivity of Character Composition with Surjective Homomorphism
Informal description
Let $A$ and $B$ be additive monoids, $M$ a multiplicative monoid, and $f : A \to B$ a surjective additive monoid homomorphism. Then the map $\psi \mapsto \psi \circ f$ from additive characters of $B$ to additive characters of $A$ is injective.
AddChar.compAddMonoidHom_injective_right theorem
(ψ : AddChar B M) (hψ : Injective ψ) : Injective fun f : A →+ B ↦ ψ.compAddMonoidHom f
Full source 
lemma compAddMonoidHom_injective_right (ψ : AddChar B M) (hψ : Injective ψ) :
    Injective fun f : A →+ B ↦ ψ.compAddMonoidHom f := by
  rintro f g h
  rw [DFunLike.ext'_iff] at h ⊢; exact hψ.comp_left h
Injectivity of Composition with Injective Additive Character
Informal description
Let $\psi: B \to M$ be an injective additive character. Then the map sending an additive monoid homomorphism $f: A \to B$ to the composition $\psi \circ f$ is injective. In other words, if $\psi \circ f_1 = \psi \circ f_2$ for two homomorphisms $f_1, f_2: A \to B$, then $f_1 = f_2$.
AddChar.ne_one_iff theorem
: ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1
Full source 
lemma ne_one_iff : ψ ≠ 1ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
Non-triviality criterion for additive characters
Informal description
An additive character $\psi$ from an additive monoid $A$ to a multiplicative monoid $M$ is not the trivial character (which sends all elements to $1$) if and only if there exists some $x \in A$ such that $\psi(x) \neq 1$.
AddChar.ne_zero_iff theorem
: ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1
Full source 
lemma ne_zero_iff : ψ ≠ 0ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
Non-triviality criterion for additive characters: $\psi \neq 0 \iff \exists x, \psi(x) \neq 1$
Informal description
An additive character $\psi$ from an additive monoid $A$ to a multiplicative monoid $M$ is not the zero character (which sends all elements to the multiplicative identity $1$) if and only if there exists some $x \in A$ such that $\psi(x) \neq 1$.
AddChar.instDecidableEq instance
: DecidableEq (AddChar A M)
Full source 
noncomputable instance : DecidableEq (AddChar A M) := Classical.decEq _
Decidability of Equality for Additive Characters
Informal description
For any additive monoid $A$ and multiplicative monoid $M$, equality of additive characters $\psi_1, \psi_2 : A \to M$ is decidable.
AddChar.instCommMonoid instance
: CommMonoid (AddChar A M)
Full source 
/-- When `M` is commutative, `AddChar A M` is a commutative monoid. -/
instance instCommMonoid : CommMonoid (AddChar A M) := toMonoidHomEquiv.commMonoid
Commutative Monoid Structure on Additive Characters
Informal description
For any additive monoid $A$ and commutative multiplicative monoid $M$, the set of additive characters $\text{AddChar}(A, M)$ forms a commutative monoid under pointwise multiplication.
AddChar.instAddCommMonoid instance
: AddCommMonoid (AddChar A M)
Full source 
/-- When `M` is commutative, `AddChar A M` is an additive commutative monoid. -/
instance instAddCommMonoid : AddCommMonoid (AddChar A M) := Additive.addCommMonoid
Additive Commutative Monoid Structure on Additive Characters
Informal description
For any additive monoid $A$ and commutative multiplicative monoid $M$, the set of additive characters $\text{AddChar}(A, M)$ forms an additive commutative monoid under pointwise addition.
AddChar.coe_mul theorem
(ψ χ : AddChar A M) : ⇑(ψ * χ) = ψ * χ
Full source 
@[simp, norm_cast] lemma coe_mul (ψ χ : AddChar A M) : ⇑(ψ * χ) = ψ * χ := rfl
Pointwise Product of Additive Characters
Informal description
For any two additive characters $\psi, \chi : A \to M$, the underlying function of their product $\psi * \chi$ is equal to the pointwise product of the functions $\psi$ and $\chi$, i.e., $(\psi * \chi)(x) = \psi(x) \cdot \chi(x)$ for all $x \in A$.
AddChar.coe_add theorem
(ψ χ : AddChar A M) : ⇑(ψ + χ) = ψ * χ
Full source 
@[simp, norm_cast] lemma coe_add (ψ χ : AddChar A M) : ⇑(ψ + χ) = ψ * χ := rfl
Pointwise Product as Sum of Additive Characters
Informal description
For any two additive characters $\psi, \chi : A \to M$, the underlying function of their sum $\psi + \chi$ is equal to the pointwise product of the functions $\psi$ and $\chi$, i.e., $(\psi + \chi)(x) = \psi(x) \cdot \chi(x)$ for all $x \in A$.
AddChar.coe_pow theorem
(ψ : AddChar A M) (n : ℕ) : ⇑(ψ ^ n) = ψ ^ n
Full source 
@[simp, norm_cast] lemma coe_pow (ψ : AddChar A M) (n : ℕ) : ⇑(ψ ^ n) = ψ ^ n := rfl
Power of Additive Character is Pointwise Power
Informal description
For any additive character $\psi: A \to M$ and any natural number $n$, the $n$-th power of $\psi$ (defined pointwise) satisfies $(\psi^n)(x) = (\psi(x))^n$ for all $x \in A$.
AddChar.coe_nsmul theorem
(n : ℕ) (ψ : AddChar A M) : ⇑(n • ψ) = ψ ^ n
Full source 
@[simp, norm_cast] lemma coe_nsmul (n : ℕ) (ψ : AddChar A M) : ⇑(n • ψ) = ψ ^ n := rfl
Scalar Multiple of Additive Character Equals Pointwise Power: $n \cdot \psi = \psi^n$
Informal description
For any natural number $n$ and any additive character $\psi \colon A \to M$, the $n$-th scalar multiple of $\psi$ (under the additive group structure of additive characters) equals the $n$-th power of $\psi$ (under the multiplicative group structure of additive characters). In other words, the function associated with $n \cdot \psi$ is equal to $\psi^n$ pointwise.
AddChar.coe_prod theorem
(s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i)
Full source 
@[simp, norm_cast]
lemma coe_prod (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i) := by
  induction s using Finset.cons_induction <;> simp [*]
Pointwise Product of Additive Characters Equals Monoid Product
Informal description
For any finite set $s$ of indices and any family of additive characters $\psi_i : A \to M$ indexed by $i \in s$, the product of the characters $\prod_{i \in s} \psi_i$ as elements of the commutative monoid of additive characters is equal to the pointwise product of the functions $\prod_{i \in s} \psi_i(x)$ for any $x \in A$.
AddChar.coe_sum theorem
(s : Finset ι) (ψ : ι → AddChar A M) : ∑ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i)
Full source 
@[simp, norm_cast]
lemma coe_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∑ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i) := by
  induction s using Finset.cons_induction <;> simp [*]
Sum of Additive Characters Equals Pointwise Product
Informal description
For any finite set $s$ of indices and any family of additive characters $\psi_i : A \to M$ indexed by $i \in s$, the sum of the characters $\sum_{i \in s} \psi_i$ as elements of the additive commutative monoid of additive characters is equal to the pointwise product of the functions $\prod_{i \in s} \psi_i(x)$ for any $x \in A$.
AddChar.mul_apply theorem
(ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a
Full source 
@[simp] lemma mul_apply (ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a := rfl
Pointwise Product of Additive Characters
Informal description
For any additive characters $\psi, \phi \colon A \to M$ and any element $a \in A$, the product character $(\psi \cdot \phi)(a)$ is equal to the product $\psi(a) \cdot \phi(a)$ in $M$.
AddChar.add_apply theorem
(ψ φ : AddChar A M) (a : A) : (ψ + φ) a = ψ a * φ a
Full source 
@[simp] lemma add_apply (ψ φ : AddChar A M) (a : A) : (ψ + φ) a = ψ a * φ a := rfl
Pointwise Sum of Additive Characters Evaluates as Product of Character Values
Informal description
For any additive characters $\psi, \phi \colon A \to M$ and any element $a \in A$, the sum of characters $(\psi + \phi)(a)$ is equal to the product $\psi(a) \cdot \phi(a)$ in $M$.
AddChar.pow_apply theorem
(ψ : AddChar A M) (n : ℕ) (a : A) : (ψ ^ n) a = (ψ a) ^ n
Full source 
@[simp] lemma pow_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (ψ ^ n) a = (ψ a) ^ n := rfl
Power of Additive Character Evaluates as Power of Character Value
Informal description
For any additive character $\psi \colon A \to M$, natural number $n \in \mathbb{N}$, and element $a \in A$, the $n$-th power of $\psi$ evaluated at $a$ equals the $n$-th power of $\psi(a)$, i.e., $(\psi^n)(a) = (\psi(a))^n$.
AddChar.nsmul_apply theorem
(ψ : AddChar A M) (n : ℕ) (a : A) : (n • ψ) a = (ψ a) ^ n
Full source 
@[simp] lemma nsmul_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (n • ψ) a = (ψ a) ^ n := rfl
Scalar Multiplication of Additive Character Evaluates as Power of Character Value
Informal description
For any additive character $\psi \colon A \to M$, natural number $n \in \mathbb{N}$, and element $a \in A$, the scalar multiple $n \cdot \psi$ evaluated at $a$ equals the $n$-th power of $\psi(a)$, i.e., $(n \cdot \psi)(a) = (\psi(a))^n$.
AddChar.prod_apply theorem
(s : Finset ι) (ψ : ι → AddChar A M) (a : A) : (∏ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a
Full source 
lemma prod_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
    (∏ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a := by rw [coe_prod, Finset.prod_apply]
Pointwise Product of Additive Characters Equals Product of Evaluations
Informal description
For any finite set $s$ of indices, any family of additive characters $\psi_i \colon A \to M$ indexed by $i \in s$, and any element $a \in A$, the product of the characters $\prod_{i \in s} \psi_i$ evaluated at $a$ equals the product of the evaluations $\prod_{i \in s} \psi_i(a)$.
AddChar.sum_apply theorem
(s : Finset ι) (ψ : ι → AddChar A M) (a : A) : (∑ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a
Full source 
lemma sum_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
    (∑ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a := by rw [coe_sum, Finset.prod_apply]
Sum of Additive Characters Evaluates as Product of Values
Informal description
For any finite set $s$ of indices, any family of additive characters $\psi_i \colon A \to M$ indexed by $i \in s$, and any element $a \in A$, the sum of the characters $\sum_{i \in s} \psi_i$ evaluated at $a$ equals the product of the evaluations $\prod_{i \in s} \psi_i(a)$.
AddChar.mul_eq_add theorem
(ψ χ : AddChar A M) : ψ * χ = ψ + χ
Full source 
lemma mul_eq_add (ψ χ : AddChar A M) : ψ * χ = ψ + χ := rfl
Pointwise Product Equals Sum for Additive Characters
Informal description
For any additive characters $\psi, \chi : A \to M$, the pointwise product $\psi \cdot \chi$ is equal to the pointwise sum $\psi + \chi$ as additive characters.
AddChar.pow_eq_nsmul theorem
(ψ : AddChar A M) (n : ℕ) : ψ ^ n = n • ψ
Full source 
lemma pow_eq_nsmul (ψ : AddChar A M) (n : ℕ) : ψ ^ n = n • ψ := rfl
Power of Additive Character Equals Scalar Multiple: $\psi^n = n \cdot \psi$
Informal description
For any additive character $\psi : A \to M$ and any natural number $n$, the $n$-th power of $\psi$ (defined via pointwise multiplication) is equal to the $n$-th scalar multiple of $\psi$ (defined via pointwise addition). That is, $\psi^n = n \cdot \psi$.
AddChar.prod_eq_sum theorem
(s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∑ i ∈ s, ψ i
Full source 
lemma prod_eq_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∑ i ∈ s, ψ i := rfl
Product of Additive Characters Equals Their Sum
Informal description
For any finite set $s$ and any family of additive characters $\psi_i : A \to M$ indexed by $i \in s$, the product of the characters $\prod_{i \in s} \psi_i$ equals their sum $\sum_{i \in s} \psi_i$ as functions from $A$ to $M$.
AddChar.toMonoidHomEquiv_add theorem
(ψ φ : AddChar A M) : toMonoidHomEquiv (ψ + φ) = toMonoidHomEquiv ψ * toMonoidHomEquiv φ
Full source 
@[simp] lemma toMonoidHomEquiv_add (ψ φ : AddChar A M) :
    toMonoidHomEquiv (ψ + φ) = toMonoidHomEquiv ψ * toMonoidHomEquiv φ := rfl
Additive-Multiplicative Equivalence Preserves Pointwise Operations
Informal description
For any additive characters $\psi, \phi \colon A \to M$, the equivalence between additive characters and monoid homomorphisms satisfies \[ \text{toMonoidHomEquiv}(\psi + \phi) = \text{toMonoidHomEquiv}(\psi) \cdot \text{toMonoidHomEquiv}(\phi), \] where the addition on the left is pointwise addition of additive characters and the multiplication on the right is pointwise multiplication of monoid homomorphisms.
AddChar.toMonoidHomEquiv_symm_mul theorem
(ψ φ : Multiplicative A →* M) : toMonoidHomEquiv.symm (ψ * φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ
Full source 
@[simp] lemma toMonoidHomEquiv_symm_mul (ψ φ : MultiplicativeMultiplicative A →* M) :
    toMonoidHomEquiv.symm (ψ * φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ := rfl
Inverse of Additive Character Equivalence Preserves Sum under Pointwise Product
Informal description
For any monoid homomorphisms $\psi, \varphi \colon \text{Multiplicative}\, A \to^* M$, the inverse of the equivalence $\text{toMonoidHomEquiv}$ maps their pointwise product to the sum of the inverses, i.e., \[ \text{toMonoidHomEquiv}^{-1}(\psi \cdot \varphi) = \text{toMonoidHomEquiv}^{-1}(\psi) + \text{toMonoidHomEquiv}^{-1}(\varphi). \]
AddChar.toMonoidHomMulEquiv definition
: AddChar A M ≃* (Multiplicative A →* M)
Full source 
/-- The natural equivalence to `(Multiplicative A →* M)` is a monoid isomorphism. -/
def toMonoidHomMulEquiv : AddCharAddChar A M ≃* (Multiplicative A →* M) :=
  { toMonoidHomEquiv with map_mul' := fun φ ψ ↦ by rfl }
Multiplicative isomorphism between additive characters and monoid homomorphisms
Informal description
The natural equivalence between additive characters $\text{AddChar}\, A\, M$ and monoid homomorphisms $\text{Multiplicative}\, A \to^* M$ is a multiplicative isomorphism. Specifically, it maps the pointwise product of additive characters to the pointwise product of the corresponding monoid homomorphisms.
AddChar.toAddMonoidAddEquiv definition
: Additive (AddChar A M) ≃+ (A →+ Additive M)
Full source 
/-- Additive characters `A → M` are the same thing as additive homomorphisms from `A` to
`Additive M`. -/
def toAddMonoidAddEquiv : AdditiveAdditive (AddChar A M) ≃+ (A →+ Additive M) :=
  { toAddMonoidHomEquiv with map_add' := fun φ ψ ↦ by rfl }
Additive equivalence between additive characters and additive monoid homomorphisms
Informal description
The additive equivalence between the additive group of additive characters $\text{AddChar}(A, M)$ and the group of additive monoid homomorphisms from $A$ to the additive version of $M$, denoted $A \to^+ \text{Additive } M$. This equivalence maps each additive character $\psi : A \to M$ to its corresponding additive monoid homomorphism $\psi : A \to \text{Additive } M$, preserving the additive structure. The inverse map converts additive monoid homomorphisms back to additive characters. The equivalence satisfies that for any additive characters $\varphi, \psi$, the sum $\varphi + \psi$ corresponds to the pointwise product of their images in $\text{Additive } M$.
AddChar.doubleDualEmb definition
: A →+ AddChar (AddChar A M) M
Full source 
/-- The double dual embedding. -/
def doubleDualEmb : A →+ AddChar (AddChar A M) M where
  toFun a := { toFun := fun ψ ↦ ψ a
               map_zero_eq_one' := by simp
               map_add_eq_mul' := by simp }
  map_zero' := by ext; simp
  map_add' _ _ := by ext; simp [map_add_eq_mul]
Double dual embedding of additive characters
Informal description
The double dual embedding is an additive monoid homomorphism from $A$ to the additive characters of the additive characters of $A$ with values in $M$. Specifically, for each $a \in A$, it maps $\psi \mapsto \psi(a)$ for any additive character $\psi \colon A \to M$.
AddChar.doubleDualEmb_apply theorem
(a : A) (ψ : AddChar A M) : doubleDualEmb a ψ = ψ a
Full source 
@[simp] lemma doubleDualEmb_apply (a : A) (ψ : AddChar A M) : doubleDualEmb a ψ = ψ a := rfl
Double Dual Embedding Evaluation: $\text{doubleDualEmb}(a)(\psi) = \psi(a)$
Informal description
For any element $a$ in an additive monoid $A$ and any additive character $\psi \colon A \to M$ with values in a multiplicative monoid $M$, the double dual embedding evaluated at $a$ and $\psi$ equals $\psi(a)$.
AddChar.sum_eq_ite theorem
(ψ : AddChar A R) [Decidable (ψ = 0)] : ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0
Full source 
lemma sum_eq_ite (ψ : AddChar A R) [Decidable (ψ = 0)] :
    ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0 := by
  split_ifs with h
  · simp [h]
  obtain ⟨x, hx⟩ := ne_one_iff.1 h
  refine eq_zero_of_mul_eq_self_left hx ?_
  rw [Finset.mul_sum]
  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm
Sum of additive character values: $\sum_{a \in A} \psi(a) = \begin{cases} |A| & \text{if } \psi = 0 \\ 0 & \text{otherwise} \end{cases}$
Informal description
Let $A$ be a finite additive monoid, $R$ a multiplicative monoid, and $\psi \colon A \to R$ an additive character. Then the sum $\sum_{a \in A} \psi(a)$ equals the cardinality of $A$ if $\psi$ is the zero character (sending all elements to $1$), and equals $0$ otherwise.
AddChar.sum_eq_zero_iff_ne_zero theorem
: ∑ x, ψ x = 0 ↔ ψ ≠ 0
Full source 
lemma sum_eq_zero_iff_ne_zero : ∑ x, ψ x∑ x, ψ x = 0 ↔ ψ ≠ 0 := by
  classical
  rw [sum_eq_ite, Ne.ite_eq_right_iff]; exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
Sum of additive character values is zero if and only if character is non-trivial
Informal description
Let $A$ be a finite additive monoid, $R$ a multiplicative monoid, and $\psi \colon A \to R$ an additive character. Then the sum $\sum_{x \in A} \psi(x)$ equals zero if and only if $\psi$ is not the zero character (i.e., $\psi$ does not send all elements to $1$).
AddChar.sum_ne_zero_iff_eq_zero theorem
: ∑ x, ψ x ≠ 0 ↔ ψ = 0
Full source 
lemma sum_ne_zero_iff_eq_zero : ∑ x, ψ x∑ x, ψ x ≠ 0∑ x, ψ x ≠ 0 ↔ ψ = 0 := sum_eq_zero_iff_ne_zero.not_left
Non-zero Sum of Additive Character Values if and only if Character is Trivial
Informal description
For a finite additive monoid $A$ and multiplicative monoid $R$, given an additive character $\psi \colon A \to R$, the sum $\sum_{x \in A} \psi(x)$ is non-zero if and only if $\psi$ is the zero character (i.e., $\psi$ sends all elements to $1$).
AddChar.instCommGroup instance
: CommGroup (AddChar A M)
Full source 
/-- 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). -/
instance instCommGroup : CommGroup (AddChar A M) :=
  { instCommMonoid with
    inv := fun ψ ↦ ψ.compAddMonoidHom negAddMonoidHom
    inv_mul_cancel := fun ψ ↦ by ext1 x; simp [negAddMonoidHom, ← map_add_eq_mul]}
Commutative Group Structure on Additive Characters
Informal description
For any commutative additive group $A$ and commutative multiplicative monoid $M$, the set of additive characters $\text{AddChar}(A, M)$ forms a commutative group under pointwise multiplication. The inverse of a character $\psi$ is given by $\psi^{-1}(x) = \psi(-x)$ for all $x \in A$.
AddChar.instAddCommGroup instance
: AddCommGroup (AddChar A M)
Full source 
/-- The additive characters on a commutative additive group form a commutative group. -/
instance : AddCommGroup (AddChar A M) := Additive.addCommGroup
Additive Characters Form an Additive Commutative Group
Informal description
For any commutative additive group $A$ and commutative multiplicative monoid $M$, the set of additive characters $\text{AddChar}(A, M)$ forms an additive commutative group, where the addition is defined pointwise and the negation of a character $\psi$ is given by $\psi^{-1}(x) = \psi(-x)$ for all $x \in A$.
AddChar.inv_apply theorem
(ψ : AddChar A M) (a : A) : ψ⁻¹ a = ψ (-a)
Full source 
@[simp] lemma inv_apply (ψ : AddChar A M) (a : A) : ψ⁻¹ a = ψ (-a) := rfl
Inverse of Additive Character Evaluates as Character at Negative Point
Informal description
For any additive character $\psi \colon A \to M$ and any element $a \in A$, the inverse character evaluated at $a$ satisfies $\psi^{-1}(a) = \psi(-a)$.
AddChar.neg_apply theorem
(ψ : AddChar A M) (a : A) : (-ψ) a = ψ (-a)
Full source 
@[simp] lemma neg_apply (ψ : AddChar A M) (a : A) : (-ψ) a = ψ (-a) := rfl
Negation of Additive Character Evaluates as Character at Negative Point
Informal description
For any additive character $\psi \colon A \to M$ and any element $a \in A$, the negation of the character evaluated at $a$ satisfies $(-\psi)(a) = \psi(-a)$.
AddChar.div_apply theorem
(ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a * χ (-a)
Full source 
lemma div_apply (ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a * χ (-a) := rfl
Quotient of Additive Characters Evaluated at a Point
Informal description
Let $A$ be an additive group and $M$ a multiplicative monoid. For any additive characters $\psi, \chi \colon A \to M$ and any element $a \in A$, the value of the quotient character $\psi / \chi$ at $a$ is given by $(\psi / \chi)(a) = \psi(a) \cdot \chi(-a)$.
AddChar.sub_apply theorem
(ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a * χ (-a)
Full source 
lemma sub_apply (ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a * χ (-a) := rfl
Difference of Additive Characters Evaluated at a Point: $(\psi - \chi)(a) = \psi(a) \cdot \chi(-a)$
Informal description
Let $A$ be an additive group and $M$ a multiplicative monoid. For any additive characters $\psi, \chi \colon A \to M$ and any element $a \in A$, the value of the difference character $\psi - \chi$ at $a$ is given by $(\psi - \chi)(a) = \psi(a) \cdot \chi(-a)$.
AddChar.val_isUnit theorem
{A M} [AddGroup A] [Monoid M] (φ : AddChar A M) (a : A) : IsUnit (φ a)
Full source 
/-- The values of an additive character on an additive group are units. -/
lemma val_isUnit {A M} [AddGroup A] [Monoid M] (φ : AddChar A M) (a : A) : IsUnit (φ a) :=
  IsUnit.map φ.toMonoidHom <| Group.isUnit (Multiplicative.ofAdd a)
Values of Additive Characters are Units
Informal description
Let $A$ be an additive group and $M$ a multiplicative monoid. For any additive character $\varphi \colon A \to M$ and any element $a \in A$, the value $\varphi(a)$ is a unit in $M$.
AddChar.map_neg_eq_inv theorem
(ψ : AddChar A M) (a : A) : ψ (-a) = (ψ a)⁻¹
Full source 
/-- An additive character maps negatives to inverses (when defined) -/
lemma map_neg_eq_inv (ψ : AddChar A M) (a : A) : ψ (-a) = (ψ a)⁻¹ := by
  apply eq_inv_of_mul_eq_one_left
  simp only [← map_add_eq_mul, neg_add_cancel, map_zero_eq_one]
Additive Character Maps Negatives to Inverses: $\psi(-a) = (\psi a)^{-1}$
Informal description
For any additive character $\psi$ from an additive group $A$ to a multiplicative monoid $M$, and for any element $a \in A$, the character maps the additive inverse $-a$ to the multiplicative inverse of $\psi(a)$, i.e., $\psi(-a) = (\psi a)^{-1}$.
AddChar.map_zsmul_eq_zpow theorem
(ψ : AddChar A M) (n : ℤ) (a : A) : ψ (n • a) = (ψ a) ^ n
Full source 
/-- An additive character maps integer scalar multiples to integer powers. -/
lemma map_zsmul_eq_zpow (ψ : AddChar A M) (n : ℤ) (a : A) : ψ (n • a) = (ψ a) ^ n :=
  ψ.toMonoidHom.map_zpow a n
Additive Character Maps Integer Scalar Multiplication to Integer Power: $\psi(n \cdot a) = (\psi a)^n$
Informal description
Let $A$ be an additive group and $M$ a multiplicative monoid. For any additive character $\psi \colon A \to M$, any integer $n \in \mathbb{Z}$, and any element $a \in A$, the character satisfies $\psi(n \cdot a) = (\psi(a))^n$, where $n \cdot a$ denotes the integer scalar multiplication of $a$ by $n$.
AddChar.inv_apply' theorem
(ψ : AddChar A M) (a : A) : ψ⁻¹ a = (ψ a)⁻¹
Full source 
lemma inv_apply' (ψ : AddChar A M) (a : A) : ψ⁻¹ a = (ψ a)⁻¹ := by rw [inv_apply, map_neg_eq_inv]
Inverse of Additive Character Evaluates as Multiplicative Inverse: $\psi^{-1}(a) = (\psi a)^{-1}$
Informal description
For any additive character $\psi \colon A \to M$ and any element $a \in A$, the inverse character evaluated at $a$ satisfies $\psi^{-1}(a) = (\psi(a))^{-1}$.
AddChar.neg_apply' theorem
(ψ : AddChar A M) (a : A) : (-ψ) a = (ψ a)⁻¹
Full source 
lemma neg_apply' (ψ : AddChar A M) (a : A) : (-ψ) a = (ψ a)⁻¹ := map_neg_eq_inv _ _
Negation of Additive Character Yields Multiplicative Inverse: $(-\psi)(a) = (\psi(a))^{-1}$
Informal description
For any additive character $\psi$ from an additive group $A$ to a multiplicative monoid $M$, and for any element $a \in A$, the negation of $\psi$ evaluated at $a$ equals the multiplicative inverse of $\psi$ evaluated at $a$, i.e., $(-\psi)(a) = (\psi(a))^{-1}$.
AddChar.div_apply' theorem
(ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a / χ a
Full source 
lemma div_apply' (ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a / χ a := by
  rw [div_apply, map_neg_eq_inv, div_eq_mul_inv]
Quotient of Additive Characters Evaluated at a Point: $(\psi / \chi)(a) = \psi(a) / \chi(a)$
Informal description
Let $A$ be an additive group and $M$ a multiplicative monoid. For any additive characters $\psi, \chi \colon A \to M$ and any element $a \in A$, the value of the quotient character $\psi / \chi$ at $a$ is given by $(\psi / \chi)(a) = \psi(a) / \chi(a)$.
AddChar.sub_apply' theorem
(ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a / χ a
Full source 
lemma sub_apply' (ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a / χ a := by
  rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]
Difference of Additive Characters Evaluated at a Point: $(\psi - \chi)(a) = \psi(a) / \chi(a)$
Informal description
Let $A$ be an additive group and $M$ a multiplicative monoid. For any additive characters $\psi, \chi \colon A \to M$ and any element $a \in A$, the value of the difference character $\psi - \chi$ at $a$ is given by $(\psi - \chi)(a) = \psi(a) / \chi(a)$.
AddChar.zsmul_apply theorem
(n : ℤ) (ψ : AddChar A M) (a : A) : (n • ψ) a = ψ a ^ n
Full source 
@[simp] lemma zsmul_apply (n : ℤ) (ψ : AddChar A M) (a : A) : (n • ψ) a = ψ a ^ n := by
  cases n <;> simp [-neg_apply, neg_apply']
Power Law for Scalar Multiples of Additive Characters: $(n \cdot \psi)(a) = \psi(a)^n$
Informal description
For any integer $n$, any additive character $\psi \colon A \to M$ from an additive group $A$ to a multiplicative monoid $M$, and any element $a \in A$, the value of the $n$-scalar multiple of $\psi$ at $a$ is equal to $\psi(a)$ raised to the power $n$, i.e., $(n \cdot \psi)(a) = \psi(a)^n$.
AddChar.zpow_apply theorem
(ψ : AddChar A M) (n : ℤ) (a : A) : (ψ ^ n) a = ψ a ^ n
Full source 
@[simp] lemma zpow_apply (ψ : AddChar A M) (n : ℤ) (a : A) : (ψ ^ n) a = ψ a ^ n := zsmul_apply ..
Power Law for Additive Characters: $(\psi^n)(a) = \psi(a)^n$
Informal description
For any additive character $\psi \colon A \to M$ from an additive group $A$ to a multiplicative monoid $M$, any integer $n$, and any element $a \in A$, the value of the $n$-th power of $\psi$ at $a$ is equal to $\psi(a)$ raised to the power $n$, i.e., $(\psi^n)(a) = \psi(a)^n$.
AddChar.map_sub_eq_div theorem
(ψ : AddChar A M) (a b : A) : ψ (a - b) = ψ a / ψ b
Full source 
lemma map_sub_eq_div (ψ : AddChar A M) (a b : A) : ψ (a - b) = ψ a / ψ b :=
  ψ.toMonoidHom.map_div _ _
Additive Character Difference Property: $\psi(a - b) = \psi(a)/\psi(b)$
Informal description
For any additive character $\psi \colon A \to M$ and any elements $a, b \in A$, the character satisfies $\psi(a - b) = \psi(a) / \psi(b)$.
AddChar.injective_iff theorem
{ψ : AddChar A M} : Injective ψ ↔ ∀ ⦃x⦄, ψ x = 1 → x = 0
Full source 
lemma injective_iff {ψ : AddChar A M} : InjectiveInjective ψ ↔ ∀ ⦃x⦄, ψ x = 1 → x = 0 :=
  ψ.toMonoidHom.ker_eq_bot_iff.symm.trans eq_bot_iff
Injective Additive Character Criterion: $\psi$ injective $\iff$ $\psi(x)=1 \Rightarrow x=0$
Informal description
An additive character $\psi \colon A \to M$ is injective if and only if for every $x \in A$, $\psi(x) = 1$ implies $x = 0$.
AddChar.mulShift definition
(ψ : AddChar R M) (r : R) : AddChar R M
Full source 
/-- Define the multiplicative shift of an additive character.
This satisfies `mulShift ψ a x = ψ (a * x)`. -/
def mulShift (ψ : AddChar R M) (r : R) : AddChar R M :=
  ψ.compAddMonoidHom (AddMonoidHom.mulLeft r)
Multiplicative shift of an additive character
Informal description
Given an additive character $\psi \colon R \to M$ and an element $r \in R$, the multiplicative shift $\psi_r$ is the additive character defined by $\psi_r(x) = \psi(r \cdot x)$ for all $x \in R$.
AddChar.mulShift_apply theorem
{ψ : AddChar R M} {r : R} {x : R} : mulShift ψ r x = ψ (r * x)
Full source 
@[simp] lemma mulShift_apply {ψ : AddChar R M} {r : R} {x : R} : mulShift ψ r x = ψ (r * x) :=
  rfl
Evaluation of Multiplicative Shift: $\psi_r(x) = \psi(rx)$
Informal description
For any additive character $\psi \colon R \to M$ of a ring $R$ into a multiplicative monoid $M$, and for any elements $r, x \in R$, the multiplicative shift $\psi_r$ evaluated at $x$ satisfies $\psi_r(x) = \psi(r \cdot x)$.
AddChar.inv_mulShift theorem
(ψ : AddChar R M) : ψ⁻¹ = mulShift ψ (-1)
Full source 
/-- `ψ⁻¹ = mulShift ψ (-1))`. -/
theorem inv_mulShift (ψ : AddChar R M) : ψ⁻¹ = mulShift ψ (-1) := by
  ext
  rw [inv_apply, mulShift_apply, neg_mul, one_mul]
Inverse of Additive Character as Multiplicative Shift by $-1$
Informal description
For any additive character $\psi \colon R \to M$ of a ring $R$ into a multiplicative monoid $M$, the inverse character $\psi^{-1}$ is equal to the multiplicative shift of $\psi$ by $-1$, i.e., $\psi^{-1} = \psi_{-1}$ where $\psi_{-1}(x) = \psi(-x)$ for all $x \in R$.
AddChar.mulShift_spec' theorem
(ψ : AddChar R M) (n : ℕ) (x : R) : mulShift ψ n x = ψ x ^ n
Full source 
/-- If `n` is a natural number, then `mulShift ψ n x = (ψ x) ^ n`. -/
theorem mulShift_spec' (ψ : AddChar R M) (n : ℕ) (x : R) : mulShift ψ n x = ψ x ^ n := by
  rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]
Power Property of Multiplicative Shift: $\psi_n(x) = \psi(x)^n$
Informal description
For any additive character $\psi \colon R \to M$ from a ring $R$ to a multiplicative monoid $M$, any natural number $n$, and any element $x \in R$, the multiplicative shift $\psi_n$ evaluated at $x$ satisfies $\psi_n(x) = (\psi(x))^n$.
AddChar.pow_mulShift theorem
(ψ : AddChar R M) (n : ℕ) : ψ ^ n = mulShift ψ n
Full source 
/-- If `n` is a natural number, then `ψ ^ n = mulShift ψ n`. -/
theorem pow_mulShift (ψ : AddChar R M) (n : ℕ) : ψ ^ n = mulShift ψ n := by
  ext x
  rw [pow_apply, ← mulShift_spec']
Power of Additive Character as Multiplicative Shift: $\psi^n = \psi_n$
Informal description
For any additive character $\psi \colon R \to M$ from a ring $R$ to a multiplicative monoid $M$ and any natural number $n$, the $n$-th power of $\psi$ equals the multiplicative shift of $\psi$ by $n$, i.e., $\psi^n = \psi_n$ where $\psi_n(x) = \psi(n \cdot x)$ for all $x \in R$.
AddChar.mulShift_mul theorem
(ψ : AddChar R M) (r s : R) : mulShift ψ r * mulShift ψ s = mulShift ψ (r + s)
Full source 
/-- The product of `mulShift ψ r` and `mulShift ψ s` is `mulShift ψ (r + s)`. -/
theorem mulShift_mul (ψ : AddChar R M) (r s : R) :
    mulShift ψ r * mulShift ψ s = mulShift ψ (r + s) := by
  ext
  rw [mulShift_apply, right_distrib, map_add_eq_mul]; norm_cast
Additive property of multiplicative shifts: $\psi_r \cdot \psi_s = \psi_{r+s}$
Informal description
Let $R$ be a ring and $M$ a multiplicative monoid. For any additive character $\psi \colon R \to M$ and elements $r, s \in R$, the pointwise product of the multiplicative shifts $\psi_r$ and $\psi_s$ equals the multiplicative shift $\psi_{r+s}$. That is, $\psi_r \cdot \psi_s = \psi_{r+s}$.
AddChar.mulShift_mulShift theorem
(ψ : AddChar R M) (r s : R) : mulShift (mulShift ψ r) s = mulShift ψ (r * s)
Full source 
lemma mulShift_mulShift (ψ : AddChar R M) (r s : R) :
    mulShift (mulShift ψ r) s = mulShift ψ (r * s) := by
  ext
  simp only [mulShift_apply, mul_assoc]
Composition of Multiplicative Shifts of Additive Characters
Informal description
Let $R$ be a ring and $M$ a multiplicative monoid. For any additive character $\psi \colon R \to M$ and elements $r, s \in R$, the multiplicative shift of $\psi$ by $s$ after shifting by $r$ equals the multiplicative shift of $\psi$ by the product $r \cdot s$. In other words, $(\psi_r)_s = \psi_{r \cdot s}$.
AddChar.mulShift_zero theorem
(ψ : AddChar R M) : mulShift ψ 0 = 1
Full source 
/-- `mulShift ψ 0` is the trivial character. -/
@[simp]
theorem mulShift_zero (ψ : AddChar R M) : mulShift ψ 0 = 1 := by
  ext; rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]
Multiplicative Shift by Zero Yields Trivial Character
Informal description
For any additive character $\psi \colon R \to M$ of a ring $R$ into a multiplicative monoid $M$, the multiplicative shift of $\psi$ by $0$ is the trivial additive character, i.e., $\psi_0 = \mathbf{1}$.
AddChar.mulShift_one theorem
(ψ : AddChar R M) : mulShift ψ 1 = ψ
Full source 
@[simp]
lemma mulShift_one (ψ : AddChar R M) : mulShift ψ 1 = ψ := by
  ext; rw [mulShift_apply, one_mul]
Multiplicative shift by one preserves the additive character
Informal description
For any additive character $\psi \colon R \to M$ of a ring $R$ into a multiplicative monoid $M$, the multiplicative shift of $\psi$ by the multiplicative identity $1 \in R$ equals $\psi$ itself, i.e., $\psi_1 = \psi$.
AddChar.mulShift_unit_eq_one_iff theorem
(ψ : AddChar R M) {u : R} (hu : IsUnit u) : ψ.mulShift u = 1 ↔ ψ = 1
Full source 
lemma mulShift_unit_eq_one_iff (ψ : AddChar R M) {u : R} (hu : IsUnit u) :
    ψ.mulShift u = 1 ↔ ψ = 1 := by
  refine ⟨fun h ↦ ?_, ?_⟩
  · ext1 y
    rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]
    simpa only [mulShift_apply] using DFunLike.ext_iff.mp h (hu.unit⁻¹ * y)
  · rintro rfl
    ext1 y
    rw [mulShift_apply, one_apply, one_apply]
Multiplicative Shift by Unit is Trivial if and only if Character is Trivial
Informal description
Let $R$ be a ring and $M$ a multiplicative monoid. For any additive character $\psi \colon R \to M$ and any unit $u \in R$, the multiplicative shift $\psi_u$ is equal to the trivial character $\mathbf{1}$ if and only if $\psi$ itself is the trivial character. That is, $\psi_u = \mathbf{1} \leftrightarrow \psi = \mathbf{1}$.