feat(category_theory/preadditive): Schur's lemma (#7366)
We prove Schur's lemma for `𝕜`-linear categories with finite dimensional hom spaces,
over an algebraically closed field `𝕜`:
the hom space `X ⟶ Y` between simple objects `X` and `Y` is at most one dimensional,
and is 1-dimensional iff `X` and `Y` are isomorphic.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
