feat(CategoryTheory/Monoidal): add whiskerings to free monoidal categ…

…ories (#11172)

Since the coherence tactic assume that a certain defeq property holds for structural morphisms in a monoidal category and their corresponding morphisms in the free monoidal category, we want free monoidal categories to have the whiskering operators as primitives.

This PR also simplified the proof of the coherence theorem, and removed some porting notes.

Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

@@ -71,6 +71,8 @@ inductive Hom : F C → F C → Type u
   | ρ_hom (X : F C) : Hom (X.tensor unit) X
   | ρ_inv (X : F C) : Hom X (X.tensor unit)
   | comp {X Y Z} (f : Hom X Y) (g : Hom Y Z) : Hom X Z
+  | whiskerLeft (X : F C) {Y₁ Y₂} (f : Hom Y₁ Y₂) : Hom (X.tensor Y₁) (X.tensor Y₂)
+  | whiskerRight {X₁ X₂} (f : Hom X₁ X₂) (Y : F C) : Hom (X₁.tensor Y) (X₂.tensor Y)
   | tensor {W X Y Z} (f : Hom W Y) (g : Hom X Z) : Hom (W.tensor X) (Y.tensor Z)
 #align category_theory.free_monoidal_category.hom CategoryTheory.FreeMonoidalCategory.Hom
 
@@ -84,8 +86,14 @@ inductive HomEquiv : ∀ {X Y : F C}, (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop
   | trans {X Y} {f g h : X ⟶ᵐ Y} : HomEquiv f g → HomEquiv g h → HomEquiv f h
   | comp {X Y Z} {f f' : X ⟶ᵐ Y} {g g' : Y ⟶ᵐ Z} :
       HomEquiv f f' → HomEquiv g g' → HomEquiv (f.comp g) (f'.comp g')
+  | whiskerLeft (X) {Y Z} (f f' : Y ⟶ᵐ Z) :
+      HomEquiv f f' → HomEquiv (f.whiskerLeft X) (f'.whiskerLeft X)
+  | whiskerRight {Y Z} (f f' : Y ⟶ᵐ Z) (X) :
+      HomEquiv f f' → HomEquiv (f.whiskerRight X) (f'.whiskerRight X)
   | tensor {W X Y Z} {f f' : W ⟶ᵐ X} {g g' : Y ⟶ᵐ Z} :
       HomEquiv f f' → HomEquiv g g' → HomEquiv (f.tensor g) (f'.tensor g')
+  | tensorHom_def {X₁ Y₁ X₂ Y₂} (f : X₁ ⟶ᵐ Y₁) (g : X₂ ⟶ᵐ Y₂) :
+      HomEquiv (f.tensor g) ((f.whiskerRight X₂).comp (g.whiskerLeft Y₁))
   | comp_id {X Y} (f : X ⟶ᵐ Y) : HomEquiv (f.comp (Hom.id _)) f
   | id_comp {X Y} (f : X ⟶ᵐ Y) : HomEquiv ((Hom.id _).comp f) f
   | assoc {X Y U V : F C} (f : X ⟶ᵐ U) (g : U ⟶ᵐ V) (h : V ⟶ᵐ Y) :
@@ -94,6 +102,8 @@ inductive HomEquiv : ∀ {X Y : F C}, (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop
   | tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : F C} (f₁ : X₁ ⟶ᵐ Y₁) (f₂ : X₂ ⟶ᵐ Y₂) (g₁ : Y₁ ⟶ᵐ Z₁)
       (g₂ : Y₂ ⟶ᵐ Z₂) :
     HomEquiv ((f₁.comp g₁).tensor (f₂.comp g₂)) ((f₁.tensor f₂).comp (g₁.tensor g₂))
+  | whiskerLeft_id (X Y) : HomEquiv ((Hom.id Y).whiskerLeft X) (Hom.id (X.tensor Y))
+  | id_whiskerRight (X Y) : HomEquiv ((Hom.id X).whiskerRight Y) (Hom.id (X.tensor Y))
   | α_hom_inv {X Y Z} : HomEquiv ((Hom.α_hom X Y Z).comp (Hom.α_inv X Y Z)) (Hom.id _)
   | α_inv_hom {X Y Z} : HomEquiv ((Hom.α_inv X Y Z).comp (Hom.α_hom X Y Z)) (Hom.id _)
   | associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃} (f₁ : X₁ ⟶ᵐ Y₁) (f₂ : X₂ ⟶ᵐ Y₂) (f₃ : X₃ ⟶ᵐ Y₃) :
@@ -102,19 +112,19 @@ inductive HomEquiv : ∀ {X Y : F C}, (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop
   | ρ_hom_inv {X} : HomEquiv ((Hom.ρ_hom X).comp (Hom.ρ_inv X)) (Hom.id _)
   | ρ_inv_hom {X} : HomEquiv ((Hom.ρ_inv X).comp (Hom.ρ_hom X)) (Hom.id _)
   | ρ_naturality {X Y} (f : X ⟶ᵐ Y) :
-      HomEquiv ((f.tensor (Hom.id unit)).comp (Hom.ρ_hom Y)) ((Hom.ρ_hom X).comp f)
+      HomEquiv ((f.whiskerRight unit).comp (Hom.ρ_hom Y)) ((Hom.ρ_hom X).comp f)
   | l_hom_inv {X} : HomEquiv ((Hom.l_hom X).comp (Hom.l_inv X)) (Hom.id _)
   | l_inv_hom {X} : HomEquiv ((Hom.l_inv X).comp (Hom.l_hom X)) (Hom.id _)
   | l_naturality {X Y} (f : X ⟶ᵐ Y) :
-      HomEquiv (((Hom.id unit).tensor f).comp (Hom.l_hom Y)) ((Hom.l_hom X).comp f)
+      HomEquiv ((f.whiskerLeft unit).comp (Hom.l_hom Y)) ((Hom.l_hom X).comp f)
   | pentagon {W X Y Z} :
       HomEquiv
-        (((Hom.α_hom W X Y).tensor (Hom.id Z)).comp
-          ((Hom.α_hom W (X.tensor Y) Z).comp ((Hom.id W).tensor (Hom.α_hom X Y Z))))
+        (((Hom.α_hom W X Y).whiskerRight Z).comp
+          ((Hom.α_hom W (X.tensor Y) Z).comp ((Hom.α_hom X Y Z).whiskerLeft W)))
         ((Hom.α_hom (W.tensor X) Y Z).comp (Hom.α_hom W X (Y.tensor Z)))
   | triangle {X Y} :
-      HomEquiv ((Hom.α_hom X unit Y).comp ((Hom.id X).tensor (Hom.l_hom Y)))
-        ((Hom.ρ_hom X).tensor (Hom.id Y))
+      HomEquiv ((Hom.α_hom X unit Y).comp ((Hom.l_hom Y).whiskerLeft X))
+        ((Hom.ρ_hom X).whiskerRight Y)
 set_option linter.uppercaseLean3 false
 #align category_theory.free_monoidal_category.HomEquiv CategoryTheory.FreeMonoidalCategory.HomEquiv
 
@@ -135,13 +145,8 @@ open FreeMonoidalCategory.HomEquiv
 
 instance categoryFreeMonoidalCategory : Category.{u} (F C) where
   Hom X Y := Quotient (FreeMonoidalCategory.setoidHom X Y)
-  id X := ⟦FreeMonoidalCategory.Hom.id _⟧
-  comp := @fun X Y Z f g =>
-    Quotient.map₂ Hom.comp
-      (by
-        intro f f' hf g g' hg
-        exact comp hf hg)
-      f g
+  id X := ⟦Hom.id X⟧
+  comp := Quotient.map₂ Hom.comp (fun _ _ hf _ _ hg ↦ HomEquiv.comp hf hg)
   id_comp := by
     rintro X Y ⟨f⟩
     exact Quotient.sound (id_comp f)
@@ -155,36 +160,18 @@ instance categoryFreeMonoidalCategory : Category.{u} (F C) where
 
 instance : MonoidalCategory (F C) where
   tensorObj X Y := FreeMonoidalCategory.tensor X Y
-  tensorHom := @fun X₁ Y₁ X₂ Y₂ =>
-    Quotient.map₂ Hom.tensor <| by
-      intro _ _ h _ _ h'
-      exact HomEquiv.tensor h h'
-  whiskerLeft := fun X _ _ f =>
-    Quotient.map (fun f' => Hom.tensor (Hom.id X) f')
-      (fun _ _ h => HomEquiv.tensor (HomEquiv.refl (Hom.id X)) h) f
-  whiskerRight := fun f Y =>
-    Quotient.map (fun f' => Hom.tensor f' (Hom.id Y))
-      (fun _ _ h => HomEquiv.tensor h (HomEquiv.refl (Hom.id Y))) f
+  tensorHom := Quotient.map₂ Hom.tensor (fun _ _ hf _ _ hg ↦ HomEquiv.tensor hf hg)
+  whiskerLeft X _ _ f := Quot.map (fun f ↦ Hom.whiskerLeft X f) (fun f f' ↦ .whiskerLeft X f f') f
+  whiskerRight f Y := Quot.map (fun f ↦ Hom.whiskerRight f Y) (fun f f' ↦ .whiskerRight f f' Y) f
   tensorHom_def := by
     rintro W X Y Z ⟨f⟩ ⟨g⟩
-    apply Quotient.sound
-    calc Hom.tensor f g
-      _ ≈ Hom.tensor (Hom.comp f (Hom.id X)) (Hom.comp (Hom.id Y) g) := by
-        apply HomEquiv.tensor (HomEquiv.comp_id f).symm (HomEquiv.id_comp g).symm
-      _ ≈ Hom.comp (Hom.tensor f (Hom.id Y)) (Hom.tensor (Hom.id X) g) := by
-        apply HomEquiv.tensor_comp
-  whiskerLeft_id := by
-    rintro X Y
-    apply Quotient.sound
-    apply HomEquiv.tensor_id
-  id_whiskerRight := by
-    intro X Y
-    apply Quotient.sound
-    apply HomEquiv.tensor_id
-  tensor_id X Y := Quotient.sound tensor_id
+    exact Quotient.sound (tensorHom_def _ _)
+  tensor_id X Y := Quot.sound tensor_id
   tensor_comp := @fun X₁ Y₁ Z₁ X₂ Y₂ Z₂ => by
     rintro ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩
     exact Quotient.sound (tensor_comp _ _ _ _)
+  whiskerLeft_id X Y := Quot.sound (HomEquiv.whiskerLeft_id X Y)
+  id_whiskerRight X Y := Quot.sound (HomEquiv.id_whiskerRight X Y)
   tensorUnit := FreeMonoidalCategory.unit
   associator X Y Z :=
     ⟨⟦Hom.α_hom X Y Z⟧, ⟦Hom.α_inv X Y Z⟧, Quotient.sound α_hom_inv, Quotient.sound α_inv_hom⟩
@@ -215,6 +202,16 @@ theorem mk_tensor {X₁ Y₁ X₂ Y₂ : F C} (f : X₁ ⟶ᵐ Y₁) (g : X₂ 
   rfl
 #align category_theory.free_monoidal_category.mk_tensor CategoryTheory.FreeMonoidalCategory.mk_tensor
 
+@[simp]
+theorem mk_whiskerLeft (X : F C) {Y₁ Y₂ : F C} (f : Y₁ ⟶ᵐ Y₂) :
+    ⟦f.whiskerLeft X⟧ = MonoidalCategory.whiskerLeft (C := F C) (X := X) (f := ⟦f⟧) :=
+  rfl
+
+@[simp]
+theorem mk_whiskerRight {X₁ X₂ : F C} (f : X₁ ⟶ᵐ X₂) (Y : F C) :
+    ⟦f.whiskerRight Y⟧ = MonoidalCategory.whiskerRight (C := F C) (f := ⟦f⟧) (Y := Y) :=
+  rfl
+
 @[simp]
 theorem mk_id {X : F C} : ⟦Hom.id X⟧ = 𝟙 X :=
   rfl
@@ -260,6 +257,44 @@ theorem unit_eq_unit : FreeMonoidalCategory.unit = 𝟙_ (F C) :=
   rfl
 #align category_theory.free_monoidal_category.unit_eq_unit CategoryTheory.FreeMonoidalCategory.unit_eq_unit
 
+/-- The abbreviation for `⟦f⟧`. -/
+/- This is useful since the notation `⟦f⟧` often behaves like an element of the quotient set,
+but not like a morphism. This is why we need weird `@CategoryStruct.comp (F C) ...` in the
+statement in `mk_comp` above. -/
+abbrev homMk {X Y : F C} (f : X ⟶ᵐ Y) : X ⟶ Y := ⟦f⟧
+
+theorem Hom.inductionOn {motive : {X Y : F C} → (X ⟶ Y) → Prop} {X Y : F C} (t : X ⟶ Y)
+    (id : (X : F C) → motive (𝟙 X))
+    (α_hom : (X Y Z : F C) → motive (α_ X Y Z).hom)
+    (α_inv : (X Y Z : F C) → motive (α_ X Y Z).inv)
+    (l_hom : (X : F C) → motive (λ_ X).hom)
+    (l_inv : (X : F C) → motive (λ_ X).inv)
+    (ρ_hom : (X : F C) → motive (ρ_ X).hom)
+    (ρ_inv : (X : F C) → motive (ρ_ X).inv)
+    (comp : {X Y Z : F C} → (f : X ⟶ Y) → (g : Y ⟶ Z) → motive f → motive g → motive (f ≫ g))
+    (whiskerLeft : (X : F C) → {Y Z : F C} → (f : Y ⟶ Z) → motive f → motive (X ◁ f))
+    (whiskerRight : {X Y : F C} → (f : X ⟶ Y) → (Z : F C) → motive f → motive (f ▷ Z)) :
+    motive t := by
+  apply Quotient.inductionOn
+  intro f
+  induction f with
+  | id X => exact id X
+  | α_hom X Y Z => exact α_hom X Y Z
+  | α_inv X Y Z => exact α_inv X Y Z
+  | l_hom X => exact l_hom X
+  | l_inv X => exact l_inv X
+  | ρ_hom X => exact ρ_hom X
+  | ρ_inv X => exact ρ_inv X
+  | comp f g hf hg => exact comp _ _ (hf ⟦f⟧) (hg ⟦g⟧)
+  | whiskerLeft X f hf => exact whiskerLeft X _ (hf ⟦f⟧)
+  | whiskerRight f X hf => exact whiskerRight _ X (hf ⟦f⟧)
+  | @tensor W X Y Z f g hf hg =>
+      have : homMk f ⊗ homMk g = homMk f ▷ X ≫ Y ◁ homMk g :=
+        Quotient.sound (HomEquiv.tensorHom_def f g)
+      change motive (homMk f ⊗ homMk g)
+      rw [this]
+      exact comp _ _ (whiskerRight _ _ (hf ⟦f⟧)) (whiskerLeft _ _ (hg ⟦g⟧))
+
 section Functor
 
 variable {D : Type u'} [Category.{v'} D] [MonoidalCategory D] (f : C → D)
@@ -288,6 +323,8 @@ def projectMapAux : ∀ {X Y : F C}, (X ⟶ᵐ Y) → (projectObj f X ⟶ projec
   | _, _, ρ_hom _ => (ρ_ _).hom
   | _, _, ρ_inv _ => (ρ_ _).inv
   | _, _, Hom.comp f g => projectMapAux f ≫ projectMapAux g
+  | _, _, Hom.whiskerLeft X p => projectObj f X ◁ projectMapAux p
+  | _, _, Hom.whiskerRight p X => projectMapAux p ▷ projectObj f X
   | _, _, Hom.tensor f g => projectMapAux f ⊗ projectMapAux g
 #align category_theory.free_monoidal_category.project_map_aux CategoryTheory.FreeMonoidalCategory.projectMapAux
 
@@ -301,12 +338,22 @@ def projectMap (X Y : F C) : (X ⟶ Y) → (projectObj f X ⟶ projectObj f Y) :
     | symm _ _ _ hfg' => exact hfg'.symm
     | trans _ _ hfg hgh => exact hfg.trans hgh
     | comp _ _ hf hg => dsimp only [projectMapAux]; rw [hf, hg]
+    | whiskerLeft _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
+    | whiskerRight _ _ _ _ hf => dsimp only [projectMapAux, projectObj]; rw [hf]
     | tensor _ _ hfg hfg' => dsimp only [projectMapAux]; rw [hfg, hfg']
+    | tensorHom_def _ _ =>
+        dsimp only [projectMapAux, projectObj]; rw [MonoidalCategory.tensorHom_def]
     | comp_id => dsimp only [projectMapAux]; rw [Category.comp_id]
     | id_comp => dsimp only [projectMapAux]; rw [Category.id_comp]
     | assoc => dsimp only [projectMapAux]; rw [Category.assoc]
     | tensor_id => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_id]; rfl
     | tensor_comp => dsimp only [projectMapAux]; rw [MonoidalCategory.tensor_comp]
+    | whiskerLeft_id =>
+        dsimp only [projectMapAux, projectObj]
+        rw [MonoidalCategory.whiskerLeft_id]
+    | id_whiskerRight =>
+        dsimp only [projectMapAux, projectObj]
+        rw [MonoidalCategory.id_whiskerRight]
     | α_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
     | α_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
     | associator_naturality =>
@@ -315,21 +362,18 @@ def projectMap (X Y : F C) : (X ⟶ Y) → (projectObj f X ⟶ projectObj f Y) :
     | ρ_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
     | ρ_naturality =>
         dsimp only [projectMapAux, projectObj]
-        rw [tensorHom_id, MonoidalCategory.rightUnitor_naturality]
+        rw [MonoidalCategory.rightUnitor_naturality]
     | l_hom_inv => dsimp only [projectMapAux]; rw [Iso.hom_inv_id]
     | l_inv_hom => dsimp only [projectMapAux]; rw [Iso.inv_hom_id]
     | l_naturality =>
         dsimp only [projectMapAux, projectObj]
-        rw [id_tensorHom]
-        exact MonoidalCategory.leftUnitor_naturality _
+        rw [MonoidalCategory.leftUnitor_naturality]
     | pentagon =>
-        dsimp only [projectMapAux]
-        simp only [tensorHom_id, id_tensorHom]
-        exact MonoidalCategory.pentagon _ _ _ _
+        dsimp only [projectMapAux, projectObj]
+        rw [MonoidalCategory.pentagon]
     | triangle =>
-        dsimp only [projectMapAux]
-        simp only [tensorHom_id, id_tensorHom]
-        exact MonoidalCategory.triangle _ _
+        dsimp only [projectMapAux, projectObj]
+        rw [MonoidalCategory.triangle]
 #align category_theory.free_monoidal_category.project_map CategoryTheory.FreeMonoidalCategory.projectMap
 
 end