From ef78db7e00e989f71af21dd11bcfd6b7caf560da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 30 Oct 2024 00:13:47 +0000 Subject: [PATCH] refactor(CategoryTheory): simplicial categories are generalized to enriched "ordinary" categories (#18175) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The API for simplicial categories is refactored. It fits more generally in the context of ordinary categories `C` (a type `C` and an instance `[Category C]`) that are also enriched over a monoidal category `V` (`EnrichedCategory V C`) in such a way that types of morphisms in `C` identify to types of morphisms `𝟙_ V ⟶ (X ⟶[V] Y)` in `V`. This defines a new class `EnrichedOrdinaryCategory`, and `SimplicialCategory` is made an abbreviation for the particular case `V` is the category of simplicial sets. --- Mathlib.lean | 1 + .../SimplicialCategory/Basic.lean | 63 +------- .../SimplicialCategory/SimplicialObject.lean | 2 +- Mathlib/CategoryTheory/Enriched/Basic.lean | 10 +- Mathlib/CategoryTheory/Enriched/Ordinary.lean | 138 ++++++++++++++++++ 5 files changed, 150 insertions(+), 64 deletions(-) create mode 100644 Mathlib/CategoryTheory/Enriched/Ordinary.lean diff --git a/Mathlib.lean b/Mathlib.lean index d4ccdcc497893..4980495fc5cfb 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1587,6 +1587,7 @@ import Mathlib.CategoryTheory.Elementwise import Mathlib.CategoryTheory.Endofunctor.Algebra import Mathlib.CategoryTheory.Endomorphism import Mathlib.CategoryTheory.Enriched.Basic +import Mathlib.CategoryTheory.Enriched.Ordinary import Mathlib.CategoryTheory.EpiMono import Mathlib.CategoryTheory.EqToHom import Mathlib.CategoryTheory.Equivalence diff --git a/Mathlib/AlgebraicTopology/SimplicialCategory/Basic.lean b/Mathlib/AlgebraicTopology/SimplicialCategory/Basic.lean index 7611deaafc8d6..88f5cb27d8813 100644 --- a/Mathlib/AlgebraicTopology/SimplicialCategory/Basic.lean +++ b/Mathlib/AlgebraicTopology/SimplicialCategory/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal -import Mathlib.CategoryTheory.Enriched.Basic +import Mathlib.CategoryTheory.Enriched.Ordinary /-! # Simplicial categories @@ -42,13 +42,7 @@ variable (C : Type u) [Category.{v} C] /-- A simplicial category is a category `C` that is enriched over the category of simplicial sets in such a way that morphisms in `C` identify to the `0`-simplices of the enriched hom. -/ -class SimplicialCategory extends EnrichedCategory SSet.{v} C where - /-- morphisms identify to `0`-simplices of the enriched hom -/ - homEquiv (K L : C) : (K ⟶ L) ≃ (𝟙_ SSet.{v} ⟶ EnrichedCategory.Hom K L) - homEquiv_id (K : C) : homEquiv K K (𝟙 K) = eId SSet K := by aesop_cat - homEquiv_comp {K L M : C} (f : K ⟶ L) (g : L ⟶ M) : - homEquiv K M (f ≫ g) = (λ_ _).inv ≫ (homEquiv K L f ⊗ homEquiv L M g) ≫ - eComp SSet K L M := by aesop_cat +abbrev SimplicialCategory := EnrichedOrdinaryCategory SSet.{v} C namespace SimplicialCategory @@ -57,7 +51,7 @@ variable [SimplicialCategory C] variable {C} /-- Abbreviation for the enriched hom of a simplicial category. -/ -abbrev sHom (K L : C) : SSet.{v} := EnrichedCategory.Hom K L +abbrev sHom (K L : C) : SSet.{v} := K ⟶[SSet] L /-- Abbreviation for the enriched composition in a simplicial category. -/ abbrev sHomComp (K L M : C) : sHom K L ⊗ sHom L M ⟶ sHom K M := eComp SSet K L M @@ -65,58 +59,11 @@ abbrev sHomComp (K L M : C) : sHom K L ⊗ sHom L M ⟶ sHom K M := eComp SSet K /-- The bijection `(K ⟶ L) ≃ sHom K L _[0]` for all objects `K` and `L` in a simplicial category. -/ def homEquiv' (K L : C) : (K ⟶ L) ≃ sHom K L _[0] := - (homEquiv K L).trans (sHom K L).unitHomEquiv - -/-- The morphism `sHom K' L ⟶ sHom K L` induced by a morphism `K ⟶ K'`. -/ -noncomputable def sHomWhiskerRight {K K' : C} (f : K ⟶ K') (L : C) : - sHom K' L ⟶ sHom K L := - (λ_ _).inv ≫ homEquiv K K' f ▷ _ ≫ sHomComp K K' L - -@[simp] -lemma sHomWhiskerRight_id (K L : C) : sHomWhiskerRight (𝟙 K) L = 𝟙 _ := by - simp [sHomWhiskerRight, homEquiv_id] - -@[simp, reassoc] -lemma sHomWhiskerRight_comp {K K' K'' : C} (f : K ⟶ K') (f' : K' ⟶ K'') (L : C) : - sHomWhiskerRight (f ≫ f') L = sHomWhiskerRight f' L ≫ sHomWhiskerRight f L := by - dsimp [sHomWhiskerRight] - simp only [assoc, homEquiv_comp, comp_whiskerRight, leftUnitor_inv_whiskerRight, ← e_assoc'] - rfl - -/-- The morphism `sHom K L ⟶ sHom K L'` induced by a morphism `L ⟶ L'`. -/ -noncomputable def sHomWhiskerLeft (K : C) {L L' : C} (g : L ⟶ L') : - sHom K L ⟶ sHom K L' := - (ρ_ _).inv ≫ _ ◁ homEquiv L L' g ≫ sHomComp K L L' - -@[simp] -lemma sHomWhiskerLeft_id (K L : C) : sHomWhiskerLeft K (𝟙 L) = 𝟙 _ := by - simp [sHomWhiskerLeft, homEquiv_id] - -@[simp, reassoc] -lemma sHomWhiskerLeft_comp (K : C) {L L' L'' : C} (g : L ⟶ L') (g' : L' ⟶ L'') : - sHomWhiskerLeft K (g ≫ g') = sHomWhiskerLeft K g ≫ sHomWhiskerLeft K g' := by - dsimp [sHomWhiskerLeft] - simp only [homEquiv_comp, MonoidalCategory.whiskerLeft_comp, assoc, ← e_assoc] - rfl - -@[reassoc] -lemma sHom_whisker_exchange {K K' L L' : C} (f : K ⟶ K') (g : L ⟶ L') : - sHomWhiskerLeft K' g ≫ sHomWhiskerRight f L' = - sHomWhiskerRight f L ≫ sHomWhiskerLeft K g := - ((ρ_ _).inv ≫ _ ◁ homEquiv L L' g ≫ (λ_ _).inv ≫ homEquiv K K' f ▷ _) ≫= - (e_assoc SSet.{v} K K' L L').symm - -attribute [local simp] sHom_whisker_exchange + (eHomEquiv SSet).trans (sHom K L).unitHomEquiv variable (C) in /-- The bifunctor `Cᵒᵖ ⥤ C ⥤ SSet.{v}` which sends `K : Cᵒᵖ` and `L : C` to `sHom K.unop L`. -/ -@[simps] -noncomputable def sHomFunctor : Cᵒᵖ ⥤ C ⥤ SSet.{v} where - obj K := - { obj := fun L => sHom K.unop L - map := fun φ => sHomWhiskerLeft K.unop φ } - map φ := - { app := fun L => sHomWhiskerRight φ.unop L } +noncomputable abbrev sHomFunctor : Cᵒᵖ ⥤ C ⥤ SSet.{v} := eHomFunctor _ _ end SimplicialCategory diff --git a/Mathlib/AlgebraicTopology/SimplicialCategory/SimplicialObject.lean b/Mathlib/AlgebraicTopology/SimplicialCategory/SimplicialObject.lean index 899ce960ebcf0..2dde40d7ea1e5 100644 --- a/Mathlib/AlgebraicTopology/SimplicialCategory/SimplicialObject.lean +++ b/Mathlib/AlgebraicTopology/SimplicialCategory/SimplicialObject.lean @@ -31,7 +31,7 @@ noncomputable instance : EnrichedCategory SSet.{v} (SimplicialObject D) := inferInstanceAs (EnrichedCategory (_ ⥤ Type v) (_ ⥤ D)) noncomputable instance : SimplicialCategory (SimplicialObject D) where - homEquiv _ _ := Functor.natTransEquiv.symm + homEquiv := Functor.natTransEquiv.symm noncomputable instance : SimplicialCategory SSet.{v} := inferInstanceAs (SimplicialCategory (SimplicialObject (Type v))) diff --git a/Mathlib/CategoryTheory/Enriched/Basic.lean b/Mathlib/CategoryTheory/Enriched/Basic.lean index 5d8c33011683e..36747f57c3e68 100644 --- a/Mathlib/CategoryTheory/Enriched/Basic.lean +++ b/Mathlib/CategoryTheory/Enriched/Basic.lean @@ -30,7 +30,7 @@ We verify that when `V = Type v`, all these notion reduce to the usual ones. -/ -universe w v u₁ u₂ u₃ +universe w w' v v' u₁ u₂ u₃ noncomputable section @@ -94,7 +94,7 @@ theorem e_assoc' (W X Y Z : C) : section -variable {V} {W : Type v} [Category.{w} W] [MonoidalCategory W] +variable {V} {W : Type v'} [Category.{w'} W] [MonoidalCategory W] -- Porting note: removed `@[nolint hasNonemptyInstance]` /-- A type synonym for `C`, which should come equipped with a `V`-enriched category structure. @@ -163,7 +163,7 @@ def enrichedCategoryTypeEquivCategory (C : Type u₁) : section -variable {W : Type (v + 1)} [Category.{v} W] [MonoidalCategory W] [EnrichedCategory W C] +variable {W : Type v} [Category.{w} W] [MonoidalCategory W] [EnrichedCategory W C] -- Porting note(#5171): removed `@[nolint has_nonempty_instance]` /-- A type synonym for `C`, which should come equipped with a `V`-enriched category structure. @@ -184,7 +184,7 @@ For `V = Algebra R`, the usual forgetful functor is coyoneda of `R[X]`, not of ` (Perhaps we should have a typeclass for this situation: `ConcreteMonoidal`?) -/ @[nolint unusedArguments] -def ForgetEnrichment (W : Type (v + 1)) [Category.{v} W] [MonoidalCategory W] (C : Type u₁) +def ForgetEnrichment (W : Type v) [Category.{w} W] [MonoidalCategory W] (C : Type u₁) [EnrichedCategory W C] := C @@ -208,7 +208,7 @@ theorem ForgetEnrichment.of_to (X : ForgetEnrichment W C) : rfl instance categoryForgetEnrichment : Category (ForgetEnrichment W C) := by - let I : EnrichedCategory (Type v) (TransportEnrichment (coyonedaTensorUnit W) C) := + let I : EnrichedCategory (Type w) (TransportEnrichment (coyonedaTensorUnit W) C) := inferInstance exact enrichedCategoryTypeEquivCategory C I diff --git a/Mathlib/CategoryTheory/Enriched/Ordinary.lean b/Mathlib/CategoryTheory/Enriched/Ordinary.lean new file mode 100644 index 0000000000000..e7081037f3137 --- /dev/null +++ b/Mathlib/CategoryTheory/Enriched/Ordinary.lean @@ -0,0 +1,138 @@ +/- +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.Enriched.Basic +import Mathlib.CategoryTheory.Monoidal.Types.Coyoneda + +/-! +# Enriched ordinary categories + +If `V` is a monoidal category, a `V`-enriched category `C` does not need +to be a category. However, when we have both `Category C` and `EnrichedCategory V C`, +we may require that the type of morphisms `X ⟶ Y` in `C` identify to +`𝟙_ V ⟶ EnrichedCategory.Hom X Y`. This data shall be packaged in the +typeclass `EnrichedOrdinaryCategory V C`. + +In particular, if `C` is a `V`-enriched category, it is shown that +the "underlying" category `ForgetEnrichment V C` is equipped with a +`EnrichedOrdinaryCategory V C` instance. + +Simplicial categories are implemented in `AlgebraicTopology.SimplicialCategory.Basic` +using an abbreviation for `EnrichedOrdinaryCategory SSet C`. + +-/ + +universe v' v u u' + +open CategoryTheory Category MonoidalCategory + +namespace CategoryTheory + +variable (V : Type u') [Category.{v'} V] [MonoidalCategory V] + (C : Type u) [Category.{v} C] + +/-- An enriched ordinary category is a category `C` that is also enriched +over a category `V` in such a way that morphisms `X ⟶ Y` in `C` identify +to morphisms `𝟙_ V ⟶ (X ⟶[V] Y)` in `V`. -/ +class EnrichedOrdinaryCategory extends EnrichedCategory V C where + /-- morphisms `X ⟶ Y` in the category identify morphisms + `𝟙_ V ⟶ (X ⟶[V] Y)` in `V` -/ + homEquiv {X Y : C} : (X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y)) + homEquiv_id (X : C) : homEquiv (𝟙 X) = eId V X := by aesop_cat + homEquiv_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : + homEquiv (f ≫ g) = (λ_ _).inv ≫ (homEquiv f ⊗ homEquiv g) ≫ + eComp V X Y Z := by aesop_cat + +variable [EnrichedOrdinaryCategory V C] {C} + +/-- The bijection `(X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y))` given by a +`EnrichedOrdinaryCategory` instance. -/ +def eHomEquiv {X Y : C} : (X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y)) := + EnrichedOrdinaryCategory.homEquiv + +@[simp] +lemma eHomEquiv_id (X : C) : eHomEquiv V (𝟙 X) = eId V X := + EnrichedOrdinaryCategory.homEquiv_id _ + +@[reassoc] +lemma eHomEquiv_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : + eHomEquiv V (f ≫ g) = (λ_ _).inv ≫ (eHomEquiv V f ⊗ eHomEquiv V g) ≫ eComp V X Y Z := + EnrichedOrdinaryCategory.homEquiv_comp _ _ + +/-- The morphism `(X' ⟶[V] Y) ⟶ (X ⟶[V] Y)` induced by a morphism `X ⟶ X'`. -/ +noncomputable def eHomWhiskerRight {X X' : C} (f : X ⟶ X') (Y : C) : + (X' ⟶[V] Y) ⟶ (X ⟶[V] Y) := + (λ_ _).inv ≫ eHomEquiv V f ▷ _ ≫ eComp V X X' Y + +@[simp] +lemma eHomWhiskerRight_id (X Y : C) : eHomWhiskerRight V (𝟙 X) Y = 𝟙 _ := by + simp [eHomWhiskerRight] + +@[simp, reassoc] +lemma eHomWhiskerRight_comp {X X' X'' : C} (f : X ⟶ X') (f' : X' ⟶ X'') (Y : C) : + eHomWhiskerRight V (f ≫ f') Y = eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y := by + dsimp [eHomWhiskerRight] + rw [assoc, assoc, eHomEquiv_comp, comp_whiskerRight_assoc, comp_whiskerRight_assoc, ← e_assoc', + tensorHom_def', comp_whiskerRight_assoc, id_whiskerLeft, comp_whiskerRight_assoc, + ← comp_whiskerRight_assoc, Iso.inv_hom_id, id_whiskerRight_assoc, + comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc, + ← associator_inv_naturality_left_assoc, Iso.inv_hom_id_assoc, + ← whisker_exchange_assoc, id_whiskerLeft_assoc, Iso.inv_hom_id_assoc] + +/-- The morphism `(X ⟶[V] Y) ⟶ (X ⟶[V] Y')` induced by a morphism `Y ⟶ Y'`. -/ +noncomputable def eHomWhiskerLeft (X : C) {Y Y' : C} (g : Y ⟶ Y') : + (X ⟶[V] Y) ⟶ (X ⟶[V] Y') := + (ρ_ _).inv ≫ _ ◁ eHomEquiv V g ≫ eComp V X Y Y' + +@[simp] +lemma eHomWhiskerLeft_id (X Y : C) : eHomWhiskerLeft V X (𝟙 Y) = 𝟙 _ := by + simp [eHomWhiskerLeft] + +@[simp, reassoc] +lemma eHomWhiskerLeft_comp (X : C) {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : + eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g' := by + dsimp [eHomWhiskerLeft] + rw [assoc, assoc, eHomEquiv_comp, MonoidalCategory.whiskerLeft_comp_assoc, + MonoidalCategory.whiskerLeft_comp_assoc, ← e_assoc, tensorHom_def, + MonoidalCategory.whiskerRight_id_assoc, MonoidalCategory.whiskerLeft_comp_assoc, + MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc, + whiskerLeft_rightUnitor_assoc, whiskerLeft_rightUnitor_inv_assoc, + triangle_assoc_comp_left_inv_assoc, MonoidalCategory.whiskerRight_id_assoc, + Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, + associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc, + whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc] + +@[reassoc] +lemma eHom_whisker_exchange {X X' Y Y' : C} (f : X ⟶ X') (g : Y ⟶ Y') : + eHomWhiskerLeft V X' g ≫ eHomWhiskerRight V f Y' = + eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g := by + dsimp [eHomWhiskerLeft, eHomWhiskerRight] + rw [assoc, assoc, assoc, assoc, leftUnitor_inv_naturality_assoc, + whisker_exchange_assoc, ← e_assoc, leftUnitor_tensor_inv_assoc, + associator_inv_naturality_left_assoc, Iso.hom_inv_id_assoc, + ← comp_whiskerRight_assoc, whisker_exchange_assoc, + MonoidalCategory.whiskerRight_id_assoc, assoc, Iso.inv_hom_id_assoc, + whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc] + +attribute [local simp] eHom_whisker_exchange + +variable (C) in +/-- The bifunctor `Cᵒᵖ ⥤ C ⥤ V` which sends `X : Cᵒᵖ` and `Y : C` to `X ⟶[V] Y`. -/ +@[simps] +noncomputable def eHomFunctor : Cᵒᵖ ⥤ C ⥤ V where + obj X := + { obj := fun Y => X.unop ⟶[V] Y + map := fun φ => eHomWhiskerLeft V X.unop φ } + map φ := + { app := fun Y => eHomWhiskerRight V φ.unop Y } + +instance ForgetEnrichment.EnrichedOrdinaryCategory {D : Type*} [EnrichedCategory V D] : + EnrichedOrdinaryCategory V (ForgetEnrichment V D) where + toEnrichedCategory := inferInstanceAs (EnrichedCategory V D) + homEquiv := Equiv.refl _ + homEquiv_id _ := Category.id_comp _ + homEquiv_comp _ _ := Category.assoc _ _ _ + +end CategoryTheory