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 associators an unitor natural isomorphisms satisfy the triangle and pentagon identities.
def
CategoryTheory.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).
Equations
- CategoryTheory.whiskerLeft F α = { app := fun (X : C) => α.app (F.obj X), naturality := ⋯ }
@[simp]
theorem
CategoryTheory.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.NatTrans.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)
:
def
CategoryTheory.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) ⟶ (G ⋙ F) has components F.map (α.app X).
Equations
- CategoryTheory.whiskerRight α F = { app := fun (X : C) => F.map (α.app X), naturality := ⋯ }
Instances For
- CategoryTheory.Adjunction.whiskerRight_counit_iso_of_L_fully_faithful
- CategoryTheory.Adjunction.whiskerRight_unit_iso_of_R_fully_faithful
- CategoryTheory.Presheaf.instIsLocallySurjectiveHomObjForgetTypeWhiskerRightOpposite
- CategoryTheory.Presheaf.isLocallyInjective_forget
- CategoryTheory.instEpiFunctorWhiskerRightOfPreservesEpimorphisms
- CategoryTheory.instMonoFunctorWhiskerRightOfPreservesMonomorphisms
- CategoryTheory.isIso_whiskerRight
@[simp]
theorem
CategoryTheory.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.NatTrans.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)
:
def
CategoryTheory.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.
@[simp]
theorem
CategoryTheory.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.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)
:
@[simp]
theorem
CategoryTheory.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)
:
def
CategoryTheory.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.
@[simp]
theorem
CategoryTheory.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.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.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.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.{u_2, u_1} C]
:
((CategoryTheory.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.
@[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.{u_2, u_1} C]
{X✝ Y✝ : Functor C D}
(f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y✝)
(X : C)
:
theorem
CategoryTheory.whiskeringLeft_obj_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
:
def
CategoryTheory.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.
theorem
CategoryTheory.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.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
- CategoryTheory.whiskeringLeftObjCompIso F G = CategoryTheory.Iso.refl ((CategoryTheory.whiskeringLeft C D' E).obj (F.comp G))
theorem
CategoryTheory.whiskeringRight_obj_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
:
def
CategoryTheory.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.
@[deprecated CategoryTheory.whiskeringRightObjIdIso (since := "2025-04-04")]
def
CategoryTheory.wiskeringRightObjIdIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{E : Type u₃}
[Category.{v₃, u₃} E]
:
Alias of CategoryTheory.whiskeringRightObjIdIso.
The isomorphism between right-whiskering on the identity functor and the identity of the functor between the resulting functor categories.
theorem
CategoryTheory.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.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
- CategoryTheory.whiskeringRightObjCompIso F G = CategoryTheory.Iso.refl (((CategoryTheory.whiskeringRight E C D).obj F).comp ((CategoryTheory.whiskeringRight E D D').obj G))
instance
CategoryTheory.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.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.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.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.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.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.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 (whiskerLeft F (CategoryStruct.comp α β)) h = CategoryStruct.comp (whiskerLeft F α) (CategoryStruct.comp (whiskerLeft F β) h)
@[simp]
theorem
CategoryTheory.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.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.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 (whiskerLeft F β) (whiskerRight α K) = CategoryStruct.comp (whiskerRight α H) (whiskerLeft G β)
theorem
CategoryTheory.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 (whiskerLeft F β) (CategoryStruct.comp (whiskerRight α K) h) = CategoryStruct.comp (whiskerRight α H) (CategoryStruct.comp (whiskerLeft G β) h)
theorem
CategoryTheory.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)
:
def
CategoryTheory.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
- CategoryTheory.isoWhiskerLeft F α = ((CategoryTheory.whiskeringLeft C D E).obj F).mapIso α
@[simp]
theorem
CategoryTheory.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.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.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.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.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.isoWhiskerRight α F = ((CategoryTheory.whiskeringRight C D E).obj F).mapIso α
@[simp]
theorem
CategoryTheory.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.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.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.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.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 (whiskerLeft F α)
instance
CategoryTheory.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.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)
:
@[simp]
theorem
CategoryTheory.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.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)
:
@[simp]
theorem
CategoryTheory.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)
:
whiskerLeft F (whiskerLeft G α) = CategoryStruct.comp (F.associator G H).inv (CategoryStruct.comp (whiskerLeft (F.comp G) α) (F.associator G K).hom)
@[simp]
theorem
CategoryTheory.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.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 (whiskerLeft F α) K = CategoryStruct.comp (F.associator G K).hom
(CategoryStruct.comp (whiskerLeft F (whiskerRight α K)) (F.associator H K).inv)
@[simp]
theorem
CategoryTheory.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)
:
isoWhiskerLeft F (isoWhiskerLeft G α) = (F.associator G H).symm ≪≫ isoWhiskerLeft (F.comp G) α ≪≫ F.associator G K
@[simp]
theorem
CategoryTheory.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.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 (isoWhiskerLeft F α) K = F.associator G K ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫ F.associator H K
theorem
CategoryTheory.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)
:
isoWhiskerLeft F (isoWhiskerRight α K) = (F.associator G K).symm ≪≫ isoWhiskerRight (isoWhiskerLeft F α) K ≪≫ (F.associator H K).symm
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.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 ≪≫ isoWhiskerLeft F (G.associator H K) = (F.comp G).associator H K ≪≫ F.associator G (H.comp K)
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 (whiskerLeft F 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 (whiskerLeft F (G.associator H K).hom)) = CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom
def
CategoryTheory.whiskeringLeft₂
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
(E : Type u_7)
[Category.{u_12, u_7} 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.
@[simp]
theorem
CategoryTheory.whiskeringLeft₂_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
(E : Type u_7)
[Category.{u_12, u_7} 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.whiskeringLeft₂_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
(E : Type u_7)
[Category.{u_12, u_7} 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.whiskeringLeft₂_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
(E : Type u_7)
[Category.{u_12, u_7} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(X : Functor D₁ (Functor D₂ E))
(X✝ : C₁)
(X✝ : C₂)
:
@[simp]
theorem
CategoryTheory.whiskeringLeft₂_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
(E : Type u_7)
[Category.{u_12, u_7} 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.whiskeringLeft₂_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
(E : Type u_7)
[Category.{u_12, u_7} 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.whiskeringLeft₂_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
(E : Type u_7)
[Category.{u_12, u_7} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(X : Functor D₁ (Functor D₂ E))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
:
def
CategoryTheory.whiskeringLeft₃ObjObjObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.
@[simp]
theorem
CategoryTheory.whiskeringLeft₃ObjObjObj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃ObjObjObj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃ObjObjObj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃ObjObjObj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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₃)
:
@[simp]
theorem
CategoryTheory.whiskeringLeft₃ObjObjObj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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✝)
:
def
CategoryTheory.whiskeringLeft₃ObjObjMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.
@[simp]
theorem
CategoryTheory.whiskeringLeft₃ObjObjMap_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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 = whiskerLeft F₁ (whiskerLeft F (((whiskeringLeft₂ E).obj F₂).map τ₃))
def
CategoryTheory.whiskeringLeft₃ObjObj
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_4}
{D₂ : Type u_5}
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.
@[simp]
theorem
CategoryTheory.whiskeringLeft₃ObjObj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_4}
{D₂ : Type u_5}
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
(F₃ : Functor C₃ D₃)
:
@[simp]
theorem
CategoryTheory.whiskeringLeft₃ObjObj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_4}
{D₂ : Type u_5}
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
{X✝ Y✝ : Functor C₃ D₃}
(τ₃ : X✝ ⟶ Y✝)
:
def
CategoryTheory.whiskeringLeft₃ObjMap
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_4}
{D₂ : Type u_5}
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.
@[simp]
theorem
CategoryTheory.whiskeringLeft₃ObjMap_app
{C₁ : Type u_1}
{C₂ : Type u_2}
(C₃ : Type u_3)
{D₁ : Type u_4}
{D₂ : Type u_5}
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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₁)
def
CategoryTheory.whiskeringLeft₃Obj
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_4}
(D₂ : Type u_5)
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} E]
(F₁ : Functor C₁ D₁)
:
Auxiliary definition for whiskeringLeft₃.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.whiskeringLeft₃Obj_map
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_4}
(D₂ : Type u_5)
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} E]
(F₁ : Functor C₁ D₁)
{X✝ Y✝ : Functor C₂ D₂}
(τ₂ : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.whiskeringLeft₃Obj_obj
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_4}
(D₂ : Type u_5)
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} E]
(F₁ : Functor C₁ D₁)
(F₂ : Functor C₂ D₂)
:
def
CategoryTheory.whiskeringLeft₃Map
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_4}
(D₂ : Type u_5)
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.
@[simp]
theorem
CategoryTheory.whiskeringLeft₃Map_app_app
{C₁ : Type u_1}
(C₂ : Type u_2)
(C₃ : Type u_3)
{D₁ : Type u_4}
(D₂ : Type u_5)
(D₃ : Type u_6)
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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₃ = whiskerLeft
((whiskeringRight D₁ (Functor D₂ (Functor D₃ E)) (Functor C₂ (Functor C₃ E))).obj
(((whiskeringLeft₂ E).obj F₂).obj F₃))
((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ E))).map τ₁)
def
CategoryTheory.whiskeringLeft₃
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.
@[simp]
theorem
CategoryTheory.whiskeringLeft₃_obj_obj_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃_obj_obj_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃_obj_obj_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃_map_app_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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₃)
:
@[simp]
theorem
CategoryTheory.whiskeringLeft₃_obj_map_app_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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.whiskeringLeft₃_obj_obj_obj_obj_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
{D₁ : Type u_4}
{D₂ : Type u_5}
{D₃ : Type u_6}
[Category.{u_8, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_10, u_3} C₃]
[Category.{u_11, u_4} D₁]
[Category.{u_12, u_5} D₂]
[Category.{u_13, u_6} D₃]
(E : Type u_7)
[Category.{u_14, u_7} 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₃)
:
def
CategoryTheory.Functor.postcompose₂
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
{E : Type u_7}
[Category.{u_11, u_7} E]
{E' : Type u_8}
[Category.{u_12, u_8} E']
:
The "postcomposition" with a functor E ⥤ E' gives a functor
(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E'.
Equations
- CategoryTheory.Functor.postcompose₂ = (CategoryTheory.whiskeringRight C₂ E E').comp (CategoryTheory.whiskeringRight C₁ (CategoryTheory.Functor C₂ E) (CategoryTheory.Functor C₂ E'))
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_obj_obj_obj_map
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
{E : Type u_7}
[Category.{u_11, u_7} E]
{E' : Type u_8}
[Category.{u_12, u_8} 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_obj_map_app
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
{E : Type u_7}
[Category.{u_11, u_7} E]
{E' : Type u_8}
[Category.{u_12, u_8} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ E))
{X✝ Y✝ : C₁}
(f : X✝ ⟶ Y✝)
(X✝¹ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
{E : Type u_7}
[Category.{u_11, u_7} E]
{E' : Type u_8}
[Category.{u_12, u_8} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ E))
(X✝ : C₁)
(X✝ : C₂)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₂_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
{E : Type u_7}
[Category.{u_11, u_7} E]
{E' : Type u_8}
[Category.{u_12, u_8} 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_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
{E : Type u_7}
[Category.{u_11, u_7} E]
{E' : Type u_8}
[Category.{u_12, u_8} E']
(X : Functor E E')
{X✝ Y✝ : Functor C₁ (Functor C₂ E)}
(α : X✝ ⟶ Y✝)
(X✝¹ : C₁)
(X✝¹ : C₂)
:
def
CategoryTheory.Functor.postcompose₃
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
[Category.{u_11, u_3} C₃]
{E : Type u_7}
[Category.{u_12, u_7} E]
{E' : Type u_8}
[Category.{u_13, u_8} 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.
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_obj_map_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
[Category.{u_11, u_3} C₃]
{E : Type u_7}
[Category.{u_12, u_7} E]
{E' : Type u_8}
[Category.{u_13, u_8} 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₃_obj_obj_obj_obj_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
[Category.{u_11, u_3} C₃]
{E : Type u_7}
[Category.{u_12, u_7} E]
{E' : Type u_8}
[Category.{u_13, u_8} 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.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
[Category.{u_11, u_3} C₃]
{E : Type u_7}
[Category.{u_12, u_7} E]
{E' : Type u_8}
[Category.{u_13, u_8} 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₃_map_app_app_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
[Category.{u_11, u_3} C₃]
{E : Type u_7}
[Category.{u_12, u_7} E]
{E' : Type u_8}
[Category.{u_13, u_8} E']
{X✝ Y✝ : Functor E E'}
(f : X✝ ⟶ Y✝)
(F : Functor C₁ (Functor C₂ (Functor C₃ E)))
(c : C₁)
(c✝ : C₂)
(c✝ : C₃)
:
@[simp]
theorem
CategoryTheory.Functor.postcompose₃_obj_obj_map_app_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[Category.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
[Category.{u_11, u_3} C₃]
{E : Type u_7}
[Category.{u_12, u_7} E]
{E' : Type u_8}
[Category.{u_13, u_8} 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.{u_9, u_1} C₁]
[Category.{u_10, u_2} C₂]
[Category.{u_11, u_3} C₃]
{E : Type u_7}
[Category.{u_12, u_7} E]
{E' : Type u_8}
[Category.{u_13, u_8} E']
(X : Functor E E')
(F : Functor C₁ (Functor C₂ (Functor C₃ E)))
(X✝ : C₁)
{X✝¹ Y✝ : C₂}
(f : X✝¹ ⟶ Y✝)
(X✝ : C₃)
: