mathlib3 documentation

category_theory.monoidal.free.coherence

The monoidal coherence theorem #

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

In this file, we prove the monoidal coherence theorem, stated in the following form: the free monoidal category over any type C is thin.

We follow a proof described by Ilya Beylin and Peter Dybjer, which has been previously formalized in the proof assistant ALF. The idea is to declare a normal form (with regard to association and adding units) on objects of the free monoidal category and consider the discrete subcategory of objects that are in normal form. A normalization procedure is then just a functor full_normalize : free_monoidal_category C ⥤ discrete (normal_monoidal_object C), where functoriality says that two objects which are related by associators and unitors have the same normal form. Another desirable property of a normalization procedure is that an object is isomorphic (i.e., related via associators and unitors) to its normal form. In the case of the specific normalization procedure we use we not only get these isomorphismns, but also that they assemble into a natural isomorphism 𝟭 (free_monoidal_category C) ≅ full_normalize ⋙ inclusion. But this means that any two parallel morphisms in the free monoidal category factor through a discrete category in the same way, so they must be equal, and hence the free monoidal category is thin.

References #

source
@[nolint]
inductive category_theory.free_monoidal_category.normal_monoidal_object (C : Type u) :
Type u

We say an object in the free monoidal category is in normal form if it is of the form (((𝟙_ C) ⊗ X₁) ⊗ X₂) ⊗ ⋯.

Instances for category_theory.free_monoidal_category.normal_monoidal_object
  • category_theory.free_monoidal_category.normal_monoidal_object.has_sizeof_inst
source
@[simp]
def category_theory.free_monoidal_category.inclusion_obj {C : Type u} :
category_theory.free_monoidal_category.normal_monoidal_object C → category_theory.free_monoidal_category C

Auxiliary definition for inclusion.

Equations
source
@[simp]
def category_theory.free_monoidal_category.inclusion {C : Type u} :
(category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C ⥤ category_theory.free_monoidal_category C

The discrete subcategory of objects in normal form includes into the free monoidal category.

Equations
source
@[simp]
def category_theory.free_monoidal_category.normalize_obj {C : Type u} :
category_theory.free_monoidal_category C → category_theory.free_monoidal_category.normal_monoidal_object C → (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C

Auxiliary definition for normalize.

Equations
source
@[simp]
theorem category_theory.free_monoidal_category.normalize_obj_unitor {C : Type u} (n : category_theory.free_monoidal_category.normal_monoidal_object C) :
(𝟙_ (category_theory.free_monoidal_category C)).normalize_obj n = {as := n}
source
@[simp]
theorem category_theory.free_monoidal_category.normalize_obj_tensor {C : Type u} (X Y : category_theory.free_monoidal_category C) (n : category_theory.free_monoidal_category.normal_monoidal_object C) :
(X ⊗ Y).normalize_obj n = Y.normalize_obj (X.normalize_obj n).as
source
@[simp]
def category_theory.free_monoidal_category.normalize_map_aux {C : Type u} {X Y : category_theory.free_monoidal_category C} :
X.hom Y → (category_theory.discrete.functor X.normalize_obj ⟶ category_theory.discrete.functor Y.normalize_obj)

Auxiliary definition for normalize. Here we prove that objects that are related by associators and unitors map to the same normal form.

Equations
source
@[simp]
def category_theory.free_monoidal_category.normalize (C : Type u) :
category_theory.free_monoidal_category C ⥤ (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C ⥤ (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C

Our normalization procedure works by first defining a functor F C ⥤ (N C ⥤ N C) (which turns out to be very easy), and then obtain a functor F C ⥤ N C by plugging in the normal object 𝟙_ C.

Equations
source
@[simp]
def category_theory.free_monoidal_category.normalize' (C : Type u) :
category_theory.free_monoidal_category C ⥤ (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C ⥤ category_theory.free_monoidal_category C

A variant of the normalization functor where we consider the result as an object in the free monoidal category (rather than an object of the discrete subcategory of objects in normal form).

Equations
source
def category_theory.free_monoidal_category.full_normalize (C : Type u) :
category_theory.free_monoidal_category C ⥤ (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C

The normalization functor for the free monoidal category over C.

Equations
source
@[simp]
def category_theory.free_monoidal_category.tensor_func (C : Type u) :
category_theory.free_monoidal_category C ⥤ (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C ⥤ category_theory.free_monoidal_category C

Given an object X of the free monoidal category and an object n in normal form, taking the tensor product n ⊗ X in the free monoidal category is functorial in both X and n.

Equations
source
theorem category_theory.free_monoidal_category.tensor_func_map_app (C : Type u) {X Y : category_theory.free_monoidal_category C} (f : X ⟶ Y) (n : (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C) :
((category_theory.free_monoidal_category.tensor_func C).map f).app n = 𝟙 (category_theory.free_monoidal_category.inclusion.obj {as := n.as}) ⊗ f
source
theorem category_theory.free_monoidal_category.tensor_func_obj_map (C : Type u) (Z : category_theory.free_monoidal_category C) {n n' : (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C} (f : n ⟶ n') :
((category_theory.free_monoidal_category.tensor_func C).obj Z).map f = category_theory.free_monoidal_category.inclusion.map f ⊗ 𝟙 Z
source
@[simp]
def category_theory.free_monoidal_category.normalize_iso_app (C : Type u) (X : category_theory.free_monoidal_category C) (n : (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C) :
((category_theory.free_monoidal_category.tensor_func C).obj X).obj n ≅ ((category_theory.free_monoidal_category.normalize' C).obj X).obj n

Auxiliary definition for normalize_iso. Here we construct the isomorphism between n ⊗ X and normalize X n.

Equations
source
@[simp]
theorem category_theory.free_monoidal_category.normalize_iso_app_tensor (C : Type u) (X Y : category_theory.free_monoidal_category C) (n : (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C) :
category_theory.free_monoidal_category.normalize_iso_app C (X ⊗ Y) n = (α_ (category_theory.free_monoidal_category.inclusion.obj {as := n.as}) X Y).symm ≪≫ (category_theory.free_monoidal_category.normalize_iso_app C X n ⊗ category_theory.iso.refl Y) ≪≫ category_theory.free_monoidal_category.normalize_iso_app C Y (((category_theory.free_monoidal_category.normalize C).obj X).obj n)
source
@[simp]
theorem category_theory.free_monoidal_category.normalize_iso_app_unitor (C : Type u) (n : (category_theory.discrete ∘ category_theory.free_monoidal_category.normal_monoidal_object) C) :
category_theory.free_monoidal_category.normalize_iso_app C (𝟙_ (category_theory.free_monoidal_category C)) n = ρ_ (category_theory.free_monoidal_category.inclusion.obj {as := n.as})
source
@[simp]
def category_theory.free_monoidal_category.normalize_iso_aux (C : Type u) (X : category_theory.free_monoidal_category C) :
(category_theory.free_monoidal_category.tensor_func C).obj X ≅ (category_theory.free_monoidal_category.normalize' C).obj X

Auxiliary definition for normalize_iso.

Equations
source
@[simp]
theorem category_theory.free_monoidal_category.discrete_functor_obj_eq_as {D : Type u} [category_theory.category D] {I : Type u} (f : I → D) (X : category_theory.discrete I) :
(category_theory.discrete.functor f).obj X = f X.as
source
@[simp]
theorem category_theory.free_monoidal_category.discrete_functor_map_eq_id {D : Type u} [category_theory.category D] {I : Type u} (f : I → D) (X : category_theory.discrete I) (g : X ⟶ X) :
(category_theory.discrete.functor f).map g = 𝟙 ((category_theory.discrete.functor f).obj X)
source
def category_theory.free_monoidal_category.normalize_iso (C : Type u) :
category_theory.free_monoidal_category.tensor_func C ≅ category_theory.free_monoidal_category.normalize' C

The isomorphism between n ⊗ X and normalize X n is natural (in both X and n, but naturality in n is trivial and was "proved" in normalize_iso_aux). This is the real heart of our proof of the coherence theorem.

Equations
source
def category_theory.free_monoidal_category.full_normalize_iso (C : Type u) :
𝟭 (category_theory.free_monoidal_category C) ≅ category_theory.free_monoidal_category.full_normalize C ⋙ category_theory.free_monoidal_category.inclusion

The isomorphism between an object and its normal form is natural.

Equations
source
@[protected, instance]
def category_theory.free_monoidal_category.subsingleton_hom {C : Type u} :
quiver.is_thin (category_theory.free_monoidal_category C)

The monoidal coherence theorem.

source
def category_theory.free_monoidal_category.inverse_aux {C : Type u} {X Y : category_theory.free_monoidal_category C} :
X.hom Y → Y.hom X

Auxiliary construction for showing that the free monoidal category is a groupoid. Do not use this, use is_iso.inv instead.

Equations
source
@[protected, instance]
def category_theory.free_monoidal_category.category_theory.groupoid {C : Type u} :
category_theory.groupoid (category_theory.free_monoidal_category C)
Equations