From e41208d80dcb8ee8ea1342c7cbcf1cd073cdd9d8 Mon Sep 17 00:00:00 2001
From: Oleksandr Manzyuk <manzyuk@gmail.com>
Date: Sun, 3 Apr 2022 00:36:47 +0000
Subject: [PATCH] feat(category_theory/monoidal): define monoidal structures on
 cartesian products of monoidal categories, (lax) monoidal functors and
 monoidal natural transformations (#13033)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR contains (fairly straightforward) definitions / proofs of the following facts:
- Cartesian product of monoidal categories is a monoidal category.
- Cartesian product of (lax) monoidal functors is a (lax) monoidal functor.
- Cartesian product of monoidal natural transformations is a monoidal natural transformation.

These are prerequisites to defining a monoidal category structure on the category of monoids in a braided monoidal category (with the approach that I've chosen).  In particular, the first bullet point above is a prerequisite to endowing the tensor product functor, viewed as a functor from `C × C` to `C`, where `C` is a braided monoidal category, with a strength that turns it into a monoidal functor (stacked  PR).

This fits as follows into the general strategy for defining a monoidal category structure on the category of monoids in a braided monoidal category `C`, at least conceptually:
first, define a monoidal category structure on the category of lax monoidal functors into `C`, and then transport this structure to the category `Mon_ C` of monoids along the equivalence between `Mon_ C` and the category `lax_monoid_functor (discrete punit) C`.  All, not necessarily lax monoidal functors into `C` form a monoidal category with "pointwise" tensor product.  The tensor product of two lax monoidal functors equals the composition of their cartesian product, which is lax monoidal, with the tensor product on`C`, which is monoidal if `C` is braided.  This gives a way to define a tensor product of two lax monoidal functors.  The details still need to be fleshed out.
---
 src/category_theory/monoidal/category.lean    | 45 +++++++++++
 src/category_theory/monoidal/functor.lean     | 75 +++++++++++++++++++
 .../monoidal/natural_transformation.lean      | 13 ++++
 src/category_theory/products/basic.lean       | 37 +++++++++
 4 files changed, 170 insertions(+)

diff --git a/src/category_theory/monoidal/category.lean b/src/category_theory/monoidal/category.lean
index 9deda9a754d7c..f3d03b1cb6ab0 100644
--- a/src/category_theory/monoidal/category.lean
+++ b/src/category_theory/monoidal/category.lean
@@ -600,6 +600,51 @@ end
 
 end
 
+section
+
+universes v₁ v₂ u₁ u₂
+
+variables (C₁ : Type u₁) [category.{v₁} C₁] [monoidal_category.{v₁} C₁]
+variables (C₂ : Type u₂) [category.{v₂} C₂] [monoidal_category.{v₂} C₂]
+
+local attribute [simp]
+associator_naturality left_unitor_naturality right_unitor_naturality pentagon
+
+@[simps tensor_obj tensor_hom tensor_unit associator]
+instance prod_monoidal : monoidal_category (C₁ × C₂) :=
+{ tensor_obj := λ X Y, (X.1 ⊗ Y.1, X.2 ⊗ Y.2),
+  tensor_hom := λ _ _ _ _ f g, (f.1 ⊗ g.1, f.2 ⊗ g.2),
+  tensor_unit := (𝟙_ C₁, 𝟙_ C₂),
+  associator := λ X Y Z, (α_ X.1 Y.1 Z.1).prod (α_ X.2 Y.2 Z.2),
+  left_unitor := λ ⟨X₁, X₂⟩, (λ_ X₁).prod (λ_ X₂),
+  right_unitor := λ ⟨X₁, X₂⟩, (ρ_ X₁).prod (ρ_ X₂) }
+
+@[simp] lemma prod_monoidal_left_unitor_hom_fst (X : C₁ × C₂) :
+  ((λ_ X).hom : (𝟙_ _) ⊗ X ⟶ X).1 = (λ_ X.1).hom := by { cases X, refl }
+
+@[simp] lemma prod_monoidal_left_unitor_hom_snd (X : C₁ × C₂) :
+  ((λ_ X).hom : (𝟙_ _) ⊗ X ⟶ X).2 = (λ_ X.2).hom := by { cases X, refl }
+
+@[simp] lemma prod_monoidal_left_unitor_inv_fst (X : C₁ × C₂) :
+  ((λ_ X).inv : X ⟶ (𝟙_ _) ⊗ X).1 = (λ_ X.1).inv := by { cases X, refl }
+
+@[simp] lemma prod_monoidal_left_unitor_inv_snd (X : C₁ × C₂) :
+  ((λ_ X).inv : X ⟶ (𝟙_ _) ⊗ X).2 = (λ_ X.2).inv := by { cases X, refl }
+
+@[simp] lemma prod_monoidal_right_unitor_hom_fst (X : C₁ × C₂) :
+  ((ρ_ X).hom : X ⊗ (𝟙_ _) ⟶ X).1 = (ρ_ X.1).hom := by { cases X, refl }
+
+@[simp] lemma prod_monoidal_right_unitor_hom_snd (X : C₁ × C₂) :
+  ((ρ_ X).hom : X ⊗ (𝟙_ _) ⟶ X).2 = (ρ_ X.2).hom := by { cases X, refl }
+
+@[simp] lemma prod_monoidal_right_unitor_inv_fst (X : C₁ × C₂) :
+  ((ρ_ X).inv : X ⟶ X ⊗ (𝟙_ _)).1 = (ρ_ X.1).inv := by { cases X, refl }
+
+@[simp] lemma prod_monoidal_right_unitor_inv_snd (X : C₁ × C₂) :
+  ((ρ_ X).inv : X ⟶ X ⊗ (𝟙_ _)).2 = (ρ_ X.2).inv := by { cases X, refl }
+
+end
+
 end monoidal_category
 
 end category_theory
diff --git a/src/category_theory/monoidal/functor.lean b/src/category_theory/monoidal/functor.lean
index 9211029b454f9..fdbf664adf0ee 100644
--- a/src/category_theory/monoidal/functor.lean
+++ b/src/category_theory/monoidal/functor.lean
@@ -5,6 +5,7 @@ Authors: Michael Jendrusch, Scott Morrison, Bhavik Mehta
 -/
 import category_theory.monoidal.category
 import category_theory.adjunction.basic
+import category_theory.products.basic
 
 /-!
 # (Lax) monoidal functors
@@ -288,6 +289,53 @@ infixr ` ⊗⋙ `:80 := comp
 
 end lax_monoidal_functor
 
+namespace lax_monoidal_functor
+universes v₀ u₀
+variables {B : Type u₀} [category.{v₀} B] [monoidal_category.{v₀} B]
+variables (F : lax_monoidal_functor.{v₀ v₁} B C) (G : lax_monoidal_functor.{v₂ v₃} D E)
+
+local attribute [simp] μ_natural associativity left_unitality right_unitality
+
+/-- The cartesian product of two lax monoidal functors is lax monoidal. -/
+@[simps]
+def prod : lax_monoidal_functor (B × D) (C × E) :=
+{ ε := (ε F, ε G),
+  μ := λ X Y, (μ F X.1 Y.1, μ G X.2 Y.2),
+  .. (F.to_functor).prod (G.to_functor) }
+
+end lax_monoidal_functor
+
+namespace monoidal_functor
+variable (C)
+
+/-- The diagonal functor as a monoidal functor. -/
+@[simps]
+def diag : monoidal_functor C (C × C) :=
+{ ε := 𝟙 _,
+  μ := λ X Y, 𝟙 _,
+  .. functor.diag C }
+
+end monoidal_functor
+
+namespace lax_monoidal_functor
+variables (F : lax_monoidal_functor.{v₁ v₂} C D) (G : lax_monoidal_functor.{v₁ v₃} C E)
+
+/-- The cartesian product of two lax monoidal functors starting from the same monoidal category `C`
+    is lax monoidal. -/
+def prod' : lax_monoidal_functor C (D × E) :=
+(monoidal_functor.diag C).to_lax_monoidal_functor ⊗⋙ (F.prod G)
+
+@[simp] lemma prod'_to_functor :
+  (F.prod' G).to_functor = (F.to_functor).prod' (G.to_functor) := rfl
+
+@[simp] lemma prod'_ε : (F.prod' G).ε = (F.ε, G.ε) :=
+by { dsimp [prod'], simp }
+
+@[simp] lemma prod'_μ (X Y : C) : (F.prod' G).μ X Y = (F.μ X Y, G.μ X Y) :=
+by { dsimp [prod'], simp }
+
+end lax_monoidal_functor
+
 namespace monoidal_functor
 
 variables (F : monoidal_functor.{v₁ v₂} C D) (G : monoidal_functor.{v₂ v₃} D E)
@@ -303,6 +351,33 @@ infixr ` ⊗⋙ `:80 := comp -- We overload notation; potentially dangerous, but
 
 end monoidal_functor
 
+namespace monoidal_functor
+universes v₀ u₀
+variables {B : Type u₀} [category.{v₀} B] [monoidal_category.{v₀} B]
+variables (F : monoidal_functor.{v₀ v₁} B C) (G : monoidal_functor.{v₂ v₃} D E)
+
+/-- The cartesian product of two monoidal functors is monoidal. -/
+@[simps]
+def prod : monoidal_functor (B × D) (C × E) :=
+{ ε_is_iso := (is_iso_prod_iff C E).mpr ⟨ε_is_iso F, ε_is_iso G⟩,
+  μ_is_iso := λ X Y, (is_iso_prod_iff C E).mpr ⟨μ_is_iso F X.1 Y.1, μ_is_iso G X.2 Y.2⟩,
+  .. (F.to_lax_monoidal_functor).prod (G.to_lax_monoidal_functor) }
+
+end monoidal_functor
+
+namespace monoidal_functor
+variables (F : monoidal_functor.{v₁ v₂} C D) (G : monoidal_functor.{v₁ v₃} C E)
+
+/-- The cartesian product of two monoidal functors starting from the same monoidal category `C`
+    is monoidal. -/
+def prod' : monoidal_functor C (D × E) := diag C ⊗⋙ (F.prod G)
+
+@[simp] lemma prod'_to_lax_monoidal_functor :
+    (F.prod' G).to_lax_monoidal_functor
+  = (F.to_lax_monoidal_functor).prod' (G.to_lax_monoidal_functor) := rfl
+
+end monoidal_functor
+
 /--
 If we have a right adjoint functor `G` to a monoidal functor `F`, then `G` has a lax monoidal
 structure as well.
diff --git a/src/category_theory/monoidal/natural_transformation.lean b/src/category_theory/monoidal/natural_transformation.lean
index 1b9787e64a5b6..2c981aed5aaae 100644
--- a/src/category_theory/monoidal/natural_transformation.lean
+++ b/src/category_theory/monoidal/natural_transformation.lean
@@ -103,6 +103,19 @@ def hcomp {F G : lax_monoidal_functor C D} {H K : lax_monoidal_functor D E}
   end,
   ..(nat_trans.hcomp α.to_nat_trans β.to_nat_trans) }
 
+section
+
+local attribute [simp] nat_trans.naturality monoidal_nat_trans.unit monoidal_nat_trans.tensor
+
+/-- The cartesian product of two monoidal natural transformations is monoidal. -/
+@[simps]
+def prod {F G : lax_monoidal_functor C D} {H K : lax_monoidal_functor C E}
+  (α : monoidal_nat_trans F G) (β : monoidal_nat_trans H K) :
+  monoidal_nat_trans (F.prod' H) (G.prod' K) :=
+{ app := λ X, (α.app X, β.app X) }
+
+end
+
 end monoidal_nat_trans
 
 namespace monoidal_nat_iso
diff --git a/src/category_theory/products/basic.lean b/src/category_theory/products/basic.lean
index f807623a3a060..c04ed48c87490 100644
--- a/src/category_theory/products/basic.lean
+++ b/src/category_theory/products/basic.lean
@@ -46,6 +46,31 @@ instance prod : category.{max v₁ v₂} (C × D) :=
 @[simp] lemma prod_comp {P Q R : C} {S T U : D} (f : (P, S) ⟶ (Q, T)) (g : (Q, T) ⟶ (R, U)) :
   f ≫ g = (f.1 ≫ g.1, f.2 ≫ g.2) := rfl
 
+lemma is_iso_prod_iff {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} :
+  is_iso f ↔ is_iso f.1 ∧ is_iso f.2 :=
+begin
+  split,
+  { rintros ⟨g, hfg, hgf⟩,
+    simp at hfg hgf,
+    rcases hfg with ⟨hfg₁, hfg₂⟩,
+    rcases hgf with ⟨hgf₁, hgf₂⟩,
+    exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩ },
+  { rintros ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩,
+    dsimp at hfg₁ hgf₁ hfg₂ hgf₂,
+    refine ⟨⟨(g₁, g₂), _, _⟩⟩; { simp; split; assumption } }
+end
+
+section
+variables {C D}
+
+/-- Construct an isomorphism in `C × D` out of two isomorphisms in `C` and `D`. -/
+@[simps]
+def iso.prod {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (P, S) ≅ (Q, T) :=
+{ hom := (f.hom, g.hom),
+  inv := (f.inv, g.inv), }
+
+end
+
 end
 
 section
@@ -164,6 +189,18 @@ namespace functor
 { obj := λ a, (F.obj a, G.obj a),
   map := λ x y f, (F.map f, G.map f), }
 
+section
+variable (C)
+
+/-- The diagonal functor. -/
+def diag : C ⥤ C × C := (𝟭 C).prod' (𝟭 C)
+
+@[simp] lemma diag_obj (X : C) : (diag C).obj X = (X, X) := rfl
+
+@[simp] lemma diag_map {X Y : C} (f : X ⟶ Y) : (diag C).map f = (f, f) := rfl
+
+end
+
 end functor
 
 namespace nat_trans