# Schur's lemma

We prove the part of Schur's Lemma that holds in any preadditive category with kernels, that any nonzero morphism between simple objects is an isomorphism.

## TODO

If the category is enriched over finite dimensional vector spaces over an algebraically closed field, then we can further prove that dim (X ⟶ Y) ≤ 1.

(Probably easiest to prove this for endomorphisms first: some polynomial p in f : X ⟶ X vanishes by finite dimensionality, that polynomial factors linearly, and at least one factor must be non-invertible, hence zero, so f is a scalar multiple of the identity. Then for any two nonzero f g : X ⟶ Y, observe f ≫ g⁻¹ is a multiple of the identity.)

def category_theory.is_iso_of_hom_simple {C : Type u} {X Y : C} {f : X Y} :
f 0

Schur's Lemma (for a general preadditive category), that a nonzero morphism between simple objects is an isomorphism.

Equations
def category_theory.is_iso_equiv_nonzero {C : Type u} {X Y : C} {f : X Y} :
f 0

As a corollary of Schur's lemma, any morphism between simple objects is (exclusively) either an isomorphism or zero.

Equations