Linear independence from a trace supported at the identity #
A linear functional on an algebra that is nonzero at the identity of a group representation and zero at every other group element separates the represented elements. Its translates give dual functionals, so the group elements are linearly independent.
theorem
RS.linearIndependent_of_group_trace
{G : Type u_1}
{A : Type u_2}
[Group G]
[DecidableEq G]
[Ring A]
[Algebra ℂ A]
(ρ : G →* A)
(τ : A →ₗ[ℂ] ℂ)
{c : ℂ}
(hc : c ≠ 0)
(hτ : ∀ (σ : G), τ (ρ σ) = if σ = 1 then c else 0)
:
LinearIndependent ℂ fun (σ : G) => ρ σ
A trace supported at the identity separates every element of a group representation.
theorem
RS.card_le_finrank_of_group_trace
{G : Type u_1}
{A : Type u_2}
[Group G]
[DecidableEq G]
[Fintype G]
[Ring A]
[Algebra ℂ A]
[Module.Finite ℂ A]
(ρ : G →* A)
(τ : A →ₗ[ℂ] ℂ)
{c : ℂ}
(hc : c ≠ 0)
(hτ : ∀ (σ : G), τ (ρ σ) = if σ = 1 then c else 0)
:
In a finite-dimensional algebra a group representation with such a trace has at most the dimension many group elements.