doc-next-gen

Mathlib.CategoryTheory.Whiskering

Module docstring

{"# 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. "}

CategoryTheory.whiskerLeft definition
(F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : F ⋙ G ⟶ F ⋙ H
Full source 
/-- If `α : G ⟶ H` then
`whiskerLeft F α : (F ⋙ G) ⟶ (F ⋙ H)` has components `α.app (F.obj X)`.
-/
@[simps]
def whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) :
    F ⋙ GF ⋙ G ⟶ F ⋙ H where
  app X := α.app (F.obj X)
  naturality X Y f := by rw [Functor.comp_map, Functor.comp_map, α.naturality]
Left whiskering of natural transformations
Informal description
Given a functor $F \colon C \to D$ and natural transformation $\alpha \colon G \to H$ between functors $G, H \colon D \to E$, the whiskering $\text{whiskerLeft}\, F\, \alpha$ is a natural transformation from $F \circ G$ to $F \circ H$ whose component at an object $X$ in $C$ is given by $\alpha$ evaluated at $F(X)$.
CategoryTheory.NatTrans.id_hcomp theorem
(F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : 𝟙 F ◫ α = whiskerLeft F α
Full source 
@[simp]
lemma NatTrans.id_hcomp (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : 𝟙𝟙 F ◫ α = whiskerLeft F α := by
  ext
  simp
Horizontal Composition of Identity with Natural Transformation Equals Left Whiskering
Informal description
Given a functor $F \colon C \to D$ and a natural transformation $\alpha \colon G \to H$ between functors $G, H \colon D \to E$, the horizontal composition of the identity natural transformation $𝟙_F$ with $\alpha$ is equal to the left whiskering of $F$ with $\alpha$, i.e., $𝟙_F ◫ \alpha = \text{whiskerLeft}\, F\, \alpha$.
CategoryTheory.whiskerRight definition
{G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : G ⋙ F ⟶ H ⋙ F
Full source 
/-- If `α : G ⟶ H` then
`whiskerRight α F : (G ⋙ F) ⟶ (G ⋙ F)` has components `F.map (α.app X)`.
-/
@[simps]
def whiskerRight {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) :
    G ⋙ FG ⋙ F ⟶ H ⋙ F where
  app X := F.map (α.app X)
  naturality X Y f := by
    rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
Right whiskering of natural transformations
Informal description
Given functors $G, H \colon C \to D$ and a natural transformation $\alpha \colon G \to H$, the whiskering $\alpha \circ F \colon (G \circ F) \to (H \circ F)$ is the natural transformation whose component at each object $X$ in $C$ is given by $F(\alpha_X)$, where $F \colon D \to E$ is a functor. This construction ensures that the naturality condition is preserved.
CategoryTheory.NatTrans.hcomp_id theorem
{G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : α ◫ 𝟙 F = whiskerRight α F
Full source 
@[simp]
lemma NatTrans.hcomp_id {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : α ◫ 𝟙 F = whiskerRight α F := by
  ext
  simp
Horizontal Composition with Identity Equals Right Whiskering
Informal description
Given functors $G, H \colon C \to D$, a natural transformation $\alpha \colon G \to H$, and a functor $F \colon D \to E$, the horizontal composition of $\alpha$ with the identity natural transformation on $F$ is equal to the right whiskering of $\alpha$ by $F$. That is, $\alpha \square \mathrm{id}_F = \alpha \circ F$.
CategoryTheory.whiskeringLeft definition
: (C ⥤ D) ⥤ (D ⥤ E) ⥤ C ⥤ E
Full source 
/-- 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 α`.
-/
@[simps]
def whiskeringLeft : (C ⥤ D) ⥤ (D ⥤ E) ⥤ C ⥤ E where
  obj F :=
    { obj := fun G => F ⋙ G
      map := fun α => whiskerLeft F α }
  map τ :=
    { app := fun H =>
        { app := fun c => H.map (τ.app c)
          naturality := fun X Y f => by dsimp; rw [← H.map_comp, ← H.map_comp, ← τ.naturality] }
      naturality := fun X Y f => by ext; dsimp; rw [f.naturality] }
Left whiskering functor
Informal description
The functor `whiskeringLeft` takes a functor $F \colon C \to D$ and produces a functor from the category of functors $D \to E$ to the category of functors $C \to E$. Specifically, for any functor $G \colon D \to E$, the functor maps $G$ to the composition $F \circ G$, and for any natural transformation $\alpha \colon G \to H$, it maps $\alpha$ to the left whiskering $\text{whiskerLeft}\, F\, \alpha$.
CategoryTheory.whiskeringRight definition
: (D ⥤ E) ⥤ (C ⥤ D) ⥤ C ⥤ E
Full source 
/-- 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`.
-/
@[simps]
def whiskeringRight : (D ⥤ E) ⥤ (C ⥤ D) ⥤ C ⥤ E where
  obj H :=
    { obj := fun F => F ⋙ H
      map := fun α => whiskerRight α H }
  map τ :=
    { app := fun F =>
        { app := fun c => τ.app (F.obj c)
          naturality := fun X Y f => by dsimp; rw [τ.naturality] }
      naturality := fun X Y f => by ext; dsimp; rw [← NatTrans.naturality] }
Right whiskering functor
Informal description
The functor that takes a functor $H \colon D \to E$ and produces a functor from $(C \to D) \to (C \to E)$ by right-composition with $H$. Specifically, for any functor $F \colon C \to D$, the functor maps $F$ to $F \circ H$, and for any natural transformation $\alpha$ between functors $G, H \colon C \to D$, it maps $\alpha$ to the right whiskering $\alpha \circ H$.
CategoryTheory.faithful_whiskeringRight_obj instance
{F : D ⥤ E} [F.Faithful] : ((whiskeringRight C D E).obj F).Faithful
Full source 
instance faithful_whiskeringRight_obj {F : D ⥤ E} [F.Faithful] :
    ((whiskeringRight C D E).obj F).Faithful where
  map_injective hαβ := by
    ext X
    exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X
Faithfulness of Right Whiskering by a Faithful Functor
Informal description
For any faithful functor $F \colon D \to E$, the right whiskering functor $(F \circ -) \colon (C \to D) \to (C \to E)$ is also faithful.
CategoryTheory.Functor.FullyFaithful.whiskeringRight definition
{F : D ⥤ E} (hF : F.FullyFaithful) (C : Type*) [Category C] : ((whiskeringRight C D E).obj F).FullyFaithful
Full source 
/-- If `F : D ⥤ E` is fully faithful, then so is
`(whiskeringRight C D E).obj F : (C ⥤ D) ⥤ C ⥤ E`. -/
@[simps]
def Functor.FullyFaithful.whiskeringRight {F : D ⥤ E} (hF : F.FullyFaithful)
    (C : Type*) [Category C] :
    ((whiskeringRight C D E).obj F).FullyFaithful where
  preimage f :=
    { app := fun X => hF.preimage (f.app X)
      naturality := fun _ _ g => by
        apply hF.map_injective
        dsimp
        simp only [map_comp, map_preimage]
        apply f.naturality }
Full faithfulness of right whiskering by a fully faithful functor
Informal description
Given a fully faithful functor $F \colon D \to E$, the right whiskering functor $(F \circ -) \colon (C \to D) \to (C \to E)$ is also fully faithful. Specifically, for any natural transformation $f$ between functors in $C \to E$, there exists a unique natural transformation in $C \to D$ whose image under right whiskering by $F$ is $f$.
CategoryTheory.whiskeringLeft_obj_id theorem
: (whiskeringLeft C C E).obj (𝟭 _) = 𝟭 _
Full source 
theorem whiskeringLeft_obj_id : (whiskeringLeft C C E).obj (𝟭 _) = 𝟭 _ :=
  rfl
Left Whiskering with Identity Functor Yields Identity
Informal description
The left whiskering functor applied to the identity functor $\text{id}_C \colon C \to C$ yields the identity functor on the category of functors from $C$ to $E$, i.e., $\text{whiskeringLeft}_{C,C,E}(\text{id}_C) = \text{id}_{C \to E}$.
CategoryTheory.whiskeringLeftObjIdIso definition
: (whiskeringLeft C C E).obj (𝟭 _) ≅ 𝟭 _
Full source 
/-- The isomorphism between left-whiskering on the identity functor and the identity of the functor
between the resulting functor categories. -/
def whiskeringLeftObjIdIso : (whiskeringLeft C C E).obj (𝟭 _) ≅ 𝟭 _ :=
  Iso.refl _
Isomorphism between left-whiskering of identity and identity functor
Informal description
The isomorphism between the left-whiskering functor applied to the identity functor $\text{id}_C \colon C \to C$ and the identity functor on the category of functors from $C$ to $E$. In other words, this is the natural isomorphism showing that $\text{whiskeringLeft}_{C,C,E}(\text{id}_C)$ is isomorphic to $\text{id}_{C \to E}$.
CategoryTheory.whiskeringLeft_obj_comp theorem
{D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') : (whiskeringLeft C D' E).obj (F ⋙ G) = (whiskeringLeft D D' E).obj G ⋙ (whiskeringLeft C D E).obj F
Full source 
theorem whiskeringLeft_obj_comp {D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') :
    (whiskeringLeft C D' E).obj (F ⋙ G) =
    (whiskeringLeft D D' E).obj G ⋙ (whiskeringLeft C D E).obj F :=
  rfl
Composition of Left Whiskering Functors
Informal description
Let $C$, $D$, $D'$, and $E$ be categories, with $F \colon C \to D$ and $G \colon D \to D'$ functors. Then the left whiskering functor applied to the composition $F \circ G$ is equal to the composition of the left whiskering functors applied to $G$ and $F$ respectively, i.e., $$ \text{whiskeringLeft}_{C,D',E}(F \circ G) = \text{whiskeringLeft}_{D,D',E}(G) \circ \text{whiskeringLeft}_{C,D,E}(F). $$
CategoryTheory.whiskeringLeftObjCompIso definition
{D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') : (whiskeringLeft C D' E).obj (F ⋙ G) ≅ (whiskeringLeft D D' E).obj G ⋙ (whiskeringLeft C D E).obj F
Full source 
/-- The isomorphism between left-whiskering on the composition of functors and the composition
of two left-whiskering applications. -/
def whiskeringLeftObjCompIso {D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') :
    (whiskeringLeft C D' E).obj (F ⋙ G) ≅
    (whiskeringLeft D D' E).obj G ⋙ (whiskeringLeft C D E).obj F :=
  Iso.refl _
Natural isomorphism for left-whiskering composition
Informal description
Given categories $C$, $D$, $D'$, and $E$, and functors $F \colon C \to D$ and $G \colon D \to D'$, there is a natural isomorphism between the left-whiskering of the composition $F \circ G$ and the composition of the left-whiskering functors applied to $G$ and $F$ respectively. In other words, the following diagram commutes up to natural isomorphism: $$ \text{whiskeringLeft}_{C,D',E}(F \circ G) \cong \text{whiskeringLeft}_{D,D',E}(G) \circ \text{whiskeringLeft}_{C,D,E}(F). $$
CategoryTheory.whiskeringRight_obj_id theorem
: (whiskeringRight E C C).obj (𝟭 _) = 𝟭 _
Full source 
theorem whiskeringRight_obj_id : (whiskeringRight E C C).obj (𝟭 _) = 𝟭 _ :=
  rfl
Right Whiskering Preserves Identity Functor
Informal description
The right whiskering functor applied to the identity functor $\text{id}_C \colon C \to C$ yields the identity functor on the functor category $(C \to E)$, i.e., $\text{whiskeringRight}(E, C, C)(\text{id}_C) = \text{id}_{C \to E}$.
CategoryTheory.whiskeringRightObjIdIso definition
: (whiskeringRight E C C).obj (𝟭 _) ≅ 𝟭 _
Full source 
/-- The isomorphism between right-whiskering on the identity functor and the identity of the functor
between the resulting functor categories. -/
def whiskeringRightObjIdIso : (whiskeringRight E C C).obj (𝟭 _) ≅ 𝟭 _ :=
  Iso.refl _
Right whiskering of identity functor is identity
Informal description
The isomorphism between the right-whiskering of the identity functor $\text{id}_C \colon C \to C$ and the identity functor on the functor category $(C \to E)$. In other words, the right whiskering functor applied to the identity functor is naturally isomorphic to the identity functor on the category of functors from $C$ to $E$.
CategoryTheory.whiskeringRight_obj_comp theorem
{D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') : (whiskeringRight E C D).obj F ⋙ (whiskeringRight E D D').obj G = (whiskeringRight E C D').obj (F ⋙ G)
Full source 
theorem whiskeringRight_obj_comp {D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') :
    (whiskeringRight E C D).obj F ⋙ (whiskeringRight E D D').obj G =
    (whiskeringRight E C D').obj (F ⋙ G) :=
  rfl
Composition of Right Whiskering Functors
Informal description
For categories $C$, $D$, $D'$, and $E$, and functors $F \colon C \to D$ and $G \colon D \to D'$, the composition of the right whiskering functors associated with $F$ and $G$ is equal to the right whiskering functor associated with the composition $F \circ G \colon C \to D'$. That is, \[ \text{whiskeringRight}(E, C, D)(F) \circ \text{whiskeringRight}(E, D, D')(G) = \text{whiskeringRight}(E, C, D')(F \circ G). \]
CategoryTheory.whiskeringRightObjCompIso definition
{D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') : (whiskeringRight E C D).obj F ⋙ (whiskeringRight E D D').obj G ≅ (whiskeringRight E C D').obj (F ⋙ G)
Full source 
/-- The isomorphism between right-whiskering on the composition of functors and the composition
of two right-whiskering applications. -/
def whiskeringRightObjCompIso {D' : Type u₄} [Category.{v₄} D'] (F : C ⥤ D) (G : D ⥤ D') :
    (whiskeringRight E C D).obj F ⋙ (whiskeringRight E D D').obj G(whiskeringRight E C D).obj F ⋙ (whiskeringRight E D D').obj G ≅
    (whiskeringRight E C D').obj (F ⋙ G) :=
  Iso.refl _
Natural isomorphism between composition of right whiskering functors and right whiskering of composed functors
Informal description
Given categories \( C \), \( D \), \( D' \), and \( E \), and functors \( F \colon C \to D \) and \( G \colon D \to D' \), the composition of the right whiskering functors associated with \( F \) and \( G \) is naturally isomorphic to the right whiskering functor associated with the composition \( F \circ G \colon C \to D' \). That is, \[ \text{whiskeringRight}(E, C, D)(F) \circ \text{whiskeringRight}(E, D, D')(G) \cong \text{whiskeringRight}(E, C, D')(F \circ G). \]
CategoryTheory.full_whiskeringRight_obj instance
{F : D ⥤ E} [F.Faithful] [F.Full] : ((whiskeringRight C D E).obj F).Full
Full source 
instance full_whiskeringRight_obj {F : D ⥤ E} [F.Faithful] [F.Full] :
    ((whiskeringRight C D E).obj F).Full :=
  ((Functor.FullyFaithful.ofFullyFaithful F).whiskeringRight C).full
Fullness of Right Whiskering by a Fully Faithful Functor
Informal description
For any fully faithful functor $F \colon D \to E$, the right whiskering functor $(F \circ -) \colon (C \to D) \to (C \to E)$ is full. That is, for any natural transformation between functors in $C \to E$, there exists a natural transformation in $C \to D$ whose image under right whiskering by $F$ is the given transformation.
CategoryTheory.whiskerLeft_id theorem
(F : C ⥤ D) {G : D ⥤ E} : whiskerLeft F (NatTrans.id G) = NatTrans.id (F.comp G)
Full source 
@[simp]
theorem whiskerLeft_id (F : C ⥤ D) {G : D ⥤ E} :
    whiskerLeft F (NatTrans.id G) = NatTrans.id (F.comp G) :=
  rfl
Identity Whiskering: $\text{whiskerLeft}\, F\, \mathrm{id}_G = \mathrm{id}_{F \circ G}$
Informal description
For any functor $F \colon C \to D$ and any functor $G \colon D \to E$, the left whiskering of the identity natural transformation $\mathrm{id}_G$ along $F$ is equal to the identity natural transformation on the composition $F \circ G$, i.e., $$ \text{whiskerLeft}\, F\, \mathrm{id}_G = \mathrm{id}_{F \circ G}. $$
CategoryTheory.whiskerLeft_id' theorem
(F : C ⥤ D) {G : D ⥤ E} : whiskerLeft F (𝟙 G) = 𝟙 (F.comp G)
Full source 
@[simp]
theorem whiskerLeft_id' (F : C ⥤ D) {G : D ⥤ E} : whiskerLeft F (𝟙 G) = 𝟙 (F.comp G) :=
  rfl
Left Whiskering Preserves Identity Natural Transformation
Informal description
Given a functor $F \colon C \to D$ and a functor $G \colon D \to E$, the left whiskering of the identity natural transformation $\mathbb{1}_G$ by $F$ is equal to the identity natural transformation on the composition $F \circ G$, i.e., $\text{whiskerLeft}\, F\, \mathbb{1}_G = \mathbb{1}_{F \circ G}$.
CategoryTheory.whiskerRight_id theorem
{G : C ⥤ D} (F : D ⥤ E) : whiskerRight (NatTrans.id G) F = NatTrans.id (G.comp F)
Full source 
@[simp]
theorem whiskerRight_id {G : C ⥤ D} (F : D ⥤ E) :
    whiskerRight (NatTrans.id G) F = NatTrans.id (G.comp F) :=
  ((whiskeringRight C D E).obj F).map_id _
Identity Whiskering: $\text{whiskerRight}\, \mathrm{id}_G\, F = \mathrm{id}_{G \circ F}$
Informal description
For any functor $G \colon C \to D$ and any functor $F \colon D \to E$, the right whiskering of the identity natural transformation $\mathrm{id}_G$ along $F$ is equal to the identity natural transformation on the composition $G \circ F$, i.e., $$ \text{whiskerRight}\, \mathrm{id}_G\, F = \mathrm{id}_{G \circ F}. $$
CategoryTheory.whiskerRight_id' theorem
{G : C ⥤ D} (F : D ⥤ E) : whiskerRight (𝟙 G) F = 𝟙 (G.comp F)
Full source 
@[simp]
theorem whiskerRight_id' {G : C ⥤ D} (F : D ⥤ E) : whiskerRight (𝟙 G) F = 𝟙 (G.comp F) :=
  ((whiskeringRight C D E).obj F).map_id _
Right Whiskering Preserves Identity Natural Transformation
Informal description
For any functor $G \colon C \to D$ and any functor $F \colon D \to E$, the right whiskering of the identity natural transformation $\mathbb{1}_G$ along $F$ is equal to the identity natural transformation on the composition $G \circ F$, i.e., $$ \text{whiskerRight}\, \mathbb{1}_G\, F = \mathbb{1}_{G \circ F}. $$
CategoryTheory.whiskerLeft_comp theorem
(F : C ⥤ D) {G H K : D ⥤ E} (α : G ⟶ H) (β : H ⟶ K) : whiskerLeft F (α ≫ β) = whiskerLeft F α ≫ whiskerLeft F β
Full source 
@[simp, reassoc]
theorem whiskerLeft_comp (F : C ⥤ D) {G H K : D ⥤ E} (α : G ⟶ H) (β : H ⟶ K) :
    whiskerLeft F (α ≫ β) = whiskerLeftwhiskerLeft F α ≫ whiskerLeft F β :=
  rfl
Composition of Left Whiskerings Equals Left Whiskering of Compositions
Informal description
Given a functor $F \colon C \to D$ and natural transformations $\alpha \colon G \to H$ and $\beta \colon H \to K$ between functors $G, H, K \colon D \to E$, the left whiskering of the composition $\alpha \circ \beta$ with $F$ is equal to the composition of the left whiskerings of $\alpha$ and $\beta$ with $F$. That is, $\text{whiskerLeft}\, F\, (\alpha \circ \beta) = (\text{whiskerLeft}\, F\, \alpha) \circ (\text{whiskerLeft}\, F\, \beta)$.
CategoryTheory.whiskerRight_comp theorem
{G H K : C ⥤ D} (α : G ⟶ H) (β : H ⟶ K) (F : D ⥤ E) : whiskerRight (α ≫ β) F = whiskerRight α F ≫ whiskerRight β F
Full source 
@[simp, reassoc]
theorem whiskerRight_comp {G H K : C ⥤ D} (α : G ⟶ H) (β : H ⟶ K) (F : D ⥤ E) :
    whiskerRight (α ≫ β) F = whiskerRightwhiskerRight α F ≫ whiskerRight β F :=
  ((whiskeringRight C D E).obj F).map_comp α β
Right Whiskering Preserves Composition of Natural Transformations
Informal description
Given functors $G, H, K \colon C \to D$, natural transformations $\alpha \colon G \to H$ and $\beta \colon H \to K$, and a functor $F \colon D \to E$, the right whiskering of the composition $\alpha \circ \beta$ with $F$ is equal to the composition of the right whiskerings of $\alpha$ and $\beta$ with $F$. That is, \[ \text{whiskerRight}\, (\alpha \circ \beta)\, F = (\text{whiskerRight}\, \alpha\, F) \circ (\text{whiskerRight}\, \beta\, F). \]
CategoryTheory.whiskerLeft_comp_whiskerRight theorem
{F G : C ⥤ D} {H K : D ⥤ E} (α : F ⟶ G) (β : H ⟶ K) : whiskerLeft F β ≫ whiskerRight α K = whiskerRight α H ≫ whiskerLeft G β
Full source 
@[reassoc]
theorem whiskerLeft_comp_whiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α : F ⟶ G) (β : H ⟶ K) :
    whiskerLeftwhiskerLeft F β ≫ whiskerRight α K = whiskerRightwhiskerRight α H ≫ whiskerLeft G β := by
  ext
  simp
Commutation of Left and Right Whiskering
Informal description
Given functors $F, G \colon C \to D$ and $H, K \colon D \to E$, and natural transformations $\alpha \colon F \to G$ and $\beta \colon H \to K$, the following diagram of natural transformations commutes: \[ (F \circ H) \xrightarrow{\text{whiskerLeft}\, F\, \beta} (F \circ K) \xrightarrow{\text{whiskerRight}\, \alpha\, K} (G \circ K) \] \[ (F \circ H) \xrightarrow{\text{whiskerRight}\, \alpha\, H} (G \circ H) \xrightarrow{\text{whiskerLeft}\, G\, \beta} (G \circ K) \] In other words, the composition of left whiskering of $\beta$ with $F$ followed by right whiskering of $\alpha$ with $K$ is equal to the composition of right whiskering of $\alpha$ with $H$ followed by left whiskering of $\beta$ with $G$.
CategoryTheory.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight theorem
{F G : C ⥤ D} {H K : D ⥤ E} (α : F ⟶ G) (β : H ⟶ K) : α ◫ β = whiskerLeft F β ≫ whiskerRight α K
Full source 
lemma NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight {F G : C ⥤ D} {H K : D ⥤ E}
    (α : F ⟶ G) (β : H ⟶ K) : α ◫ β = whiskerLeftwhiskerLeft F β ≫ whiskerRight α K := by
  ext
  simp
Horizontal Composition as Whiskering Composition
Informal description
Given functors $F, G \colon C \to D$ and $H, K \colon D \to E$, and natural transformations $\alpha \colon F \to G$ and $\beta \colon H \to K$, the horizontal composition $\alpha \square \beta$ is equal to the composition of the left whiskering of $\beta$ with $F$ and the right whiskering of $\alpha$ with $K$, i.e., \[ \alpha \square \beta = \text{whiskerLeft}\, F\, \beta \circ \text{whiskerRight}\, \alpha\, K. \]
CategoryTheory.isoWhiskerLeft definition
(F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) : F ⋙ G ≅ F ⋙ H
Full source 
/-- If `α : G ≅ H` is a natural isomorphism then
`isoWhiskerLeft F α : (F ⋙ G) ≅ (F ⋙ H)` has components `α.app (F.obj X)`.
-/
def isoWhiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) : F ⋙ GF ⋙ G ≅ F ⋙ H :=
  ((whiskeringLeft C D E).obj F).mapIso α
Left whiskering of a natural isomorphism
Informal description
Given a functor \( F \colon \mathcal{C} \to \mathcal{D} \) and a natural isomorphism \( \alpha \colon G \cong H \) between functors \( G, H \colon \mathcal{D} \to \mathcal{E} \), the construction `isoWhiskerLeft F α` yields a natural isomorphism \( F \circ G \cong F \circ H \) whose components at each object \( X \) in \( \mathcal{C} \) are given by \( \alpha_{F(X)} \).
CategoryTheory.isoWhiskerLeft_hom theorem
(F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) : (isoWhiskerLeft F α).hom = whiskerLeft F α.hom
Full source 
@[simp]
theorem isoWhiskerLeft_hom (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) :
    (isoWhiskerLeft F α).hom = whiskerLeft F α.hom :=
  rfl
Homomorphism Component of Left-Whiskered Natural Isomorphism
Informal description
Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon \mathcal{D} \to \mathcal{E}$, the homomorphism component of the whiskered isomorphism $\text{isoWhiskerLeft}\, F\, \alpha$ is equal to the left whiskering of $F$ with the homomorphism component of $\alpha$, i.e., \[ (\text{isoWhiskerLeft}\, F\, \alpha).\text{hom} = \text{whiskerLeft}\, F\, \alpha.\text{hom}. \]
CategoryTheory.isoWhiskerLeft_inv theorem
(F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) : (isoWhiskerLeft F α).inv = whiskerLeft F α.inv
Full source 
@[simp]
theorem isoWhiskerLeft_inv (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) :
    (isoWhiskerLeft F α).inv = whiskerLeft F α.inv :=
  rfl
Inverse of Left-Whiskered Natural Isomorphism Equals Left-Whiskering of Inverse
Informal description
Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon \mathcal{D} \to \mathcal{E}$, the inverse component of the left-whiskered isomorphism $\text{isoWhiskerLeft}\, F\, \alpha$ is equal to the left whiskering of $F$ with the inverse component of $\alpha$, i.e., \[ (\text{isoWhiskerLeft}\, F\, \alpha)^{-1} = \text{whiskerLeft}\, F\, \alpha^{-1}. \]
CategoryTheory.isoWhiskerLeft_symm theorem
(F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) : (isoWhiskerLeft F α).symm = isoWhiskerLeft F α.symm
Full source 
lemma isoWhiskerLeft_symm (F : C ⥤ D) {G H : D ⥤ E} (α : G ≅ H) :
    (isoWhiskerLeft F α).symm = isoWhiskerLeft F α.symm :=
  rfl
Inverse of Left-Whiskered Natural Isomorphism Equals Left-Whiskering of Inverse
Informal description
Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon \mathcal{D} \to \mathcal{E}$, the inverse of the left-whiskered isomorphism $\text{isoWhiskerLeft}\, F\, \alpha$ is equal to the left-whiskering of $F$ with the inverse isomorphism $\alpha^{-1}$, i.e., \[ (\text{isoWhiskerLeft}\, F\, \alpha)^{-1} = \text{isoWhiskerLeft}\, F\, \alpha^{-1}. \]
CategoryTheory.isoWhiskerLeft_refl theorem
(F : C ⥤ D) (G : D ⥤ E) : isoWhiskerLeft F (Iso.refl G) = Iso.refl _
Full source 
@[simp]
lemma isoWhiskerLeft_refl (F : C ⥤ D) (G : D ⥤ E) :
    isoWhiskerLeft F (Iso.refl G) = Iso.refl _ :=
  rfl
Left Whiskering of Identity Isomorphism Yields Identity
Informal description
Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and a functor $G \colon \mathcal{D} \to \mathcal{E}$, the left whiskering of the identity natural isomorphism $\text{Iso.refl}(G)$ by $F$ is equal to the identity natural isomorphism on the composite functor $F \circ G$, i.e., \[ \text{isoWhiskerLeft}_F (\text{Iso.refl}(G)) = \text{Iso.refl}(F \circ G). \]
CategoryTheory.isoWhiskerRight definition
{G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : G ⋙ F ≅ H ⋙ F
Full source 
/-- If `α : G ≅ H` then
`isoWhiskerRight α F : (G ⋙ F) ≅ (H ⋙ F)` has components `F.map_iso (α.app X)`.
-/
def isoWhiskerRight {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : G ⋙ FG ⋙ F ≅ H ⋙ F :=
  ((whiskeringRight C D E).obj F).mapIso α
Right whiskering of an isomorphism of functors
Informal description
Given an isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon \mathcal{C} \to \mathcal{D}$ and a functor $F \colon \mathcal{D} \to \mathcal{E}$, the isomorphism $\text{isoWhiskerRight} \alpha F \colon G \circ F \cong H \circ F$ is constructed by applying $F$ to the components of $\alpha$. Specifically, for each object $X$ in $\mathcal{C}$, the component of the isomorphism at $X$ is given by $F(\alpha_X)$.
CategoryTheory.isoWhiskerRight_hom theorem
{G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : (isoWhiskerRight α F).hom = whiskerRight α.hom F
Full source 
@[simp]
theorem isoWhiskerRight_hom {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) :
    (isoWhiskerRight α F).hom = whiskerRight α.hom F :=
  rfl
Homomorphism of Right-Whiskered Isomorphism Equals Whiskering of Homomorphism
Informal description
Given an isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon \mathcal{C} \to \mathcal{D}$ and a functor $F \colon \mathcal{D} \to \mathcal{E}$, the homomorphism component of the right-whiskered isomorphism $\text{isoWhiskerRight} \alpha F \colon G \circ F \cong H \circ F$ is equal to the right whiskering of the homomorphism component of $\alpha$ with $F$, i.e., \[ (\text{isoWhiskerRight} \alpha F).\text{hom} = \text{whiskerRight} \alpha.\text{hom} F. \]
CategoryTheory.isoWhiskerRight_inv theorem
{G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : (isoWhiskerRight α F).inv = whiskerRight α.inv F
Full source 
@[simp]
theorem isoWhiskerRight_inv {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) :
    (isoWhiskerRight α F).inv = whiskerRight α.inv F :=
  rfl
Inverse of Right-Whiskered Isomorphism Equals Whiskering of Inverse
Informal description
Given an isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon \mathcal{C} \to \mathcal{D}$ and a functor $F \colon \mathcal{D} \to \mathcal{E}$, the inverse of the whiskered isomorphism $\text{isoWhiskerRight} \alpha F \colon G \circ F \cong H \circ F$ is equal to the whiskering of the inverse of $\alpha$ with $F$, i.e., $(\text{isoWhiskerRight} \alpha F)^{-1} = \text{whiskerRight} \alpha^{-1} F$.
CategoryTheory.isoWhiskerRight_symm theorem
{G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : (isoWhiskerRight α F).symm = isoWhiskerRight α.symm F
Full source 
lemma isoWhiskerRight_symm {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) :
    (isoWhiskerRight α F).symm = isoWhiskerRight α.symm F :=
  rfl
Inverse of Right-Whiskered Isomorphism Equals Right-Whiskering of Inverse
Informal description
Given an isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon \mathcal{C} \to \mathcal{D}$ and a functor $F \colon \mathcal{D} \to \mathcal{E}$, the inverse of the right-whiskered isomorphism $\text{isoWhiskerRight} \alpha F \colon G \circ F \cong H \circ F$ is equal to the right-whiskering of the inverse isomorphism $\alpha^{-1} \colon H \cong G$ with $F$, i.e., $(\text{isoWhiskerRight} \alpha F)^{-1} = \text{isoWhiskerRight} \alpha^{-1} F$.
CategoryTheory.isoWhiskerRight_refl theorem
(F : C ⥤ D) (G : D ⥤ E) : isoWhiskerRight (Iso.refl F) G = Iso.refl _
Full source 
@[simp]
lemma isoWhiskerRight_refl (F : C ⥤ D) (G : D ⥤ E) :
    isoWhiskerRight (Iso.refl F) G = Iso.refl _ := by
  aesop_cat
Right Whiskering of Identity Isomorphism Yields Identity
Informal description
For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and any functor $G \colon \mathcal{D} \to \mathcal{E}$, the right whiskering of the identity isomorphism $\text{id}_F$ with $G$ is equal to the identity isomorphism on the composition $F \circ G$, i.e., $$ \text{isoWhiskerRight}\, \text{id}_F\, G = \text{id}_{F \circ G}. $$
CategoryTheory.isIso_whiskerLeft instance
(F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) [IsIso α] : IsIso (whiskerLeft F α)
Full source 
instance isIso_whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) [IsIso α] :
    IsIso (whiskerLeft F α) :=
  (isoWhiskerLeft F (asIso α)).isIso_hom
Left Whiskering Preserves Isomorphisms
Informal description
Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and a natural isomorphism $\alpha \colon G \to H$ between functors $G, H \colon \mathcal{D} \to \mathcal{E}$, the left whiskering $\text{whiskerLeft}\, F\, \alpha$ is also a natural isomorphism.
CategoryTheory.isIso_whiskerRight instance
{G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) [IsIso α] : IsIso (whiskerRight α F)
Full source 
instance isIso_whiskerRight {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) [IsIso α] :
    IsIso (whiskerRight α F) :=
  (isoWhiskerRight (asIso α) F).isIso_hom
Right Whiskering Preserves Isomorphisms of Natural Transformations
Informal description
Given functors $G, H \colon \mathcal{C} \to \mathcal{D}$ and a natural transformation $\alpha \colon G \to H$ that is an isomorphism, and a functor $F \colon \mathcal{D} \to \mathcal{E}$, the right whiskering $\alpha \circ F \colon (G \circ F) \to (H \circ F)$ is also an isomorphism.
CategoryTheory.isoWhiskerLeft_trans theorem
(F : C ⥤ D) {G H K : D ⥤ E} (α : G ≅ H) (β : H ≅ K) : isoWhiskerLeft F (α ≪≫ β) = isoWhiskerLeft F α ≪≫ isoWhiskerLeft F β
Full source 
@[simp]
theorem isoWhiskerLeft_trans (F : C ⥤ D) {G H K : D ⥤ E} (α : G ≅ H) (β : H ≅ K) :
    isoWhiskerLeft F (α ≪≫ β) = isoWhiskerLeftisoWhiskerLeft F α ≪≫ isoWhiskerLeft F β :=
  rfl
Functoriality of Left Whiskering with Respect to Composition of Natural Isomorphisms
Informal description
Given a functor $F \colon \mathcal{C} \to \mathcal{D}$ and natural isomorphisms $\alpha \colon G \cong H$ and $\beta \colon H \cong K$ between functors $G, H, K \colon \mathcal{D} \to \mathcal{E}$, the left whiskering of the composition $\alpha \ggg \beta$ with $F$ is equal to the composition of the left whiskerings of $\alpha$ and $\beta$ with $F$. In symbols: $$ F \circ (\alpha \ggg \beta) = (F \circ \alpha) \ggg (F \circ \beta). $$
CategoryTheory.isoWhiskerRight_trans theorem
{G H K : C ⥤ D} (α : G ≅ H) (β : H ≅ K) (F : D ⥤ E) : isoWhiskerRight (α ≪≫ β) F = isoWhiskerRight α F ≪≫ isoWhiskerRight β F
Full source 
@[simp]
theorem isoWhiskerRight_trans {G H K : C ⥤ D} (α : G ≅ H) (β : H ≅ K) (F : D ⥤ E) :
    isoWhiskerRight (α ≪≫ β) F = isoWhiskerRightisoWhiskerRight α F ≪≫ isoWhiskerRight β F :=
  ((whiskeringRight C D E).obj F).mapIso_trans α β
Functoriality of Right Whiskering with Respect to Composition of Natural Isomorphisms
Informal description
Given functors $G, H, K \colon \mathcal{C} \to \mathcal{D}$ and natural isomorphisms $\alpha \colon G \cong H$ and $\beta \colon H \cong K$, and a functor $F \colon \mathcal{D} \to \mathcal{E}$, the right whiskering of the composition $\alpha \ggg \beta$ with $F$ is equal to the composition of the right whiskerings of $\alpha$ and $\beta$ with $F$. In symbols: $$ (\alpha \ggg \beta) \circ F = (\alpha \circ F) \ggg (\beta \circ F). $$
CategoryTheory.isoWhiskerLeft_trans_isoWhiskerRight theorem
{F G : C ⥤ D} {H K : D ⥤ E} (α : F ≅ G) (β : H ≅ K) : isoWhiskerLeft F β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ isoWhiskerLeft G β
Full source 
theorem isoWhiskerLeft_trans_isoWhiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α : F ≅ G) (β : H ≅ K) :
    isoWhiskerLeftisoWhiskerLeft F β ≪≫ isoWhiskerRight α K = isoWhiskerRightisoWhiskerRight α H ≪≫ isoWhiskerLeft G β := by
  ext
  simp
Interchange Law for Whiskering of Natural Isomorphisms
Informal description
Given functors $F, G \colon \mathcal{C} \to \mathcal{D}$ and $H, K \colon \mathcal{D} \to \mathcal{E}$, along with natural isomorphisms $\alpha \colon F \cong G$ and $\beta \colon H \cong K$, the following diagram commutes: \[ F \circ \beta \ggg \alpha \circ K = \alpha \circ H \ggg G \circ \beta \] Here, $\circ$ denotes horizontal composition (whiskering) of natural transformations, and $\ggg$ denotes vertical composition of natural transformations.
CategoryTheory.whiskerLeft_twice theorem
(F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) : whiskerLeft F (whiskerLeft G α) = (Functor.associator _ _ _).inv ≫ whiskerLeft (F ⋙ G) α ≫ (Functor.associator _ _ _).hom
Full source 
@[simp]
theorem whiskerLeft_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) :
    whiskerLeft F (whiskerLeft G α) =
    (Functor.associator _ _ _).inv ≫ whiskerLeft (F ⋙ G) α ≫ (Functor.associator _ _ _).hom := by
  aesop_cat
Double Left Whiskering via Associator
Informal description
Given functors $F \colon B \to C$, $G \colon C \to D$, and a natural transformation $\alpha \colon H \to K$ between functors $H, K \colon D \to E$, the double left whiskering $\text{whiskerLeft}\, F\, (\text{whiskerLeft}\, G\, \alpha)$ is equal to the composition of the inverse associator natural isomorphism, the whiskering $\text{whiskerLeft}\, (F \circ G)\, \alpha$, and the associator natural isomorphism. That is, the following diagram commutes: \[ \text{whiskerLeft}\, F\, (\text{whiskerLeft}\, G\, \alpha) = \text{associator}^{-1} \circ \text{whiskerLeft}\, (F \circ G)\, \alpha \circ \text{associator} \]
CategoryTheory.whiskerRight_twice theorem
{H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) : whiskerRight (whiskerRight α F) G = (Functor.associator _ _ _).hom ≫ whiskerRight α (F ⋙ G) ≫ (Functor.associator _ _ _).inv
Full source 
@[simp]
theorem whiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) :
    whiskerRight (whiskerRight α F) G =
    (Functor.associator _ _ _).hom ≫ whiskerRight α (F ⋙ G) ≫ (Functor.associator _ _ _).inv := by
  aesop_cat
Double Right Whiskering via Associator
Informal description
Given functors $H, K \colon B \to C$, $F \colon C \to D$, $G \colon D \to E$, and a natural transformation $\alpha \colon H \to K$, the double right whiskering $\text{whiskerRight}\, (\text{whiskerRight}\, \alpha\, F)\, G$ is equal to the composition of the associator natural isomorphism, the whiskering $\text{whiskerRight}\, \alpha\, (F \circ G)$, and the inverse associator natural isomorphism. That is, the following diagram commutes: \[ \text{whiskerRight}\, (\text{whiskerRight}\, \alpha\, F)\, G = \text{associator} \circ \text{whiskerRight}\, \alpha\, (F \circ G) \circ \text{associator}^{-1} \]
CategoryTheory.whiskerRight_left theorem
(F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) : whiskerRight (whiskerLeft F α) K = (Functor.associator _ _ _).hom ≫ whiskerLeft F (whiskerRight α K) ≫ (Functor.associator _ _ _).inv
Full source 
theorem whiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) :
    whiskerRight (whiskerLeft F α) K =
    (Functor.associator _ _ _).hom ≫ whiskerLeft F (whiskerRight α K) ≫
      (Functor.associator _ _ _).inv := by
  aesop_cat
Interchange Law for Left and Right Whiskering via Associator
Informal description
Given functors $F \colon B \to C$, $G, H \colon C \to D$, a natural transformation $\alpha \colon G \to H$, and a functor $K \colon D \to E$, the following diagram commutes: \[ \text{whiskerRight}\, (\text{whiskerLeft}\, F\, \alpha)\, K = \text{associator} \circ \text{whiskerLeft}\, F\, (\text{whiskerRight}\, \alpha\, K) \circ \text{associator}^{-1} \] where $\text{associator}$ is the associator natural isomorphism for functor composition.
CategoryTheory.isoWhiskerLeft_twice theorem
(F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ≅ K) : isoWhiskerLeft F (isoWhiskerLeft G α) = (Functor.associator _ _ _).symm ≪≫ isoWhiskerLeft (F ⋙ G) α ≪≫ Functor.associator _ _ _
Full source 
@[simp]
theorem isoWhiskerLeft_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ≅ K) :
    isoWhiskerLeft F (isoWhiskerLeft G α) =
    (Functor.associator _ _ _).symm ≪≫ isoWhiskerLeft (F ⋙ G) α ≪≫ Functor.associator _ _ _ := by
  aesop_cat
Double Left Whiskering of Natural Isomorphism via Associator
Informal description
Given functors $F \colon B \to C$, $G \colon C \to D$, and a natural isomorphism $\alpha \colon H \cong K$ between functors $H, K \colon D \to E$, the double left whiskering $\text{isoWhiskerLeft}\, F\, (\text{isoWhiskerLeft}\, G\, \alpha)$ is naturally isomorphic to the composition of the inverse associator natural isomorphism, the whiskering $\text{isoWhiskerLeft}\, (F \circ G)\, \alpha$, and the associator natural isomorphism. That is, the following diagram commutes: \[ \text{isoWhiskerLeft}\, F\, (\text{isoWhiskerLeft}\, G\, \alpha) \cong \text{associator}^{-1} \circ \text{isoWhiskerLeft}\, (F \circ G)\, \alpha \circ \text{associator} \]
CategoryTheory.isoWhiskerRight_twice theorem
{H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ≅ K) : isoWhiskerRight (isoWhiskerRight α F) G = Functor.associator _ _ _ ≪≫ isoWhiskerRight α (F ⋙ G) ≪≫ (Functor.associator _ _ _).symm
Full source 
@[simp]
theorem isoWhiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ≅ K) :
    isoWhiskerRight (isoWhiskerRight α F) G =
    Functor.associatorFunctor.associator _ _ _ ≪≫ isoWhiskerRight α (F ⋙ G) ≪≫ (Functor.associator _ _ _).symm := by
  aesop_cat
Double Right Whiskering of Isomorphisms via Associator
Informal description
Given functors $H, K \colon B \to C$, $F \colon C \to D$, $G \colon D \to E$, and an isomorphism $\alpha \colon H \cong K$ of functors, the double right whiskering $\text{isoWhiskerRight}\, (\text{isoWhiskerRight}\, \alpha\, F)\, G$ is equal to the composition of the associator natural isomorphism, the whiskering $\text{isoWhiskerRight}\, \alpha\, (F \circ G)$, and the inverse associator natural isomorphism. That is, the following diagram commutes: \[ \text{isoWhiskerRight}\, (\text{isoWhiskerRight}\, \alpha\, F)\, G = \text{associator} \circ \text{isoWhiskerRight}\, \alpha\, (F \circ G) \circ \text{associator}^{-1} \]
CategoryTheory.isoWhiskerRight_left theorem
(F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D ⥤ E) : isoWhiskerRight (isoWhiskerLeft F α) K = Functor.associator _ _ _ ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫ Functor.associator _ _ _
Full source 
theorem isoWhiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D ⥤ E) :
    isoWhiskerRight (isoWhiskerLeft F α) K =
    Functor.associatorFunctor.associator _ _ _ ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫
      Functor.associator _ _ _ := by
  aesop_cat
Compatibility of Left and Right Whiskering with Associator
Informal description
Given functors $F \colon \mathcal{B} \to \mathcal{C}$, $G, H \colon \mathcal{C} \to \mathcal{D}$, and $K \colon \mathcal{D} \to \mathcal{E}$, and a natural isomorphism $\alpha \colon G \cong H$, the following diagram of natural isomorphisms commutes: \[ \text{isoWhiskerRight}(\text{isoWhiskerLeft}(F, \alpha), K) = \text{associator}(F, G, K) \ggg \text{isoWhiskerLeft}(F, \text{isoWhiskerRight}(\alpha, K)) \ggg \text{associator}(F, H, K)^{-1} \] Here, $\text{associator}$ denotes the associator natural isomorphism for functor composition, and $\ggg$ denotes horizontal composition of natural isomorphisms.
CategoryTheory.isoWhiskerLeft_right theorem
(F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D ⥤ E) : isoWhiskerLeft F (isoWhiskerRight α K) = (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (isoWhiskerLeft F α) K ≪≫ (Functor.associator _ _ _).symm
Full source 
theorem isoWhiskerLeft_right (F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D ⥤ E) :
    isoWhiskerLeft F (isoWhiskerRight α K) =
    (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (isoWhiskerLeft F α) K ≪≫
      (Functor.associator _ _ _).symm := by
  aesop_cat
Naturality of Left and Right Whiskering with Respect to Associators
Informal description
Given functors $F \colon \mathcal{B} \to \mathcal{C}$, $G, H \colon \mathcal{C} \to \mathcal{D}$, and $K \colon \mathcal{D} \to \mathcal{E}$, and a natural isomorphism $\alpha \colon G \cong H$, the following diagram commutes: \[ \text{isoWhiskerLeft}_F(\text{isoWhiskerRight}_\alpha K) = (\text{associator}_{F,G,K})^{-1} \circ \text{isoWhiskerRight}_{(\text{isoWhiskerLeft}_F \alpha)} K \circ (\text{associator}_{F,G,K})^{-1}. \] Here, $\text{associator}_{F,G,K}$ denotes the associator natural isomorphism for the functors $F$, $G$, and $K$.
CategoryTheory.Functor.triangleIso theorem
: associator F (𝟭 B) G ≪≫ isoWhiskerLeft F (leftUnitor G) = isoWhiskerRight (rightUnitor F) G
Full source 
theorem triangleIso :
    associatorassociator F (𝟭 B) G ≪≫ isoWhiskerLeft F (leftUnitor G) =
      isoWhiskerRight (rightUnitor F) G := by aesop_cat
Triangle Identity for Functor Composition (Isomorphism Version)
Informal description
For functors $F \colon A \to B$ and $G \colon B \to C$, the following isomorphism holds: \[ \text{associator}\, F\, \mathbf{1}_B\, G \circ \text{isoWhiskerLeft}\, F\, (\text{leftUnitor}\, G) = \text{isoWhiskerRight}\, (\text{rightUnitor}\, F)\, G \] where: - $\text{associator}$ is the associator natural isomorphism for functor composition, - $\text{leftUnitor}$ and $\text{rightUnitor}$ are the unitor natural isomorphisms, - $\mathbf{1}_B$ is the identity functor on $B$, - $\circ$ denotes horizontal composition of natural isomorphisms.
CategoryTheory.Functor.pentagonIso theorem
: isoWhiskerRight (associator F G H) K ≪≫ associator F (G ⋙ H) K ≪≫ isoWhiskerLeft F (associator G H K) = associator (F ⋙ G) H K ≪≫ associator F G (H ⋙ K)
Full source 
theorem pentagonIso :
    isoWhiskerRightisoWhiskerRight (associator F G H) K ≪≫
        associator F (G ⋙ H) K ≪≫ isoWhiskerLeft F (associator G H K) =
      associatorassociator (F ⋙ G) H K ≪≫ associator F G (H ⋙ K) := by aesop_cat
Pentagon Identity for Functor Composition (Isomorphism Version)
Informal description
For functors $F, G, H, K$ between appropriate categories, the following diagram of natural isomorphisms commutes: \[ \text{isoWhiskerRight}\, (\text{associator}\, F\, G\, H)\, K \circ \text{associator}\, F\, (G \circ H)\, K \circ \text{isoWhiskerLeft}\, F\, (\text{associator}\, G\, H\, K) = \text{associator}\, (F \circ G)\, H\, K \circ \text{associator}\, F\, G\, (H \circ K) \] where $\circ$ denotes horizontal composition of natural isomorphisms and $\text{associator}$ is the associator natural isomorphism for functor composition.
CategoryTheory.Functor.triangle theorem
: (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G
Full source 
theorem triangle :
    (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom =
      whiskerRight (rightUnitor F).hom G := by aesop_cat
Triangle Identity for Functor Composition
Informal description
For functors $F \colon A \to B$ and $G \colon B \to C$, the following diagram commutes: \[ (\text{associator}\, F\, \mathbf{1}_B\, G).\text{hom} \circ \text{whiskerLeft}\, F\, (\text{leftUnitor}\, G).\text{hom} = \text{whiskerRight}\, (\text{rightUnitor}\, F).\text{hom}\, G \] where: - $\text{associator}$ is the associator natural isomorphism for functor composition, - $\text{leftUnitor}$ and $\text{rightUnitor}$ are the unitor natural isomorphisms, - $\mathbf{1}_B$ is the identity functor on $B$, - $\circ$ denotes vertical composition of natural transformations.
CategoryTheory.Functor.pentagon theorem
: whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom = (associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom
Full source 
theorem pentagon :
    whiskerRightwhiskerRight (associator F G H).hom K ≫
        (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom =
      (associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom := by aesop_cat
Pentagon Identity for Functor Composition
Informal description
For functors $F, G, H, K$ between appropriate categories, the following diagram commutes: \[ \text{whiskerRight}\, (\text{associator}\, F\, G\, H).\text{hom}\, K \circ \text{associator}\, F\, (G \circ H)\, K \circ \text{whiskerLeft}\, F\, (\text{associator}\, G\, H\, K).\text{hom} = \text{associator}\, (F \circ G)\, H\, K \circ \text{associator}\, F\, G\, (H \circ K).\text{hom} \] where $\circ$ denotes vertical composition of natural transformations and $\text{associator}$ is the associator natural isomorphism for functor composition.
CategoryTheory.whiskeringLeft₂ definition
: (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E)
Full source 
/-- The obvious functor `(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E)`. -/
@[simps!]
def whiskeringLeft₂ :
    (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E) where
  obj F₁ :=
    { obj := fun F₂ ↦
        (whiskeringRight D₁ (D₂ ⥤ E) (C₂ ⥤ E)).obj ((whiskeringLeft C₂ D₂ E).obj F₂) ⋙
          (whiskeringLeft C₁ D₁ (C₂ ⥤ E)).obj F₁
      map := fun φ ↦ whiskerRight
        ((whiskeringRight D₁ (D₂ ⥤ E) (C₂ ⥤ E)).map ((whiskeringLeft C₂ D₂ E).map φ)) _ }
  map ψ :=
    { app := fun F₂ ↦ whiskerLeft _ ((whiskeringLeft C₁ D₁ (C₂ ⥤ E)).map ψ) }
Double left whiskering functor
Informal description
The functor `whiskeringLeft₂` takes two functors $F_1 \colon C_1 \to D_1$ and $F_2 \colon C_2 \to D_2$ and produces a functor from the category of bifunctors $D_1 \to D_2 \to E$ to the category of bifunctors $C_1 \to C_2 \to E$. Specifically, for any bifunctor $G \colon D_1 \to D_2 \to E$, the functor maps $G$ to the composition $F_1 \circ G \circ F_2$, and for any natural transformation $\alpha$ between bifunctors $G, H \colon D_1 \to D_2 \to E$, it maps $\alpha$ to the appropriate whiskering of $\alpha$ with $F_1$ and $F_2$.
CategoryTheory.whiskeringLeft₃ObjObjObj definition
(F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) (F₃ : C₃ ⥤ D₃) : (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E
Full source 
/-- Auxiliary definition for `whiskeringLeft₃`. -/
@[simps!]
def whiskeringLeft₃ObjObjObj (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) (F₃ : C₃ ⥤ D₃) :
    (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E :=
  (whiskeringRight _ _ _).obj (((whiskeringLeft₂ E).obj F₂).obj F₃) ⋙
    (whiskeringLeft C₁ D₁ _).obj F₁
Triple left whiskering functor
Informal description
For functors $F_1 \colon C_1 \to D_1$, $F_2 \colon C_2 \to D_2$, and $F_3 \colon C_3 \to D_3$, this defines a functor that takes a trifunctor $G \colon D_1 \to D_2 \to D_3 \to E$ and returns the composition $F_1 \circ F_2 \circ F_3 \circ G$ as a trifunctor $C_1 \to C_2 \to C_3 \to E$.
CategoryTheory.whiskeringLeft₃ObjObjMap definition
(F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) {F₃ F₃' : C₃ ⥤ D₃} (τ₃ : F₃ ⟶ F₃') : whiskeringLeft₃ObjObjObj E F₁ F₂ F₃ ⟶ whiskeringLeft₃ObjObjObj E F₁ F₂ F₃'
Full source 
/-- Auxiliary definition for `whiskeringLeft₃`. -/
@[simps]
def whiskeringLeft₃ObjObjMap (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) {F₃ F₃' : C₃ ⥤ D₃} (τ₃ : F₃ ⟶ F₃') :
    whiskeringLeft₃ObjObjObjwhiskeringLeft₃ObjObjObj E F₁ F₂ F₃ ⟶
      whiskeringLeft₃ObjObjObj E F₁ F₂ F₃' where
  app F := whiskerLeft _ (whiskerLeft _ (((whiskeringLeft₂ E).obj F₂).map τ₃))
Natural transformation induced by left whiskering in triple composition
Informal description
Given functors \( F_1 \colon C_1 \to D_1 \), \( F_2 \colon C_2 \to D_2 \), and a natural transformation \( \tau_3 \colon F_3 \to F_3' \) between functors \( F_3, F_3' \colon C_3 \to D_3 \), the map `whiskeringLeft₃ObjObjMap` constructs a natural transformation from the trifunctor \( F_1 \circ F_2 \circ F_3 \circ G \) to \( F_1 \circ F_2 \circ F_3' \circ G \) for any trifunctor \( G \colon D_1 \to D_2 \to D_3 \to E \). This is achieved by left whiskering \( \tau_3 \) with \( F_2 \) and then with \( F_1 \).
CategoryTheory.whiskeringLeft₃ObjObj definition
(F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) : (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E)
Full source 
/-- Auxiliary definition for `whiskeringLeft₃`. -/
@[simps]
def whiskeringLeft₃ObjObj (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) :
    (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) where
  obj F₃ := whiskeringLeft₃ObjObjObj E F₁ F₂ F₃
  map τ₃ := whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃
Double left whiskering functor for triple composition
Informal description
Given functors \( F_1 \colon C_1 \to D_1 \) and \( F_2 \colon C_2 \to D_2 \), this defines a functor that takes a functor \( F_3 \colon C_3 \to D_3 \) and returns a functor which maps a trifunctor \( G \colon D_1 \to D_2 \to D_3 \to E \) to the composition \( F_1 \circ F_2 \circ F_3 \circ G \) as a trifunctor \( C_1 \to C_2 \to C_3 \to E \). The construction also naturally transforms \( F_3 \) via left whiskering with \( F_1 \) and \( F_2 \).
CategoryTheory.whiskeringLeft₃ObjMap definition
(F₁ : C₁ ⥤ D₁) {F₂ F₂' : C₂ ⥤ D₂} (τ₂ : F₂ ⟶ F₂') : whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂ ⟶ whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂'
Full source 
/-- Auxiliary definition for `whiskeringLeft₃`. -/
@[simps]
def whiskeringLeft₃ObjMap (F₁ : C₁ ⥤ D₁) {F₂ F₂' : C₂ ⥤ D₂} (τ₂ : F₂ ⟶ F₂') :
    whiskeringLeft₃ObjObjwhiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂ ⟶ whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂' where
  app F₃ := whiskerRight ((whiskeringRight _ _ _).map (((whiskeringLeft₂ E).map τ₂).app F₃)) _
Natural transformation induced by left whiskering in triple composition for middle functor
Informal description
Given functors \( F_1 \colon C_1 \to D_1 \) and a natural transformation \( \tau_2 \colon F_2 \to F_2' \) between functors \( F_2, F_2' \colon C_2 \to D_2 \), the map `whiskeringLeft₃ObjMap` constructs a natural transformation from the functor \( \text{whiskeringLeft₃ObjObj}\, C_3\, D_3\, E\, F_1\, F_2 \) to \( \text{whiskeringLeft₃ObjObj}\, C_3\, D_3\, E\, F_1\, F_2' \). This is achieved by right whiskering the natural transformation obtained from applying \( \tau_2 \) to \( F_3 \) via the double left whiskering functor.
CategoryTheory.whiskeringLeft₃Obj definition
(F₁ : C₁ ⥤ D₁) : (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E)
Full source 
/-- Auxiliary definition for `whiskeringLeft₃`. -/
@[simps]
def whiskeringLeft₃Obj (F₁ : C₁ ⥤ D₁) :
    (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) where
  obj F₂ := whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂
  map τ₂ := whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂
Left whiskering functor for triple composition (first functor)
Informal description
Given a functor \( F_1 \colon C_1 \to D_1 \), the construction `whiskeringLeft₃Obj` defines a functor that takes a functor \( F_2 \colon C_2 \to D_2 \) and returns a functor which maps a functor \( F_3 \colon C_3 \to D_3 \) to a functor transforming a trifunctor \( G \colon D_1 \to D_2 \to D_3 \to E \) into the composition \( F_1 \circ F_2 \circ F_3 \circ G \) as a trifunctor \( C_1 \to C_2 \to C_3 \to E \). This operation is part of the left whiskering construction for triple composition of functors.
CategoryTheory.whiskeringLeft₃Map definition
{F₁ F₁' : C₁ ⥤ D₁} (τ₁ : F₁ ⟶ F₁') : whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁ ⟶ whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁'
Full source 
/-- Auxiliary definition for `whiskeringLeft₃`. -/
@[simps]
def whiskeringLeft₃Map {F₁ F₁' : C₁ ⥤ D₁} (τ₁ : F₁ ⟶ F₁') :
    whiskeringLeft₃ObjwhiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁ ⟶ whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁' where
  app F₂ := { app F₃ := whiskerLeft _ ((whiskeringLeft _ _ _).map τ₁) }
Natural transformation induced by left whiskering in triple composition for first functor
Informal description
Given a natural transformation $\tau_1 \colon F_1 \to F_1'$ between functors $F_1, F_1' \colon C_1 \to D_1$, the map `whiskeringLeft₃Map` constructs a natural transformation from the functor $\text{whiskeringLeft₃Obj}\, C_2\, C_3\, D_2\, D_3\, E\, F_1$ to $\text{whiskeringLeft₃Obj}\, C_2\, C_3\, D_2\, D_3\, E\, F_1'$. This is achieved by left whiskering $\tau_1$ with the appropriate functors in the triple composition context.
CategoryTheory.whiskeringLeft₃ definition
: (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E)
Full source 
/-- The obvious functor
`(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E)`. -/
@[simps!]
def whiskeringLeft₃ :
    (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) where
  obj F₁ := whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁
  map τ₁ := whiskeringLeft₃Map C₂ C₃ D₂ D₃ E τ₁
Left whiskering functor for triple composition
Informal description
The functor `whiskeringLeft₃` constructs a higher-order functor that takes a functor $F_1 \colon C_1 \to D_1$ and returns a functor which, given functors $F_2 \colon C_2 \to D_2$ and $F_3 \colon C_3 \to D_3$, transforms a trifunctor $G \colon D_1 \to D_2 \to D_3 \to E$ into the composition $F_1 \circ F_2 \circ F_3 \circ G$ as a trifunctor $C_1 \to C_2 \to C_3 \to E$. This operation is part of the left whiskering construction for triple composition of functors.
CategoryTheory.Functor.postcompose₂ definition
{E' : Type*} [Category E'] : (E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E'
Full source 
/-- The "postcomposition" with a functor `E ⥤ E'` gives a functor
`(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E'`. -/
@[simps!]
def Functor.postcompose₂ {E' : Type*} [Category E'] :
    (E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E' :=
  whiskeringRightwhiskeringRight C₂ _ _ ⋙ whiskeringRight C₁ _ _
Double postcomposition functor
Informal description
The functor that postcomposes a functor $F \colon E \to E'$ with functors from $C_1 \times C_2 \to E$ to obtain functors from $C_1 \times C_2 \to E'$. Specifically, it takes $F$ and produces a functor that maps any functor $G \colon C_1 \times C_2 \to E$ to the composition $F \circ G$.
CategoryTheory.Functor.postcompose₃ definition
{E' : Type*} [Category E'] : (E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E'
Full source 
/-- The "postcomposition" with a functor `E ⥤ E'` gives a functor
`(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E'`. -/
@[simps!]
def Functor.postcompose₃ {E' : Type*} [Category E'] :
    (E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E' :=
  whiskeringRightwhiskeringRight C₃ _ _ ⋙ whiskeringRight C₂ _ _ ⋙ whiskeringRight C₁ _ _
Triple postcomposition functor
Informal description
The functor that postcomposes a functor $F \colon E \to E'$ with functors from $C_1 \times C_2 \times C_3 \to E$ to obtain functors from $C_1 \times C_2 \times C_3 \to E'$. Specifically, it takes $F$ and produces a functor that maps any functor $G \colon C_1 \times C_2 \times C_3 \to E$ to the composition $F \circ G$.