# Documentation

Mathlib.RepresentationTheory.Invariants

# Subspace of invariants a group representation #

This file introduces the subspace of invariants of a group representation and proves basic results about it. The main tool used is the average of all elements of the group, seen as an element of MonoidAlgebra k G. The action of this special element gives a projection onto the subspace of invariants. In order for the definition of the average element to make sense, we need to assume for most of the results that the order of G is invertible in k (e. g. k has characteristic 0).

noncomputable def GroupAlgebra.average (k : Type u_1) (G : Type u_2) [] [] [] [] :

The average of all elements of the group G, considered as an element of MonoidAlgebra k G.

Instances For
@[simp]
theorem GroupAlgebra.mul_average_left (k : Type u_1) (G : Type u_2) [] [] [] [] (g : G) :
(fun₀ | g => 1) * =

average k G is invariant under left multiplication by elements of G.

@[simp]
theorem GroupAlgebra.mul_average_right (k : Type u_1) (G : Type u_2) [] [] [] [] (g : G) :
( * fun₀ | g => 1) =

average k G is invariant under right multiplication by elements of G.

def Representation.invariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :

The subspace of invariants, consisting of the vectors fixed by all elements of G.

Instances For
@[simp]
theorem Representation.mem_invariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (v : V) :
∀ (g : G), ↑(ρ g) v = v
theorem Representation.invariants_eq_inter {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :
noncomputable def Representation.averageMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) [] [] :

The action of average k G gives a projection map onto the subspace of invariants.

Instances For
theorem Representation.averageMap_invariant {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) [] [] (v : V) :

The averageMap sends elements of V to the subspace of invariants.

theorem Representation.averageMap_id {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) [] [] (v : V) (hv : ) :
= v

The averageMap acts as the identity on the subspace of invariants.

theorem Representation.isProj_averageMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) [] [] :
theorem Representation.linHom.mem_invariants_iff_comm {k : Type u} [] {G : GroupCat} {X : Rep k G} {Y : Rep k G} (f : X.V →ₗ[k] Y.V) (g : G) :
↑(↑(Representation.linHom () ()) g) f = f LinearMap.comp f (↑() g) = LinearMap.comp (↑() g) f
@[simp]
theorem Representation.linHom.invariantsEquivRepHom_symm_apply_coe {k : Type u} [] {G : GroupCat} (X : Rep k G) (Y : Rep k G) (f : X Y) :
↑() = f.hom
@[simp]
theorem Representation.linHom.invariantsEquivRepHom_apply_hom {k : Type u} [] {G : GroupCat} (X : Rep k G) (Y : Rep k G) (f : { x // }) :
().hom = f
def Representation.linHom.invariantsEquivRepHom {k : Type u} [] {G : GroupCat} (X : Rep k G) (Y : Rep k G) :
{ x // } ≃ₗ[k] X Y

The invariants of the representation linHom X.ρ Y.ρ correspond to the representation homomorphisms from X to Y.

Instances For
def Representation.linHom.invariantsEquivFdRepHom {k : Type u} [] {G : GroupCat} (X : FdRep k G) (Y : FdRep k G) :
{ x // } ≃ₗ[k] X Y

The invariants of the representation linHom X.ρ Y.ρ correspond to the representation homomorphisms from X to Y.

Instances For