The coherence theorem for bicategories

In this file, we prove the coherence theorem for bicategories, stated in the following form: the free bicategory over any quiver is locally thin.

The proof is almost the same as the proof of the coherence theorem for monoidal categories that has been previously formalized in mathlib, which is based on the proof described by Ilya Beylin and Peter Dybjer. The idea is to view a path on a quiver as a normal form of a 1-morphism in the free bicategory on the same quiver. A normalization procedure is then described by normalize : Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B)), which is a pseudofunctor from the free bicategory to the locally discrete bicategory on the path category. It turns out that this pseudofunctor is locally an equivalence of categories, and the coherence theorem follows immediately from this fact.

Main statements

• locally_thin : the free bicategory is locally thin, that is, there is at most one 2-morphism between two fixed 1-morphisms.

References

• [Ilya Beylin and Peter Dybjer, Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids][beylin1996]

def CategoryTheory.FreeBicategory.inclusionPathAux {B : Type u} [Quiver B] {a b : B} : Quiver.Path a b → Hom a b

Auxiliary definition for inclusionPath.

def CategoryTheory.FreeBicategory.homCategory' {B : Type u} [Quiver B] (a b : B) : Category.{max u v, max u v} (Hom a b)

Category structure on Hom a b. In this file, we will use Hom a b for a b : B (precisely, FreeBicategory.Hom a b) instead of the definitionally equal expression a ⟶ b for a b : FreeBicategory B. The main reason is that we have to annoyingly write @Quiver.Hom (FreeBicategory B) _ a b to get the latter expression when given a b : B.

def CategoryTheory.FreeBicategory.inclusionPath {B : Type u} [Quiver B] (a b : B) : Functor (Discrete (Quiver.Path a b)) (Hom a b)

The discrete category on the paths includes into the category of 1-morphisms in the free bicategory.

def CategoryTheory.FreeBicategory.preinclusion (B : Type u) [Quiver B] : PrelaxFunctor (LocallyDiscrete (Paths B)) (FreeBicategory B)

The inclusion from the locally discrete bicategory on the path category into the free bicategory as a prelax functor. This will be promoted to a pseudofunctor after proving the coherence theorem. See inclusion.

@[simp]

theorem CategoryTheory.FreeBicategory.preinclusion_obj {B : Type u} [Quiver B] (a : B) : (preinclusion B).obj { as := a } = a

@[simp]

theorem CategoryTheory.FreeBicategory.preinclusion_map₂ {B : Type u} [Quiver B] {a b : B} (f g : Discrete (Quiver.Path a b)) (η : f ⟶ g) : (preinclusion B).map₂ η = eqToHom ⋯

def CategoryTheory.FreeBicategory.normalizeAux {B : Type u} [Quiver B] {a b c : B} : Quiver.Path a b → Hom b c → Quiver.Path a c

The normalization of the composition of p : Path a b and f : Hom b c. p will eventually be taken to be nil and we then get the normalization of f alone, but the auxiliary p is necessary for Lean to accept the definition of normalizeIso and the whisker_left case of normalizeAux_congr and normalize_naturality.

def CategoryTheory.FreeBicategory.normalizeIso {B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) (f : Hom b c) : CategoryStruct.comp ((preinclusion B).map { as := p }) f ≅ (preinclusion B).map { as := normalizeAux p f }

A 2-isomorphism between a partially-normalized 1-morphism in the free bicategory to the fully-normalized 1-morphism.

theorem CategoryTheory.FreeBicategory.normalizeAux_congr {B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : Hom b c} (η : f ⟶ g) : normalizeAux p f = normalizeAux p g

Given a 2-morphism between f and g in the free bicategory, we have the equality normalizeAux p f = normalizeAux p g.

theorem CategoryTheory.FreeBicategory.normalize_naturality {B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : Hom b c} (η : f ⟶ g) : CategoryStruct.comp (Bicategory.whiskerLeft ((preinclusion B).map { as := p }) η) (normalizeIso p g).hom = CategoryStruct.comp (normalizeIso p f).hom ((preinclusion B).map₂ (eqToHom ⋯))

The 2-isomorphism normalizeIso p f is natural in f.

theorem CategoryTheory.FreeBicategory.normalizeAux_nil_comp {B : Type u} [Quiver B] {a b c : B} (f : Hom a b) (g : Hom b c) : normalizeAux Quiver.Path.nil (f.comp g) = (normalizeAux Quiver.Path.nil f).comp (normalizeAux Quiver.Path.nil g)

def CategoryTheory.FreeBicategory.normalize (B : Type u) [Quiver B] : Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B))

The normalization pseudofunctor for the free bicategory on a quiver B.

def CategoryTheory.FreeBicategory.normalizeUnitIso {B : Type u} [Quiver B] (a b : FreeBicategory B) : Functor.id (a ⟶ b) ≅ ((normalize B).mapFunctor a b).comp (inclusionPath a b)

Auxiliary definition for normalizeEquiv.

def CategoryTheory.FreeBicategory.normalizeEquiv {B : Type u} [Quiver B] (a b : B) : Hom a b ≌ Discrete (Quiver.Path a b)

Normalization as an equivalence of categories.

instance CategoryTheory.FreeBicategory.locally_thin {B : Type u} [Quiver B] {a b : FreeBicategory B} : Quiver.IsThin (a ⟶ b)

The coherence theorem for bicategories.

def CategoryTheory.FreeBicategory.inclusionMapCompAux {B : Type u} [Quiver B] {a b c : B} (f : Quiver.Path a b) (g : Quiver.Path b c) : (preinclusion B).map (CategoryStruct.comp { as := f } { as := g }) ≅ CategoryStruct.comp ((preinclusion B).map { as := f }) ((preinclusion B).map { as := g })

Auxiliary definition for inclusion.

def CategoryTheory.FreeBicategory.inclusion (B : Type u) [Quiver B] : Pseudofunctor (LocallyDiscrete (Paths B)) (FreeBicategory B)

The inclusion pseudofunctor from the locally discrete bicategory on the path category into the free bicategory.