def
CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
(F : Functor C A)
(G : Functor B D)
:
The functor that, on objects H : A ⥤ B acts by
composing left and right with functors F ⋙ H ⋙ G
F
A <--------- C
| .
| |
| .
H | | whiskeringLeftObjWhiskeringRightObj.obj H
| .
V V
B ----------> D
G
Equations
- F.whiskeringLeftObjWhiskeringRightObj G = ((CategoryTheory.Functor.whiskeringLeft C A B).obj F).comp ((CategoryTheory.Functor.whiskeringRight C B D).obj G)
Instances For
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj_obj
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
[Category.{u_7, u_3} C]
[Category.{u_8, u_4} D]
(F : Functor C A)
(G : Functor B D)
(S : Functor A B)
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj_id_id
{A : Type u_1}
{B : Type u_2}
[Category.{u_5, u_1} A]
[Category.{u_6, u_2} B]
:
@[simp]
theorem
CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj_comp_comp
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[Category.{u_11, u_1} A]
[Category.{u_12, u_2} B]
[Category.{u_9, u_3} C]
[Category.{u_10, u_4} D]
(F : Functor C A)
(G : Functor B D)
{C' : Type u_5}
{D' : Type u_6}
[Category.{u_7, u_5} C']
[Category.{u_8, u_6} D']
(F' : Functor C' C)
(G' : Functor D D')
:
(F'.comp F).whiskeringLeftObjWhiskeringRightObj (G.comp G') = (F.whiskeringLeftObjWhiskeringRightObj G).comp (F'.whiskeringLeftObjWhiskeringRightObj G')