finrank_endomorphism_simple_eq_one

English

In a k-linear category, if X is simple and End(X) is finite-dimensional, then End(X) is a division algebra; over an algebraically closed field 𝕜 it is isomorphic to 𝕜, hence one-dimensional.

Русский

В k-линейной категории простой объект X имеет End(X) делительную алгебру; при алгебраически замкнутом поле 𝕜 она изоморфна 𝕜 и следовательно одномерна.

LaTeX

$$$\mathrm{End}(X) \text{ is a division algebra; over an algebraically closed } 𝕜 \text{ it is } 𝕜$$$

Lean4

/-- **Schur's lemma** for endomorphisms in `𝕜`-linear categories.
-/
theorem finrank_endomorphism_simple_eq_one (X : C) [Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] : finrank 𝕜 (X ⟶ X) = 1 :=
  finrank_endomorphism_eq_one 𝕜 isIso_iff_nonzero

Похожие утверждения