Theorems · Theorem · category theory

CategoryTheory.finrank_hom_simple_simple_le_one

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C)
  [FiniteDimensional 𝕜 (X ⟶ X)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y], Module.finrank 𝕜 (X ⟶ Y) ≤ 1

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.

Defined in

Mathlib.CategoryTheory.Preadditive.Schur

Cited by

2 results in Mathlib

Foundations

Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveFieldIsAlgClosedCategoryTheory.LinearCategoryTheory.Limits.HasKernelsFiniteDimensionalCategoryTheory.SimpleCategoryTheory.Simple