Abelian categories

Stream: mathlib4

[Patrick Massot]

With @yannis monbru this morning, we generated abelian.pdf showing how far we are from abelian categories in mathlib4. I think I've never seen so many grey nodes in such a graph. Is this something that should be refactored in mathlib3? I'm not pushing for this, only asking.

[Ruben Van de Velde]

Could be - maybe category_theory.limits.constructions.limits_of_products_and_equalizers is a good candidate for splitting?

[Kevin Buzzard]

Even with the yoneda lemma file in the "official" list of porting targets there are many grey nodes. (edit: today's version is here)

[Patrick Massot]

Indeed the Yoneda case is even more spectacular.