Whiskering #
Given a functor F : C ⥤ D and functors G H : D ⥤ E and a natural transformation α : G ⟶ H,
we can construct a new natural transformation F ⋙ G ⟶ F ⋙ H,
called whiskerLeft F α. This is the same as the horizontal composition of 𝟙 F with α.
This operation is functorial in F, and we package this as whiskeringLeft. Here
(whiskeringLeft.obj F).obj G is F ⋙ G, and
(whiskeringLeft.obj F).map α is whiskerLeft F α.
(That is, we might have alternatively named this as the "left composition functor".)
We also provide analogues for composition on the right, and for these operations on isomorphisms.
We show the associator and unitor natural isomorphisms satisfy the triangle and pentagon identities.
@[implicit_reducible]
def
CategoryTheory.Functor.whiskerLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ⟶ H)
:
If α : G ⟶ H then whiskerLeft F α : F ⋙ G ⟶ F ⋙ H has components α.app (F.obj X).
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskerLeft_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ⟶ H)
(X : C)
:
@[simp]
theorem
CategoryTheory.Functor.id_hcomp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ⟶ H)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ⟶ H)
(F : Functor D E)
:
If α : G ⟶ H then whiskerRight α F : G ⋙ F ⟶ H ⋙ F has components F.map (α.app X).
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskerRight_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ⟶ H)
(F : Functor D E)
(X : C)
:
@[simp]
theorem
CategoryTheory.Functor.hcomp_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ⟶ H)
(F : Functor D E)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
(E : Type u₃)
[Category.{v₃, u₃} E]
:
Left-composition gives a functor (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)).
(whiskeringLeft.obj F).obj G is F ⋙ G, and
(whiskeringLeft.obj F).map α is whiskerLeft F α.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.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 : Functor C D)
{X✝ Y✝ : Functor D E}
(α : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.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]
{X✝ Y✝ : Functor C D}
(τ : X✝ ⟶ Y✝)
(H : Functor D E)
(c : C)
:
@[simp]
theorem
CategoryTheory.Functor.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 : Functor C D)
(G : Functor D E)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringRight
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
(E : Type u₃)
[Category.{v₃, u₃} E]
:
Right-composition gives a functor (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)).
(whiskeringRight.obj H).obj F is F ⋙ H, and
(whiskeringRight.obj H).map α is whiskerRight α H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.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]
{X✝ Y✝ : Functor D E}
(τ : X✝ ⟶ Y✝)
(F : Functor C D)
(c : C)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringRight_obj_map
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
(E : Type u₃)
[Category.{v₃, u₃} E]
(H : Functor D E)
{X✝ Y✝ : Functor C D}
(α : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringRight_obj_obj
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
(E : Type u₃)
[Category.{v₃, u₃} E]
(H : Functor D E)
(F : Functor C D)
:
instance
CategoryTheory.Functor.faithful_whiskeringRight_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F : Functor D E}
[F.Faithful]
:
((whiskeringRight C D E).obj F).Faithful
def
CategoryTheory.Functor.FullyFaithful.whiskeringRight
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F : Functor D E}
(hF : F.FullyFaithful)
(C : Type u_1)
[Category.{v_1, u_1} C]
:
((Functor.whiskeringRight C D E).obj F).FullyFaithful
If F : D ⥤ E is fully faithful, then so is
(whiskeringRight C D E).obj F : (C ⥤ D) ⥤ C ⥤ E.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.whiskeringRight_preimage_app
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F : Functor D E}
(hF : F.FullyFaithful)
(C : Type u_1)
[Category.{v_1, u_1} C]
{X✝ Y✝ : Functor C D}
(f : ((Functor.whiskeringRight C D E).obj F).obj X✝ ⟶ ((Functor.whiskeringRight C D E).obj F).obj Y✝)
(X : C)
:
theorem
CategoryTheory.Functor.whiskeringLeft_obj_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
:
def
CategoryTheory.Functor.whiskeringLeftObjIdIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
:
The isomorphism between left-whiskering on the identity functor and the identity of the functor between the resulting functor categories.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeftObjIdIso_hom_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
(X : Functor C E)
(X✝ : C)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeftObjIdIso_inv_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
(X : Functor C E)
(X✝ : C)
:
theorem
CategoryTheory.Functor.whiskeringLeft_obj_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
:
(whiskeringLeft C D' E).obj (F.comp G) = ((whiskeringLeft D D' E).obj G).comp ((whiskeringLeft C D E).obj F)
def
CategoryTheory.Functor.whiskeringLeftObjCompIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
:
(whiskeringLeft C D' E).obj (F.comp G) ≅ ((whiskeringLeft D D' E).obj G).comp ((whiskeringLeft C D E).obj F)
The isomorphism between left-whiskering on the composition of functors and the composition of two left-whiskering applications.
Equations
- F.whiskeringLeftObjCompIso G = CategoryTheory.Iso.refl ((CategoryTheory.Functor.whiskeringLeft C D' E).obj (F.comp G))
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeftObjCompIso_inv_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
(X : Functor D' E)
(X✝ : C)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeftObjCompIso_hom_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
(X : Functor D' E)
(X✝ : C)
:
theorem
CategoryTheory.Functor.whiskeringRight_obj_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
:
def
CategoryTheory.Functor.whiskeringRightObjIdIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
:
The isomorphism between right-whiskering on the identity functor and the identity of the functor between the resulting functor categories.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringRightObjIdIso_inv_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
(X : Functor E C)
(X✝ : E)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringRightObjIdIso_hom_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
(X : Functor E C)
(X✝ : E)
:
theorem
CategoryTheory.Functor.whiskeringRight_obj_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
:
((whiskeringRight E C D).obj F).comp ((whiskeringRight E D D').obj G) = (whiskeringRight E C D').obj (F.comp G)
def
CategoryTheory.Functor.whiskeringRightObjCompIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
:
((whiskeringRight E C D).obj F).comp ((whiskeringRight E D D').obj G) ≅ (whiskeringRight E C D').obj (F.comp G)
The isomorphism between right-whiskering on the composition of functors and the composition of two right-whiskering applications.
Equations
- F.whiskeringRightObjCompIso G = CategoryTheory.Iso.refl (((CategoryTheory.Functor.whiskeringRight E C D).obj F).comp ((CategoryTheory.Functor.whiskeringRight E D D').obj G))
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringRightObjCompIso_hom_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
(X : Functor E C)
(X✝ : E)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringRightObjCompIso_inv_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor D D')
(X : Functor E C)
(X✝ : E)
:
instance
CategoryTheory.Functor.full_whiskeringRight_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F : Functor D E}
[F.Faithful]
[F.Full]
:
((whiskeringRight C D E).obj F).Full
@[simp]
theorem
CategoryTheory.Functor.whiskerLeft_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
:
@[simp]
theorem
CategoryTheory.Functor.whiskerLeft_id'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G : Functor D E}
:
@[simp]
theorem
CategoryTheory.Functor.whiskerRight_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor C D}
(F : Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.whiskerRight_id'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor C D}
(F : Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.whiskerLeft_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H K : Functor D E}
(α : G ⟶ H)
(β : H ⟶ K)
:
theorem
CategoryTheory.Functor.whiskerLeft_comp_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H K : Functor D E}
(α : G ⟶ H)
(β : H ⟶ K)
{Z : Functor C E}
(h : F.comp K ⟶ Z)
:
CategoryStruct.comp (F.whiskerLeft (CategoryStruct.comp α β)) h = CategoryStruct.comp (F.whiskerLeft α) (CategoryStruct.comp (F.whiskerLeft β) h)
@[simp]
theorem
CategoryTheory.Functor.whiskerRight_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H K : Functor C D}
(α : G ⟶ H)
(β : H ⟶ K)
(F : Functor D E)
:
whiskerRight (CategoryStruct.comp α β) F = CategoryStruct.comp (whiskerRight α F) (whiskerRight β F)
theorem
CategoryTheory.Functor.whiskerRight_comp_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H K : Functor C D}
(α : G ⟶ H)
(β : H ⟶ K)
(F : Functor D E)
{Z : Functor C E}
(h : K.comp F ⟶ Z)
:
CategoryStruct.comp (whiskerRight (CategoryStruct.comp α β) F) h = CategoryStruct.comp (whiskerRight α F) (CategoryStruct.comp (whiskerRight β F) h)
theorem
CategoryTheory.Functor.whiskerLeft_comp_whiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F G : Functor C D}
{H K : Functor D E}
(α : F ⟶ G)
(β : H ⟶ K)
:
CategoryStruct.comp (F.whiskerLeft β) (whiskerRight α K) = CategoryStruct.comp (whiskerRight α H) (G.whiskerLeft β)
theorem
CategoryTheory.Functor.whiskerLeft_comp_whiskerRight_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F G : Functor C D}
{H K : Functor D E}
(α : F ⟶ G)
(β : H ⟶ K)
{Z : Functor C E}
(h : G.comp K ⟶ Z)
:
CategoryStruct.comp (F.whiskerLeft β) (CategoryStruct.comp (whiskerRight α K) h) = CategoryStruct.comp (whiskerRight α H) (CategoryStruct.comp (G.whiskerLeft β) h)
theorem
CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F G : Functor C D}
{H K : Functor D E}
(α : F ⟶ G)
(β : H ⟶ K)
:
theorem
CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerRight_comp_whiskerLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F G : Functor C D}
{H K : Functor D E}
(α : G ⟶ F)
(β : K ⟶ H)
:
def
CategoryTheory.Functor.isoWhiskerLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ≅ H)
:
If α : G ≅ H is a natural isomorphism then
isoWhiskerLeft F α : (F ⋙ G) ≅ (F ⋙ H) has components α.app (F.obj X).
Equations
- F.isoWhiskerLeft α = ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).mapIso α
Instances For
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerLeft_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ≅ H)
:
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerLeft_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ≅ H)
:
theorem
CategoryTheory.Functor.isoWhiskerLeft_symm
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ≅ H)
:
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerLeft_refl
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
:
def
CategoryTheory.Functor.isoWhiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ≅ H)
(F : Functor D E)
:
If α : G ≅ H then
isoWhiskerRight α F : (G ⋙ F) ≅ (H ⋙ F) has components F.map_iso (α.app X).
Equations
- CategoryTheory.Functor.isoWhiskerRight α F = ((CategoryTheory.Functor.whiskeringRight C D E).obj F).mapIso α
Instances For
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerRight_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ≅ H)
(F : Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerRight_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ≅ H)
(F : Functor D E)
:
theorem
CategoryTheory.Functor.isoWhiskerRight_symm
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ≅ H)
(F : Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerRight_refl
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
:
instance
CategoryTheory.Functor.isIso_whiskerLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ⟶ H)
[IsIso α]
:
IsIso (F.whiskerLeft α)
instance
CategoryTheory.Functor.isIso_whiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ⟶ H)
(F : Functor D E)
[IsIso α]
:
IsIso (whiskerRight α F)
@[simp]
theorem
CategoryTheory.Functor.inv_whiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H : Functor C D}
(α : G ⟶ H)
(F : Functor D E)
[IsIso α]
:
@[simp]
theorem
CategoryTheory.Functor.inv_whiskerLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H : Functor D E}
(α : G ⟶ H)
[IsIso α]
:
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerLeft_trans
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H K : Functor D E}
(α : G ≅ H)
(β : H ≅ K)
:
theorem
CategoryTheory.Functor.isoWhiskerLeft_trans_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
{G H K : Functor D E}
(α : G ≅ H)
(β : H ≅ K)
{Z : Functor C E}
(h : F.comp K ≅ Z)
:
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerRight_trans
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H K : Functor C D}
(α : G ≅ H)
(β : H ≅ K)
(F : Functor D E)
:
theorem
CategoryTheory.Functor.isoWhiskerRight_trans_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G H K : Functor C D}
(α : G ≅ H)
(β : H ≅ K)
(F : Functor D E)
{Z : Functor C E}
(h : K.comp F ≅ Z)
:
theorem
CategoryTheory.Functor.isoWhiskerLeft_trans_isoWhiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F G : Functor C D}
{H K : Functor D E}
(α : F ≅ G)
(β : H ≅ K)
:
theorem
CategoryTheory.Functor.isoWhiskerLeft_trans_isoWhiskerRight_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{F G : Functor C D}
{H K : Functor D E}
(α : F ≅ G)
(β : H ≅ K)
{Z : Functor C E}
(h : G.comp K ≅ Z)
:
@[simp]
theorem
CategoryTheory.Functor.whiskerLeft_twice
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
{H K : Functor D E}
(α : H ⟶ K)
:
F.whiskerLeft (G.whiskerLeft α) = CategoryStruct.comp (F.associator G H).inv (CategoryStruct.comp ((F.comp G).whiskerLeft α) (F.associator G K).hom)
@[simp]
theorem
CategoryTheory.Functor.whiskerRight_twice
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
{H K : Functor B C}
(F : Functor C D)
(G : Functor D E)
(α : H ⟶ K)
:
whiskerRight (whiskerRight α F) G = CategoryStruct.comp (H.associator F G).hom (CategoryStruct.comp (whiskerRight α (F.comp G)) (K.associator F G).inv)
theorem
CategoryTheory.Functor.whiskerRight_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
{G H : Functor C D}
(α : G ⟶ H)
(K : Functor D E)
:
whiskerRight (F.whiskerLeft α) K = CategoryStruct.comp (F.associator G K).hom
(CategoryStruct.comp (F.whiskerLeft (whiskerRight α K)) (F.associator H K).inv)
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerLeft_twice
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
(G : Functor C D)
{H K : Functor D E}
(α : H ≅ K)
:
F.isoWhiskerLeft (G.isoWhiskerLeft α) = (F.associator G H).symm ≪≫ (F.comp G).isoWhiskerLeft α ≪≫ F.associator G K
@[simp]
theorem
CategoryTheory.Functor.isoWhiskerRight_twice
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
{H K : Functor B C}
(F : Functor C D)
(G : Functor D E)
(α : H ≅ K)
:
isoWhiskerRight (isoWhiskerRight α F) G = H.associator F G ≪≫ isoWhiskerRight α (F.comp G) ≪≫ (K.associator F G).symm
theorem
CategoryTheory.Functor.isoWhiskerRight_twice_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
{H K : Functor B C}
(F : Functor C D)
(G : Functor D E)
(α : H ≅ K)
{Z : Functor B E}
(h : (K.comp F).comp G ≅ Z)
:
isoWhiskerRight (isoWhiskerRight α F) G ≪≫ h = H.associator F G ≪≫ isoWhiskerRight α (F.comp G) ≪≫ (K.associator F G).symm ≪≫ h
theorem
CategoryTheory.Functor.isoWhiskerRight_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
{G H : Functor C D}
(α : G ≅ H)
(K : Functor D E)
:
isoWhiskerRight (F.isoWhiskerLeft α) K = F.associator G K ≪≫ F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ (F.associator H K).symm
theorem
CategoryTheory.Functor.isoWhiskerRight_left_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
{G H : Functor C D}
(α : G ≅ H)
(K : Functor D E)
{Z : Functor B E}
(h : (F.comp H).comp K ≅ Z)
:
isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ h = F.associator G K ≪≫ F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ (F.associator H K).symm ≪≫ h
theorem
CategoryTheory.Functor.isoWhiskerLeft_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
{G H : Functor C D}
(α : G ≅ H)
(K : Functor D E)
:
F.isoWhiskerLeft (isoWhiskerRight α K) = (F.associator G K).symm ≪≫ isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K
theorem
CategoryTheory.Functor.isoWhiskerLeft_right_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(F : Functor B C)
{G H : Functor C D}
(α : G ≅ H)
(K : Functor D E)
{Z : Functor B E}
(h : F.comp (H.comp K) ≅ Z)
:
F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ h = (F.associator G K).symm ≪≫ isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K ≪≫ h
theorem
CategoryTheory.Functor.triangleIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{C : Type u₃}
[Category.{v₃, u₃} C]
(F : Functor A B)
(G : Functor B C)
:
theorem
CategoryTheory.Functor.triangleIso_assoc
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{C : Type u₃}
[Category.{v₃, u₃} C]
(F : Functor A B)
(G : Functor B C)
{Z : Functor A C}
(h : F.comp G ≅ Z)
:
F.associator (Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor ≪≫ h = isoWhiskerRight F.rightUnitor G ≪≫ h
theorem
CategoryTheory.Functor.pentagonIso
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{C : Type u₃}
[Category.{v₃, u₃} C]
{D : Type u₄}
[Category.{v₄, u₄} D]
{E : Type u₅}
[Category.{v₅, u₅} E]
(F : Functor A B)
(G : Functor B C)
(H : Functor C D)
(K : Functor D E)
:
isoWhiskerRight (F.associator G H) K ≪≫ F.associator (G.comp H) K ≪≫ F.isoWhiskerLeft (G.associator H K) = (F.comp G).associator H K ≪≫ F.associator G (H.comp K)
theorem
CategoryTheory.Functor.pentagonIso_assoc
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{C : Type u₃}
[Category.{v₃, u₃} C]
{D : Type u₄}
[Category.{v₄, u₄} D]
{E : Type u₅}
[Category.{v₅, u₅} E]
(F : Functor A B)
(G : Functor B C)
(H : Functor C D)
(K : Functor D E)
{Z : Functor A E}
(h : F.comp (G.comp (H.comp K)) ≅ Z)
:
isoWhiskerRight (F.associator G H) K ≪≫ F.associator (G.comp H) K ≪≫ F.isoWhiskerLeft (G.associator H K) ≪≫ h = (F.comp G).associator H K ≪≫ F.associator G (H.comp K) ≪≫ h
theorem
CategoryTheory.Functor.triangle
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{C : Type u₃}
[Category.{v₃, u₃} C]
(F : Functor A B)
(G : Functor B C)
:
CategoryStruct.comp (F.associator (Functor.id B) G).hom (F.whiskerLeft G.leftUnitor.hom) = whiskerRight F.rightUnitor.hom G
theorem
CategoryTheory.Functor.pentagon
{A : Type u₁}
[Category.{v₁, u₁} A]
{B : Type u₂}
[Category.{v₂, u₂} B]
{C : Type u₃}
[Category.{v₃, u₃} C]
{D : Type u₄}
[Category.{v₄, u₄} D]
{E : Type u₅}
[Category.{v₅, u₅} E]
(F : Functor A B)
(G : Functor B C)
(H : Functor C D)
(K : Functor D E)
:
CategoryStruct.comp (whiskerRight (F.associator G H).hom K)
(CategoryStruct.comp (F.associator (G.comp H) K).hom (F.whiskerLeft (G.associator H K).hom)) = CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₂
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
(E : Type u_9)
[Category.{v_9, u_9} E]
:
The obvious functor (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₂_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{X✝ Y✝ : Functor C₂ D₂}
(φ : X✝ ⟶ Y✝)
(X : Functor D₁ (Functor D₂ E))
(X✝¹ : C₁)
(c : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₂_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
(E : Type u_9)
[Category.{v_9, u_9} E]
{X✝ Y✝ : Functor C₁ D₁}
(ψ : X✝ ⟶ Y✝)
(F₂ : Functor C₂ D₂)
(X : Functor D₁ (Functor D₂ E))
(c : C₁)
(X✝¹ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(X : Functor D₁ (Functor D₂ E))
(X✝ : C₁)
(X✝¹ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(X : Functor D₁ (Functor D₂ E))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{X✝ Y✝ : Functor D₁ (Functor D₂ E)}
(f : X✝ ⟶ Y✝)
(X : C₁)
(X✝¹ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(X : Functor D₁ (Functor D₂ E))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
:
Auxiliary definition for whiskeringLeft₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X✝ : C₁)
(X✝¹ : C₂)
{X✝² Y✝ : C₃}
(f : X✝² ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
{X✝ Y✝ : Functor D₁ (Functor D₂ (Functor D₃ E))}
(f : X✝ ⟶ Y✝)
(X : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₃ObjObjMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{F₃ F₃' : Functor C₃ D₃}
(τ₃ : F₃ ⟶ F₃')
:
Auxiliary definition for whiskeringLeft₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObjMap_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{F₃ F₃' : Functor C₃ D₃}
(τ₃ : F₃ ⟶ F₃')
(F : Functor D₁ (Functor D₂ (Functor D₃ E)))
:
(whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃).app F = F₁.whiskerLeft (F.whiskerLeft (((whiskeringLeft₂ E).obj F₂).map τ₃))
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₃ObjObj
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
:
Auxiliary definition for whiskeringLeft₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjObj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{X✝ Y✝ : Functor C₃ D₃}
(τ₃ : X✝ ⟶ Y✝)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₃ObjMap
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{F₂ F₂' : Functor C₂ D₂}
(τ₂ : F₂ ⟶ F₂')
:
Auxiliary definition for whiskeringLeft₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃ObjMap_app
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{F₂ F₂' : Functor C₂ D₂}
(τ₂ : F₂ ⟶ F₂')
(F₃ : Functor C₃ D₃)
:
(whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂).app F₃ = whiskerRight
((whiskeringRight D₁ (Functor D₂ (Functor D₃ E)) (Functor C₂ (Functor C₃ E))).map
(((whiskeringLeft₂ E).map τ₂).app F₃))
((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ E))).obj F₁)
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₃Obj
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
:
Auxiliary definition for whiskeringLeft₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃Obj_obj
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃Obj_map
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{X✝ Y✝ : Functor C₂ D₂}
(τ₂ : X✝ ⟶ Y✝)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₃Map
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
{F₁ F₁' : Functor C₁ D₁}
(τ₁ : F₁ ⟶ F₁')
:
Auxiliary definition for whiskeringLeft₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃Map_app_app
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
{F₁ F₁' : Functor C₁ D₁}
(τ₁ : F₁ ⟶ F₁')
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
:
((whiskeringLeft₃Map C₂ C₃ D₂ D₃ E τ₁).app F₂).app F₃ = ((whiskeringRight D₁ (Functor D₂ (Functor D₃ E)) (Functor C₂ (Functor C₃ E))).obj
(((whiskeringLeft₂ E).obj F₂).obj F₃)).whiskerLeft
((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ E))).map τ₁)
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₃
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
:
The obvious functor
(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_obj_map_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{X✝ Y✝ : Functor C₂ D₂}
(τ₂ : X✝ ⟶ Y✝)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X✝¹ : C₁)
(c : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_map_app_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
{X✝ Y✝ : Functor C₁ D₁}
(τ₁ : X✝ ⟶ Y✝)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(c : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X✝ : C₁)
(X✝¹ : C₂)
{X✝² Y✝ : C₃}
(f : X✝² ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{X✝ Y✝ : Functor C₃ D₃}
(τ₃ : X✝ ⟶ Y✝)
(F : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X : C₁)
(X✝¹ : C₂)
(c : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
{X✝ Y✝ : Functor D₁ (Functor D₂ (Functor D₃ E))}
(f : X✝ ⟶ Y✝)
(X : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(X : Functor D₁ (Functor D₂ (Functor D₃ E)))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjObj_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjObj_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
{X✝³ Y✝ : C₄}
(f : X✝³ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjObj_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
{X✝ Y✝ : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))}
(f : X✝ ⟶ Y✝)
(X : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjObj_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
{X✝² Y✝ : C₃}
(f : X✝² ⟶ Y✝)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjObj_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjObj_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
{F₄ F₄' : Functor C₄ D₄}
(τ₄ : F₄ ⟶ F₄')
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObjMap_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
{F₄ F₄' : Functor C₄ D₄}
(τ₄ : F₄ ⟶ F₄')
(F : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
:
(whiskeringLeft₄ObjObjObjMap E F₁ F₂ F₃ τ₄).app F = F₁.whiskerLeft (F.whiskerLeft ((((whiskeringLeft₃ E).obj F₂).obj F₃).map τ₄))
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄ObjObjObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjObj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
{X✝ Y✝ : Functor C₄ D₄}
(τ₄ : X✝ ⟶ Y✝)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄ObjObjMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{F₃ F₃' : Functor C₃ D₃}
(τ₃ : F₃ ⟶ F₃')
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObjMap_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{F₃ F₃' : Functor C₃ D₃}
(τ₃ : F₃ ⟶ F₃')
(F₄ : Functor C₄ D₄)
:
(whiskeringLeft₄ObjObjMap C₄ D₄ E F₁ F₂ τ₃).app F₄ = whiskerRight
((whiskeringRight D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))) (Functor C₂ (Functor C₃ (Functor C₄ E)))).map
((((whiskeringLeft₃ E).obj F₂).map τ₃).app F₄))
((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))).obj F₁)
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄ObjObj
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjObj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{X✝ Y✝ : Functor C₃ D₃}
(τ₃ : X✝ ⟶ Y✝)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄ObjMap
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{F₂ F₂' : Functor C₂ D₂}
(τ₂ : F₂ ⟶ F₂')
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄ObjMap_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
{D₂ : Type u_6}
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{F₂ F₂' : Functor C₂ D₂}
(τ₂ : F₂ ⟶ F₂')
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
:
((whiskeringLeft₄ObjMap C₃ C₄ D₃ D₄ E F₁ τ₂).app F₃).app F₄ = whiskerRight
((whiskeringRight D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))) (Functor C₂ (Functor C₃ (Functor C₄ E)))).map
((((whiskeringLeft₃ E).map τ₂).app F₃).app F₄))
((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))).obj F₁)
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄Obj
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄Obj_map
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{X✝ Y✝ : Functor C₂ D₂}
(τ₂ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄Obj_obj
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
:
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄Map
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
{F₁ F₁' : Functor C₁ D₁}
(τ₁ : F₁ ⟶ F₁')
:
Auxiliary definition for whiskeringLeft₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄Map_app_app_app
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
(C₄ : Type u_4)
{D₁ : Type u_5}
(D₂ : Type u_6)
(D₃ : Type u_7)
(D₄ : Type u_8)
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
{F₁ F₁' : Functor C₁ D₁}
(τ₁ : F₁ ⟶ F₁')
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
:
(((whiskeringLeft₄Map C₂ C₃ C₄ D₂ D₃ D₄ E τ₁).app F₂).app F₃).app F₄ = ((whiskeringRight D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))) (Functor C₂ (Functor C₃ (Functor C₄ E)))).obj
((((whiskeringLeft₃ E).obj F₂).obj F₃).obj F₄)).whiskerLeft
((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))).map τ₁)
@[implicit_reducible]
def
CategoryTheory.Functor.whiskeringLeft₄
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
:
The obvious functor
(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (C₄ ⥤ D₄) ⥤
(D₁ ⥤ D₂ ⥤ D₃ ⥤ D₄ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_obj_obj_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_obj_obj_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
{X✝³ Y✝ : C₄}
(f : X✝³ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_map_app_app_app_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
{X✝ Y✝ : Functor C₁ D₁}
(τ₁ : X✝ ⟶ Y✝)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(c : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_obj_map_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
{X✝ Y✝ : Functor C₄ D₄}
(τ₄ : X✝ ⟶ Y✝)
(F : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
(c : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_obj_obj_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
{X✝² Y✝ : C₃}
(f : X✝² ⟶ Y✝)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_obj_obj_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_map_app_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{X✝ Y✝ : Functor C₃ D₃}
(τ₃ : X✝ ⟶ Y✝)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝¹ : C₁)
(X✝² : C₂)
(c : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_map_app_app_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
{X✝ Y✝ : Functor C₂ D₂}
(τ₂ : X✝ ⟶ Y✝)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝¹ : C₁)
(c : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_obj_obj_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
(X : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeft₄_obj_obj_obj_obj_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
{D₄ : Type u_8}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
[Category.{v_5, u_5} D₁]
[Category.{v_6, u_6} D₂]
[Category.{v_7, u_7} D₃]
[Category.{v_8, u_8} D₄]
(E : Type u_9)
[Category.{v_9, u_9} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
(F₄ : Functor C₄ D₄)
{X✝ Y✝ : Functor D₁ (Functor D₂ (Functor D₃ (Functor D₄ E)))}
(f : X✝ ⟶ Y✝)
(X : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[implicit_reducible]
def
CategoryTheory.Functor.postcompose₂
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
:
The "postcomposition" with a functor E ⥤ E' gives a functor
(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ E))
(X✝ : C₁)
(X✝¹ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ E))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
{X✝ Y✝ : Functor E E'}
(f : X✝ ⟶ Y✝)
(F : Functor C₁ (Functor C₂ E))
(c : C₁)
(c✝ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ E))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
{X✝ Y✝ : Functor C₁ (Functor C₂ E)}
(α : X✝ ⟶ Y✝)
(X✝¹ : C₁)
(X✝² : C₂)
:
@[implicit_reducible]
def
CategoryTheory.Functor.postcompose₃
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
:
The "postcomposition" with a functor E ⥤ E' gives a functor
(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ E)))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ E)))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ E)))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ E)))
(X✝ : C₁)
(X✝¹ : C₂)
{X✝² Y✝ : C₃}
(f : X✝² ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
{X✝ Y✝ : Functor C₁ (Functor C₂ (Functor C₃ E))}
(α : X✝ ⟶ Y✝)
(X✝¹ : C₁)
(X✝² : C₂)
(X✝³ : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
{X✝ Y✝ : Functor E E'}
(f : X✝ ⟶ Y✝)
(F : Functor C₁ (Functor C₂ (Functor C₃ E)))
(c : C₁)
(c✝ : C₂)
(c✝¹ : C₃)
:
@[implicit_reducible]
def
CategoryTheory.Functor.postcompose₄
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
:
The "postcomposition" with a functor E ⥤ E' gives a functor
(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ ⥤ E'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.postcompose₄_obj_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
{X✝³ Y✝ : C₄}
(f : X✝³ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₄_obj_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
{X✝² Y✝ : C₃}
(f : X✝² ⟶ Y✝)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₄_obj_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))
(X✝ : C₁)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₄_map_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
{X✝ Y✝ : Functor E E'}
(f : X✝ ⟶ Y✝)
(F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))
(c : C₁)
(c✝ : C₂)
(c✝¹ : C₃)
(c✝² : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₄_obj_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
{X✝ Y✝ : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E)))}
(α : X✝ ⟶ Y✝)
(X✝¹ : C₁)
(X✝² : C₂)
(X✝³ : C₃)
(X✝⁴ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₄_obj_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
(X✝² : C₃)
(X✝³ : C₄)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₄_obj_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{C₄ : Type u_4}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} C₃]
[Category.{v_4, u_4} C₄]
{E : Type u_9}
[Category.{v_9, u_9} E]
{E' : Type u_10}
[Category.{v_10, u_10} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ (Functor C₄ E))))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
(X✝² : C₃)
(X✝³ : C₄)
: