Schur scalarity for commuting endomorphisms

Over ℂ, an endomorphism of a finite-dimensional irreducible representation commuting with the group action is scalar: it has an eigenvalue, and the eigenspace is an invariant subspace. The image of a class-function element under a representation commutes with the action, so it acts as a scalar on every irreducible.

def RS.IsIrredRep {G : Type u_1} {V : Type u_2} [Group G] [AddCommGroup V] [Module ℂ V] (ρ : Representation ℂ G V) : Prop

Irreducibility, spelled invariant-submodule-theoretically.

Equations

• RS.IsIrredRep ρ = (Nontrivial V ∧ ∀ (p : Submodule ℂ V), (∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p) → p = ⊥ ∨ p = ⊤)

theorem RS.commuting_scalar {G : Type u_1} {V : Type u_2} [Group G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] {ρ : Representation ℂ G V} (hirr : IsIrredRep ρ) (T : Module.End ℂ V) (hT : ∀ (g : G), T ∘ₗ ρ g = ρ g ∘ₗ T) : ∃ (c : ℂ), T = c • LinearMap.id

Schur scalarity: a commuting endomorphism of an irreducible representation is scalar.

theorem RS.asAlgebraHom_classElem_comm {G : Type u_1} {V : Type u_2} [Group G] [Fintype G] [AddCommGroup V] [Module ℂ V] (ρ : Representation ℂ G V) (c : G → ℂ) (hc : ∀ (g h : G), c (h * g * h⁻¹) = c g) (g : G) : ρ.asAlgebraHom (classElem c) ∘ₗ ρ g = ρ g ∘ₗ ρ.asAlgebraHom (classElem c)

The image of a class-function element commutes with the action.

theorem RS.asAlgebraHom_classElem_scalar {G : Type u_1} {V : Type u_2} [Group G] [Fintype G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] {ρ : Representation ℂ G V} (hirr : IsIrredRep ρ) (c : G → ℂ) (hc : ∀ (g h : G), c (h * g * h⁻¹) = c g) : ∃ (z : ℂ), ρ.asAlgebraHom (classElem c) = z • LinearMap.id

Scalar action: a class-function element acts as a scalar on every irreducible representation.