Commit 2022-04-03 11:32 12128187

feat(category_theory/abelian): transferring "abelian-ness" across a functor (#13059) If C is an additive category, D is an abelian category, we have F : C ⥤ D G : D ⥤ C (both preserving zero morphisms), G is left exact (that is, preserves finite limits), and further we have adj : G ⊣ F and i : F ⋙ G ≅ 𝟭 C, then C is also abelian. See https://stacks.math.columbia.edu/tag/03A3