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₁) [Category.{v₁, u₁} C] (D : Type u₂) [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
      @[reducible, inline]

      The inclusion of left exact functors into functors is fully faithful.

      Equations
      Instances For
        def CategoryTheory.RightExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [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
            @[reducible, inline]

            The inclusion of right exact functors into functors is fully faithful.

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

              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 an exact functor into a left exact functor.

                  Equations
                  Instances For

                    Turn an exact functor into a left exact functor.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.LeftExactFunctor.ofExact_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) :
                      (ofExact C D).obj F = { obj := F.obj, property := }
                      @[simp]
                      theorem CategoryTheory.RightExactFunctor.ofExact_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) :
                      (ofExact C D).obj F = { obj := F.obj, property := }
                      @[simp]
                      theorem CategoryTheory.LeftExactFunctor.ofExact_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F G) :
                      (ofExact C D).map α = α
                      @[simp]
                      theorem CategoryTheory.RightExactFunctor.ofExact_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F G) :
                      (ofExact C D).map α = α
                      @[simp]
                      @[simp]
                      theorem CategoryTheory.LeftExactFunctor.forget_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₗ D} (α : F G) :
                      (forget C D).map α = α
                      @[simp]
                      theorem CategoryTheory.RightExactFunctor.forget_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ᵣ D} (α : F G) :
                      (forget C D).map α = α
                      @[simp]
                      theorem CategoryTheory.ExactFunctor.forget_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F G) :
                      (forget C D).map α = α

                      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

                          Turn an exact functor into an object of the category ExactFunctor C D.

                          Equations
                          Instances For

                            Whiskering a left exact functor by a left exact functor yields a left exact functor.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₗ D) (X : D ⥤ₗ E) :
                              ((whiskeringLeft C D E).obj F).obj X = { obj := F.obj.comp X.obj, property := }
                              @[simp]
                              theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : C ⥤ₗ D} (η : F G) (H : D ⥤ₗ E) (c : C) :
                              (((whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)
                              @[simp]
                              theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₗ D) {X✝ Y✝ : D ⥤ₗ E} (f : X✝ Y✝) :

                              Whiskering a left exact functor by a left exact functor yields a left exact functor.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.LeftExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : D ⥤ₗ E} (η : F G) (H : C ⥤ₗ D) (c : C) :
                                (((whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)
                                @[simp]
                                theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₗ E) {X✝ Y✝ : C ⥤ₗ D} (f : X✝ Y✝) :
                                @[simp]
                                theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₗ E) (X : C ⥤ₗ D) :
                                ((whiskeringRight C D E).obj F).obj X = { obj := X.obj.comp F.obj, property := }

                                Whiskering a right exact functor by a right exact functor yields a right exact functor.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ᵣ D) {X✝ Y✝ : D ⥤ᵣ E} (f : X✝ Y✝) :
                                  @[simp]
                                  theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ᵣ D) (X : D ⥤ᵣ E) :
                                  ((whiskeringLeft C D E).obj F).obj X = { obj := F.obj.comp X.obj, property := }
                                  @[simp]
                                  theorem CategoryTheory.RightExactFunctor.whiskeringLeft_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : C ⥤ᵣ D} (η : F G) (H : D ⥤ᵣ E) (c : C) :
                                  (((whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

                                  Whiskering a right exact functor by a right exact functor yields a right exact functor.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.RightExactFunctor.whiskeringRight_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ᵣ E) {X✝ Y✝ : C ⥤ᵣ D} (f : X✝ Y✝) :
                                    @[simp]
                                    theorem CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ᵣ E) (X : C ⥤ᵣ D) :
                                    ((whiskeringRight C D E).obj F).obj X = { obj := X.obj.comp F.obj, property := }
                                    @[simp]
                                    theorem CategoryTheory.RightExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : D ⥤ᵣ E} (η : F G) (H : C ⥤ᵣ D) (c : C) :
                                    (((whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)

                                    Whiskering an exact functor by an exact functor yields an exact functor.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.ExactFunctor.whiskeringLeft_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₑ D) {X✝ Y✝ : D ⥤ₑ E} (f : X✝ Y✝) :
                                      @[simp]
                                      theorem CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₑ D) (X : D ⥤ₑ E) :
                                      ((whiskeringLeft C D E).obj F).obj X = { obj := F.obj.comp X.obj, property := }
                                      @[simp]
                                      theorem CategoryTheory.ExactFunctor.whiskeringLeft_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : C ⥤ₑ D} (η : F G) (H : D ⥤ₑ E) (c : C) :
                                      (((whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

                                      Whiskering an exact functor by an exact functor yields an exact functor.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.ExactFunctor.whiskeringRight_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₑ E) {X✝ Y✝ : C ⥤ₑ D} (f : X✝ Y✝) :
                                        @[simp]
                                        theorem CategoryTheory.ExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : D ⥤ₑ E} (η : F G) (H : C ⥤ₑ D) (c : C) :
                                        (((whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)
                                        @[simp]
                                        theorem CategoryTheory.ExactFunctor.whiskeringRight_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₑ E) (X : C ⥤ₑ D) :
                                        ((whiskeringRight C D E).obj F).obj X = { obj := X.obj.comp F.obj, property := }