# mathlibdocumentation

representation_theory.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 monoid_algebra 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 group_algebra.average (k : Type u_1) (G : Type u_2) [group G] [fintype G] [invertible (fintype.card G)] :

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

Equations
theorem group_algebra.average_def (k : Type u_1) (G : Type u_2) [group G] [fintype G] [invertible (fintype.card G)] :
= (fintype.card G) finset.univ.sum (λ (g : G), G) g)
@[simp]
theorem group_algebra.mul_average_left (k : Type u_1) (G : Type u_2) [group G] [fintype G] [invertible (fintype.card G)] (g : G) :

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

@[simp]
theorem group_algebra.mul_average_right (k : Type u_1) (G : Type u_2) [group G] [fintype G] [invertible (fintype.card G)] (g : G) :

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} [group G] [ V] (ρ : V) :
V

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

Equations
@[simp]
theorem representation.mem_invariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) (v : V) :
v ρ.invariants ∀ (g : G), (ρ g) v = v
theorem representation.invariants_eq_inter {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) :
ρ.invariants.carrier = ⋂ (g : G),
@[simp]
noncomputable def representation.average_map {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) [fintype G] [invertible (fintype.card G)] :

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

Equations
theorem representation.average_map_invariant {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) [fintype G] [invertible (fintype.card G)] (v : V) :

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

theorem representation.average_map_id {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) [fintype G] [invertible (fintype.card G)] (v : V) (hv : v ρ.invariants) :
(ρ.average_map) v = v

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

theorem representation.is_proj_average_map {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) [fintype G] [invertible (fintype.card G)] :
theorem representation.lin_hom.mem_invariants_iff_comm {k : Type u} [comm_ring k] {G : Group} {X Y : Rep k G} (f : (X.V) →ₗ[k] (Y.V)) (g : G) :
( Y.ρ) g) f = f (X.ρ) g f = f (Y.ρ) g

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

Equations
@[simp]
theorem representation.lin_hom.invariants_equiv_Rep_hom_apply_hom {k : Type u} [comm_ring k] {G : Group} (X Y : Rep k G) (f : Y.ρ).invariants)) :
@[simp]
theorem representation.lin_hom.invariants_equiv_Rep_hom_symm_apply_coe {k : Type u} [comm_ring k] {G : Group} (X Y : Rep k G) (f : X Y) :
= f.hom