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.
At the end of the file, we provide the left and right unitors, and the associator, for functor composition. (In fact functor composition is definitionally associative, but very often relying on this causes extremely slow elaboration, so it is better to insert it explicitly.) We also show these natural isomorphisms satisfy the triangle and pentagon identities.
@[simp]
theorem
CategoryTheory.whiskerLeft_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
(α : G ⟶ H)
(X : C)
:
(CategoryTheory.whiskerLeft F α).app X = α.app (F.obj X)
@[elab_without_expected_type]
def
CategoryTheory.whiskerLeft
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
(α : G ⟶ H)
:
F.comp G ⟶ F.comp 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 := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.whiskerRight_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
(α : G ⟶ H)
(F : CategoryTheory.Functor D E)
(X : C)
:
(CategoryTheory.whiskerRight α F).app X = F.map (α.app X)
@[elab_without_expected_type]
def
CategoryTheory.whiskerRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
(α : G ⟶ H)
(F : CategoryTheory.Functor D E)
:
G.comp F ⟶ H.comp F
If α : G ⟶ H then
whisker_right α 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
@[simp]
theorem
CategoryTheory.whiskeringLeft_obj_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
:
∀ {X Y : CategoryTheory.Functor D E} (α : X ⟶ Y),
((CategoryTheory.whiskeringLeft C D E).obj F).map α = CategoryTheory.whiskerLeft F α
@[simp]
theorem
CategoryTheory.whiskeringLeft_map_app_app
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
:
∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (H : CategoryTheory.Functor D E) (c : C),
(((CategoryTheory.whiskeringLeft C D E).map τ).app H).app c = H.map (τ.app c)
@[simp]
theorem
CategoryTheory.whiskeringLeft_obj_obj
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
:
((CategoryTheory.whiskeringLeft C D E).obj F).obj G = F.comp G
def
CategoryTheory.whiskeringLeft
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
:
Left-composition gives a functor (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)).
(whiskeringLeft.obj F).obj G is F ⋙ G, and
(whiskeringLeft.obj F).map α is whiskerLeft F α.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.whiskeringRight_obj_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
(H : CategoryTheory.Functor D E)
:
∀ {X Y : CategoryTheory.Functor C D} (α : X ⟶ Y),
((CategoryTheory.whiskeringRight C D E).obj H).map α = CategoryTheory.whiskerRight α H
@[simp]
theorem
CategoryTheory.whiskeringRight_map_app_app
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
:
∀ {X Y : CategoryTheory.Functor D E} (τ : X ⟶ Y) (F : CategoryTheory.Functor C D) (c : C),
(((CategoryTheory.whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c)
@[simp]
theorem
CategoryTheory.whiskeringRight_obj_obj
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
(H : CategoryTheory.Functor D E)
(F : CategoryTheory.Functor C D)
:
((CategoryTheory.whiskeringRight C D E).obj H).obj F = F.comp H
def
CategoryTheory.whiskeringRight
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
(E : Type u₃)
[CategoryTheory.Category.{v₃, u₃} E]
:
Right-composition gives a functor (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)).
(whiskeringRight.obj H).obj F is F ⋙ H, and
(whiskeringRight.obj H).map α is whiskerRight α H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.faithful_whiskeringRight_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor D E}
[F.Faithful]
:
((CategoryTheory.whiskeringRight C D E).obj F).Faithful
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.whiskeringRight_preimage_app
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor D E}
(hF : F.FullyFaithful)
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
:
∀ {X Y : CategoryTheory.Functor C D}
(f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y)
(X_1 : C), ((hF.whiskeringRight C).preimage f).app X_1 = hF.preimage (f.app X_1)
def
CategoryTheory.Functor.FullyFaithful.whiskeringRight
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor D E}
(hF : F.FullyFaithful)
(C : Type u_1)
[CategoryTheory.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.
Instances For
instance
CategoryTheory.full_whiskeringRight_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor D E}
[F.Faithful]
[F.Full]
:
((CategoryTheory.whiskeringRight C D E).obj F).Full
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.whiskerLeft_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
:
CategoryTheory.whiskerLeft F (CategoryTheory.NatTrans.id G) = CategoryTheory.NatTrans.id (F.comp G)
@[simp]
theorem
CategoryTheory.whiskerLeft_id'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
:
@[simp]
theorem
CategoryTheory.whiskerRight_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
(F : CategoryTheory.Functor D E)
:
CategoryTheory.whiskerRight (CategoryTheory.NatTrans.id G) F = CategoryTheory.NatTrans.id (G.comp F)
@[simp]
theorem
CategoryTheory.whiskerRight_id'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
(F : CategoryTheory.Functor D E)
:
theorem
CategoryTheory.whiskerLeft_comp_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
{K : CategoryTheory.Functor D E}
(α : G ⟶ H)
(β : H ⟶ K)
{Z : CategoryTheory.Functor C E}
(h : F.comp K ⟶ Z)
:
@[simp]
theorem
CategoryTheory.whiskerLeft_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
{K : CategoryTheory.Functor D E}
(α : G ⟶ H)
(β : H ⟶ K)
:
theorem
CategoryTheory.whiskerRight_comp_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
{K : CategoryTheory.Functor C D}
(α : G ⟶ H)
(β : H ⟶ K)
(F : CategoryTheory.Functor D E)
{Z : CategoryTheory.Functor C E}
(h : K.comp F ⟶ Z)
:
@[simp]
theorem
CategoryTheory.whiskerRight_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
{K : CategoryTheory.Functor C D}
(α : G ⟶ H)
(β : H ⟶ K)
(F : CategoryTheory.Functor D E)
:
def
CategoryTheory.isoWhiskerLeft
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
(α : G ≅ H)
:
F.comp G ≅ F.comp H
If α : G ≅ H is a natural isomorphism then
iso_whisker_left F α : (F ⋙ G) ≅ (F ⋙ H) has components α.app (F.obj X).
Equations
- CategoryTheory.isoWhiskerLeft F α = ((CategoryTheory.whiskeringLeft C D E).obj F).mapIso α
Instances For
@[simp]
theorem
CategoryTheory.isoWhiskerLeft_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
(α : G ≅ H)
:
(CategoryTheory.isoWhiskerLeft F α).hom = CategoryTheory.whiskerLeft F α.hom
@[simp]
theorem
CategoryTheory.isoWhiskerLeft_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
(α : G ≅ H)
:
(CategoryTheory.isoWhiskerLeft F α).inv = CategoryTheory.whiskerLeft F α.inv
def
CategoryTheory.isoWhiskerRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
(α : G ≅ H)
(F : CategoryTheory.Functor D E)
:
G.comp F ≅ H.comp F
If α : G ≅ H then
iso_whisker_right α F : (G ⋙ F) ≅ (H ⋙ F) has components F.map_iso (α.app X).
Equations
- CategoryTheory.isoWhiskerRight α F = ((CategoryTheory.whiskeringRight C D E).obj F).mapIso α
Instances For
@[simp]
theorem
CategoryTheory.isoWhiskerRight_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
(α : G ≅ H)
(F : CategoryTheory.Functor D E)
:
(CategoryTheory.isoWhiskerRight α F).hom = CategoryTheory.whiskerRight α.hom F
@[simp]
theorem
CategoryTheory.isoWhiskerRight_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
(α : G ≅ H)
(F : CategoryTheory.Functor D E)
:
(CategoryTheory.isoWhiskerRight α F).inv = CategoryTheory.whiskerRight α.inv F
instance
CategoryTheory.isIso_whiskerLeft
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor D E}
(α : G ⟶ H)
[CategoryTheory.IsIso α]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.isIso_whiskerRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
(α : G ⟶ H)
(F : CategoryTheory.Functor D E)
[CategoryTheory.IsIso α]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.whiskerLeft_twice
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(F : CategoryTheory.Functor B C)
(G : CategoryTheory.Functor C D)
{H : CategoryTheory.Functor D E}
{K : CategoryTheory.Functor D E}
(α : H ⟶ K)
:
CategoryTheory.whiskerLeft F (CategoryTheory.whiskerLeft G α) = CategoryTheory.whiskerLeft (F.comp G) α
@[simp]
theorem
CategoryTheory.whiskerRight_twice
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
{H : CategoryTheory.Functor B C}
{K : CategoryTheory.Functor B C}
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
(α : H ⟶ K)
:
CategoryTheory.whiskerRight (CategoryTheory.whiskerRight α F) G = CategoryTheory.whiskerRight α (F.comp G)
theorem
CategoryTheory.whiskerRight_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{B : Type u₄}
[CategoryTheory.Category.{v₄, u₄} B]
(F : CategoryTheory.Functor B C)
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
(α : G ⟶ H)
(K : CategoryTheory.Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.leftUnitor_hom_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(F : CategoryTheory.Functor A B)
(X : A)
:
F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem
CategoryTheory.Functor.leftUnitor_inv_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(F : CategoryTheory.Functor A B)
(X : A)
:
F.leftUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def
CategoryTheory.Functor.leftUnitor
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(F : CategoryTheory.Functor A B)
:
(CategoryTheory.Functor.id A).comp F ≅ F
The left unitor, a natural isomorphism ((𝟭 _) ⋙ F) ≅ F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.rightUnitor_inv_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(F : CategoryTheory.Functor A B)
(X : A)
:
F.rightUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem
CategoryTheory.Functor.rightUnitor_hom_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(F : CategoryTheory.Functor A B)
(X : A)
:
F.rightUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def
CategoryTheory.Functor.rightUnitor
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
(F : CategoryTheory.Functor A B)
:
F.comp (CategoryTheory.Functor.id B) ≅ F
The right unitor, a natural isomorphism (F ⋙ (𝟭 B)) ≅ F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.associator_hom_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor A B)
(G : CategoryTheory.Functor B C)
(H : CategoryTheory.Functor C D)
:
∀ (x : A), (F.associator G H).hom.app x = CategoryTheory.CategoryStruct.id (((F.comp G).comp H).obj x)
@[simp]
theorem
CategoryTheory.Functor.associator_inv_app
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor A B)
(G : CategoryTheory.Functor B C)
(H : CategoryTheory.Functor C D)
:
∀ (x : A), (F.associator G H).inv.app x = CategoryTheory.CategoryStruct.id ((F.comp (G.comp H)).obj x)
def
CategoryTheory.Functor.associator
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor A B)
(G : CategoryTheory.Functor B C)
(H : CategoryTheory.Functor C D)
:
(F.comp G).comp H ≅ F.comp (G.comp H)
The associator for functors, a natural isomorphism ((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H)).
(In fact, iso.refl _ will work here, but it tends to make Lean slow later,
and it's usually best to insert explicit associators.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.assoc
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
(F : CategoryTheory.Functor A B)
(G : CategoryTheory.Functor B C)
(H : CategoryTheory.Functor C D)
:
(F.comp G).comp H = F.comp (G.comp H)
theorem
CategoryTheory.Functor.triangle
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
(F : CategoryTheory.Functor A B)
(G : CategoryTheory.Functor B C)
:
CategoryTheory.CategoryStruct.comp (F.associator (CategoryTheory.Functor.id B) G).hom
(CategoryTheory.whiskerLeft F G.leftUnitor.hom) = CategoryTheory.whiskerRight F.rightUnitor.hom G
theorem
CategoryTheory.Functor.pentagon
{A : Type u₁}
[CategoryTheory.Category.{v₁, u₁} A]
{B : Type u₂}
[CategoryTheory.Category.{v₂, u₂} B]
{C : Type u₃}
[CategoryTheory.Category.{v₃, u₃} C]
{D : Type u₄}
[CategoryTheory.Category.{v₄, u₄} D]
{E : Type u₅}
[CategoryTheory.Category.{v₅, u₅} E]
(F : CategoryTheory.Functor A B)
(G : CategoryTheory.Functor B C)
(H : CategoryTheory.Functor C D)
(K : CategoryTheory.Functor D E)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (F.associator G H).hom K)
(CategoryTheory.CategoryStruct.comp (F.associator (G.comp H) K).hom
(CategoryTheory.whiskerLeft F (G.associator H K).hom)) = CategoryTheory.CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom