# 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 : 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]

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

Auxiliary definition for `inclusionPath`.

Equations

- CategoryTheory.FreeBicategory.inclusionPathAux Quiver.Path.nil = CategoryTheory.FreeBicategory.Hom.id a
- CategoryTheory.FreeBicategory.inclusionPathAux (p.cons f) = (CategoryTheory.FreeBicategory.inclusionPathAux p).comp (CategoryTheory.FreeBicategory.Hom.of f)

Instances For

source
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`.

Equations

- CategoryTheory.FreeBicategory.homCategory' a b = CategoryTheory.FreeBicategory.homCategory a b

Instances For

source
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.

Equations

- CategoryTheory.FreeBicategory.inclusionPath a b = CategoryTheory.Discrete.functor CategoryTheory.FreeBicategory.inclusionPathAux

Instances For

source
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`.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.FreeBicategory.preinclusion_obj {B : Type u} [Quiver B] (a : B) :
(preinclusion B).obj { as := a } = a
source
@[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 ⋯
source
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`.

Equations

- CategoryTheory.FreeBicategory.normalizeAux x✝ (CategoryTheory.FreeBicategory.Hom.of f) = x✝.cons f
- CategoryTheory.FreeBicategory.normalizeAux x✝ (CategoryTheory.FreeBicategory.Hom.id x✝¹) = x✝
- CategoryTheory.FreeBicategory.normalizeAux x✝ (f.comp g) = CategoryTheory.FreeBicategory.normalizeAux (CategoryTheory.FreeBicategory.normalizeAux x✝ f) g

Instances For

source
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.

Equations

- One or more equations did not get rendered due to their size.
- CategoryTheory.FreeBicategory.normalizeIso x✝ (CategoryTheory.FreeBicategory.Hom.id x✝¹) = CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x✝ })

Instances For

source
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`.

source
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`.

source
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)
source
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`.

Equations

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

Instances For

source
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`.

Equations

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

Instances For

source
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.

Equations

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

Instances For

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

The coherence theorem for bicategories.

source
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`.

Equations

- One or more equations did not get rendered due to their size.
- CategoryTheory.FreeBicategory.inclusionMapCompAux x✝ Quiver.Path.nil = (CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x✝ })).symm

Instances For

source
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.

Equations

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

Instances For