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.

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

Instances

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The composition of two left exact functors is left exact.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

          Instances
            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) :
            Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

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

            Instances

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

              Instances

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

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

                      Instances

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            The composition of two right exact functors is right exact.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

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

                              Instances

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

                                Instances

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

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

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

                                    Instances

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For