def
category_theory.whisker_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G H : D ⥤ E} :
Equations
- category_theory.whisker_left F α = {app := λ (c : C), α.app (F.obj c), naturality' := _}
@[simp]
theorem
category_theory.whisker_left_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G H : D ⥤ E}
(α : G ⟶ H)
(c : C) :
(category_theory.whisker_left F α).app c = α.app (F.obj c)
def
category_theory.whisker_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G H : C ⥤ D}
(α : G ⟶ H)
(F : D ⥤ E) :
Equations
- category_theory.whisker_right α F = {app := λ (c : C), F.map (α.app c), naturality' := _}
@[simp]
theorem
category_theory.whisker_right_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G H : C ⥤ D}
(α : G ⟶ H)
(F : D ⥤ E)
(c : C) :
(category_theory.whisker_right α F).app c = F.map (α.app c)
@[simp]
theorem
category_theory.whiskering_left_obj_obj
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E) :
((category_theory.whiskering_left C D E).obj F).obj G = F ⋙ G
def
category_theory.whiskering_left
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E] :
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' := _}
@[simp]
theorem
category_theory.whiskering_left_obj_map
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(F : C ⥤ D)
(G H : D ⥤ E)
(α : G ⟶ H) :
((category_theory.whiskering_left C D E).obj F).map α = category_theory.whisker_left F α
@[simp]
theorem
category_theory.whiskering_left_map_app_app
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(F G : C ⥤ D)
(τ : F ⟶ G)
(H : D ⥤ E)
(c : C) :
@[simp]
theorem
category_theory.whiskering_right_map_app_app
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(G H : D ⥤ E)
(τ : G ⟶ H)
(F : C ⥤ D)
(c : C) :
@[simp]
theorem
category_theory.whiskering_right_obj_obj
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(H : D ⥤ E)
(F : C ⥤ D) :
((category_theory.whiskering_right C D E).obj H).obj F = F ⋙ H
@[simp]
theorem
category_theory.whiskering_right_obj_map
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E]
(H : D ⥤ E)
(_x _x_1 : C ⥤ D)
(α : _x ⟶ _x_1) :
((category_theory.whiskering_right C D E).obj H).map α = category_theory.whisker_right α H
def
category_theory.whiskering_right
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
(E : Type u₃)
[category_theory.category E] :
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' := _}
@[simp]
theorem
category_theory.whisker_left_id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G : D ⥤ E} :
@[simp]
theorem
category_theory.whisker_left_id'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G : D ⥤ E} :
category_theory.whisker_left F (𝟙 G) = 𝟙 (F ⋙ G)
@[simp]
theorem
category_theory.whisker_right_id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G : C ⥤ D}
(F : D ⥤ E) :
@[simp]
theorem
category_theory.whisker_right_id'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G : C ⥤ D}
(F : D ⥤ E) :
category_theory.whisker_right (𝟙 G) F = 𝟙 (G ⋙ F)
@[simp]
theorem
category_theory.whisker_left_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G H K : D ⥤ E}
(α : G ⟶ H)
(β : H ⟶ K) :
@[simp]
theorem
category_theory.whisker_right_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G H K : C ⥤ D}
(α : G ⟶ H)
(β : H ⟶ K)
(F : D ⥤ E) :
def
category_theory.iso_whisker_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G H : D ⥤ E} :
Equations
- category_theory.iso_whisker_left F α = ((category_theory.whiskering_left C D E).obj F).map_iso α
@[simp]
theorem
category_theory.iso_whisker_left_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G H : D ⥤ E}
(α : G ≅ H) :
@[simp]
theorem
category_theory.iso_whisker_left_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G H : D ⥤ E}
(α : G ≅ H) :
def
category_theory.iso_whisker_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G H : C ⥤ D}
(α : G ≅ H)
(F : D ⥤ E) :
Equations
- category_theory.iso_whisker_right α F = ((category_theory.whiskering_right C D E).obj F).map_iso α
@[simp]
theorem
category_theory.iso_whisker_right_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G H : C ⥤ D}
(α : G ≅ H)
(F : D ⥤ E) :
@[simp]
theorem
category_theory.iso_whisker_right_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G H : C ⥤ D}
(α : G ≅ H)
(F : D ⥤ E) :
@[instance]
def
category_theory.is_iso_whisker_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
{G H : D ⥤ E}
(α : G ⟶ H)
[category_theory.is_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' := _}
@[instance]
def
category_theory.is_iso_whisker_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{G H : C ⥤ D}
(α : G ⟶ H)
(F : D ⥤ E)
[category_theory.is_iso α] :
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' := _}
@[simp]
theorem
category_theory.whisker_left_twice
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
{H K : D ⥤ E}
(α : H ⟶ K) :
@[simp]
theorem
category_theory.whisker_right_twice
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{B : Type u₄}
[category_theory.category B]
{H K : B ⥤ C}
(F : C ⥤ D)
(G : D ⥤ E)
(α : H ⟶ K) :
theorem
category_theory.whisker_right_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
{G H : C ⥤ D}
(α : G ⟶ H)
(K : D ⥤ E) :
@[simp]
theorem
category_theory.functor.left_unitor_inv_app
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
(F : A ⥤ B)
(X : A) :
@[simp]
theorem
category_theory.functor.left_unitor_hom_app
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
(F : A ⥤ B)
(X : A) :
def
category_theory.functor.left_unitor
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
(F : A ⥤ B) :
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' := _}
@[simp]
theorem
category_theory.functor.right_unitor_inv_app
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
(F : A ⥤ B)
(X : A) :
@[simp]
theorem
category_theory.functor.right_unitor_hom_app
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
(F : A ⥤ B)
(X : A) :
def
category_theory.functor.right_unitor
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
(F : A ⥤ B) :
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' := _}
def
category_theory.functor.associator
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : A ⥤ B)
(G : B ⥤ C)
(H : C ⥤ D) :
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' := _}
@[simp]
theorem
category_theory.functor.associator_hom_app
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : A ⥤ B)
(G : B ⥤ C)
(H : C ⥤ D)
(_x : A) :
@[simp]
theorem
category_theory.functor.associator_inv_app
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
(F : A ⥤ B)
(G : B ⥤ C)
(H : C ⥤ D)
(_x : A) :
theorem
category_theory.functor.triangle
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{C : Type u₃}
[category_theory.category C]
(F : A ⥤ B)
(G : B ⥤ C) :
(F.associator (𝟭 B) G).hom ≫ category_theory.whisker_left F G.left_unitor.hom = category_theory.whisker_right F.right_unitor.hom G
theorem
category_theory.functor.pentagon
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{E : Type u₅}
[category_theory.category E]
(F : A ⥤ B)
(G : B ⥤ C)
(H : C ⥤ D)
(K : D ⥤ E) :
category_theory.whisker_right (F.associator G H).hom K ≫ (F.associator (G ⋙ H) K).hom ≫ category_theory.whisker_left F (G.associator H K).hom = ((F ⋙ G).associator H K).hom ≫ (F.associator G (H ⋙ K)).hom