From b5cf43efa9f11d617b3364daf7339797aa21176d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 29 Mar 2024 21:36:01 +0000 Subject: [PATCH] feat(AlgebraicTopology): the monoidal category structure on simplicial sets (#11396) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- Mathlib.lean | 2 + .../SimplicialSet/Monoidal.lean | 89 ++++++++++ .../CategoryTheory/ChosenFiniteProducts.lean | 62 ++++++- .../ChosenFiniteProducts/FunctorCategory.lean | 158 ++++++++++++++++++ .../OfChosenFiniteProducts/Basic.lean | 8 +- .../OfChosenFiniteProducts/Symmetric.lean | 2 +- 6 files changed, 315 insertions(+), 6 deletions(-) create mode 100644 Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean create mode 100644 Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean diff --git a/Mathlib.lean b/Mathlib.lean index 794f43a0f53ee..c572599c2b862 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean new file mode 100644 index 0000000000000..0c12ff6bec5e4 --- /dev/null +++ b/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 diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean index 4630b2926ef80..e1082f9524732 100644 --- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean +++ b/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`. -/ diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean new file mode 100644 index 0000000000000..ea00b3c610842 --- /dev/null +++ b/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 diff --git a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean index cb569b169abe2..8e94ac8c23ac7 100644 --- a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean index eab051ab27a10..9d2fa234e06ce 100644 --- a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean +++ b/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