Direct sum of additive characters #
This file defines the direct sum of additive characters.
def
AddChar.directSum
{ι : Type u_1}
{R : Type u_2}
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommGroup (G i)]
[CommMonoid R]
(ψ : (i : ι) → AddChar (G i) R)
:
Direct sum of additive characters.
Equations
- AddChar.directSum ψ = AddChar.toAddMonoidHomEquiv.symm (DirectSum.toAddMonoid fun (i : ι) => AddChar.toAddMonoidHomEquiv (ψ i))
Instances For
@[simp]
theorem
AddChar.directSum_toFun
{ι : Type u_1}
{R : Type u_2}
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommGroup (G i)]
[CommMonoid R]
(ψ : (i : ι) → AddChar (G i) R)
(a✝ : DirectSum ι fun (i : ι) => G i)
:
(AddChar.directSum ψ) a✝ = (DirectSum.toAddMonoid fun (i : ι) => AddChar.toAddMonoidHomEquiv (ψ i)) a✝
theorem
AddChar.directSum_injective
{ι : Type u_1}
{R : Type u_2}
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommGroup (G i)]
[CommMonoid R]
:
Function.Injective AddChar.directSum