mathlib3 documentation

category_theory.abelian.transfer

Transferring "abelian-ness" across a functor #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Notes #

The hypotheses, following the statement from the Stacks project, may appear suprising: we don't ask that the counit of the adjunction is an isomorphism, but just that we have some potentially unrelated isomorphism i : F ⋙ G ≅ 𝟭 C.

However Lemma A1.1.1 from [Joh02] shows that in this situation the counit itself must be an isomorphism, and thus that C is a reflective subcategory of D.

Someone may like to formalize that lemma, and restate this theorem in terms of reflective. (That lemma has a nice string diagrammatic proof that holds in any bicategory.)

No point making this an instance, as it requires i and adj.

Auxiliary construction for coimage_iso_image

Equations

Auxiliary definition: the abelian coimage and abelian image agree. We still need to check that this agrees with the canonical morphism.

Equations

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

Equations