mathlib documentation

category_theory.bicategory.basic

Bicategories #

In this file we define typeclass for bicategories.

A bicategory B consists of

We use u, v, and w as the universe variables for objects, 1-morphisms, and 2-morphisms, respectively.

A typeclass for bicategories extends category_theory.category_struct typeclass. This means that we have

For each object a b : B, the collection of 1-morphisms a ⟶ b has a category structure. The 2-morphisms in the bicategory are implemented as the morphisms in this family of categories.

The composition of 1-morphisms is in fact a object part of a functor (a ⟶ b) ⥤ (b ⟶ c) ⥤ (a ⟶ c). The definition of bicategories in this file does not require this functor directly. Instead, it requires the whiskering functions. For a 1-morphism f : a ⟶ b and a 2-morphism η : g ⟶ h between 1-morphisms g h : b ⟶ c, there is a 2-morphism whisker_left f η : f ≫ g ⟶ f ≫ h. Similarly, for a 2-morphism η : f ⟶ g between 1-morphisms f g : a ⟶ b and a 1-morphism f : b ⟶ c, there is a 2-morphism whisker_right η h : f ≫ h ⟶ g ≫ h. These satisfy the exchange law whisker_left f θ ≫ whisker_right η i = whisker_right η h ≫ whisker_left g θ, which is required as an axiom in the definition here.

@[nolint, class]
structure category_theory.bicategory (B : Type u) :
Type (max u (v+1) (w+1))

In a bicategory, we can compose the 1-morphisms f : a ⟶ b and g : b ⟶ c to obtain a 1-morphism f ≫ g : a ⟶ c. This composition does not need to be strictly associative, but there is a specified associator, α_ f g h : (f ≫ g) ≫ h ≅ f ≫ (g ≫ h). There is an identity 1-morphism 𝟙 a : a ⟶ a, with specified left and right unitor isomorphisms λ_ f : 𝟙 a ≫ f ≅ f and ρ_ f : f ≫ 𝟙 a ≅ f. These associators and unitors satisfy the pentagon and triangle equations.

See https://ncatlab.org/nlab/show/bicategory.

Instances
@[simp]
theorem category_theory.bicategory.whisker_left_id {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.whisker_right_id {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) (g : b c) :
theorem category_theory.bicategory.whisker_right_comp_assoc {B : Type u} [self : category_theory.bicategory B] {a b c : B} {f g h : a b} (η : f g) (θ : g h) (i : b c) {X' : a c} (f' : h i X') :
theorem category_theory.bicategory.whisker_left_comp_assoc {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) {g h i : b c} (η : g h) (θ : h i) {X' : a c} (f' : f i X') :
@[simp]
theorem category_theory.bicategory.hom_inv_whisker_left_assoc {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a b) {g h : b c} (η : g h) {X' : a c} (f' : f g X') :
@[simp]
theorem category_theory.bicategory.hom_inv_whisker_right_assoc {B : Type u} [category_theory.bicategory B] {a b c : B} {f g : a b} (η : f g) (h : b c) {X' : a c} (f' : f h X') :
@[simp]
theorem category_theory.bicategory.inv_hom_whisker_left_assoc {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a b) {g h : b c} (η : g h) {X' : a c} (f' : f h X') :
@[simp]
theorem category_theory.bicategory.inv_hom_whisker_right_assoc {B : Type u} [category_theory.bicategory B] {a b c : B} {f g : a b} (η : f g) (h : b c) {X' : a c} (f' : g h X') :
def category_theory.bicategory.whisker_left_iso {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a b) {g h : b c} (η : g h) :
f g f h

The left whiskering of a 2-isomorphism is a 2-isomorphism.

Equations
@[protected, instance]
def category_theory.bicategory.whisker_right_iso {B : Type u} [category_theory.bicategory B] {a b c : B} {f g : a b} (η : f g) (h : b c) :
f h g h

The right whiskering of a 2-isomorphism is a 2-isomorphism.

Equations