feat: add unitor functor for product of categories (#13663)

left and right unitor functors for product of categories



Co-authored-by: Shanghe Chen <[email protected]>

Mathlib.lean

@@ -1600,6 +1600,7 @@ import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
 import Mathlib.CategoryTheory.Products.Associator
 import Mathlib.CategoryTheory.Products.Basic
 import Mathlib.CategoryTheory.Products.Bifunctor
+import Mathlib.CategoryTheory.Products.Unitor
 import Mathlib.CategoryTheory.Quotient
 import Mathlib.CategoryTheory.Quotient.Linear
 import Mathlib.CategoryTheory.Quotient.Preadditive

Mathlib/CategoryTheory/Products/Associator.lean

@@ -53,6 +53,5 @@ instance inverseAssociatorIsEquivalence : (inverseAssociator C D E).IsEquivalenc
   (by infer_instance : (associativity C D E).inverse.IsEquivalence)
 #align category_theory.prod.inverse_associator_is_equivalence CategoryTheory.prod.inverseAssociatorIsEquivalence
 
--- TODO unitors?
 -- TODO pentagon natural transformation? ...satisfying?
 end CategoryTheory.prod

Mathlib/CategoryTheory/Products/Unitor.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2024 Shanghe Chen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shanghe Chen
+-/
+import Mathlib.CategoryTheory.Products.Basic
+import Mathlib.CategoryTheory.DiscreteCategory
+
+/-!
+# The left/right unitor equivalences `1 × C ≌ C` and `C × 1 ≌ C`.
+-/
+
+universe w v u
+
+open CategoryTheory
+
+namespace CategoryTheory.prod
+
+variable (C : Type u) [Category.{v} C]
+
+/-- The left unitor functor `1 × C ⥤ C` -/
+@[simps]
+def leftUnitor : Discrete (PUnit : Type w) × C ⥤ C where
+  obj X := X.2
+  map f := f.2
+
+/-- The right unitor functor `C × 1 ⥤ C` -/
+@[simps]
+def rightUnitor : C × Discrete (PUnit : Type w) ⥤ C where
+  obj X := X.1
+  map f := f.1
+
+/-- The left inverse unitor `C ⥤ 1 × C` -/
+@[simps]
+def leftInverseUnitor : C ⥤ Discrete (PUnit : Type w) × C where
+  obj X := ⟨⟨PUnit.unit⟩, X⟩
+  map f := ⟨𝟙 _, f⟩
+
+/-- The right inverse unitor `C ⥤ C × 1` -/
+@[simps]
+def rightInverseUnitor : C ⥤ C × Discrete (PUnit : Type w) where
+  obj X := ⟨X, ⟨PUnit.unit⟩⟩
+  map f := ⟨f, 𝟙 _⟩
+
+/-- The equivalence of categories expressing left unity of products of categories.  -/
+@[simps]
+def leftUnitorEquivalence : Discrete (PUnit : Type w) × C ≌ C where
+  functor := leftUnitor C
+  inverse := leftInverseUnitor C
+  unitIso := Iso.refl _
+  counitIso := Iso.refl _
+
+/-- The equivalence of categories expressing right unity of products of categories.  -/
+@[simps]
+def rightUnitorEquivalence : C × Discrete (PUnit : Type w) ≌ C where
+  functor := rightUnitor C
+  inverse := rightInverseUnitor C
+  unitIso := Iso.refl _
+  counitIso := Iso.refl _
+
+instance leftUnitor_isEquivalence : (leftUnitor C).IsEquivalence :=
+  (leftUnitorEquivalence C).isEquivalence_functor
+
+instance rightUnitor_isEquivalence : (rightUnitor C).IsEquivalence :=
+  (rightUnitorEquivalence C).isEquivalence_functor
+
+end CategoryTheory.prod