# mathlibdocumentation

category_theory.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.

## 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.)

theorem category_theory.abelian_of_adjunction.has_kernels {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) (i : F G 𝟭 C)  :

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

theorem category_theory.abelian_of_adjunction.has_cokernels {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) (i : F G 𝟭 C) (adj : G F) :

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

noncomputable def category_theory.abelian_of_adjunction.cokernel_iso {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) (i : F G 𝟭 C) (adj : G F) {X Y : C} (f : X Y) :

Auxiliary construction for coimage_iso_image

Equations
noncomputable def category_theory.abelian_of_adjunction.coimage_iso_image_aux {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) (i : F G 𝟭 C) (adj : G F) {X Y : C} (f : X Y) :

Auxiliary construction for coimage_iso_image

Equations
noncomputable def category_theory.abelian_of_adjunction.coimage_iso_image {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) (i : F G 𝟭 C) (adj : G F) {X Y : C} (f : X Y) :

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

Equations
theorem category_theory.abelian_of_adjunction.coimage_iso_image_hom {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) (i : F G 𝟭 C) (adj : G F) {X Y : C} (f : X Y) :
noncomputable def category_theory.abelian_of_adjunction {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) (i : F G 𝟭 C) (adj : G F) :

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.

Equations
noncomputable def category_theory.abelian_of_equivalence {C : Type u₁} {D : Type u₂} (F : C D)  :

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