Monoidal composition

Stream: maths

[Antoine Labelle]

I'm currently trying to understand the various tricks used in mathlib to avoid extremely tedious manipulations of unitors and associators in monoidal categories. docs#category_theory.monoidal_category.monoidal_comp seems interesting, but I'm having trouble understanding how to manipulate it. For example, how would you prove the following monoidal_comp version of docs#category_theory.monoidal_category.id_tensor_comp? We probably need the coherence tactic to do that but by itself it doesn't work.

 import category_theory.monoidal.coherence

open category_theory category_theory.monoidal_category

variables {C : Type*} [category C] [monoidal_category C]

example (A W X Y Z : C) (f : W ⟶ X) (g : Y ⟶ Z) [monoidal_coherence X Y] :
  (𝟙 A) ⊗ (f ⊗≫ g) = ((𝟙 A) ⊗ f) ⊗≫ ((𝟙 A) ⊗ g) := sorry

[Kevin Buzzard]

example (A W X Y Z : C) (f : W ⟶ X) (g : Y ⟶ Z) [monoidal_coherence X Y] :
  (𝟙 A) ⊗ (f ⊗≫ g) = ((𝟙 A) ⊗ f) ⊗≫ ((𝟙 A) ⊗ g) :=
by simp [tensor_hom, monoidal_comp]

[Antoine Labelle]

Thanks. Weirdly I can't even state the analog for right tensoring by the identity because monoidal_coherence (X ⊗ A) (Y ⊗ A) isn't an instance. The left version is docs#category_theory.monoidal_category.monoidal_coherence.tensor but we don't have the right version.

[Antoine Labelle]

I'm getting some very weird behavior with monoidal_coherence. The first example here fails with an error message "failed to synthesize type class instance for monoidal_coherence X (X ⊗ 𝟙_ C)", but this instance does exist as shown by the second example:

import category_theory.monoidal.coherence

open category_theory category_theory.monoidal_category

variables {C : Type*} [category C] [monoidal_category C]

lemma id_tensor_monoidal_comp (A : C) {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) [monoidal_coherence X Y] :
  (𝟙 A) ⊗ (f ⊗≫ g) = ((𝟙 A) ⊗ f) ⊗≫ ((𝟙 A) ⊗ g) := by simp [monoidal_comp]

example (A : C) {W X Z : C} (f : W ⟶ X) (g : (X ⊗ 𝟙_ C) ⟶ Z) :
  (𝟙 A) ⊗ (f ⊗≫ g) = ((𝟙 A) ⊗ f) ⊗≫ ((𝟙 A) ⊗ g) :=
  id_tensor_monoidal_comp A f g

example (X : C) : monoidal_coherence X (X ⊗ 𝟙_ C) := by apply_instance

Does anyone have an explanation?

[Reid Barton]

id_tensor_monoidal_comp is not general enough because it picked the "refl" instance of docs#category_theory.monoidal_category.monoidal_coherence.
You can fix it with

lemma id_tensor_monoidal_comp (A : C) {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z)
  [lift_obj X] [lift_obj Y] [monoidal_coherence X Y] : ...

[Antoine Labelle]

It works but I'm not sure I understand what lift_obj is doing here. What do you mean when you say it picked the "refl" instance?

[Antoine Labelle]

Also, even with lift_obj added the following fails

import category_theory.monoidal.coherence

open category_theory category_theory.monoidal_category

variables {C : Type*} [category C] [monoidal_category C]

lemma id_tensor_monoidal_comp (A : C) {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z)
  [lift_obj X] [lift_obj Y] [monoidal_coherence X Y] :
  (𝟙 A) ⊗ (f ⊗≫ g) = ((𝟙 A) ⊗ f) ⊗≫ ((𝟙 A) ⊗ g) := by simp [monoidal_comp]

example {W X Z : C} (f : W ⟶ X) (g : (X ⊗ 𝟙_ C) ⟶ Z) :
  (𝟙 (𝟙_ C)) ⊗ (f ⊗≫ g) = ((𝟙 (𝟙_ C)) ⊗ f) ⊗≫ ((𝟙 (𝟙_ C)) ⊗ g) :=
id_tensor_monoidal_comp (𝟙_ C) f g

[Reid Barton]

Whoops, I was looking at the wrong thing before. I actually meant the "of" instance of docs#category_theory.monoidal_category.lift_obj .

[Reid Barton]

But I don't actually understand how this works, and in particular why monoidal_coherence requires lift_obj instance but then doesn't use them at all.

[Antoine Labelle]

@Scott Morrison Are you familiar with that?