English
Schur's lemma for k-linear categories yields that End(X) has dimension 1 when X is simple and finite-dimensional.
Русский
Лемма Шура для k-линейных категорий: End(X) имеет размерность 1, если X прост и конечномерен.
LaTeX
$$$\dim_{\mathbb{k}}(\mathrm{End}(X))=1$$$
Lean4
/-- **Schur's lemma** for `𝕜`-linear categories:
if hom spaces are finite dimensional, then the hom space between simples is at most 1-dimensional.
See `finrank_hom_simple_simple_eq_one_iff` and `finrank_hom_simple_simple_eq_zero_iff` below
for the refinements when we know whether or not the simples are isomorphic.
-/
theorem finrank_hom_simple_simple_le_one (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [Simple X] [Simple Y] :
finrank 𝕜 (X ⟶ Y) ≤ 1 := by
obtain (h | h) := subsingleton_or_nontrivial (X ⟶ Y)
· rw [finrank_zero_of_subsingleton]
exact zero_le_one
· obtain ⟨f, nz⟩ := (nontrivial_iff_exists_ne 0).mp h
haveI fi := (isIso_iff_nonzero f).mpr nz
refine finrank_le_one f ?_
intro g
obtain ⟨c, w⟩ := endomorphism_simple_eq_smul_id 𝕜 (g ≫ inv f)
exact ⟨c, by simpa using w =≫ f⟩
