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

• (C ⥤ₗ D) = CategoryTheory.FullSubcategory fun (F : CategoryTheory.Functor C D) => Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F)

instance CategoryTheory.instCategoryLeftExactFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (C ⥤ₗ D)

Equations

• CategoryTheory.instCategoryLeftExactFunctor C D = CategoryTheory.FullSubcategory.category fun (F : CategoryTheory.Functor C D) => Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F)

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))

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

A left exact functor is in particular a functor.

Equations

• CategoryTheory.LeftExactFunctor.forget C D = CategoryTheory.fullSubcategoryInclusion fun (F : CategoryTheory.Functor C D) => Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F)

instance CategoryTheory.instFullLeftExactFunctorFunctorForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.LeftExactFunctor.forget C D).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulLeftExactFunctorFunctorForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.LeftExactFunctor.forget C D).Faithful

Equations

• ⋯ = ⋯

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

• (C ⥤ᵣ D) = CategoryTheory.FullSubcategory fun (F : CategoryTheory.Functor C D) => Nonempty (CategoryTheory.Limits.PreservesFiniteColimits F)

instance CategoryTheory.instCategoryRightExactFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (C ⥤ᵣ D)

Equations

• CategoryTheory.instCategoryRightExactFunctor C D = CategoryTheory.FullSubcategory.category fun (F : CategoryTheory.Functor C D) => Nonempty (CategoryTheory.Limits.PreservesFiniteColimits F)

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))

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

A right exact functor is in particular a functor.

Equations

• CategoryTheory.RightExactFunctor.forget C D = CategoryTheory.fullSubcategoryInclusion fun (F : CategoryTheory.Functor C D) => Nonempty (CategoryTheory.Limits.PreservesFiniteColimits F)

instance CategoryTheory.instFullRightExactFunctorFunctorForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.RightExactFunctor.forget C D).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulRightExactFunctorFunctorForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.RightExactFunctor.forget C D).Faithful

Equations

• ⋯ = ⋯

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.

instance CategoryTheory.instCategoryExactFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (C ⥤ₑ D)

Equations

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

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))

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

An exact functor is in particular a functor.

Equations

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

instance CategoryTheory.instFullExactFunctorFunctorForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.ExactFunctor.forget C D).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulExactFunctorFunctorForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.ExactFunctor.forget C D).Faithful

Equations

• ⋯ = ⋯

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

Turn an exact functor into a left exact functor.

Equations

• CategoryTheory.LeftExactFunctor.ofExact C D = CategoryTheory.FullSubcategory.map ⋯

instance CategoryTheory.instFullExactFunctorLeftExactFunctorOfExact (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.LeftExactFunctor.ofExact C D).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulExactFunctorLeftExactFunctorOfExact (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.LeftExactFunctor.ofExact C D).Faithful

Equations

• ⋯ = ⋯

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

Turn an exact functor into a left exact functor.

Equations

• CategoryTheory.RightExactFunctor.ofExact C D = CategoryTheory.FullSubcategory.map ⋯

instance CategoryTheory.instFullExactFunctorRightExactFunctorOfExact (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.RightExactFunctor.ofExact C D).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulExactFunctorRightExactFunctorOfExact (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.RightExactFunctor.ofExact C D).Faithful

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.LeftExactFunctor.ofExact_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : (CategoryTheory.LeftExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }

@[simp]

theorem CategoryTheory.RightExactFunctor.ofExact_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : (CategoryTheory.RightExactFunctor.ofExact C D).obj F = { obj := F.obj, property := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.LeftExactFunctor.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : C ⥤ₗ D} {G : C ⥤ₗ D} (α : F ⟶ G) : (CategoryTheory.LeftExactFunctor.forget C D).map α = α

@[simp]

theorem CategoryTheory.RightExactFunctor.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : C ⥤ᵣ D} {G : C ⥤ᵣ D} (α : F ⟶ G) : (CategoryTheory.RightExactFunctor.forget C D).map α = α

@[simp]

theorem CategoryTheory.ExactFunctor.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : C ⥤ₑ D} {G : C ⥤ₑ D} (α : F ⟶ G) : (CategoryTheory.ExactFunctor.forget C D).map α = α

def CategoryTheory.LeftExactFunctor.of {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : (CategoryTheory.LeftExactFunctor.of F).obj = F

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• CategoryTheory.instPreservesFiniteLimitsObjFunctorNonempty F = ⋯.some

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

Equations

• CategoryTheory.instPreservesFiniteColimitsObjFunctorNonempty F = ⋯.some

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

Equations

• CategoryTheory.instPreservesFiniteLimitsObjFunctorAndNonemptyPreservesFiniteColimits F = ⋯.some

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

Equations

• CategoryTheory.instPreservesFiniteColimitsObjFunctorAndNonemptyPreservesFiniteLimits F = ⋯.some

def CategoryTheory.LeftExactFunctor.whiskeringLeft (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (C ⥤ₗ D) (CategoryTheory.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_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F : C ⥤ₗ D} {G : C ⥤ₗ D} (η : F ⟶ G) (H : D ⥤ₗ E) (c : C) : (((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ₗ D) (X : D ⥤ₗ E) : ∀ {X_1 Y : C} (f : X_1 ⟶ Y), (((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).obj F).obj X).obj.map f = X.obj.map (F.obj.map f)

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ₗ D) : ∀ {X Y : D ⥤ₗ E} (f : X ⟶ Y) (X_1 : C), (((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).obj F).map f).app X_1 = f.app (F.obj.obj X_1)

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ₗ D) (X : D ⥤ₗ E) (X : C) : (((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).obj F).obj X✝).obj.obj X = X✝.obj.obj (F.obj.obj X)

def CategoryTheory.LeftExactFunctor.whiskeringRight (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (D ⥤ₗ E) (CategoryTheory.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_map_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F : D ⥤ₗ E} {G : D ⥤ₗ E} (η : F ⟶ G) (H : C ⥤ₗ D) (c : C) : (((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₗ E) (X : C ⥤ₗ D) (X : C) : (((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).obj X✝).obj.obj X = F.obj.obj (X✝.obj.obj X)

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₗ E) : ∀ {X Y : C ⥤ₗ D} (f : X ⟶ Y) (X_1 : C), (((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).map f).app X_1 = F.obj.map (f.app X_1)

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₗ E) (X : C ⥤ₗ D) : ∀ {X_1 Y : C} (f : X_1 ⟶ Y), (((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).obj X).obj.map f = F.obj.map (X.obj.map f)

def CategoryTheory.RightExactFunctor.whiskeringLeft (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (C ⥤ᵣ D) (CategoryTheory.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_map_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F : C ⥤ᵣ D} {G : C ⥤ᵣ D} (η : F ⟶ G) (H : D ⥤ᵣ E) (c : C) : (((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ᵣ D) : ∀ {X Y : D ⥤ᵣ E} (f : X ⟶ Y) (X_1 : C), (((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).obj F).map f).app X_1 = f.app (F.obj.obj X_1)

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ᵣ D) (X : D ⥤ᵣ E) (X : C) : (((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).obj F).obj X✝).obj.obj X = X✝.obj.obj (F.obj.obj X)

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ᵣ D) (X : D ⥤ᵣ E) : ∀ {X_1 Y : C} (f : X_1 ⟶ Y), (((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).obj F).obj X).obj.map f = X.obj.map (F.obj.map f)

def CategoryTheory.RightExactFunctor.whiskeringRight (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (D ⥤ᵣ E) (CategoryTheory.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_obj_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ᵣ E) (X : C ⥤ᵣ D) (X : C) : (((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).obj X✝).obj.obj X = F.obj.obj (X✝.obj.obj X)

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F : D ⥤ᵣ E} {G : D ⥤ᵣ E} (η : F ⟶ G) (H : C ⥤ᵣ D) (c : C) : (((CategoryTheory.RightExactFunctor.whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ᵣ E) (X : C ⥤ᵣ D) : ∀ {X_1 Y : C} (f : X_1 ⟶ Y), (((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).obj X).obj.map f = F.obj.map (X.obj.map f)

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_obj_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ᵣ E) : ∀ {X Y : C ⥤ᵣ D} (f : X ⟶ Y) (X_1 : C), (((CategoryTheory.RightExactFunctor.whiskeringRight C D E).obj F).map f).app X_1 = F.obj.map (f.app X_1)

def CategoryTheory.ExactFunctor.whiskeringLeft (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (C ⥤ₑ D) (CategoryTheory.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_obj_obj_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ₑ D) (X : D ⥤ₑ E) : ∀ {X_1 Y : C} (f : X_1 ⟶ Y), (((CategoryTheory.ExactFunctor.whiskeringLeft C D E).obj F).obj X).obj.map f = X.obj.map (F.obj.map f)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ₑ D) (X : D ⥤ₑ E) (X : C) : (((CategoryTheory.ExactFunctor.whiskeringLeft C D E).obj F).obj X✝).obj.obj X = X✝.obj.obj (F.obj.obj X)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_obj_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ₑ D) : ∀ {X Y : D ⥤ₑ E} (f : X ⟶ Y) (X_1 : C), (((CategoryTheory.ExactFunctor.whiskeringLeft C D E).obj F).map f).app X_1 = f.app (F.obj.obj X_1)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_map_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F : C ⥤ₑ D} {G : C ⥤ₑ D} (η : F ⟶ G) (H : D ⥤ₑ E) (c : C) : (((CategoryTheory.ExactFunctor.whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

def CategoryTheory.ExactFunctor.whiskeringRight (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (D ⥤ₑ E) (CategoryTheory.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_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₑ E) (X : C ⥤ₑ D) (X : C) : (((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).obj X✝).obj.obj X = F.obj.obj (X✝.obj.obj X)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] {F : D ⥤ₑ E} {G : D ⥤ₑ E} (η : F ⟶ G) (H : C ⥤ₑ D) (c : C) : (((CategoryTheory.ExactFunctor.whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_obj_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₑ E) : ∀ {X Y : C ⥤ₑ D} (f : X ⟶ Y) (X_1 : C), (((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).map f).app X_1 = F.obj.map (f.app X_1)

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_obj_obj_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₑ E) (X : C ⥤ₑ D) : ∀ {X_1 Y : C} (f : X_1 ⟶ Y), (((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).obj X).obj.map f = F.obj.map (X.obj.map f)