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 [Elephant] 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 CategoryTheory.AbelianOfAdjunction.hasKernels {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) [CategoryTheory.Limits.PreservesFiniteLimits G] : CategoryTheory.Limits.HasKernels C

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

theorem CategoryTheory.AbelianOfAdjunction.hasCokernels {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) : CategoryTheory.Limits.HasCokernels C

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

def CategoryTheory.AbelianOfAdjunction.cokernelIso {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) [CategoryTheory.Limits.HasCokernels C] {X : C} {Y : C} (f : X ⟶ Y) : G.obj (CategoryTheory.Limits.cokernel (F.map f)) ≅ CategoryTheory.Limits.cokernel f

Auxiliary construction for coimageIsoImage

Equations

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

def CategoryTheory.AbelianOfAdjunction.coimageIsoImageAux {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.PreservesFiniteLimits G] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.kernel (G.map (CategoryTheory.Limits.cokernel.π (F.map f))) ≅ CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.π f)

Auxiliary construction for coimageIsoImage

Equations

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

def CategoryTheory.AbelianOfAdjunction.coimageIsoImage {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.PreservesFiniteLimits G] [F.PreservesZeroMorphisms] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Abelian.image f

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.

theorem CategoryTheory.AbelianOfAdjunction.coimageIsoImage_hom {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.PreservesFiniteLimits G] [F.PreservesZeroMorphisms] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.AbelianOfAdjunction.coimageIsoImage F G i adj f).hom = CategoryTheory.Abelian.coimageImageComparison f

def CategoryTheory.abelianOfAdjunction {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits G] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) : CategoryTheory.Abelian C

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

• CategoryTheory.abelianOfAdjunction F G i adj = let_fun this := ⋯; CategoryTheory.Abelian.ofCoimageImageComparisonIsIso

def CategoryTheory.abelianOfEquivalence {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.IsEquivalence] : CategoryTheory.Abelian C

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

• CategoryTheory.abelianOfEquivalence F = CategoryTheory.abelianOfAdjunction F F.inv F.asEquivalence.unitIso.symm F.asEquivalence.symm.toAdjunction