Theorems · Theorem · category theory

CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : DivisionRing 𝕜] [CategoryTheory.Limits.HasKernels C] [inst_4 : CategoryTheory.Linear 𝕜 C] {X Y : C}
  [CategoryTheory.Simple X] [CategoryTheory.Simple Y], (∀ (a : X ≅ Y), False) → Module.finrank 𝕜 (X ⟶ Y) = 0

Part of Schur's lemma for 𝕜-linear categories: the hom space between two non-isomorphic simple objects is 0-dimensional.

Defined in

Mathlib.CategoryTheory.Preadditive.Schur

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveDivisionRingCategoryTheory.Limits.HasKernelsCategoryTheory.LinearCategoryTheory.SimpleCategoryTheory.Simple