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.)
Schur's Lemma (for a general preadditive category), that a nonzero morphism between simple objects is an isomorphism.
As a corollary of Schur's lemma, any morphism between simple objects is (exclusively) either an isomorphism or zero.
Equations
- category_theory.is_iso_equiv_nonzero = {to_fun := _, inv_fun := λ (w : f ≠ 0), category_theory.is_iso_of_hom_simple w, left_inv := _, right_inv := _}