Bicategories of lax functors #

Given bicategories B and C, we give bicategory structures on LaxFunctor B C whose

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

def CategoryTheory.Lax.LaxTrans.whiskerLeft {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) :

CategoryStruct.comp η θ ⟶ CategoryStruct.comp η ι

Left whiskering of a lax natural transformation and a modification.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.whiskerLeft_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B) :

(whiskerLeft η Γ).as.app a = Bicategory.whiskerLeft (η.app a) (Γ.as.app a)

source

def CategoryTheory.Lax.LaxTrans.whiskerRight {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) :

CategoryStruct.comp η ι ⟶ CategoryStruct.comp θ ι

Right whiskering of a lax natural transformation and a modification.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.whiskerRight_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B) :

(whiskerRight Γ ι).as.app a = Bicategory.whiskerRight (Γ.as.app a) (ι.app a)

source

def CategoryTheory.Lax.LaxTrans.associator {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) :

CategoryStruct.comp (CategoryStruct.comp η θ) ι ≅ CategoryStruct.comp η (CategoryStruct.comp θ ι)

Associator for the vertical composition of lax natural transformations.

Equations

CategoryTheory.Lax.LaxTrans.associator η θ ι = CategoryTheory.Lax.LaxTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.associator_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :

(associator η θ ι).hom.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.associator_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :

(associator η θ ι).inv.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

source

def CategoryTheory.Lax.LaxTrans.leftUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) :

CategoryStruct.comp (CategoryStruct.id F) η ≅ η

Left unitor for the vertical composition of lax natural transformations.

Equations

CategoryTheory.Lax.LaxTrans.leftUnitor η = CategoryTheory.Lax.LaxTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.leftUnitor (η.app a)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.leftUnitor_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(leftUnitor η).inv.as.app a = (Bicategory.leftUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.leftUnitor_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(leftUnitor η).hom.as.app a = (Bicategory.leftUnitor (η.app a)).hom

source

def CategoryTheory.Lax.LaxTrans.rightUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) :

CategoryStruct.comp η (CategoryStruct.id G) ≅ η

Right unitor for the vertical composition of lax natural transformations.

Equations

CategoryTheory.Lax.LaxTrans.rightUnitor η = CategoryTheory.Lax.LaxTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.rightUnitor (η.app a)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.rightUnitor_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(rightUnitor η).hom.as.app a = (Bicategory.rightUnitor (η.app a)).hom

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.rightUnitor_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(rightUnitor η).inv.as.app a = (Bicategory.rightUnitor (η.app a)).inv

source

@[implicit_reducible]

def CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :

Bicategory (LaxFunctor B C)

A bicategory structure on the lax functors between bicategories, with lax transformations.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.leftUnitor η).inv.as.app a = (Bicategory.leftUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (x✝³ x✝⁴ : x✝¹ ⟶ x✝²) (Γ : x✝³ ⟶ x✝⁴) (a : B) :

(Bicategory.whiskerLeft η Γ).as.app a = Bicategory.whiskerLeft (η.app a) (Γ.as.app a)

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (x✝³ : LaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :

(Bicategory.associator η θ ι).hom.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.rightUnitor η).hom.as.app a = (Bicategory.rightUnitor (η.app a)).hom

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (x✝³ : LaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :

(Bicategory.associator η θ ι).inv.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerRight_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (x✝³ x✝⁴ : x✝ ⟶ x✝¹) (Γ : x✝³ ⟶ x✝⁴) (ι : x✝¹ ⟶ x✝²) (a : B) :

(Bicategory.whiskerRight Γ ι).as.app a = Bicategory.whiskerRight (Γ.as.app a) (ι.app a)

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.rightUnitor η).inv.as.app a = (Bicategory.rightUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.leftUnitor η).hom.as.app a = (Bicategory.leftUnitor (η.app a)).hom

source

def CategoryTheory.Lax.OplaxTrans.whiskerLeft {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) :

CategoryStruct.comp η θ ⟶ CategoryStruct.comp η ι

Left whiskering of an oplax natural transformation and a modification.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.whiskerLeft_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B) :

(whiskerLeft η Γ).as.app a = Bicategory.whiskerLeft (η.app a) (Γ.as.app a)

source

def CategoryTheory.Lax.OplaxTrans.whiskerRight {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) :

CategoryStruct.comp η ι ⟶ CategoryStruct.comp θ ι

Right whiskering of an oplax natural transformation and a modification.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.whiskerRight_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : LaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B) :

(whiskerRight Γ ι).as.app a = Bicategory.whiskerRight (Γ.as.app a) (ι.app a)

source

def CategoryTheory.Lax.OplaxTrans.associator {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) :

CategoryStruct.comp (CategoryStruct.comp η θ) ι ≅ CategoryStruct.comp η (CategoryStruct.comp θ ι)

Associator for the vertical composition of oplax natural transformations.

Equations

CategoryTheory.Lax.OplaxTrans.associator η θ ι = CategoryTheory.Lax.OplaxTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.associator_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :

(associator η θ ι).inv.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.associator_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H I : LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B) :

(associator η θ ι).hom.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

source

def CategoryTheory.Lax.OplaxTrans.leftUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) :

CategoryStruct.comp (CategoryStruct.id F) η ≅ η

Left unitor for the vertical composition of oplax natural transformations.

Equations

CategoryTheory.Lax.OplaxTrans.leftUnitor η = CategoryTheory.Lax.OplaxTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.leftUnitor (η.app a)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.leftUnitor_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(leftUnitor η).inv.as.app a = (Bicategory.leftUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.leftUnitor_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(leftUnitor η).hom.as.app a = (Bicategory.leftUnitor (η.app a)).hom

source

def CategoryTheory.Lax.OplaxTrans.rightUnitor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) :

CategoryStruct.comp η (CategoryStruct.id G) ≅ η

Right unitor for the vertical composition of oplax natural transformations.

Equations

CategoryTheory.Lax.OplaxTrans.rightUnitor η = CategoryTheory.Lax.OplaxTrans.isoMk (fun (a : B) => CategoryTheory.Bicategory.rightUnitor (η.app a)) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.rightUnitor_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(rightUnitor η).inv.as.app a = (Bicategory.rightUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.rightUnitor_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) :

(rightUnitor η).hom.as.app a = (Bicategory.rightUnitor (η.app a)).hom

source

@[implicit_reducible]

def CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :

Bicategory (LaxFunctor B C)

A bicategory structure on the lax functors between bicategories, with oplax transformations.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (x✝³ x✝⁴ : x✝¹ ⟶ x✝²) (Γ : x✝³ ⟶ x✝⁴) (a : B) :

(Bicategory.whiskerLeft η Γ).as.app a = Bicategory.whiskerLeft (η.app a) (Γ.as.app a)

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.rightUnitor η).inv.as.app a = (Bicategory.rightUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (x✝³ : LaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :

(Bicategory.associator η θ ι).inv.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.leftUnitor η).inv.as.app a = (Bicategory.leftUnitor (η.app a)).inv

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_associator_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (x✝³ : LaxFunctor B C) (η : x✝ ⟶ x✝¹) (θ : x✝¹ ⟶ x✝²) (ι : x✝² ⟶ x✝³) (a : B) :

(Bicategory.associator η θ ι).hom.as.app a = (Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.rightUnitor η).hom.as.app a = (Bicategory.rightUnitor (η.app a)).hom

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerRight_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ x✝² : LaxFunctor B C} (x✝³ x✝⁴ : x✝ ⟶ x✝¹) (Γ : x✝³ ⟶ x✝⁴) (ι : x✝¹ ⟶ x✝²) (a : B) :

(Bicategory.whiskerRight Γ ι).as.app a = Bicategory.whiskerRight (Γ.as.app a) (ι.app a)

source

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_leftUnitor_hom_as_app (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {x✝ x✝¹ : LaxFunctor B C} (η : x✝ ⟶ x✝¹) (a : B) :

(Bicategory.leftUnitor η).hom.as.app a = (Bicategory.leftUnitor (η.app a)).hom

Documentation

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Bicategories of lax functors #