Documentation

Mathlib.CategoryTheory.Limits.HasExactLimitsOfShape

Exact (co)limits #

We introduce a typeclass HasExactColimitsOfShape J C in order to express that colimits of shape J in a category C are exact. The dual notion is HasExactLimitsOfShape J C. That HasExactColimitsOfShape J C is invariant under equivalences in both parameters is shown in the lemmas HasExactColimitsOfShape.of_domain_equivalence and HasExactColimitsOfShape.of_codomain_equivalence.

See the file Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean for the applications to the AB axioms in abelian categories.

References #

source
class CategoryTheory.HasExactColimitsOfShape (J : Type u') [Category.{v', u'} J] (C : Type u) [Category.{v, u} C] [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).

Instances
    source
    class CategoryTheory.HasExactLimitsOfShape (J : Type u') [Category.{v', u'} J] (C : Type u) [Category.{v, u} C] [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).

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

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

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

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

      source
      theorem CategoryTheory.HasExactColimitsOfShape.of_domain_equivalence (C : Type u) [Category.{v, u} C] {J : Type u_1} {J' : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} J'] (e : J ≌ J') [Limits.HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
      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.

      source
      theorem CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence {C : Type u} [Category.{v, u} C] (J : Type u_1) [Category.{v_1, u_1} J] {D : Type u_2} [Category.{v_2, u_2} D] (e : C ≌ D) [Limits.HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
      HasExactColimitsOfShape J D
      source
      theorem CategoryTheory.HasExactLimitsOfShape.of_domain_equivalence (C : Type u) [Category.{v, u} C] {J : Type u_1} {J' : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} J'] (e : J ≌ J') [Limits.HasLimitsOfShape J C] [HasExactLimitsOfShape J C] :
      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 an initial functor, see hasExactLimitsOfShape_of_initial below.

      source
      theorem CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalence {C : Type u} [Category.{v, u} C] (J : Type u_1) [Category.{v_1, u_1} J] {D : Type u_2} [Category.{v_2, u_2} D] (e : C ≌ D) [Limits.HasLimitsOfShape J C] [HasExactLimitsOfShape J C] :
      HasExactLimitsOfShape J D
      source
      theorem CategoryTheory.Adjunction.hasExactColimitsOfShape {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.Full] [G.Faithful] (J : Type u') [Category.{v', u'} J] [Limits.HasColimitsOfShape J C] [Limits.HasColimitsOfShape J D] [HasExactColimitsOfShape J C] [Limits.HasFiniteLimits D] [Limits.PreservesFiniteLimits F] :
      HasExactColimitsOfShape J D

      Let adj : F ⊣ G be an adjunction, with G : D ⥤ C reflective. Assume that D has finite limits and F commutes with them. If C has exact colimits of shape J, then D also has exact colimits of shape J.

      source
      theorem CategoryTheory.Adjunction.hasExactLimitsOfShape {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Full] [F.Faithful] (J : Type u') [Category.{v', u'} J] [Limits.HasLimitsOfShape J C] [Limits.HasLimitsOfShape J D] [HasExactLimitsOfShape J D] [Limits.HasFiniteColimits C] [Limits.PreservesFiniteColimits G] :
      HasExactLimitsOfShape J C

      Let adj : F ⊣ G be an adjunction, with F : C ⥤ D coreflective. Assume that C has finite colimits and G commutes with them. If D has exact limits of shape J, then C also has exact limits of shape J.