mathlib3 documentation

representation_theory.invariants

Subspace of invariants a group representation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) [comm_semiring k] [group G] [fintype G] [invertible ↑(fintype.card G)] :

monoid_algebra k G

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

Equations

group_algebra.average k G = ⅟ ↑(fintype.card G) • finset.univ.sum (λ (g : G), ⇑(monoid_algebra.of k G) g)

@[simp]

theorem group_algebra.mul_average_left (k : Type u_1) (G : Type u_2) [comm_semiring k] [group G] [fintype G] [invertible ↑(fintype.card G)] (g : G) :

finsupp.single g 1 * group_algebra.average k G = group_algebra.average k 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) [comm_semiring k] [group G] [fintype G] [invertible ↑(fintype.card G)] (g : G) :

group_algebra.average k G * finsupp.single g 1 = group_algebra.average k 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G V) :

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

Equations

ρ.invariants = {carrier := {v : V | ∀ (g : G), ⇑(⇑ρ g) v = v}, add_mem' := _, zero_mem' := _, smul_mem' := _}

@[simp]

theorem representation.mem_invariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G V) :

ρ.invariants.carrier = ⋂ (g : G), function.fixed_points ⇑(⇑ρ g)

@[simp]

noncomputable def representation.average_map {k : Type u_1} {G : Type u_2} {V : Type u_3} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G V) [fintype G] [invertible ↑(fintype.card G)] :

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

Equations

ρ.average_map = ⇑(ρ.as_algebra_hom) (group_algebra.average k G)

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

⇑(ρ.average_map) v ∈ ρ.invariants

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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G V) [fintype G] [invertible ↑(fintype.card G)] :

linear_map.is_proj ρ.invariants ρ.average_map

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) :

⇑(⇑(X.ρ.lin_hom Y.ρ) g) f = f ↔ f.comp (⇑(X.ρ) g) = (⇑(Y.ρ) g).comp f

def representation.lin_hom.invariants_equiv_Rep_hom {k : Type u} [comm_ring k] {G : Group} (X Y : Rep k ↥G) :

↥((X.ρ.lin_hom Y.ρ).invariants) ≃ₗ[k] X ⟶ Y

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

Equations

representation.lin_hom.invariants_equiv_Rep_hom X Y = {to_fun := λ (f : ↥((X.ρ.lin_hom Y.ρ).invariants)), {hom := f.val, comm' := _}, map_add' := _, map_smul' := _, inv_fun := λ (f : X ⟶ Y), ⟨f.hom, _⟩, left_inv := _, right_inv := _}

@[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 : ↥((X.ρ.lin_hom Y.ρ).invariants)) :

(⇑(representation.lin_hom.invariants_equiv_Rep_hom X Y) f).hom = f.val

@[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) :

↑(⇑((representation.lin_hom.invariants_equiv_Rep_hom X Y).symm) f) = f.hom

def representation.lin_hom.invariants_equiv_fdRep_hom {k : Type u} [field k] {G : Group} (X Y : fdRep k ↥G) :

↥((representation.lin_hom X.ρ Y.ρ).invariants) ≃ₗ[k] X ⟶ Y

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

Equations

representation.lin_hom.invariants_equiv_fdRep_hom X Y = _.mpr (_.mpr ((representation.lin_hom.invariants_equiv_Rep_hom ((category_theory.forget₂ (fdRep k ↥G) (Rep k ↥G)).obj X) ((category_theory.forget₂ (fdRep k ↥G) (Rep k ↥G)).obj Y)).trans (X.forget₂_hom_linear_equiv Y)))