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.

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

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

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

source
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) (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 (with G 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.

Stacks Tag 03A3

Equations
Instances For
    source
    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.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
    Instances For
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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)
      source
      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)
      source
      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