The bicategory of oplax functors between two bicategories

Given bicategories B and C, we give a bicategory structure on OplaxFunctor B C whose

• objects are oplax functors,
• 1-morphisms are oplax natural transformations, and
• 2-morphisms are modifications.

@[simp]

theorem CategoryTheory.OplaxNatTrans.whiskerLeft_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) {θ : G ⟶ H} {ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B) : (CategoryTheory.OplaxNatTrans.whiskerLeft η Γ).app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a)

def CategoryTheory.OplaxNatTrans.whiskerLeft {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) {θ : G ⟶ H} {ι : G ⟶ H} (Γ : θ ⟶ ι) : CategoryTheory.CategoryStruct.comp η θ ⟶ CategoryTheory.CategoryStruct.comp η ι

Left whiskering of an oplax natural transformation and a modification.

Equations

• CategoryTheory.OplaxNatTrans.whiskerLeft η Γ = { app := fun (a : B) => CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.OplaxNatTrans.whiskerRight_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B) : (CategoryTheory.OplaxNatTrans.whiskerRight Γ ι).app a = CategoryTheory.Bicategory.whiskerRight (Γ.app a) (ι.app a)

def CategoryTheory.OplaxNatTrans.whiskerRight {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) : CategoryTheory.CategoryStruct.comp η ι ⟶ CategoryTheory.CategoryStruct.comp θ ι

Right whiskering of an oplax natural transformation and a modification.

Equations

• CategoryTheory.OplaxNatTrans.whiskerRight Γ ι = { app := fun (a : B) => CategoryTheory.Bicategory.whiskerRight (Γ.app a) (ι.app a), naturality := ⋯ }

@[simp]

theorem CategoryTheory.OplaxNatTrans.associator_hom_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} {I : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) : (CategoryTheory.OplaxNatTrans.associator η θ ι).hom.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

@[simp]

theorem CategoryTheory.OplaxNatTrans.associator_inv_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} {I : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) : (CategoryTheory.OplaxNatTrans.associator η θ ι).inv.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

def CategoryTheory.OplaxNatTrans.associator {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} {I : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι ≅ CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι)

Associator for the vertical composition of oplax natural transformations.

Equations

• CategoryTheory.OplaxNatTrans.associator η θ ι = CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents (fun (a : B) => CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)) ⋯

@[simp]

theorem CategoryTheory.OplaxNatTrans.leftUnitor_hom_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B) : (CategoryTheory.OplaxNatTrans.leftUnitor η).hom.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom

@[simp]

theorem CategoryTheory.OplaxNatTrans.leftUnitor_inv_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B) : (CategoryTheory.OplaxNatTrans.leftUnitor η).inv.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv

def CategoryTheory.OplaxNatTrans.leftUnitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id F) η ≅ η

Left unitor for the vertical composition of oplax natural transformations.

Equations

• CategoryTheory.OplaxNatTrans.leftUnitor η = CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents (fun (a : B) => CategoryTheory.Bicategory.leftUnitor (η.app a)) ⋯

@[simp]

theorem CategoryTheory.OplaxNatTrans.rightUnitor_hom_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B) : (CategoryTheory.OplaxNatTrans.rightUnitor η).hom.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom

@[simp]

theorem CategoryTheory.OplaxNatTrans.rightUnitor_inv_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B) : (CategoryTheory.OplaxNatTrans.rightUnitor η).inv.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv

def CategoryTheory.OplaxNatTrans.rightUnitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.id G) ≅ η

Right unitor for the vertical composition of oplax natural transformations.

Equations

• CategoryTheory.OplaxNatTrans.rightUnitor η = CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents (fun (a : B) => CategoryTheory.Bicategory.rightUnitor (η.app a)) ⋯

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_homCategory_comp_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (a : CategoryTheory.OplaxFunctor B C) (b : CategoryTheory.OplaxFunctor B C) : ∀ {X Y Z : a ⟶ b} (Γ : CategoryTheory.OplaxNatTrans.Modification X Y) (Δ : CategoryTheory.OplaxNatTrans.Modification Y Z) (a_1 : B), (CategoryTheory.CategoryStruct.comp Γ Δ).app a_1 = CategoryTheory.CategoryStruct.comp (Γ.app a_1) (Δ.app a_1)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_whiskerRight_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 x_4 : x ⟶ x_1) (Γ : x_3 ⟶ x_4) (η : x_1 ⟶ x_2) (a : B), (CategoryTheory.Bicategory.whiskerRight Γ η).app a = CategoryTheory.Bicategory.whiskerRight (Γ.app a) (η.app a)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_whiskerLeft_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (x_3 x_4 : x_1 ⟶ x_2) (Γ : x_3 ⟶ x_4) (a : B), (CategoryTheory.Bicategory.whiskerLeft η Γ).app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_id_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) : (CategoryTheory.CategoryStruct.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_associator_inv_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2) (ι : x_2 ⟶ x_3) (a : B), (CategoryTheory.Bicategory.associator η θ ι).inv.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_id_naturality (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) : ∀ {x x_1 : B} (f : x ⟶ x_1), (CategoryTheory.CategoryStruct.id F).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_leftUnitor_inv_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B), (CategoryTheory.Bicategory.leftUnitor η).inv.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_rightUnitor_inv_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B), (CategoryTheory.Bicategory.rightUnitor η).inv.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_comp_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.OplaxNatTrans X Y) (θ : CategoryTheory.OplaxNatTrans Y Z) (a : B), (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_Hom (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor B C) : (F ⟶ G) = CategoryTheory.OplaxNatTrans F G

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_leftUnitor_hom_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B), (CategoryTheory.Bicategory.leftUnitor η).hom.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_associator_hom_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2) (ι : x_2 ⟶ x_3) (a : B), (CategoryTheory.Bicategory.associator η θ ι).hom.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_homCategory_id_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (a : CategoryTheory.OplaxFunctor B C) (b : CategoryTheory.OplaxFunctor B C) (η : a✝ ⟶ b) (a : B) : (CategoryTheory.CategoryStruct.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_comp_naturality (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.OplaxNatTrans X Y) (θ : CategoryTheory.OplaxNatTrans Y Z) {a b : B} (f : a ⟶ b), (CategoryTheory.CategoryStruct.comp η θ).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (θ.app b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f)) (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).inv)))

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_rightUnitor_hom_app (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : ∀ {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B), (CategoryTheory.Bicategory.rightUnitor η).hom.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom

instance CategoryTheory.OplaxFunctor.bicategory (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] : CategoryTheory.Bicategory (CategoryTheory.OplaxFunctor B C)

A bicategory structure on the oplax functors between bicategories.

Equations

• One or more equations did not get rendered due to their size.