mathlib3 documentation

category_theory.bicategory.coherence

The coherence theorem for bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (free_bicategory B) (locally_discrete (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

@[simp]

def category_theory.free_bicategory.inclusion_path_aux {B : Type u} [quiver B] {a b : B} :

quiver.path a b → category_theory.free_bicategory.hom a b

Auxiliary definition for inclusion_path.

Equations

def category_theory.free_bicategory.inclusion_path {B : Type u} [quiver B] (a b : B) :

category_theory.discrete (quiver.path a b) ⥤ category_theory.free_bicategory.hom a b

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

Equations

category_theory.free_bicategory.inclusion_path a b = category_theory.discrete.functor category_theory.free_bicategory.inclusion_path_aux

def category_theory.free_bicategory.preinclusion (B : Type u) [quiver B] :

category_theory.prelax_functor (category_theory.locally_discrete (category_theory.paths B)) (category_theory.free_bicategory 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

category_theory.free_bicategory.preinclusion B = {obj := id (category_theory.locally_discrete (category_theory.paths B)), map := λ (a b : category_theory.locally_discrete (category_theory.paths B)), (category_theory.free_bicategory.inclusion_path a b).obj, map₂ := λ (a b : category_theory.locally_discrete (category_theory.paths B)) (f g : a ⟶ b) (η : f ⟶ g), (category_theory.free_bicategory.inclusion_path a b).map η}

@[simp]

theorem category_theory.free_bicategory.preinclusion_obj {B : Type u} [quiver B] (a : B) :

(category_theory.free_bicategory.preinclusion B).obj a = a

@[simp]

theorem category_theory.free_bicategory.preinclusion_map₂ {B : Type u} [quiver B] {a b : B} (f g : category_theory.discrete (quiver.path a b)) (η : f ⟶ g) :

(category_theory.free_bicategory.preinclusion B).map₂ η = category_theory.eq_to_hom _

@[simp]

def category_theory.free_bicategory.normalize_aux {B : Type u} [quiver B] {a b c : B} :

quiver.path a b → category_theory.free_bicategory.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 normalize_iso and the whisker_left case of normalize_aux_congr and normalize_naturality.

Equations

@[simp]

def category_theory.free_bicategory.normalize_iso {B : Type u} [quiver B] {a b c : B} (p : quiver.path a b) (f : category_theory.free_bicategory.hom b c) :

(category_theory.free_bicategory.preinclusion B).map {as := p} ≫ f ≅ (category_theory.free_bicategory.preinclusion B).map {as := category_theory.free_bicategory.normalize_aux p f}

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

Equations

theorem category_theory.free_bicategory.normalize_aux_congr {B : Type u} [quiver B] {a b c : B} (p : quiver.path a b) {f g : category_theory.free_bicategory.hom b c} (η : f ⟶ g) :

category_theory.free_bicategory.normalize_aux p f = category_theory.free_bicategory.normalize_aux p g

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

theorem category_theory.free_bicategory.normalize_naturality {B : Type u} [quiver B] {a b c : B} (p : quiver.path a b) {f g : category_theory.free_bicategory.hom b c} (η : f ⟶ g) :

category_theory.bicategory.whisker_left ((category_theory.free_bicategory.preinclusion B).map {as := p}) η ≫ (category_theory.free_bicategory.normalize_iso p g).hom = (category_theory.free_bicategory.normalize_iso p f).hom ≫ (category_theory.free_bicategory.preinclusion B).map₂ (category_theory.eq_to_hom _)

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

@[simp]

theorem category_theory.free_bicategory.normalize_aux_nil_comp {B : Type u} [quiver B] {a b c : B} (f : category_theory.free_bicategory.hom a b) (g : category_theory.free_bicategory.hom b c) :

category_theory.free_bicategory.normalize_aux quiver.path.nil (f.comp g) = (category_theory.free_bicategory.normalize_aux quiver.path.nil f).comp (category_theory.free_bicategory.normalize_aux quiver.path.nil g)

def category_theory.free_bicategory.normalize (B : Type u) [quiver B] :

category_theory.pseudofunctor (category_theory.free_bicategory B) (category_theory.locally_discrete (category_theory.paths B))

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

Equations

category_theory.free_bicategory.normalize B = {obj := id (category_theory.free_bicategory B), map := λ (a b : category_theory.free_bicategory B) (f : a ⟶ b), {as := category_theory.free_bicategory.normalize_aux quiver.path.nil f}, map₂ := λ (a b : category_theory.free_bicategory B) (f g : a ⟶ b) (η : f ⟶ g), category_theory.eq_to_hom _, map_id := λ (a : category_theory.free_bicategory B), category_theory.eq_to_iso _, map_comp := λ (a b c : category_theory.free_bicategory B) (f : a ⟶ b) (g : b ⟶ c), category_theory.eq_to_iso _, map₂_id' := _, map₂_comp' := _, map₂_whisker_left' := _, map₂_whisker_right' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

def category_theory.free_bicategory.normalize_unit_iso {B : Type u} [quiver B] (a b : category_theory.free_bicategory B) :

𝟭 (a ⟶ b) ≅ (category_theory.free_bicategory.normalize B).map_functor a b ⋙ category_theory.free_bicategory.inclusion_path a b

Auxiliary definition for normalize_equiv.

Equations

a.normalize_unit_iso b = category_theory.nat_iso.of_components (λ (f : a ⟶ b), (category_theory.bicategory.left_unitor f).symm ≪≫ category_theory.free_bicategory.normalize_iso quiver.path.nil f) _

def category_theory.free_bicategory.normalize_equiv {B : Type u} [quiver B] (a b : B) :

category_theory.free_bicategory.hom a b ≌ category_theory.discrete (quiver.path a b)

Normalization as an equivalence of categories.

Equations

category_theory.free_bicategory.normalize_equiv a b = category_theory.equivalence.mk ((category_theory.free_bicategory.normalize B).map_functor a b) (category_theory.free_bicategory.inclusion_path a b) (category_theory.free_bicategory.normalize_unit_iso a b) (category_theory.discrete.nat_iso (λ (f : category_theory.discrete (quiver.path a b)), category_theory.eq_to_iso _))

@[protected, instance]

def category_theory.free_bicategory.locally_thin {B : Type u} [quiver B] {a b : category_theory.free_bicategory B} :

quiver.is_thin (a ⟶ b)

The coherence theorem for bicategories.

def category_theory.free_bicategory.inclusion_map_comp_aux {B : Type u} [quiver B] {a b c : B} (f : quiver.path a b) (g : quiver.path b c) :

(category_theory.free_bicategory.preinclusion B).map ({as := f} ≫ {as := g}) ≅ (category_theory.free_bicategory.preinclusion B).map {as := f} ≫ (category_theory.free_bicategory.preinclusion B).map {as := g}

Auxiliary definition for inclusion.

Equations

def category_theory.free_bicategory.inclusion (B : Type u) [quiver B] :

category_theory.pseudofunctor (category_theory.locally_discrete (category_theory.paths B)) (category_theory.free_bicategory B)

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

Equations

category_theory.free_bicategory.inclusion B = {obj := (category_theory.free_bicategory.preinclusion B).obj, map := (category_theory.free_bicategory.preinclusion B).map, map₂ := (category_theory.free_bicategory.preinclusion B).map₂, map_id := λ (a : category_theory.locally_discrete (category_theory.paths B)), category_theory.iso.refl (𝟙 a), map_comp := λ (a b c : category_theory.locally_discrete (category_theory.paths B)) (f : a ⟶ b) (g : b ⟶ c), category_theory.free_bicategory.inclusion_map_comp_aux f.as g.as, map₂_id' := _, map₂_comp' := _, map₂_whisker_left' := _, map₂_whisker_right' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}