finrank_hom_simple_simple — Mathlib

English

Endomorphism algebra End(X) is a field when X is simple and End(X) is finite-dimensional; in a semisimple setting this yields a one-dimensional endomorphism space.

Русский

Эндоморфизм‑алгебра End(X) является полем, если X прост и End(X) конечномерен; в полуклассическом случае получается одномерное пространство эндоморфизмов.

LaTeX

$$$\dim_{\mathbb{k}}(\mathrm{End}(X))=1$$$

Lean4

theorem finrank_hom_simple_simple (X Y : C) [∀ X Y : C, FiniteDimensional 𝕜 (X ⟶ Y)] [Simple X] [Simple Y] :
    finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0 :=
  by
  split_ifs with h
  · exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h
  · exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)

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