Grothendieck Axioms

This file defines some of the Grothendieck Axioms for abelian categories, and proves basic facts about them.

Definitions

• HasExactColimitsOfShape J C -- colimits of shape J in C are exact.
• The dual of the above definitions, called HasExactLimitsOfShape.
• AB4 -- coproducts are exact (this is formulated in terms of HasExactColimitsOfShape).
• AB5 -- filtered colimits are exact (this is formulated in terms of HasExactColimitsOfShape).

Theorems

• The implication from AB5 to AB4 is established in AB4.ofAB5.
• That HasExactColimitsOfShape J C is invariant under equivalences in both parameters is shown in HasExactColimitsOfShape.of_domain_equivalence and HasExactColimitsOfShape.of_codomain_equivalence.

Remarks

For AB4 and AB5, we only require left exactness as right exactness is automatic. A comparison with Grothendieck's original formulation of the properties can be found in the comments of the linked Stacks page. Exactness as the preservation of short exact sequences is introduced in CategoryTheory.Abelian.Exact.

We do not require Abelian in the definition of AB4 and AB5 because these classes represent individual axioms. An AB4 category is an abelian category satisfying AB4, and similarly for AB5.

References

• Stacks: Grothendieck's AB conditions

class CategoryTheory.HasExactColimitsOfShape (J : Type u') [CategoryTheory.Category.{v', u'} J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] : Prop

A category C is said to have exact colimits of shape J provided that colimits of shape J exist and are exact (in the sense that they preserve finite limits).

• preservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

  Exactness of J-shaped colimits stated as colim : (J ⥤ C) ⥤ C preserving finite limits.

class CategoryTheory.HasExactLimitsOfShape (J : Type u') [CategoryTheory.Category.{v', u'} J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] : Prop

A category C is said to have exact limits of shape J provided that limits of shape J exist and are exact (in the sense that they preserve finite colimits).

• preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim

  Exactness of J-shaped limits stated as lim : (J ⥤ C) ⥤ C preserving finite colimits.

theorem CategoryTheory.HasExactColimitsOfShape.domain_of_functor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} (J : Type u_2) [CategoryTheory.Category.{u_3, u_2} J] [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.HasExactColimitsOfShape J D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.ReflectsFiniteLimits F] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesColimitsOfShape J F] : CategoryTheory.HasExactColimitsOfShape J C

Pull back a HasExactColimitsOfShape J along a functor which preserves and reflects finite limits and preserves colimits of shape J

theorem CategoryTheory.HasExactLimitsOfShape.domain_of_functor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} (J : Type u_2) [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.HasExactLimitsOfShape J D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.ReflectsFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.HasExactLimitsOfShape J C

Pull back a HasExactLimitsOfShape J along a functor which preserves and reflects finite colimits and preserves limits of shape J

theorem CategoryTheory.HasExactColimitsOfShape.of_domain_equivalence (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type u_1} {J' : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} J'] (e : J ≌ J') [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] : CategoryTheory.HasExactColimitsOfShape J' C

Transport a HasExactColimitsOfShape along an equivalence of the shape.

Note: When C has finite limits, this lemma holds with the equivalence replaced by a final functor, see hasExactColimitsOfShape_of_final below.

theorem CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type u_1) [CategoryTheory.Category.{u_3, u_1} J] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D) [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] : CategoryTheory.HasExactColimitsOfShape J D

theorem CategoryTheory.HasExactLimitsOfShape.of_domain_equivalence (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type u_1} {J' : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} J'] (e : J ≌ J') [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.HasExactLimitsOfShape J' C

Transport a HasExactLimitsOfShape along an equivalence of the shape.

Note: When C has finite colimits, this lemma holds with the equivalence replaced by a initial functor, see hasExactLimitsOfShape_of_initial below.

theorem CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type u_1) [CategoryTheory.Category.{u_3, u_1} J] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.HasExactLimitsOfShape J D

class CategoryTheory.AB4OfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] : Prop

A category C which has coproducts is said to have AB4 of size w provided that coproducts of size w are exact.

• ofShape (α : Type w) : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete α) C

@[reducible, inline]

abbrev CategoryTheory.AB4 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] : Prop

A category C which has coproducts is said to have AB4 provided that coproducts are exact.

Stacks Tag 079B

Equations

• CategoryTheory.AB4 C = CategoryTheory.AB4OfSize.{?u.27, ?u.27, ?u.26} C

theorem CategoryTheory.AB4OfSize_shrink (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.AB4OfSize.{max w w', v, u} C] : CategoryTheory.AB4OfSize.{w, v, u} C

@[instance 100]

instance CategoryTheory.instAB4OfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.AB4OfSize.{w, v, u} C] : CategoryTheory.AB4OfSize.{0, v, u} C

class CategoryTheory.AB4StarOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : Prop

A category C which has products is said to have AB4Star (in literature AB4*) provided that products are exact.

Stacks Tag 079B

• ofShape (α : Type w) : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C

@[reducible, inline]

abbrev CategoryTheory.AB4Star (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] : Prop

A category C which has products is said to have AB4Star (in literature AB4*) provided that products are exact.

Equations

• CategoryTheory.AB4Star C = CategoryTheory.AB4StarOfSize.{?u.27, ?u.27, ?u.26} C

theorem CategoryTheory.AB4StarOfSize_shrink (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.AB4StarOfSize.{max w w', v, u} C] : CategoryTheory.AB4StarOfSize.{w, v, u} C

@[instance 100]

instance CategoryTheory.instAB4StarOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.AB4StarOfSize.{w, v, u} C] : CategoryTheory.AB4StarOfSize.{0, v, u} C

class CategoryTheory.CountableAB4 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCountableCoproducts C] : Prop

A category C which has countable coproducts is said to have countable AB4 provided that countable coproducts are exact.

• ofShape (α : Type) [Countable α] : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete α) C

@[instance 100]

instance CategoryTheory.instCountableAB4OfAB4OfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.AB4OfSize.{0, v, u} C] : CategoryTheory.CountableAB4 C

class CategoryTheory.CountableAB4Star (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCountableProducts C] : Prop

A category C which has countable coproducts is said to have countable AB4Star provided that countable products are exact.

• ofShape (α : Type) [Countable α] : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete α) C

@[instance 100]

instance CategoryTheory.instCountableAB4StarOfAB4StarOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.AB4StarOfSize.{0, v, u} C] : CategoryTheory.CountableAB4Star C

class CategoryTheory.AB5OfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', v, u} C] : Prop

A category C which has filtered colimits of a given size is said to have AB5 of that size provided that these filtered colimits are exact.

AB5OfSize.{w, w'} C means that C has exact colimits of shape J : Type w' with Category.{w} J such that J is filtered.

• ofShape (J : Type w') [CategoryTheory.Category.{w, w'} J] [CategoryTheory.IsFiltered J] : CategoryTheory.HasExactColimitsOfShape J C

@[reducible, inline]

abbrev CategoryTheory.AB5 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFilteredColimits C] : Prop

A category C which has filtered colimits is said to have AB5 provided that filtered colimits are exact.

Stacks Tag 079B

Equations

• CategoryTheory.AB5 C = CategoryTheory.AB5OfSize.{?u.23, ?u.23, ?u.23, ?u.22} C

theorem CategoryTheory.AB5OfSize_of_univLE (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w₂, w₂', v, u} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}] [CategoryTheory.AB5OfSize.{w₂, w₂', v, u} C] : CategoryTheory.AB5OfSize.{w, w', v, u} C

theorem CategoryTheory.AB5OfSize_shrink (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{max w w₂, max w' w₂', v, u} C] [CategoryTheory.AB5OfSize.{max w w₂, max w' w₂', v, u} C] : CategoryTheory.AB5OfSize.{w, w', v, u} C

class CategoryTheory.AB5StarOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w', v, u} C] : Prop

A category C which has cofiltered limits is said to have AB5Star (in literature AB5*) provided that cofiltered limits are exact.

Stacks Tag 079B

• ofShape (J : Type w') [CategoryTheory.Category.{w, w'} J] [CategoryTheory.IsCofiltered J] : CategoryTheory.HasExactLimitsOfShape J C

@[reducible, inline]

abbrev CategoryTheory.AB5Star (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCofilteredLimits C] : Prop

A category C which has cofiltered limits is said to have AB5Star (in literature AB5*) provided that cofiltered limits are exact.

Equations

• CategoryTheory.AB5Star C = CategoryTheory.AB5StarOfSize.{?u.23, ?u.23, ?u.23, ?u.22} C

theorem CategoryTheory.AB5StarOfSize_of_univLE (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}] [CategoryTheory.AB5StarOfSize.{w₂, w₂', v, u} C] : CategoryTheory.AB5StarOfSize.{w, w', v, u} C

theorem CategoryTheory.AB5StarOfSize_shrink (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{max w w₂, max w' w₂', v, u} C] [CategoryTheory.AB5StarOfSize.{max w w₂, max w' w₂', v, u} C] : CategoryTheory.AB5StarOfSize.{w, w', v, u} C

theorem CategoryTheory.hasExactColimitsOfShape_of_final (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] {J : Type u_1} {J' : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} J'] (F : CategoryTheory.Functor J J') [F.Final] [CategoryTheory.Limits.HasColimitsOfShape J' C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] : CategoryTheory.HasExactColimitsOfShape J' C

HasExactColimitsOfShape can be "pushed forward" along final functors

theorem CategoryTheory.hasExactLimitsOfShape_of_initial (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] {J : Type u_1} {J' : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} J'] (F : CategoryTheory.Functor J J') [F.Initial] [CategoryTheory.Limits.HasLimitsOfShape J' C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.HasExactLimitsOfShape J' C

HasExactLimitsOfShape can be "pushed forward" along initial functors

instance CategoryTheory.preservesFiniteLimits_liftToFinset (C : Type u) [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α)

theorem CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] (J : Type u_1) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete J)) C] [CategoryTheory.HasExactColimitsOfShape (Finset (CategoryTheory.Discrete J)) C] : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C

HasExactColimitsOfShape (Finset (Discrete J)) C implies HasExactColimitsOfShape (Discrete J) C

theorem CategoryTheory.AB4.of_AB5 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] [CategoryTheory.AB5OfSize.{w, w, v, u} C] : CategoryTheory.AB4OfSize.{w, v, u} C

A category with finite biproducts and finite limits is AB4 if it is AB5.

theorem CategoryTheory.CountableAB4.of_countableAB5 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape ℕ C] [CategoryTheory.HasExactColimitsOfShape ℕ C] [CategoryTheory.Limits.HasCountableCoproducts C] : CategoryTheory.CountableAB4 C

A category with finite biproducts and finite limits has countable AB4 if sequential colimits are exact.

instance CategoryTheory.preservesFiniteColimits_liftToFinset (C : Type u) [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α)

theorem CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] (J : Type u_1) [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C] [CategoryTheory.HasExactLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C] : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C

HasExactLimitsOfShape (Finset (Discrete J))ᵒᵖ C implies HasExactLimitsOfShape (Discrete J) C

theorem CategoryTheory.AB4Star.of_AB5Star (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C] [CategoryTheory.AB5StarOfSize.{w, w, v, u} C] : CategoryTheory.AB4StarOfSize.{w, v, u} C

A category with finite biproducts and finite limits is AB4 if it is AB5.

theorem CategoryTheory.CountableAB4Star.of_countableAB5Star (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] [CategoryTheory.HasExactLimitsOfShape ℕᵒᵖ C] [CategoryTheory.Limits.HasCountableProducts C] : CategoryTheory.CountableAB4Star C

A category with finite biproducts and finite limits has countable AB4* if sequential limits are exact.

theorem CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat_and_finite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCountableCoproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [∀ (J : Type) [inst : Finite J], CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4 C

Checking exactness of colimits of shape Discrete ℕ and Discrete J for finite J is enough for countable AB4.

theorem CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCountableProducts C] [CategoryTheory.Limits.HasFiniteColimits C] [∀ (J : Type) [inst : Finite J], CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4Star C

Checking exactness of limits of shape Discrete ℕ and Discrete J for finite J is enough for countable AB4*.

instance CategoryTheory.hasExactColimitsOfShape_discrete_finite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] (J : Type u_1) [Finite J] : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C

instance CategoryTheory.hasExactLimitsOfShape_discrete_finite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type u_1} [Finite J] : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C

theorem CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasCountableCoproducts C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4 C

Checking AB of shape Discrete ℕ is enough for countable AB4, provided that the category has finite biproducts and finite limits.

theorem CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasCountableProducts C] [CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4Star C

Checking AB* of shape Discrete ℕ is enough for countable AB4*, provided that the category has finite biproducts and finite colimits.

theorem CategoryTheory.hasExactColimitsOfShape_of_preservesMono (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.colim.PreservesMonomorphisms] : CategoryTheory.HasExactColimitsOfShape J C

If colim of shape J into an abelian category C preserves monomorphisms, then C has AB of shape J.

theorem CategoryTheory.hasExactLimitsOfShape_of_preservesEpi (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.lim.PreservesEpimorphisms] : CategoryTheory.HasExactLimitsOfShape J C

If lim of shape J into an abelian category C preserves epimorphisms, then C has AB* of shape J.