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.

Equations

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

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.

Equations

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

Instances For

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

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

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

Instances For

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

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

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

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.

Equations

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

Instances For

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

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

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_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.CategoryStruct.id F).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (CategoryTheory.Bicategory.leftUnitor (F.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_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_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

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

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

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.

Documentation

Mathlib.CategoryTheory.Bicategory.FunctorBicategory

The bicategory of oplax functors between two bicategories #