[Merged by Bors] - feat(category_theory/abelian): Schur's lemma

[semorrison]

I wrote this mostly to gain some familiarity with @TwoFX's work on abelian categories from #2817.

That all looked great, and Schur's lemma was pleasantly straightforward.

[semorrison]

I should temper expectations. This is the part of Schur's lemma that holds in any abelian category. The fact that over an algebraically closed field dim = 0 or 1 is still to come.

[jcommelin]

Could you please resolve the conflicts and merge master, so that the diff becomes small again (-;

[semorrison]

Could you please resolve the conflicts and merge master, so that the diff becomes small again (-;

Done.

[semorrison]

I just added has_kernel f as an abbreviation for has_limit (parallel_pair f 0), as this was getting a bit repetitive.

[semorrison]

I added a note that simple contains data, and showed that it is nevertheless a subsingleton.

[jcommelin]

Let's get this merged.

[semorrison]

Let's get this merged.

Sounds good to me. Now that we have has_finite_biproducts we can define semisimple, and when the Maschke's theorem PR is merged we can do the second stage of proving the Rep G is semisimple for a finite group G!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs