feat(AlgebraicTopology): the monoidal category structure on simplicia…

…l sets (#11396)

If a category `C` has chosen finite products, then the functor category `J ⥤ C` also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products. 

Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of `Functor.empty.{0} C` rather than `Functor.empty.{v} C` so as to be consistent with the limits API for terminal objects.

Co-authored-by: Jack McKoen <mckoen@ualberta.ca>

Mathlib.lean

@@ -598,6 +598,7 @@ import Mathlib.AlgebraicTopology.Quasicategory
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialSet
+import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
 import Mathlib.AlgebraicTopology.SingularSet
 import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.TopologicalSimplex
@@ -1067,6 +1068,7 @@ import Mathlib.CategoryTheory.Category.RelCat
 import Mathlib.CategoryTheory.Category.TwoP
 import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.ChosenFiniteProducts
+import Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory
 import Mathlib.CategoryTheory.Closed.Cartesian
 import Mathlib.CategoryTheory.Closed.Functor
 import Mathlib.CategoryTheory.Closed.FunctorCategory

Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Jack McKoen
+-/
+import Mathlib.AlgebraicTopology.SimplicialSet
+import Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory
+import Mathlib.CategoryTheory.Monoidal.Types.Basic
+
+/-!
+# The monoidal category structure on simplicial sets
+
+This file defines an instance of chosen finite products
+for the category `SSet`. It follows from the fact
+the `SSet` if a category of functors to the category
+of types and that the category of types have chosen
+finite products. As a result, we obtain a monoidal
+category structure on `SSet`.
+
+-/
+
+universe u
+
+open Simplicial CategoryTheory MonoidalCategory
+
+namespace SSet
+
+noncomputable instance : ChosenFiniteProducts SSet.{u} :=
+  (inferInstance : ChosenFiniteProducts (SimplexCategoryᵒᵖ ⥤ Type u))
+
+@[simp]
+lemma leftUnitor_hom_app_apply (K : SSet.{u}) {Δ : SimplexCategoryᵒᵖ} (x : (𝟙_ _ ⊗ K).obj Δ) :
+    (λ_ K).hom.app Δ x = x.2 := rfl
+
+@[simp]
+lemma leftUnitor_inv_app_apply (K : SSet.{u}) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ) :
+    (λ_ K).inv.app Δ x = ⟨PUnit.unit, x⟩ := rfl
+
+@[simp]
+lemma rightUnitor_hom_app_apply (K : SSet.{u}) {Δ : SimplexCategoryᵒᵖ} (x : (K ⊗ 𝟙_ _).obj Δ) :
+    (ρ_ K).hom.app Δ x = x.1 := rfl
+
+@[simp]
+lemma rightUnitor_inv_app_apply (K : SSet.{u}) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ) :
+    (ρ_ K).inv.app Δ x = ⟨x, PUnit.unit⟩ := rfl
+
+@[simp]
+lemma tensorHom_app_apply {K K' L L' : SSet.{u}} (f : K ⟶ K') (g : L ⟶ L')
+    {Δ : SimplexCategoryᵒᵖ} (x : (K ⊗ L).obj Δ) :
+    (f ⊗ g).app Δ x = ⟨f.app Δ x.1, g.app Δ x.2⟩ := rfl
+
+@[simp]
+lemma whiskerLeft_app_apply (K : SSet.{u}) {L L' : SSet.{u}} (g : L ⟶ L')
+    {Δ : SimplexCategoryᵒᵖ} (x : (K ⊗ L).obj Δ) :
+    (K ◁ g).app Δ x = ⟨x.1, g.app Δ x.2⟩ := rfl
+
+@[simp]
+lemma whiskerRight_app_apply {K K' : SSet.{u}} (f : K ⟶ K') (L : SSet.{u})
+    {Δ : SimplexCategoryᵒᵖ} (x : (K ⊗ L).obj Δ) :
+    (f ▷ L).app Δ x = ⟨f.app Δ x.1, x.2⟩ := rfl
+
+@[simp]
+lemma associator_hom_app_apply (K L M : SSet.{u}) {Δ : SimplexCategoryᵒᵖ}
+    (x : ((K ⊗ L) ⊗ M).obj Δ) :
+    (α_ K L M).hom.app Δ x = ⟨x.1.1, x.1.2, x.2⟩ := rfl
+
+@[simp]
+lemma associator_inv_app_apply (K L M : SSet.{u}) {Δ : SimplexCategoryᵒᵖ}
+    (x : (K ⊗ L ⊗ M).obj Δ) :
+    (α_ K L M).inv.app Δ x = ⟨⟨x.1, x.2.1⟩, x.2.2⟩ := rfl
+
+/-- The bijection `(𝟙_ SSet ⟶ K) ≃ K _[0]`. -/
+def unitHomEquiv (K : SSet.{u}) : (𝟙_ _ ⟶ K) ≃ K _[0] where
+  toFun φ := φ.app _ PUnit.unit
+  invFun x :=
+    { app := fun Δ _ => K.map (SimplexCategory.const Δ.unop [0] 0).op x
+      naturality := fun Δ Δ' f => by
+        ext ⟨⟩
+        dsimp
+        rw [← FunctorToTypes.map_comp_apply]
+        rfl }
+  left_inv φ := by
+    ext Δ ⟨⟩
+    dsimp
+    rw [← FunctorToTypes.naturality]
+    rfl
+  right_inv x := by simp
+
+end SSet

Mathlib/CategoryTheory/ChosenFiniteProducts.lean

@@ -41,7 +41,7 @@ class ChosenFiniteProducts (C : Type u) [Category.{v} C] where
   /-- A choice of a limit binary fan for any two objects of the category.-/
   product : (X Y : C) → Limits.LimitCone (Limits.pair X Y)
   /-- A choice of a terminal object. -/
-  terminal : Limits.LimitCone (Functor.empty.{v} C)
+  terminal : Limits.LimitCone (Functor.empty.{0} C)
 
 namespace ChosenFiniteProducts
 
@@ -110,6 +110,66 @@ lemma hom_ext {T X Y : C} (f g : T ⟶ X ⊗ Y)
     f = g :=
   (product X Y).isLimit.hom_ext fun ⟨j⟩ => j.recOn h_fst h_snd
 
+@[reassoc (attr := simp)]
+lemma tensorHom_fst {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
+    (f ⊗ g) ≫ fst _ _ = fst _ _ ≫ f := lift_fst _ _
+
+@[reassoc (attr := simp)]
+lemma tensorHom_snd {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
+    (f ⊗ g) ≫ snd _ _ = snd _ _ ≫ g := lift_snd _ _
+
+@[reassoc (attr := simp)]
+lemma whiskerLeft_fst (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
+    (X ◁ g) ≫ fst _ _ = fst _ _ :=
+  (tensorHom_fst _ _).trans (by simp)
+
+@[reassoc (attr := simp)]
+lemma whiskerLeft_snd (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
+    (X ◁ g) ≫ snd _ _ = snd _ _ ≫ g :=
+  tensorHom_snd _ _
+
+@[reassoc (attr := simp)]
+lemma whiskerRight_fst {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
+    (f ▷ Y) ≫ fst _ _ = fst _ _ ≫ f :=
+  tensorHom_fst _ _
+
+@[reassoc (attr := simp)]
+lemma whiskerRight_snd {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
+    (f ▷ Y) ≫ snd _ _ = snd _ _ :=
+  (tensorHom_snd _ _).trans (by simp)
+
+@[reassoc (attr := simp)]
+lemma associator_hom_fst (X Y Z : C) :
+    (α_ X Y Z).hom ≫ fst _ _ = fst _ _ ≫ fst _ _ := lift_fst _ _
+
+@[reassoc (attr := simp)]
+lemma associator_hom_snd_fst (X Y Z : C) :
+    (α_ X Y Z).hom ≫ snd _ _ ≫ fst _ _ = fst _ _ ≫ snd _ _  := by
+  erw [lift_snd_assoc, lift_fst]
+  rfl
+
+@[reassoc (attr := simp)]
+lemma associator_hom_snd_snd (X Y Z : C) :
+    (α_ X Y Z).hom ≫ snd _ _ ≫ snd _ _ = snd _ _  := by
+  erw [lift_snd_assoc, lift_snd]
+  rfl
+
+@[reassoc (attr := simp)]
+lemma associator_inv_fst (X Y Z : C) :
+    (α_ X Y Z).inv ≫ fst _ _ ≫ fst _ _ = fst _ _ := by
+  erw [lift_fst_assoc, lift_fst]
+  rfl
+
+@[reassoc (attr := simp)]
+lemma associator_inv_fst_snd (X Y Z : C) :
+    (α_ X Y Z).inv ≫ fst _ _ ≫ snd _ _ = snd _ _ ≫ fst _ _ := by
+  erw [lift_fst_assoc, lift_snd]
+  rfl
+
+@[reassoc (attr := simp)]
+lemma associator_inv_snd (X Y Z : C) :
+    (α_ X Y Z).inv ≫ snd _ _ = snd _ _ ≫ snd _ _ := lift_snd _ _
+
 /--
 Construct an instance of `ChosenFiniteProducts C` given an instance of `HasFiniteProducts C`.
 -/

Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean

@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.ChosenFiniteProducts
+import Mathlib.CategoryTheory.Limits.FunctorCategory
+
+/-!
+# Functor categories have chosen finite products
+
+If `C` is a category with chosen finite products, then so is `J ⥤ C`.
+
+-/
+
+namespace CategoryTheory
+
+open Limits MonoidalCategory Category
+
+variable (J C : Type*) [Category J] [Category C] [ChosenFiniteProducts C]
+
+namespace Functor
+
+/-- The chosen terminal object in `J ⥤ C`. -/
+abbrev chosenTerminal : J ⥤ C := ((Functor.const J).obj (𝟙_ C))
+
+/-- The chosen terminal object in `J ⥤ C` is terminal. -/
+def chosenTerminalIsTerminal : IsTerminal (chosenTerminal J C) :=
+  evaluationJointlyReflectsLimits _
+    (fun _ => isLimitChangeEmptyCone _ ChosenFiniteProducts.terminal.2 _ (Iso.refl _))
+
+section
+
+variable {J C}
+variable (F₁ F₂ : J ⥤ C)
+
+/-- The chosen binary product on `J ⥤ C`. -/
+@[simps]
+def chosenProd : J ⥤ C where
+  obj j := F₁.obj j ⊗ F₂.obj j
+  map φ := F₁.map φ ⊗ F₂.map φ
+
+namespace chosenProd
+
+/-- The first projection `chosenProd F₁ F₂ ⟶ F₁`. -/
+@[simps]
+def fst : chosenProd F₁ F₂ ⟶ F₁ where
+  app _ := ChosenFiniteProducts.fst _ _
+
+/-- The second projection `chosenProd F₁ F₂ ⟶ F₂`. -/
+@[simps]
+def snd : chosenProd F₁ F₂ ⟶ F₂ where
+  app j := ChosenFiniteProducts.snd _ _
+
+/-- `Functor.chosenProd F₁ F₂` is a binary product of `F₁` and `F₂`. -/
+noncomputable def isLimit : IsLimit (BinaryFan.mk (fst F₁ F₂) (snd F₁ F₂)) :=
+  evaluationJointlyReflectsLimits _ (fun j =>
+    (IsLimit.postcomposeHomEquiv (mapPairIso (by exact Iso.refl _) (by exact Iso.refl _)) _).1
+      (IsLimit.ofIsoLimit (ChosenFiniteProducts.product (X := F₁.obj j) (Y := F₂.obj j)).2
+        (Cones.ext (Iso.refl _) (by rintro ⟨_|_⟩; all_goals aesop_cat))))
+
+end chosenProd
+
+end
+
+noncomputable instance chosenFiniteProducts :
+    ChosenFiniteProducts (J ⥤ C) where
+  terminal := ⟨_, chosenTerminalIsTerminal J C⟩
+  product F₁ F₂ := ⟨_, chosenProd.isLimit F₁ F₂⟩
+
+namespace Monoidal
+
+open ChosenFiniteProducts
+
+variable {J C}
+
+@[simp]
+lemma leftUnitor_hom_app (F : J ⥤ C) (j : J) :
+    (λ_ F).hom.app j = (λ_ (F.obj j)).hom := rfl
+
+@[simp]
+lemma leftUnitor_inv_app (F : J ⥤ C) (j : J) :
+    (λ_ F).inv.app j = (λ_ (F.obj j)).inv := by
+  rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_hom_app,
+    Iso.inv_hom_id_app]
+
+@[simp]
+lemma rightUnitor_hom_app (F : J ⥤ C) (j : J) :
+    (ρ_ F).hom.app j = (ρ_ (F.obj j)).hom := rfl
+
+@[simp]
+lemma rightUnitor_inv_app (F : J ⥤ C) (j : J) :
+    (ρ_ F).inv.app j = (ρ_ (F.obj j)).inv := by
+  rw [← cancel_mono ((ρ_ (F.obj j)).hom), Iso.inv_hom_id, ← rightUnitor_hom_app,
+    Iso.inv_hom_id_app]
+
+@[reassoc (attr := simp)]
+lemma tensorHom_app_fst {F₁ F₁' F₂ F₂' : J ⥤ C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) :
+    (f ⊗ g).app j ≫ fst _ _ = fst _ _ ≫ f.app j := by
+  change (f ⊗ g).app j ≫ (fst F₁' F₂').app j = _
+  rw [← NatTrans.comp_app, tensorHom_fst, NatTrans.comp_app]
+  rfl
+
+@[reassoc (attr := simp)]
+lemma tensorHom_app_snd {F₁ F₁' F₂ F₂' : J ⥤ C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) :
+    (f ⊗ g).app j ≫ snd _ _ = snd _ _ ≫ g.app j := by
+  change (f ⊗ g).app j ≫ (snd F₁' F₂').app j = _
+  rw [← NatTrans.comp_app, tensorHom_snd, NatTrans.comp_app]
+  rfl
+
+@[reassoc (attr := simp)]
+lemma whiskerLeft_app_fst (F₁ : J ⥤ C) {F₂ F₂' : J ⥤ C} (g : F₂ ⟶ F₂') (j : J) :
+    (F₁ ◁ g).app j ≫ fst _ _ = fst _ _ :=
+  (tensorHom_app_fst (𝟙 F₁) g j).trans (by simp)
+
+@[reassoc (attr := simp)]
+lemma whiskerLeft_app_snd (F₁ : J ⥤ C) {F₂ F₂' : J ⥤ C} (g : F₂ ⟶ F₂') (j : J) :
+    (F₁ ◁ g).app j ≫ snd _ _ = snd _ _ ≫ g.app j :=
+  (tensorHom_app_snd (𝟙 F₁) g j)
+
+@[reassoc (attr := simp)]
+lemma whiskerRight_app_fst {F₁ F₁' : J ⥤ C} (f : F₁ ⟶ F₁') (F₂ : J ⥤ C) (j : J) :
+    (f ▷ F₂).app j ≫ fst _ _ = fst _ _ ≫ f.app j :=
+  (tensorHom_app_fst f (𝟙 F₂) j)
+
+@[reassoc (attr := simp)]
+lemma whiskerRight_app_snd {F₁ F₁' : J ⥤ C} (f : F₁ ⟶ F₁') (F₂ : J ⥤ C) (j : J) :
+    (f ▷ F₂).app j ≫ snd _ _ = snd _ _ :=
+  (tensorHom_app_snd f (𝟙 F₂) j).trans (by simp)
+
+@[simp]
+lemma associator_hom_app (F₁ F₂ F₃ : J ⥤ C) (j : J) :
+    (α_ F₁ F₂ F₃).hom.app j = (α_ _ _ _).hom := by
+  apply hom_ext
+  · change _ ≫ (fst F₁ (F₂ ⊗ F₃)).app j = _
+    rw [← NatTrans.comp_app, associator_hom_fst]
+    erw [associator_hom_fst]
+    rfl
+  · apply hom_ext
+    · change (_ ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (fst F₂ F₃).app j = _
+      rw [← NatTrans.comp_app, ← NatTrans.comp_app, assoc, associator_hom_snd_fst, assoc]
+      erw [associator_hom_snd_fst]
+      rfl
+    · change (_ ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (snd F₂ F₃).app j = _
+      rw [← NatTrans.comp_app, ← NatTrans.comp_app, assoc, associator_hom_snd_snd, assoc]
+      erw [associator_hom_snd_snd]
+      rfl
+
+@[simp]
+lemma associator_inv_app (F₁ F₂ F₃ : J ⥤ C) (j : J) :
+    (α_ F₁ F₂ F₃).inv.app j = (α_ _ _ _).inv := by
+  rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]
+
+end Monoidal
+
+end Functor
+
+end CategoryTheory

Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean

@@ -186,7 +186,7 @@ def BinaryFan.associatorOfLimitCone (L : ∀ X Y : C, LimitCone (pair X Y)) (X Y
 /-- Construct a left unitor from specified limit cones.
 -/
 @[simps]
-def BinaryFan.leftUnitor {X : C} {s : Cone (Functor.empty.{v} C)} (P : IsLimit s)
+def BinaryFan.leftUnitor {X : C} {s : Cone (Functor.empty.{0} C)} (P : IsLimit s)
     {t : BinaryFan s.pt X} (Q : IsLimit t) : t.pt ≅ X where
   hom := t.snd
   inv := Q.lift <| BinaryFan.mk (P.lift ⟨_, fun x => x.as.elim, fun {x} => x.as.elim⟩) (𝟙 _)
@@ -201,7 +201,7 @@ def BinaryFan.leftUnitor {X : C} {s : Cone (Functor.empty.{v} C)} (P : IsLimit s
 /-- Construct a right unitor from specified limit cones.
 -/
 @[simps]
-def BinaryFan.rightUnitor {X : C} {s : Cone (Functor.empty.{v} C)} (P : IsLimit s)
+def BinaryFan.rightUnitor {X : C} {s : Cone (Functor.empty.{0} C)} (P : IsLimit s)
     {t : BinaryFan X s.pt} (Q : IsLimit t) : t.pt ≅ X where
   hom := t.fst
   inv := Q.lift <| BinaryFan.mk (𝟙 _) <| P.lift ⟨_, fun x => x.as.elim, fun {x} => x.as.elim⟩
@@ -225,7 +225,7 @@ section
 -- attribute [local tidy] tactic.case_bash
 
 variable {C}
-variable (𝒯 : LimitCone (Functor.empty.{v} C))
+variable (𝒯 : LimitCone (Functor.empty.{0} C))
 variable (ℬ : ∀ X Y : C, LimitCone (pair X Y))
 
 namespace MonoidalOfChosenFiniteProducts
@@ -347,7 +347,7 @@ This is an implementation detail for `SymmetricOfChosenFiniteProducts`.
 -- Porting note: no `has_nonempty_instance` linter.
 -- @[nolint has_nonempty_instance]
 @[nolint unusedArguments]
-def MonoidalOfChosenFiniteProductsSynonym (_𝒯 : LimitCone (Functor.empty.{v} C))
+def MonoidalOfChosenFiniteProductsSynonym (_𝒯 : LimitCone (Functor.empty.{0} C))
     (_ℬ : ∀ X Y : C, LimitCone (pair X Y)) :=
   C
 #align category_theory.monoidal_of_chosen_finite_products.monoidal_of_chosen_finite_products_synonym CategoryTheory.MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym

Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean

@@ -22,7 +22,7 @@ variable {C : Type u} [Category.{v} C] {X Y : C}
 
 open CategoryTheory.Limits
 
-variable (𝒯 : LimitCone (Functor.empty.{v} C))
+variable (𝒯 : LimitCone (Functor.empty.{0} C))
 variable (ℬ : ∀ X Y : C, LimitCone (pair X Y))
 
 open MonoidalOfChosenFiniteProducts