Schur's lemma and multiplicities

TheoremSchur's lemma, dimension form#✓fully proved

Let \(G\) be a finite group, \(k\) an algebraically closed field, and \(\rho\), \(\sigma\) irreducible representations of \(G\) on finite-dimensional \(k\)-vector spaces. Then the space \(\operatorname{Hom}_G(\rho, \sigma)\) of intertwining maps from \(\rho\) to \(\sigma\) has dimension \(1\) over \(k\) if \(\sigma\) and \(\rho\) are equivalent, and dimension \(0\) otherwise.

theorem finrank_intertwiningMap_eq_one_or_zero
    {k : Type uK} [Field k] [IsAlgClosed k]
    {G : Type uG} [Group G] [Fintype G]
    {V : Type uV} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
    {W : Type uW} [AddCommGroup W] [Module k W] [FiniteDimensional k W]
    (ρ : Representation k G V) (σ : Representation k G W)
    [ρ.IsIrreducible] [σ.IsIrreducible] :
    Module.finrank k (ρ.IntertwiningMap σ) =
      if Nonempty (Representation.Equiv σ ρ) then 1 else 0

TheoremMultiplicity equals the dimension of the intertwining space#✓fully proved

Let \(G\) be a finite group, \(k\) an algebraically closed field, and \((\rho_i)_{i \in I}\) a family, indexed by a finite set \(I\), of irreducible representations of \(G\) on finite-dimensional \(k\)-vector spaces that are pairwise non-equivalent: \(\rho_i\) and \(\rho_j\) are not equivalent whenever \(i \ne j\). Let \(\sigma\) be a representation of \(G\) on a finite-dimensional \(k\)-vector space, and let \((d_i)_{i \in I}\) be natural numbers such that \(\sigma\) is equivalent to the direct sum of \(d_i\) copies of \(\rho_i\) over all \(i \in I\). Then for every \(i \in I\), \(d_i\) equals the dimension over \(k\) of the space \(\operatorname{Hom}_G(\rho_i, \sigma)\) of intertwining maps from \(\rho_i\) to \(\sigma\).

theorem multiplicity_eq_finrank_intertwiningMap
    {G k : Type*} [Group G] [Fintype G] [Field k] [IsAlgClosed k]
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {V : ι → Type*} [∀ i, AddCommGroup (V i)] [∀ i, Module k (V i)]
    [∀ i, FiniteDimensional k (V i)]
    (ρ : ∀ i, Representation k G (V i))
    [∀ i, (ρ i).IsIrreducible]
    (h_pairwise : ∀ i j, i ≠ j → ¬Nonempty (Representation.Equiv (ρ i) (ρ j)))
    {W : Type*} [AddCommGroup W] [Module k W] [FiniteDimensional k W]
    (σ : Representation k G W)
    (d : ι → ℕ)
    (h_decomp : Nonempty (Representation.Equiv σ
      (Representation.directSum (ι := (i : ι) × Fin (d i)) (fun p => ρ p.1)))) :
    ∀ i, d i = Module.finrank k ((ρ i).IntertwiningMap σ)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.