Coherence Tactics

3.1. monoidal and bicategory🔗

This chapter is about the user-facing tactics monoidal and bicategory. The previous chapter treated the coherence theorem and the tactics monoidal_coherence and bicategory_coherence. Here the focus is on the more common situation where a goal contains actual maps, and coherence is only part of the proof.

3.1.1. The monoidal Tactic🔗

The tactic monoidal solves equalities of morphisms in a monoidal category when the same actual morphisms (such as f and g) appear in the same order on both sides, and only the surrounding coherence data differ.

🔗def
Mathlib.Tactic.Monoidal.monoidal (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)
Mathlib.Tactic.Monoidal.monoidal
  (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)

Use the coherence theorem for monoidal categories to solve equations in a monoidal category, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, monoidal can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using monoidal_coherence.

In typical use, the rewriting lemmas that change the actual morphisms are applied first. Once those morphisms already match on both sides, monoidal is used to prove that the remaining structural part (that is, the part built only from associators and unitors) is equal on the two sides. The calc pattern below is the usual way to reach that point in a proof.

3.1.2. The bicategory Tactic🔗

The tactic bicategory is the bicategorical analogue of monoidal. It applies when the same actual 2-morphisms, such as η, ε, or a naturality map, appear in the same order on both sides, and only the surrounding coherence data differ.

🔗def
Mathlib.Tactic.Bicategory.bicategory (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)
Mathlib.Tactic.Bicategory.bicategory
  (mvarId : Lean.MVarId) :
  Lean.MetaM (List Lean.MVarId)

Use the coherence theorem for bicategories to solve equations in a bicategory, where the two sides only differ by replacing strings of bicategory structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, bicategory can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using bicategory_coherence.

In typical use, the rewriting lemmas that change the actual 2-morphisms are applied first. Once those 2-morphisms already match on both sides, bicategory is used to remove the remaining coherence layer. The bicategorical proof in the overview is the main example of this pattern.

3.1.3. Working in calc🔗

In practice, these tactics are most useful inside a calc block. As in the overview, one writes the mathematically meaningful rewrites as the lines of the calc, and uses the tactic only for the intermediate steps where the two sides differ by associators and unitors. To use rw, one often has to place parentheses appropriately so that the lemma at hand applies. This creates intermediate goals in which only the coherence data differ.

The monoidal example below shows this pattern explicitly:

theorem monoidal_calc {C : Type*} [Category C] [MonoidalCategory C] [BraidedCategory C] (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) : tensorμ (X₁ ⊗ X₂) X₃ (Y₁ ⊗ Y₂) Y₃ ≫ (tensorμ X₁ X₂ Y₁ Y₂ ▷ (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫ tensorμ X₁ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃) ≫ ((X₁ ⊗ Y₁) ◁ tensorμ X₂ X₃ Y₂ Y₃) := C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ tensorμ (X₁ ⊗ X₂) X₃ (Y₁ ⊗ Y₂) Y₃ ≫ tensorμ X₁ X₂ Y₁ Y₂ ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫ tensorμ X₁ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃) ≫ (X₁ ⊗ Y₁) ◁ tensorμ X₂ X₃ Y₂ Y₃ C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫ (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫ (X₁ ⊗ X₂) ◁ (β_ X₃ (Y₁ ⊗ Y₂)).hom ▷ Y₃ ≫ (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫ ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫ X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫ ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫ X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫ X₁ ◁ (β_ (X₂ ⊗ X₃) Y₁).hom ▷ (Y₂ ⊗ Y₃) ≫ X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫ (X₁ ⊗ Y₁) ◁ ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫ X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv) with_panel_widgets [Mathlib.Tactic.Widget.StringDiagram] calc _ = 𝟙 _ ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 _ := C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫ (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫ (X₁ ⊗ X₂) ◁ (β_ X₃ (Y₁ ⊗ Y₂)).hom ▷ Y₃ ≫ (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫ ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫ X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫ (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫ (X₁ ⊗ X₂) ◁ ((α_ X₃ Y₁ Y₂).inv ≫ (β_ X₃ Y₁).hom ▷ Y₂ ≫ (α_ Y₁ X₃ Y₂).hom ≫ Y₁ ◁ (β_ X₃ Y₂).hom ≫ (α_ Y₁ Y₂ X₃).inv) ▷ Y₃ ≫ (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫ ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫ X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) All goals completed! 🐙 _ = 𝟙 _ ⊗≫ X₁ ◁ (((α_ X₂ X₃ Y₁).hom ≫ X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom)) ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ Y₁ ◁ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ⊗≫ 𝟙 _ := C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) = 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ ((α_ X₂ X₃ Y₁).hom ≫ X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom) ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ Y₁ ◁ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ ((β_ X₂ Y₁).hom ▷ (X₃ ⊗ Y₂) ≫ (Y₁ ⊗ X₂) ◁ (β_ X₃ Y₂).hom) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) = 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ ((α_ X₂ X₃ Y₁).hom ≫ X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom) ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ Y₁ ◁ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) All goals completed! 🐙 _ = _ := C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ ((α_ X₂ X₃ Y₁).hom ≫ X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom) ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ Y₁ ◁ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) = ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫ ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫ X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫ X₁ ◁ (β_ (X₂ ⊗ X₃) Y₁).hom ▷ (Y₂ ⊗ Y₃) ≫ X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫ (X₁ ⊗ Y₁) ◁ ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫ X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv) C:Type u_1inst✝²:Category.{u_2, u_1} Cinst✝¹:MonoidalCategory Cinst✝:BraidedCategory CX₁:CX₂:CX₃:CY₁:CY₂:CY₃:C⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫ X₁ ◁ (β_ (X₂ ⊗ X₃) Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫ X₁ ◁ Y₁ ◁ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) = ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫ ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫ X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫ X₁ ◁ (β_ (X₂ ⊗ X₃) Y₁).hom ▷ (Y₂ ⊗ Y₃) ≫ X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫ (X₁ ⊗ Y₁) ◁ ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫ X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv) All goals completed! 🐙

The visible rewrites come from the braiding lemmas and the exchange law, while monoidal closes the remaining coherence step after each rewrite.

This proof can also be visualized with the string diagram widget Mathlib.Tactic.Widget.StringDiagram. As in the overview, Verso does not display the widget directly yet, so the diagrams are shown below without mouseover Lean information:

Step 1.

Loading string diagram...

Step 2.

Loading string diagram...

Step 3.

Loading string diagram...

3.1.4. Tracing🔗

To inspect the normalization performed by the tactics, enable tracing with set_option trace.monoidal true or set_option trace.bicategory true. The trace output prints the normalization steps.