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

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 α

source

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

source

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

source

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

category_theory.iso_whisker_right α F = ((category_theory.whiskering_right C D E).obj F).map_iso α

source

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

source

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

source

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

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

source

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

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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