mathlib documentation

category_theory.whiskering

@[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) (X : C) :

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} :
(G H)(F G F H)

If α : G ⟶ H then whisker_left F α : (F ⋙ G) ⟶ (F ⋙ H) has components α.app (F.obj X).

Equations
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) :
G F H F

If α : G ⟶ H then whisker_right α F : (G ⋙ F) ⟶ (G ⋙ F) has components F.map (α.app X).

Equations
@[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) (X : C) :

@[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) :

@[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) :

@[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) :
(((category_theory.whiskering_left C D E).map τ).app H).app c = H.map (τ.app c)

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] :
(C D) (D E) C E

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
@[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) :

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] :
(D E) (C D) C E

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
@[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) :

@[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) :
(((category_theory.whiskering_right C D E).map τ).app F).app c = τ.app (F.obj c)

@[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_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_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} :
(G H)(F G F H)

If α : G ≅ H is a natural isomorphism then iso_whisker_left F α : (F ⋙ G) ≅ (F ⋙ H) has components α.app (F.obj X).

Equations
@[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) :
G F H F

If α : G ≅ H then iso_whisker_right α F : (G ⋙ F) ≅ (G ⋙ F) has components F.map_iso (α.app X).

Equations
@[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) :

@[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) :

@[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) :

@[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) :

def category_theory.functor.left_unitor {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] (F : A B) :
𝟭 A F F

The left unitor, a natural isomorphism ((𝟭 _) ⋙ F) ≅ F.

Equations
@[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) :

def category_theory.functor.right_unitor {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] (F : A B) :
F 𝟭 B F

The right unitor, a natural isomorphism (F ⋙ (𝟭 B)) ≅ F.

Equations
@[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) :

@[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) :
(F.associator G H).inv.app _x = 𝟙 ((F G H).obj _x)

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) :
(F G) H F G 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
@[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) :
(F.associator G H).hom.app _x = 𝟙 (((F G) H).obj _x)

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) :