English
Let k be algebraically closed, and V, W be irreducible representations of G over k. Then the dimension of Hom_G(V,W) is 1 if V ≅ W and 0 otherwise.
Русский
Пусть k алгебраически замкнуто, а V, W — неприводимые представления G над k. Тогда размерность пространства морфизмов Hom_G(V,W) равна 1, если V ≅ W, и 0 иначе.
LaTeX
$$$\dim_k \mathrm{Hom}_G(V,W) = \begin{cases}1, & V \cong W \\ 0, & V \ncong W\end{cases}$$$
Lean4
/-- Schur's Lemma: the dimension of the `Hom`-space between two irreducible representation is `0` if
they are not isomorphic, and `1` if they are. -/
theorem finrank_hom_simple_simple [IsAlgClosed k] (V W : FDRep k G) [Simple V] [Simple W] :
finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0 :=
CategoryTheory.finrank_hom_simple_simple k V W
