English
If X is a simple object with End(X) finite-dimensional over 𝕜 and every nonzero endomorphism is invertible, then End(X) is 1-dimensional over 𝕜 (hence isomorphic to the field 𝕜).
Русский
Пусть X – простый объект, End(X) конечномерное над 𝕜 и каждый ненулевой эндоморфизм обратим. Тогда End(X) имеет размерность 1 над 𝕜 (то есть изоморфен полю 𝕜).
LaTeX
$$$\dim_{\mathbb{k}}\bigl(\mathrm{End}(X)\bigr)=1$$$
Lean4
/-- As a corollary of Schur's lemma for preadditive categories,
any morphism between simple objects is (exclusively) either an isomorphism or zero.
-/
theorem isIso_iff_nonzero [HasKernels C] {X Y : C} [Simple X] [Simple Y] (f : X ⟶ Y) : IsIso f ↔ f ≠ 0 :=
⟨fun I => by
intro h
apply id_nonzero X
simp only [← IsIso.hom_inv_id f, h, zero_comp], fun w => isIso_of_hom_simple w⟩
