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.

@[reducible, deprecated CategoryTheory.ObjectProperty.preservesFiniteLimits (since := "2026-10-28")]

def CategoryTheory.leftExactFunctor {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : ObjectProperty (Functor J C)

Left-exactness, as a property of objects in C ⥤ D.

Equations

• @CategoryTheory.leftExactFunctor = @CategoryTheory.ObjectProperty.preservesFiniteLimits

@[deprecated CategoryTheory.ObjectProperty.preservesFiniteLimits_iff (since := "2026-10-28")]

theorem CategoryTheory.leftExactFunctor_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : leftExactFunctor F ↔ Limits.PreservesFiniteLimits F

@[reducible, inline]

abbrev 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

• (C ⥤ₗ D) = CategoryTheory.ObjectProperty.preservesFiniteLimits.FullSubcategory

def CategoryTheory.«term_⥤ₗ_» : Lean.TrailingParserDescr

C ⥤ₗ D denotes left exact functors C ⥤ D

Equations

• CategoryTheory.«term_⥤ₗ_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_⥤ₗ_» 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ₗ ") (Lean.ParserDescr.cat `term 26))

@[reducible, inline]

abbrev CategoryTheory.LeftExactFunctor.forget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C ⥤ₗ D) (Functor C D)

A left exact functor is in particular a functor.

Equations

• CategoryTheory.LeftExactFunctor.forget C D = CategoryTheory.ObjectProperty.preservesFiniteLimits.ι

@[reducible, inline]

abbrev CategoryTheory.LeftExactFunctor.fullyFaithful (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (forget C D).FullyFaithful

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

Equations

• CategoryTheory.LeftExactFunctor.fullyFaithful C D = CategoryTheory.ObjectProperty.preservesFiniteLimits.fullyFaithfulι

@[reducible, deprecated CategoryTheory.ObjectProperty.preservesFiniteColimits (since := "2026-10-28")]

def CategoryTheory.rightExactFunctor {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : ObjectProperty (Functor J C)

Right-exactness, as a property of objects in C ⥤ D.

Equations

• @CategoryTheory.rightExactFunctor = @CategoryTheory.ObjectProperty.preservesFiniteColimits

@[deprecated CategoryTheory.ObjectProperty.preservesFiniteColimits_iff (since := "2026-10-28")]

theorem CategoryTheory.rightExactFunctor_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : rightExactFunctor F ↔ Limits.PreservesFiniteColimits F

@[reducible, inline]

abbrev 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

• (C ⥤ᵣ D) = CategoryTheory.ObjectProperty.preservesFiniteColimits.FullSubcategory

def CategoryTheory.«term_⥤ᵣ_» : Lean.TrailingParserDescr

C ⥤ᵣ D denotes right exact functors C ⥤ D

Equations

• CategoryTheory.«term_⥤ᵣ_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_⥤ᵣ_» 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ᵣ ") (Lean.ParserDescr.cat `term 26))

@[reducible, inline]

abbrev CategoryTheory.RightExactFunctor.forget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C ⥤ᵣ D) (Functor C D)

A right exact functor is in particular a functor.

Equations

• CategoryTheory.RightExactFunctor.forget C D = CategoryTheory.ObjectProperty.preservesFiniteColimits.ι

@[reducible, inline]

abbrev CategoryTheory.RightExactFunctor.fullyFaithful (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (forget C D).FullyFaithful

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

Equations

• CategoryTheory.RightExactFunctor.fullyFaithful C D = CategoryTheory.ObjectProperty.preservesFiniteColimits.fullyFaithfulι

def CategoryTheory.exactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : ObjectProperty (Functor C D)

Exactness, as a property of objects in C ⥤ D.

Equations

• CategoryTheory.exactFunctor C D = CategoryTheory.ObjectProperty.preservesFiniteLimits ⊓ CategoryTheory.ObjectProperty.preservesFiniteColimits

@[simp]

theorem CategoryTheory.exactFunctor_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : exactFunctor C D F ↔ Limits.PreservesFiniteLimits F ∧ Limits.PreservesFiniteColimits F

instance CategoryTheory.instIsClosedUnderIsomorphismsFunctorExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : (exactFunctor C D).IsClosedUnderIsomorphisms

@[reducible, inline]

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

Bundled exact functors.

Equations

• (C ⥤ₑ D) = (CategoryTheory.exactFunctor C D).FullSubcategory

def CategoryTheory.«term_⥤ₑ_» : Lean.TrailingParserDescr

C ⥤ₑ D denotes exact functors C ⥤ D

Equations

• CategoryTheory.«term_⥤ₑ_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_⥤ₑ_» 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ₑ ") (Lean.ParserDescr.cat `term 26))

@[reducible, inline]

abbrev CategoryTheory.ExactFunctor.forget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C ⥤ₑ D) (Functor C D)

An exact functor is in particular a functor.

Equations

• CategoryTheory.ExactFunctor.forget C D = (CategoryTheory.exactFunctor C D).ι

theorem CategoryTheory.exactFunctor_le_preservesFiniteLimits (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : exactFunctor C D ≤ ObjectProperty.preservesFiniteLimits

theorem CategoryTheory.exactFunctor_le_preservesFiniteColimits (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : exactFunctor C D ≤ ObjectProperty.preservesFiniteColimits

@[deprecated CategoryTheory.exactFunctor_le_preservesFiniteLimits (since := "2026-10-28")]

theorem CategoryTheory.exactFunctor_le_leftExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : exactFunctor C D ≤ ObjectProperty.preservesFiniteLimits

Alias of CategoryTheory.exactFunctor_le_preservesFiniteLimits.

@[deprecated CategoryTheory.exactFunctor_le_preservesFiniteColimits (since := "2026-10-28")]

theorem CategoryTheory.exactFunctor_le_rightExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : exactFunctor C D ≤ ObjectProperty.preservesFiniteColimits

Alias of CategoryTheory.exactFunctor_le_preservesFiniteColimits.

@[reducible, inline]

abbrev CategoryTheory.LeftExactFunctor.ofExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C ⥤ₑ D) (C ⥤ₗ D)

Turn an exact functor into a left exact functor.

Equations

• CategoryTheory.LeftExactFunctor.ofExact C D = CategoryTheory.ObjectProperty.ιOfLE ⋯

@[reducible, inline]

abbrev CategoryTheory.RightExactFunctor.ofExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] : Functor (C ⥤ₑ D) (C ⥤ᵣ D)

Turn an exact functor into a right exact functor.

Equations

• CategoryTheory.RightExactFunctor.ofExact C D = CategoryTheory.ObjectProperty.ιOfLE ⋯

@[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_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((ofExact C D).map α).hom = α.hom

@[simp]

theorem CategoryTheory.RightExactFunctor.ofExact_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((ofExact C D).map α).hom = α.hom

@[simp]

theorem CategoryTheory.LeftExactFunctor.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₗ D) : (forget C D).obj F = F.obj

@[simp]

theorem CategoryTheory.RightExactFunctor.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ᵣ D) : (forget C D).obj F = F.obj

@[simp]

theorem CategoryTheory.ExactFunctor.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) : (forget C D).obj F = F.obj

@[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 α = α.hom

@[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 α = α.hom

@[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 α = α.hom

def CategoryTheory.LeftExactFunctor.of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] : C ⥤ₗ D

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

Equations

• CategoryTheory.LeftExactFunctor.of F = { obj := F, property := ⋯ }

def CategoryTheory.RightExactFunctor.of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteColimits F] : C ⥤ᵣ D

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

Equations

• CategoryTheory.RightExactFunctor.of F = { obj := F, property := ⋯ }

def CategoryTheory.ExactFunctor.of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : C ⥤ₑ D

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

Equations

• CategoryTheory.ExactFunctor.of F = { obj := F, property := ⋯ }

@[simp]

theorem CategoryTheory.LeftExactFunctor.of_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] : (of F).obj = F

@[simp]

theorem CategoryTheory.RightExactFunctor.of_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteColimits F] : (of F).obj = F

@[simp]

theorem CategoryTheory.ExactFunctor.of_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : (of F).obj = F

theorem CategoryTheory.LeftExactFunctor.forget_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] : (forget C D).obj (of F) = F

theorem CategoryTheory.RightExactFunctor.forget_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteColimits F] : (forget C D).obj (of F) = F

theorem CategoryTheory.ExactFunctor.forget_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : (forget C D).obj (of F) = F

instance CategoryTheory.instPreservesFiniteLimitsObjFunctorPreservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₗ D) : Limits.PreservesFiniteLimits F.obj

instance CategoryTheory.instPreservesFiniteColimitsObjFunctorPreservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ᵣ D) : Limits.PreservesFiniteColimits F.obj

instance CategoryTheory.instPreservesFiniteLimitsObjFunctorExactFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) : Limits.PreservesFiniteLimits F.obj

instance CategoryTheory.instPreservesFiniteColimitsObjFunctorExactFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) : Limits.PreservesFiniteColimits F.obj

def CategoryTheory.LeftExactFunctor.whiskeringLeft (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (C ⥤ₗ D) (Functor (D ⥤ₗ E) (C ⥤ₗ E))

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.

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_map_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) : ((whiskeringLeft C D E).map η).app H = ObjectProperty.homMk (((Functor.whiskeringLeft C D E).map η.hom).app H.obj)

@[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✝) : ((whiskeringLeft C D E).obj F).map f = ObjectProperty.homMk (F.obj.whiskerLeft f.hom)

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_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

def CategoryTheory.LeftExactFunctor.whiskeringRight (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (D ⥤ₗ E) (Functor (C ⥤ₗ D) (C ⥤ₗ E))

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.

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_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

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_map_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) : ((whiskeringRight C D E).map η).app H = ObjectProperty.homMk (((Functor.whiskeringRight C D E).map η.hom).app H.obj)

@[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✝) : ((whiskeringRight C D E).obj F).map f = ObjectProperty.homMk (Functor.whiskerRight f.hom F.obj)

def CategoryTheory.RightExactFunctor.whiskeringLeft (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (C ⥤ᵣ D) (Functor (D ⥤ᵣ E) (C ⥤ᵣ E))

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.

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_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

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_map_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) : ((whiskeringLeft C D E).map η).app H = ObjectProperty.homMk (((Functor.whiskeringLeft C D E).map η.hom).app H.obj)

@[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✝) : ((whiskeringLeft C D E).obj F).map f = ObjectProperty.homMk (F.obj.whiskerLeft f.hom)

def CategoryTheory.RightExactFunctor.whiskeringRight (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (D ⥤ᵣ E) (Functor (C ⥤ᵣ D) (C ⥤ᵣ E))

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.

@[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✝) : ((whiskeringRight C D E).obj F).map f = ObjectProperty.homMk (Functor.whiskerRight f.hom F.obj)

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_obj_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

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_map_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) : ((whiskeringRight C D E).map η).app H = ObjectProperty.homMk (((Functor.whiskeringRight C D E).map η.hom).app H.obj)

def CategoryTheory.ExactFunctor.whiskeringLeft (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (C ⥤ₑ D) (Functor (D ⥤ₑ E) (C ⥤ₑ E))

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.

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_map_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) : ((whiskeringLeft C D E).map η).app H = ObjectProperty.homMk (((Functor.whiskeringLeft C D E).map η.hom).app H.obj)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_obj_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

@[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✝) : ((whiskeringLeft C D E).obj F).map f = ObjectProperty.homMk (F.obj.whiskerLeft f.hom)

def CategoryTheory.ExactFunctor.whiskeringRight (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (D ⥤ₑ E) (Functor (C ⥤ₑ D) (C ⥤ₑ E))

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.

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_obj_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

@[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✝) : ((whiskeringRight C D E).obj F).map f = ObjectProperty.homMk (Functor.whiskerRight f.hom F.obj)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_map_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) : ((whiskeringRight C D E).map η).app H = ObjectProperty.homMk (((Functor.whiskeringRight C D E).map η.hom).app H.obj)