If α : G ⟶ H
then
whisker_left F α : (F ⋙ G) ⟶ (F ⋙ H)
has components α.app (F.obj X)
.
Equations
- category_theory.whisker_left F α = {app := λ (X : C), α.app (F.obj X), naturality' := _}
If α : G ⟶ H
then
whisker_right α F : (G ⋙ F) ⟶ (G ⋙ F)
has components F.map (α.app X)
.
Equations
- category_theory.whisker_right α F = {app := λ (X : C), F.map (α.app X), naturality' := _}
Left-composition gives a functor (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E))
.
(whiskering_lift.obj F).obj G
is F ⋙ G
, and
(whiskering_lift.obj F).map α
is whisker_left F α
.
Equations
- category_theory.whiskering_left C D E = {obj := λ (F : C ⥤ D), {obj := λ (G : D ⥤ E), F ⋙ G, map := λ (G H : D ⥤ E) (α : G ⟶ H), category_theory.whisker_left F α, map_id' := _, map_comp' := _}, map := λ (F G : C ⥤ D) (τ : F ⟶ G), {app := λ (H : D ⥤ E), {app := λ (c : C), H.map (τ.app c), naturality' := _}, naturality' := _}, map_id' := _, map_comp' := _}
Right-composition gives a functor (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E))
.
(whiskering_right.obj H).obj F
is F ⋙ H
, and
(whiskering_right.obj H).map α
is whisker_right α H
.
Equations
- category_theory.whiskering_right C D E = {obj := λ (H : D ⥤ E), {obj := λ (F : C ⥤ D), F ⋙ H, map := λ (_x _x_1 : C ⥤ D) (α : _x ⟶ _x_1), category_theory.whisker_right α H, map_id' := _, map_comp' := _}, map := λ (G H : D ⥤ E) (τ : G ⟶ H), {app := λ (F : C ⥤ D), {app := λ (c : C), τ.app (F.obj c), naturality' := _}, naturality' := _}, map_id' := _, map_comp' := _}
If α : G ≅ H
is a natural isomorphism then
iso_whisker_left F α : (F ⋙ G) ≅ (F ⋙ H)
has components α.app (F.obj X)
.
Equations
- category_theory.iso_whisker_left F α = ((category_theory.whiskering_left C D E).obj F).map_iso α
If α : G ≅ H
then
iso_whisker_right α F : (G ⋙ F) ≅ (G ⋙ F)
has components F.map_iso (α.app X)
.
Equations
- category_theory.iso_whisker_right α F = ((category_theory.whiskering_right C D E).obj F).map_iso α
Equations
- category_theory.is_iso_whisker_left F α = {inv := (category_theory.iso_whisker_left F (category_theory.as_iso α)).inv, hom_inv_id' := _, inv_hom_id' := _}
Equations
- category_theory.is_iso_whisker_right α F = {inv := (category_theory.iso_whisker_right (category_theory.as_iso α) F).inv, hom_inv_id' := _, inv_hom_id' := _}
The left unitor, a natural isomorphism ((𝟭 _) ⋙ F) ≅ F
.
Equations
- F.left_unitor = {hom := {app := λ (X : A), 𝟙 (F.obj X), naturality' := _}, inv := {app := λ (X : A), 𝟙 (F.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
The right unitor, a natural isomorphism (F ⋙ (𝟭 B)) ≅ F
.
Equations
- F.right_unitor = {hom := {app := λ (X : A), 𝟙 (F.obj X), naturality' := _}, inv := {app := λ (X : A), 𝟙 (F.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
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
- F.associator G H = {hom := {app := λ (_x : A), 𝟙 (((F ⋙ G) ⋙ H).obj _x), naturality' := _}, inv := {app := λ (_x : A), 𝟙 ((F ⋙ G ⋙ H).obj _x), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}