Documentation

Mathlib.CategoryTheory.Limits.Preserves.Finite

Preservation of finite (co)limits. #

These functors are also known as left exact (flat) or right exact functors when the categories involved are abelian, or more generally, finitely (co)complete.

source
class CategoryTheory.Limits.PreservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
Prop

A functor is said to preserve finite limits, if it preserves all limits of shape J, where J : Type is a finite category.

Instances
    source
    instance CategoryTheory.Limits.instSubsingletonPreservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
    Subsingleton (PreservesFiniteLimits F)
    source
    @[instance 100]
    instance CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteLimits F] (J : Type w) [SmallCategory J] [FinCategory J] :
    PreservesLimitsOfShape J F

    Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.

    source
    theorem CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
    PreservesFiniteLimits F

    If we preserve limits of some arbitrary size, then we preserve all finite limits.

    source
    @[instance 120]
    instance CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
    PreservesFiniteLimits F
    source
    @[instance 120]
    instance CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimits F] :
    PreservesFiniteLimits F
    source
    theorem CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F) :
    PreservesFiniteLimits F

    We can always derive PreservesFiniteLimits C by showing that we are preserving limits at an arbitrary universe.

    source
    theorem CategoryTheory.Limits.comp_preservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteLimits F] [PreservesFiniteLimits G] :
    PreservesFiniteLimits (F.comp G)

    The composition of two left exact functors is left exact.

    source
    theorem CategoryTheory.Limits.preservesFiniteLimits_of_natIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F ≅ G) [PreservesFiniteLimits F] :
    PreservesFiniteLimits G

    Transfer preservation of finite limits along a natural isomorphism in the functor.

    source
    class CategoryTheory.Limits.PreservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
    Prop

    A functor F preserves finite products if it preserves all from Discrete J for Fintype J

    Instances
      source
      instance CategoryTheory.Limits.instSubsingletonPreservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
      Subsingleton (PreservesFiniteProducts F)
      source
      @[instance 100]
      instance CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : Type u) [Finite J] [PreservesFiniteProducts F] :
      PreservesLimitsOfShape (Discrete J) F
      source
      instance CategoryTheory.Limits.comp_preservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteProducts F] [PreservesFiniteProducts G] :
      PreservesFiniteProducts (F.comp G)
      source
      instance CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteLimits F] :
      PreservesFiniteProducts F
      source
      class CategoryTheory.Limits.ReflectsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
      Prop

      A functor is said to reflect finite limits, if it reflects all limits of shape J, where J : Type is a finite category.

      Instances
        source
        instance CategoryTheory.Limits.instSubsingletonReflectsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
        Subsingleton (ReflectsFiniteLimits F)
        source
        class CategoryTheory.Limits.ReflectsFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
        Prop

        A functor F preserves finite products if it reflects limits of shape Discrete J for finite J

        Instances
          source
          instance CategoryTheory.Limits.instSubsingletonReflectsFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
          Subsingleton (ReflectsFiniteProducts F)
          source
          theorem CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
          ReflectsFiniteLimits F

          If we reflect limits of some arbitrary size, then we reflect all finite limits.

          source
          @[instance 120]
          instance CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
          ReflectsFiniteLimits F
          source
          @[instance 120]
          instance CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsLimits F] :
          ReflectsFiniteLimits F
          source
          theorem CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteLimits (F.comp G)] [ReflectsFiniteLimits G] :
          PreservesFiniteLimits F

          If F ⋙ G preserves finite limits and G reflects finite limits, then F preserves finite limits.

          source
          theorem CategoryTheory.Limits.preservesFiniteProducts_of_reflects_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteProducts (F.comp G)] [ReflectsFiniteProducts G] :
          PreservesFiniteProducts F

          If F ⋙ G preserves finite products and G reflects finite products, then F preserves finite products.

          source
          instance CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteLimits C] [PreservesFiniteLimits F] :
          ReflectsFiniteLimits F
          source
          instance CategoryTheory.Limits.reflectsFiniteProducts_of_reflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteProducts C] [PreservesFiniteProducts F] :
          ReflectsFiniteProducts F
          source
          instance CategoryTheory.Limits.comp_reflectsFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [ReflectsFiniteProducts F] [ReflectsFiniteProducts G] :
          ReflectsFiniteProducts (F.comp G)
          source
          instance CategoryTheory.Limits.instReflectsFiniteProductsOfReflectsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteLimits F] :
          ReflectsFiniteProducts F
          source
          class CategoryTheory.Limits.PreservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
          Prop

          A functor is said to preserve finite colimits, if it preserves all colimits of shape J, where J : Type is a finite category.

          Instances
            source
            instance CategoryTheory.Limits.instSubsingletonPreservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
            Subsingleton (PreservesFiniteColimits F)
            source
            @[instance 100]
            instance CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteColimits F] (J : Type w) [SmallCategory J] [FinCategory J] :
            PreservesColimitsOfShape J F

            Preserving finite colimits also implies preserving colimits over finite shapes in higher universes.

            source
            theorem CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
            PreservesFiniteColimits F

            If we preserve colimits of some arbitrary size, then we preserve all finite colimits.

            source
            @[instance 120]
            instance CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
            PreservesFiniteColimits F
            source
            @[instance 120]
            instance CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimits F] :
            PreservesFiniteColimits F
            source
            theorem CategoryTheory.Limits.preservesFiniteColimits_of_preservesFiniteColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesColimitsOfShape J F) :
            PreservesFiniteColimits F

            We can always derive PreservesFiniteColimits C by showing that we are preserving colimits at an arbitrary universe.

            source
            theorem CategoryTheory.Limits.comp_preservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteColimits F] [PreservesFiniteColimits G] :
            PreservesFiniteColimits (F.comp G)

            The composition of two right exact functors is right exact.

            source
            theorem CategoryTheory.Limits.preservesFiniteColimits_of_natIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F ≅ G) [PreservesFiniteColimits F] :
            PreservesFiniteColimits G

            Transfer preservation of finite colimits along a natural isomorphism in the functor.

            source
            class CategoryTheory.Limits.PreservesFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
            Prop

            A functor F preserves finite products if it preserves all from Discrete J for Fintype J

            Instances
              source
              instance CategoryTheory.Limits.instSubsingletonPreservesFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
              Subsingleton (PreservesFiniteCoproducts F)
              source
              @[instance 100]
              instance CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (J : Type u) [Finite J] [PreservesFiniteCoproducts F] :
              PreservesColimitsOfShape (Discrete J) F
              source
              instance CategoryTheory.Limits.comp_preservesFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteCoproducts F] [PreservesFiniteCoproducts G] :
              PreservesFiniteCoproducts (F.comp G)
              source
              instance CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteColimits F] :
              PreservesFiniteCoproducts F
              source
              class CategoryTheory.Limits.ReflectsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
              Prop

              A functor is said to reflect finite colimits, if it reflects all colimits of shape J, where J : Type is a finite category.

              Instances
                source
                instance CategoryTheory.Limits.instSubsingletonReflectsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
                Subsingleton (ReflectsFiniteColimits F)
                source
                theorem CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
                ReflectsFiniteColimits F

                If we reflect colimits of some arbitrary size, then we reflect all finite colimits.

                source
                @[instance 120]
                instance CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
                ReflectsFiniteColimits F
                source
                @[instance 120]
                instance CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsColimits F] :
                ReflectsFiniteColimits F
                source
                class CategoryTheory.Limits.ReflectsFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
                Prop

                A functor F preserves finite coproducts if it reflects colimits of shape Discrete J for finite J

                Instances
                  source
                  instance CategoryTheory.Limits.instSubsingletonReflectsFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
                  Subsingleton (ReflectsFiniteCoproducts F)
                  source
                  theorem CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteColimits (F.comp G)] [ReflectsFiniteColimits G] :
                  PreservesFiniteColimits F

                  If F ⋙ G preserves finite colimits and G reflects finite colimits, then F preserves finite colimits.

                  source
                  theorem CategoryTheory.Limits.preservesFiniteCoproducts_of_reflects_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [PreservesFiniteCoproducts (F.comp G)] [ReflectsFiniteCoproducts G] :
                  PreservesFiniteCoproducts F

                  If F ⋙ G preserves finite coproducts and G reflects finite coproducts, then F preserves finite coproducts.

                  source
                  instance CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteColimits C] [PreservesFiniteColimits F] :
                  ReflectsFiniteColimits F
                  source
                  instance CategoryTheory.Limits.reflectsFiniteCoproductsOfReflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.ReflectsIsomorphisms] [HasFiniteCoproducts C] [PreservesFiniteCoproducts F] :
                  ReflectsFiniteCoproducts F
                  source
                  instance CategoryTheory.Limits.comp_reflectsFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [ReflectsFiniteCoproducts F] [ReflectsFiniteCoproducts G] :
                  ReflectsFiniteCoproducts (F.comp G)
                  source
                  instance CategoryTheory.Limits.instReflectsFiniteCoproductsOfReflectsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteColimits F] :
                  ReflectsFiniteCoproducts F