# The monoidal coherence theorem #

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 `fullNormalize : FreeMonoidalCategory C ⥤ Discrete (NormalMonoidalObject 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 isomorphisms, but also that they assemble into a natural isomorphism `𝟭 (FreeMonoidalCategory C) ≅ fullNormalize ⋙ 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 #

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

source
inductive CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject (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₂) ⊗ ⋯`.

- unit {C : Type u} : NormalMonoidalObject C
- tensor {C : Type u} : NormalMonoidalObject C → C → NormalMonoidalObject C

Instances For

source
instance CategoryTheory.FreeMonoidalCategory.instSubsingletonHomCompDiscreteNormalMonoidalObject {C : Type u} (x y : (Discrete ∘ NormalMonoidalObject) C) :
Subsingleton (x ⟶ y)
source
def CategoryTheory.FreeMonoidalCategory.inclusionObj {C : Type u} :
NormalMonoidalObject C → FreeMonoidalCategory C

Auxiliary definition for `inclusion`.

Equations

- CategoryTheory.FreeMonoidalCategory.inclusionObj CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit = CategoryTheory.FreeMonoidalCategory.unit
- CategoryTheory.FreeMonoidalCategory.inclusionObj (n.tensor a) = (CategoryTheory.FreeMonoidalCategory.inclusionObj n).tensor (CategoryTheory.FreeMonoidalCategory.of a)

Instances For

source
def CategoryTheory.FreeMonoidalCategory.inclusion {C : Type u} :
Functor ((Discrete ∘ NormalMonoidalObject) C) (FreeMonoidalCategory C)

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

Equations

- CategoryTheory.FreeMonoidalCategory.inclusion = CategoryTheory.Discrete.functor CategoryTheory.FreeMonoidalCategory.inclusionObj

Instances For

source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.inclusion_obj {C : Type u} (X : (Discrete ∘ NormalMonoidalObject) C) :
inclusion.obj X = inclusionObj X.as
source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.inclusion_map {C : Type u} {X Y : (Discrete ∘ NormalMonoidalObject) C} (f : X ⟶ Y) :
inclusion.map f = eqToHom ⋯
source
def CategoryTheory.FreeMonoidalCategory.normalizeObj {C : Type u} :
FreeMonoidalCategory C → NormalMonoidalObject C → NormalMonoidalObject C

Auxiliary definition for `normalize`.

Equations

- CategoryTheory.FreeMonoidalCategory.unit.normalizeObj x✝ = x✝
- (CategoryTheory.FreeMonoidalCategory.of X).normalizeObj x✝ = x✝.tensor X
- (X.tensor Y).normalizeObj x✝ = Y.normalizeObj (X.normalizeObj x✝)

Instances For

source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.normalizeObj_unitor {C : Type u} (n : NormalMonoidalObject C) :
(MonoidalCategoryStruct.tensorUnit (FreeMonoidalCategory C)).normalizeObj n = n
source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.normalizeObj_tensor {C : Type u} (X Y : FreeMonoidalCategory C) (n : NormalMonoidalObject C) :
(MonoidalCategoryStruct.tensorObj X Y).normalizeObj n = Y.normalizeObj (X.normalizeObj n)
source
def CategoryTheory.FreeMonoidalCategory.normalizeObj' {C : Type u} (X : FreeMonoidalCategory C) :
Functor ((Discrete ∘ NormalMonoidalObject) C) ((Discrete ∘ NormalMonoidalObject) C)

Auxiliary definition for `normalize`.

Equations

- X.normalizeObj' = CategoryTheory.Discrete.functor fun (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) => { as := X.normalizeObj n }

Instances For

source
def CategoryTheory.FreeMonoidalCategory.normalizeMapAux {C : Type u} {X Y : FreeMonoidalCategory C} :
X.Hom Y → (X.normalizeObj' ⟶ Y.normalizeObj')

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

Equations

- One or more equations did not get rendered due to their size.
- CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.id x✝) = CategoryTheory.CategoryStruct.id x✝.normalizeObj'

Instances For

source
def CategoryTheory.FreeMonoidalCategory.normalize (C : Type u) :
Functor (FreeMonoidalCategory C) (Functor ((Discrete ∘ NormalMonoidalObject) C) ((Discrete ∘ NormalMonoidalObject) 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

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

Instances For

source
def CategoryTheory.FreeMonoidalCategory.normalize' (C : Type u) :
Functor (FreeMonoidalCategory C) (Functor ((Discrete ∘ NormalMonoidalObject) C) (FreeMonoidalCategory 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

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

Instances For

source
def CategoryTheory.FreeMonoidalCategory.fullNormalize (C : Type u) :
Functor (FreeMonoidalCategory C) ((Discrete ∘ NormalMonoidalObject) C)

The normalization functor for the free monoidal category over `C`.

Equations

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

Instances For

source
def CategoryTheory.FreeMonoidalCategory.tensorFunc (C : Type u) :
Functor (FreeMonoidalCategory C) (Functor ((Discrete ∘ NormalMonoidalObject) C) (FreeMonoidalCategory 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

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

Instances For

source
theorem CategoryTheory.FreeMonoidalCategory.tensorFunc_map_app (C : Type u) {X Y : FreeMonoidalCategory C} (f : X ⟶ Y) (n : (Discrete ∘ NormalMonoidalObject) C) :
((tensorFunc C).map f).app n = MonoidalCategoryStruct.whiskerLeft (inclusion.obj { as := n.as }) f
source
theorem CategoryTheory.FreeMonoidalCategory.tensorFunc_obj_map (C : Type u) (Z : FreeMonoidalCategory C) {n n' : (Discrete ∘ NormalMonoidalObject) C} (f : n ⟶ n') :
((tensorFunc C).obj Z).map f = MonoidalCategoryStruct.whiskerRight (inclusion.map f) Z
source
def CategoryTheory.FreeMonoidalCategory.normalizeIsoApp (C : Type u) (X : FreeMonoidalCategory C) (n : (Discrete ∘ NormalMonoidalObject) C) :
((tensorFunc C).obj X).obj n ≅ ((normalize' C).obj X).obj n

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

Equations

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

Instances For

source
def CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' (C : Type u) (X : FreeMonoidalCategory C) (n : NormalMonoidalObject C) :
MonoidalCategoryStruct.tensorObj (inclusionObj n) X ≅ inclusionObj (X.normalizeObj n)

Almost non-definitionally equal to `normalizeIsoApp`, but has a better definitional property in the proof of `normalize_naturality`.

Equations

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

Instances For

source
theorem CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_eq (C : Type u) (X : FreeMonoidalCategory C) (n : (Discrete ∘ NormalMonoidalObject) C) :
normalizeIsoApp C X n = normalizeIsoApp' C X n.as
source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_tensor (C : Type u) (X Y : FreeMonoidalCategory C) (n : (Discrete ∘ NormalMonoidalObject) C) :
normalizeIsoApp C (MonoidalCategoryStruct.tensorObj X Y) n = (MonoidalCategoryStruct.associator (inclusion.obj { as := n.as }) X Y).symm ≪≫ MonoidalCategory.whiskerRightIso (normalizeIsoApp C X n) Y ≪≫ normalizeIsoApp C Y { as := X.normalizeObj n.as }
source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_unitor (C : Type u) (n : (Discrete ∘ NormalMonoidalObject) C) :
normalizeIsoApp C (MonoidalCategoryStruct.tensorUnit (FreeMonoidalCategory C)) n = MonoidalCategoryStruct.rightUnitor (inclusion.obj { as := n.as })
source
def CategoryTheory.FreeMonoidalCategory.normalizeIsoAux (C : Type u) (X : FreeMonoidalCategory C) :
(tensorFunc C).obj X ≅ (normalize' C).obj X

Auxiliary definition for `normalizeIso`.

Equations

- CategoryTheory.FreeMonoidalCategory.normalizeIsoAux C X = CategoryTheory.NatIso.ofComponents (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.normalizeIsoAux_hom_app (C : Type u) (X : FreeMonoidalCategory C) (X✝ : (Discrete ∘ NormalMonoidalObject) C) :
(normalizeIsoAux C X).hom.app X✝ = (normalizeIsoApp C X X✝).hom
source
@[simp]
theorem CategoryTheory.FreeMonoidalCategory.normalizeIsoAux_inv_app (C : Type u) (X : FreeMonoidalCategory C) (X✝ : (Discrete ∘ NormalMonoidalObject) C) :
(normalizeIsoAux C X).inv.app X✝ = (normalizeIsoApp C X X✝).inv
source
theorem CategoryTheory.FreeMonoidalCategory.normalizeObj_congr {C : Type u} (n : NormalMonoidalObject C) {X Y : FreeMonoidalCategory C} (f : X ⟶ Y) :
X.normalizeObj n = Y.normalizeObj n
source
theorem CategoryTheory.FreeMonoidalCategory.normalize_naturality {C : Type u} (n : NormalMonoidalObject C) {X Y : FreeMonoidalCategory C} (f : X ⟶ Y) :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (inclusionObj n) f) (normalizeIsoApp' C Y n).hom = CategoryStruct.comp (normalizeIsoApp' C X n).hom (inclusion.map (eqToHom ⋯))
source
def CategoryTheory.FreeMonoidalCategory.normalizeIso (C : Type u) :
tensorFunc C ≅ 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 `normalizeIsoAux`). This is the real heart of our proof of the coherence theorem.

Equations

- CategoryTheory.FreeMonoidalCategory.normalizeIso C = CategoryTheory.NatIso.ofComponents (CategoryTheory.FreeMonoidalCategory.normalizeIsoAux C) ⋯

Instances For

source
def CategoryTheory.FreeMonoidalCategory.fullNormalizeIso (C : Type u) :
Functor.id (FreeMonoidalCategory C) ≅ (fullNormalize C).comp inclusion

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

Equations

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

Instances For

source
instance CategoryTheory.FreeMonoidalCategory.subsingleton_hom {C : Type u} :
Quiver.IsThin (FreeMonoidalCategory C)

The monoidal coherence theorem.

source
def CategoryTheory.FreeMonoidalCategory.inverseAux {C : Type u} {X Y : FreeMonoidalCategory C} :
X.Hom Y → Y.Hom X

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

Equations

- One or more equations did not get rendered due to their size.
- CategoryTheory.FreeMonoidalCategory.inverseAux (CategoryTheory.FreeMonoidalCategory.Hom.id x✝) = CategoryTheory.FreeMonoidalCategory.Hom.id x✝
- CategoryTheory.FreeMonoidalCategory.inverseAux (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z) = CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z
- CategoryTheory.FreeMonoidalCategory.inverseAux (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z) = CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z
- CategoryTheory.FreeMonoidalCategory.inverseAux (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom x✝) = CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv x✝
- CategoryTheory.FreeMonoidalCategory.inverseAux (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv x✝) = CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom x✝
- CategoryTheory.FreeMonoidalCategory.inverseAux (CategoryTheory.FreeMonoidalCategory.Hom.l_hom x✝) = CategoryTheory.FreeMonoidalCategory.Hom.l_inv x✝
- CategoryTheory.FreeMonoidalCategory.inverseAux (CategoryTheory.FreeMonoidalCategory.Hom.l_inv x✝) = CategoryTheory.FreeMonoidalCategory.Hom.l_hom x✝
- CategoryTheory.FreeMonoidalCategory.inverseAux (f.comp g) = (CategoryTheory.FreeMonoidalCategory.inverseAux g).comp (CategoryTheory.FreeMonoidalCategory.inverseAux f)
- CategoryTheory.FreeMonoidalCategory.inverseAux (f.whiskerRight X) = (CategoryTheory.FreeMonoidalCategory.inverseAux f).whiskerRight X
- CategoryTheory.FreeMonoidalCategory.inverseAux (f.tensor g) = (CategoryTheory.FreeMonoidalCategory.inverseAux f).tensor (CategoryTheory.FreeMonoidalCategory.inverseAux g)

Instances For

source
instance CategoryTheory.FreeMonoidalCategory.instGroupoid {C : Type u} :
Groupoid (FreeMonoidalCategory C)
Equations

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