Documentation

LeanPool.RegtsSevenster.RS.Classical.SchurTheory.BlockKill

Kill criteria for the block development #

Vanishing of the ofModule action is elementwise annihilation; intertwiners commute with the whole algebra action, so annihilation transports along equivalences of representations.

theorem RS.intertwiner_comp_asAlgebraHom {G : Type u_1} [Group G] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ G V} {σ : Representation ℂ G W} (f : V →ₗ[ℂ] W) (hf : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) (y : MonoidAlgebra ℂ G) :

An intertwiner commutes with the algebra action.