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.

Instances For

    C ⥤ₗ D denotes left exact functors C ⥤ D

    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.

      Instances For

        C ⥤ᵣ D denotes right exact functors C ⥤ D

        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.

          Instances For

            C ⥤ₑ D denotes exact functors C ⥤ D

            Instances For

              Turn an exact functor into a left exact functor.

              Instances For

                Turn an exact functor into a left exact functor.

                Instances For