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)

source

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.

Instances For

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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} :

∀ (x x_1 : F ⟶ G) (Γ : x ⟶ x_1) (η : G ⟶ H) (a : B), (CategoryTheory.Bicategory.whiskerRight Γ η).app a = CategoryTheory.Bicategory.whiskerRight (Γ.app a) (η.app a)

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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.Bicategory.associator η θ ι).hom.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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.Bicategory.rightUnitor η).hom.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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.Bicategory.rightUnitor η).inv.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_id_naturality (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) :

CategoryTheory.OplaxNatTrans.naturality (CategoryTheory.CategoryStruct.id F) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor ((↑F.toPrelaxFunctor).map f)).hom (CategoryTheory.Bicategory.leftUnitor ((↑F.toPrelaxFunctor).map f)).inv

source

@[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 : B), (CategoryTheory.CategoryStruct.comp Γ Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)

source

@[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.toPrelaxFunctor).obj a)

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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.Bicategory.leftUnitor η).hom.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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) :

∀ (x x_1 : G ⟶ H) (Γ : x ⟶ x_1) (a : B), (CategoryTheory.Bicategory.whiskerLeft η Γ).app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a)

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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.Bicategory.associator η θ ι).inv.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

source

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

source

@[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.OplaxNatTrans.naturality (CategoryTheory.CategoryStruct.comp η θ) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑X.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxNatTrans.naturality η f) (θ.app b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) ((↑Y.toPrelaxFunctor).map f) (θ.app b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.OplaxNatTrans.naturality θ f)) (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) ((↑Z.toPrelaxFunctor).map f)).inv)))

source

@[simp]

theorem CategoryTheory.OplaxFunctor.bicategory_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.Bicategory.leftUnitor η).inv.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv

source

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

source

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

source

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.