Documentation

Mathlib.CategoryTheory.Abelian.Transfer

Transferring "abelian-ness" across a functor #

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 surprising: 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 coimageIsoImage

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      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
      Instances For

        If C is an additive category equivalent to an abelian category D via a functor that preserves zero morphisms, then C is also abelian.

        Equations
        Instances For