mathlib documentation

category_theory.whiskering

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 whisker_left F α. This is the same as the horizontal composition of 𝟙 F with α.

This operation is functorial in F, and we package this as whiskering_left. Here (whiskering_left.obj F).obj G is F ⋙ G, and (whiskering_left.obj F).map α is whisker_left 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 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) :

(category_theory.whisker_left F α).app X = α.app (F.obj X)

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

category_theory.whisker_left F α = {app := λ (X : C), α.app (F.obj X), naturality' := _}

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

category_theory.whisker_right α F = {app := λ (X : C), F.map (α.app X), 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) (X : C) :

(category_theory.whisker_right α F).app X = F.map (α.app X)

@[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_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

@[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_left.obj F).obj G is F ⋙ G, and (whiskering_left.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' := _}

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

(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

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.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_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} :

category_theory.whisker_left F (category_theory.nat_trans.id G) = category_theory.nat_trans.id (F ⋙ G)

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

category_theory.whisker_right (category_theory.nat_trans.id G) F = category_theory.nat_trans.id (G ⋙ F)

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

category_theory.whisker_left F (α ≫ β) = category_theory.whisker_left F α ≫ category_theory.whisker_left F β

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

category_theory.whisker_right (α ≫ β) F = category_theory.whisker_right α F ≫ category_theory.whisker_right β F

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

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

(category_theory.iso_whisker_left F α).hom = category_theory.whisker_left F α.hom

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

(category_theory.iso_whisker_left F α).inv = category_theory.whisker_left F α.inv

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) ≅ (H ⋙ 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 α

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

(category_theory.iso_whisker_right α F).hom = category_theory.whisker_right α.hom F

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

(category_theory.iso_whisker_right α F).inv = category_theory.whisker_right α.inv F

@[protected, 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 α] :

category_theory.is_iso (category_theory.whisker_left F α)

@[protected, 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 α] :

category_theory.is_iso (category_theory.whisker_right α F)

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

category_theory.whisker_left F (category_theory.whisker_left G α) = category_theory.whisker_left (F ⋙ G) α

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

category_theory.whisker_right (category_theory.whisker_right α F) G = category_theory.whisker_right α (F ⋙ G)

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

category_theory.whisker_right (category_theory.whisker_left F α) K = category_theory.whisker_left F (category_theory.whisker_right α 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) :

F.left_unitor.hom.app X = 𝟙 (F.obj X)

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

F.left_unitor.inv.app X = 𝟙 (F.obj X)

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

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

F.right_unitor.inv.app X = 𝟙 (F.obj X)

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

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' := _}

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

F.right_unitor.hom.app X = 𝟙 (F.obj X)

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

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

(F.associator G H).hom.app _x = 𝟙 (((F ⋙ G) ⋙ H).obj _x)

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