2. The Coherence Theorem🔗

In a monoidal category, the tensor product is associative and unital only up to specified isomorphism. Thus X \otimes (Y \otimes Z) and (X \otimes Y) \otimes Z are different objects, and so are I \otimes X and X, or X \otimes I and X. To pass between such expressions one uses the associator \alpha and the left and right unitors \lambda and \rho.

In mathlib these are:

associator with notation α_ X Y Z
leftUnitor with notation λ_ X
rightUnitor with notation ρ_ X

For general tensor expressions, one can write several different composites of associators and unitors with the same source and target. For example,

(((a \otimes (b \otimes (I \otimes c))) \otimes d) \otimes e) \cong ((I \otimes (a \otimes b)) \otimes (c \otimes (d \otimes e))).

One would like all composites of this kind to agree. If stated directly, this would be an infinite axiom scheme, because there are infinitely many source and target expressions and infinitely many formally different composites between them.

Mac Lane's coherence theorem says that one does not need to impose all of those equalities. It is enough to assume only the pentagon and triangle identities. In mathlib these are pentagon and triangle.

The monoidal_coherence tactic is a direct implementation of this theorem. It proves that any two composites built only from associators and unitors with the same source and target are equal.

theorem unitors_equal {C : Type*} [Category C] [MonoidalCategory C] :
    (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := byC:Type u_1inst✝¹:Category.{u_2, u_1} Cinst✝:MonoidalCategory C⊢ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom
  monoidal_coherenceAll goals completed! 🐙

def

Mathlib.Tactic.Monoidal.pureCoherence (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)
Mathlib.Tactic.Monoidal.pureCoherence
  (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)

Close the goal of the form η = θ, where η and θ are 2-isomorphisms made up only of associators, unitors, and identities.

example {C : Type} [Category* C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  monoidal_coherence

A proof of this theorem, and the one that underlies mathlib's implementation, follows the accumulator-style normalization argument of Beylin and Dybjer. For the original source, see Ilya Beylin and Peter Dybjer, 1996. “Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids”. In Types for Proofs and Programs: International Workshop, TYPES '95, Torino, Italy, June 5-8, 1995, Selected Papers. (Lecture Notes in Computer Science 1158).

It begins by specifying a class of normal forms. The normal forms are the left-associated expressions with the unit object on the far left:

((\cdots ((I \otimes X_1) \otimes X_2) \otimes \cdots) \otimes X_n).

For example, the normalization of the source object in the example above is [((a \otimes (b \otimes (I \otimes c))) \otimes d) \otimes e] = ((((I \otimes a) \otimes b) \otimes c) \otimes d) \otimes e.

The recursion is set up on [N \otimes X], where N is already normalized, rather than on [X] directly. The definition proceeds by structural recursion on X:

[N \otimes I] := N

[N \otimes (X \otimes Y)] := [[N \otimes X] \otimes Y]

[N \otimes A] := N \otimes A

for atomic A.

At the same time we define a normalization isomorphism

\nu_{N,X} : N \otimes X \xrightarrow{\cong} [N \otimes X].

Again the definition is recursive:

N \otimes I \xrightarrow{\rho_N} N = [N \otimes I].

\begin{aligned} N \otimes (X \otimes Y) &\xrightarrow{\alpha_{N,X,Y}} (N \otimes X) \otimes Y \\ &\xrightarrow{\nu_{N,X} \otimes \mathrm{id}_Y} [N \otimes X] \otimes Y \\ &\xrightarrow{\nu_{[N \otimes X],Y}} [[N \otimes X] \otimes Y] = [N \otimes (X \otimes Y)]. \end{aligned}

N \otimes A \xrightarrow{\mathrm{id}} N \otimes A = [N \otimes A]

where A is atomic.

The key lemma is that a canonical composite built from associators and unitors does not affect the result of normalization. If f : X \cong Y is built only from associators and unitors, then the composite

\begin{aligned} N \otimes X &\xrightarrow{\mathrm{id}_N \otimes f} N \otimes Y \\ &\xrightarrow{\nu_{N,Y}} [N \otimes Y] \end{aligned}

is equal to the normalization isomorphism

\nu_{N,X} : N \otimes X \xrightarrow{\cong} [N \otimes X].

This is the point where the axioms of a monoidal category are actually used. When f is an associator, the proof uses the pentagon identity, and when f is a unitor, the proof uses the triangle identity.

Once the key lemma is available, one proves the coherence theorem by taking N = I. If f, g : X \cong Y are both built only from associators and unitors, then the key lemma gives

\nu_{I,Y} \circ (\mathrm{id}_I \otimes f) = \nu_{I,X} \qquad\text{and}\qquad \nu_{I,Y} \circ (\mathrm{id}_I \otimes g) = \nu_{I,X}.

Since \nu_{I,Y} is an isomorphism, it follows that

\mathrm{id}_I \otimes f = \mathrm{id}_I \otimes g.

The original maps are recovered from these tensorings by the left unitor:

f = (\lambda_X)^{-1} \circ (\mathrm{id}_I \otimes f) \circ \lambda_Y \qquad\text{and}\qquad g = (\lambda_X)^{-1} \circ (\mathrm{id}_I \otimes g) \circ \lambda_Y.

Therefore f = g.

The same proof works for bicategories, and the corresponding tactic is bicategory_coherence.

def

Mathlib.Tactic.Bicategory.pureCoherence (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)
Mathlib.Tactic.Bicategory.pureCoherence
  (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)

Close the goal of the form η.hom = θ.hom, where η and θ are 2-isomorphisms made up only of associators, unitors, and identities.

example {B : Type} [Bicategory B] {a : B} :
  (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom := by
  bicategory_coherence

2.1. Implementation