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

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

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

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

def CategoryTheory.AbelianOfAdjunction.cokernelIso {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) (G : Functor D C) [G.PreservesZeroMorphisms] [Limits.HasCokernels C] (i : F.comp G ≅ Functor.id C) (adj : G ⊣ F) {X Y : C} (f : X ⟶ Y) : G.obj (Limits.cokernel (F.map f)) ≅ 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₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) (G : Functor D C) [G.PreservesZeroMorphisms] [Limits.HasCokernels C] [Limits.HasKernels C] [Limits.PreservesFiniteLimits G] (i : F.comp G ≅ Functor.id C) (adj : G ⊣ F) {X Y : C} (f : X ⟶ Y) : Limits.kernel (G.map (Limits.cokernel.π (F.map f))) ≅ Limits.kernel (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₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) (G : Functor D C) [G.PreservesZeroMorphisms] [Limits.HasCokernels C] [Limits.HasKernels C] [Limits.PreservesFiniteLimits G] [F.PreservesZeroMorphisms] (i : F.comp G ≅ Functor.id C) (adj : G ⊣ F) {X Y : C} (f : X ⟶ Y) : Abelian.coimage f ≅ 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₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) (G : Functor D C) [G.PreservesZeroMorphisms] [Limits.HasCokernels C] [Limits.HasKernels C] [Limits.PreservesFiniteLimits G] [F.PreservesZeroMorphisms] (i : F.comp G ≅ Functor.id C) (adj : G ⊣ F) {X Y : C} (f : X ⟶ Y) : (coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f

def CategoryTheory.abelianOfAdjunction {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) [F.PreservesZeroMorphisms] (G : Functor D C) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] (i : F.comp G ≅ Functor.id C) (adj : G ⊣ F) : 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₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) [F.PreservesZeroMorphisms] [F.IsEquivalence] : 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} [Category.{u_2, u_1} C] [LocallySmall.{w, u_2, u_1} C] [Preadditive C] (P Q : 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} [Category.{u_2, u_1} C] [LocallySmall.{w, u_2, u_1} C] [Preadditive C] {P Q : C} (f g : P ⟶ Q) : (functor C).map (f + g) = (functor C).map f + (functor C).map g

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

noncomputable instance CategoryTheory.ShrinkHoms.preadditive (C : Type u_1) [Category.{u_2, u_1} C] [LocallySmall.{w, u_2, u_1} C] [Preadditive C] : Preadditive (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) [Category.{u_2, u_1} C] [LocallySmall.{w, u_2, u_1} C] [Preadditive C] : (inverse C).Additive

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

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

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

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

Equations

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