Documentation

Mathlib.CategoryTheory.Limits.ExactFunctor

Bundled exact functors #

We say that a functor F is left exact if it preserves finite limits, it is right exact if it preserves finite colimits, and it is exact if it is both left exact and right exact.

In this file, we define the categories of bundled left exact, right exact and exact functors.

def CategoryTheory.LeftExactFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
Type (max (max (max u₁ u₂) v₁) v₂)

Bundled left-exact functors.

Equations
Instances For

    C ⥤ₗ D denotes left exact functors C ⥤ D

    Equations
    Instances For
      def CategoryTheory.RightExactFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
      Type (max (max (max u₁ u₂) v₁) v₂)

      Bundled right-exact functors.

      Equations
      Instances For

        C ⥤ᵣ D denotes right exact functors C ⥤ D

        Equations
        Instances For
          def CategoryTheory.ExactFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :
          Type (max (max (max u₁ u₂) v₁) v₂)

          Bundled exact functors.

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

            C ⥤ₑ D denotes exact functors C ⥤ D

            Equations
            Instances For

              An exact functor is in particular a functor.

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

                Turn a left exact functor into an object of the category LeftExactFunctor C D.

                Equations
                Instances For

                  Turn a right exact functor into an object of the category RightExactFunctor C D.

                  Equations
                  Instances For