mathlib documentation

category_theory.preadditive.schur

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