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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
    Subsingleton (CategoryTheory.Limits.PreservesFiniteLimits F)
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    instance CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] (J : Type w) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
    CategoryTheory.Limits.PreservesLimitsOfShape J F

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

    Equations
    • ⋯ = ⋯
    source
    theorem CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
    CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
    CategoryTheory.Limits.PreservesFiniteLimits F
    Equations
    • ⋯ = ⋯
    source
    @[instance 120]
    instance CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimits F] :
    CategoryTheory.Limits.PreservesFiniteLimits F
    Equations
    • ⋯ = ⋯
    source
    theorem CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J}, CategoryTheory.FinCategory J → CategoryTheory.Limits.PreservesLimitsOfShape J F) :
    CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteLimits G] :
    CategoryTheory.Limits.PreservesFiniteLimits (F.comp G)

    The composition of two left exact functors is left exact.

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

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

    source
    class CategoryTheory.Limits.PreservesFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
      Subsingleton (CategoryTheory.Limits.PreservesFiniteProducts F)
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteProducts F] :
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F
      Equations
      • ⋯ = ⋯
      source
      instance CategoryTheory.Limits.comp_preservesFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G] :
      CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)
      Equations
      • ⋯ = ⋯
      source
      instance CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] :
      CategoryTheory.Limits.PreservesFiniteProducts F
      Equations
      • ⋯ = ⋯
      source
      class CategoryTheory.Limits.ReflectsFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
        Subsingleton (CategoryTheory.Limits.ReflectsFiniteLimits F)
        Equations
        • ⋯ = ⋯
        source
        class CategoryTheory.Limits.ReflectsFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
          Subsingleton (CategoryTheory.Limits.ReflectsFiniteProducts F)
          Equations
          • ⋯ = ⋯
          source
          theorem CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
          CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
          CategoryTheory.Limits.ReflectsFiniteLimits F
          Equations
          • ⋯ = ⋯
          source
          @[instance 120]
          instance CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimits F] :
          CategoryTheory.Limits.ReflectsFiniteLimits F
          Equations
          • ⋯ = ⋯
          source
          theorem CategoryTheory.Limits.preservesFiniteLimits_of_reflects_of_preserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteLimits (F.comp G)] [CategoryTheory.Limits.ReflectsFiniteLimits G] :
          CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)] [CategoryTheory.Limits.ReflectsFiniteProducts G] :
          CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits F] :
          CategoryTheory.Limits.ReflectsFiniteLimits F
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Limits.reflectsFiniteProducts_of_reflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.PreservesFiniteProducts F] :
          CategoryTheory.Limits.ReflectsFiniteProducts F
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Limits.comp_reflectsFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsFiniteProducts F] [CategoryTheory.Limits.ReflectsFiniteProducts G] :
          CategoryTheory.Limits.ReflectsFiniteProducts (F.comp G)
          Equations
          • ⋯ = ⋯
          source
          instance CategoryTheory.Limits.instReflectsFiniteProductsOfReflectsFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteLimits F] :
          CategoryTheory.Limits.ReflectsFiniteProducts F
          Equations
          • ⋯ = ⋯
          source
          class CategoryTheory.Limits.PreservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
            Subsingleton (CategoryTheory.Limits.PreservesFiniteColimits F)
            Equations
            • ⋯ = ⋯
            source
            @[instance 100]
            instance CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] (J : Type w) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] :
            CategoryTheory.Limits.PreservesColimitsOfShape J F

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

            Equations
            • ⋯ = ⋯
            source
            theorem CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
            CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
            CategoryTheory.Limits.PreservesFiniteColimits F
            Equations
            • ⋯ = ⋯
            source
            @[instance 120]
            instance CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F] :
            CategoryTheory.Limits.PreservesFiniteColimits F
            Equations
            • ⋯ = ⋯
            source
            theorem CategoryTheory.Limits.preservesFiniteColimits_of_preservesFiniteColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J}, CategoryTheory.FinCategory J → CategoryTheory.Limits.PreservesColimitsOfShape J F) :
            CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.PreservesFiniteColimits G] :
            CategoryTheory.Limits.PreservesFiniteColimits (F.comp G)

            The composition of two right exact functors is right exact.

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

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

            source
            class CategoryTheory.Limits.PreservesFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
              Subsingleton (CategoryTheory.Limits.PreservesFiniteCoproducts F)
              Equations
              • ⋯ = ⋯
              source
              @[instance 100]
              instance CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteCoproducts F] :
              CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Limits.comp_preservesFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteCoproducts F] [CategoryTheory.Limits.PreservesFiniteCoproducts G] :
              CategoryTheory.Limits.PreservesFiniteCoproducts (F.comp G)
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] :
              CategoryTheory.Limits.PreservesFiniteCoproducts F
              Equations
              • ⋯ = ⋯
              source
              class CategoryTheory.Limits.ReflectsFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                Subsingleton (CategoryTheory.Limits.ReflectsFiniteColimits F)
                Equations
                • ⋯ = ⋯
                source
                theorem CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] :
                CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] :
                CategoryTheory.Limits.ReflectsFiniteColimits F
                Equations
                • ⋯ = ⋯
                source
                @[instance 120]
                instance CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimits F] :
                CategoryTheory.Limits.ReflectsFiniteColimits F
                Equations
                • ⋯ = ⋯
                source
                class CategoryTheory.Limits.ReflectsFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                  Subsingleton (CategoryTheory.Limits.ReflectsFiniteCoproducts F)
                  Equations
                  • ⋯ = ⋯
                  source
                  theorem CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteColimits (F.comp G)] [CategoryTheory.Limits.ReflectsFiniteColimits G] :
                  CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteCoproducts (F.comp G)] [CategoryTheory.Limits.ReflectsFiniteCoproducts G] :
                  CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits F] :
                  CategoryTheory.Limits.ReflectsFiniteColimits F
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.Limits.reflectsFiniteCoproductsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.PreservesFiniteCoproducts F] :
                  CategoryTheory.Limits.ReflectsFiniteCoproducts F
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.Limits.comp_reflectsFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsFiniteCoproducts F] [CategoryTheory.Limits.ReflectsFiniteCoproducts G] :
                  CategoryTheory.Limits.ReflectsFiniteCoproducts (F.comp G)
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.Limits.instReflectsFiniteCoproductsOfReflectsFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteColimits F] :
                  CategoryTheory.Limits.ReflectsFiniteCoproducts F
                  Equations
                  • ⋯ = ⋯