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.

A particular example is the transfer of Abelian instances from a category C to ShrinkHoms C; see ShrinkHoms.abelian. In this case, we also transfer the Preadditive structure.

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

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] [CategoryTheory.Limits.PreservesFiniteLimits G] (i : F.comp G ≅ CategoryTheory.Functor.id C) : 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] [CategoryTheory.Limits.HasCokernels C] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) {X 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] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.PreservesFiniteLimits G] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) {X 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] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.PreservesFiniteLimits G] [F.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) {X 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] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.PreservesFiniteLimits G] [F.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C) (adj : G ⊣ F) {X 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 = 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

noncomputable instance CategoryTheory.ShrinkHoms.homGroup {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Preadditive C] (P Q : CategoryTheory.ShrinkHoms.{u_1} C) : AddCommGroup (P ⟶ Q)

Equations

• P.homGroup Q = (equivShrink (P.fromShrinkHoms ⟶ Q.fromShrinkHoms)).symm.addCommGroup

theorem CategoryTheory.ShrinkHoms.functor_map_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Preadditive C] {P Q : C} (f g : P ⟶ Q) : (CategoryTheory.ShrinkHoms.functor C).map (f + g) = (CategoryTheory.ShrinkHoms.functor C).map f + (CategoryTheory.ShrinkHoms.functor C).map g

theorem CategoryTheory.ShrinkHoms.inverse_map_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Preadditive C] {P Q : CategoryTheory.ShrinkHoms.{u_1} C} (f g : P ⟶ Q) : (CategoryTheory.ShrinkHoms.inverse C).map (f + g) = (CategoryTheory.ShrinkHoms.inverse C).map f + (CategoryTheory.ShrinkHoms.inverse C).map g

noncomputable instance CategoryTheory.ShrinkHoms.preadditive (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Preadditive (CategoryTheory.ShrinkHoms.{u_1} C)

Equations

• CategoryTheory.ShrinkHoms.preadditive C = { homGroup := CategoryTheory.ShrinkHoms.homGroup, add_comp := ⋯, comp_add := ⋯ }

instance CategoryTheory.ShrinkHoms.instAdditiveInverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Preadditive C] : (CategoryTheory.ShrinkHoms.inverse C).Additive

instance CategoryTheory.ShrinkHoms.instAdditiveFunctor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Preadditive C] : (CategoryTheory.ShrinkHoms.functor C).Additive

instance CategoryTheory.ShrinkHoms.hasLimitsOfShape (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.LocallySmall.{w, u_4, u_1} C] (J : Type u_2) [CategoryTheory.Category.{u_3, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.ShrinkHoms.{u_1} C)

instance CategoryTheory.ShrinkHoms.hasFiniteLimits (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.ShrinkHoms.{u_1} C)

noncomputable instance CategoryTheory.ShrinkHoms.abelian (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.LocallySmall.{w, u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian (CategoryTheory.ShrinkHoms.{u_1} C)

Equations

• CategoryTheory.ShrinkHoms.abelian C = CategoryTheory.abelianOfEquivalence (CategoryTheory.ShrinkHoms.inverse C)