Cartesian/monoidal closed structure on `SSet`

Stream: Infinity-Cosmos

[Dagur Asgeirsson]

I made a PR https://github.com/emilyriehl/infinity-cosmos/pull/8 where I make some modifications to the file defining infinity-cosmoi.

Namely, I think we should use the monoidal structure on SSet given by the ChosenFiniteProducts instance. This gives us good defeqs as I explain in an example in the PR. This means that we should use the ⊗-notation from the monoidal category API, and that we lose access to CartesianClosed and should use MonoidalClosed instead.

[Dagur Asgeirsson]

We need to define the SimplicialCategory structure on SSet, and then we can prove the tensor-sHomadjunction in SSet. These are the first two todo's in this file. @Joël Riou have you (or someone) started working on this?

(sorry for the edits, I was a bit unclear in my previous messages)

[Dagur Asgeirsson]

Once we have this, the definition of cotensor.underlying.iso can be finished using SimplicialCategory.homEquiv'

[Joël Riou]

The main step in proving that the category of simplicial objects in a category C is a simplicial category is obtained in https://github.com/leanprover-community/mathlib4/pull/13841 by @Jack McKoen (this is the enriched category structure). I must already have draft code for the simplicial category structure: I may PR it, unless Jack wants to do it?

[Dagur Asgeirsson]

It would also be good to get #13710 ready for review since it gives the correct MonoidalClosed instance

[Jack McKoen]

Dagur Asgeirsson said:

It would also be good to get #13710 ready for review since it gives the correct MonoidalClosed instance

I'll get that done later today :+1:

[Emily Riehl]

Thanks for these suggestions @Dagur Asgeirsson. I went ahead and merged the PR because I thought it might make it easier for others to contribute.

[Emily Riehl]

A question for either @Jack McKoen or @Dagur Asgeirsson: how do I access the enriched category structure on SSet? (In general, when something is inferred by Lean as an instance, I don't know how to find it in mathlib.)

In particular, I was trying so show that the 0-simplices in the hom spaces coincide with maps in the underlying category of SSet

instance : SimplicialCategory SSet where
  toEnrichedCategory := inferInstanceAs (EnrichedCategory (_ ⥤ Type _) (_ ⥤ Type _))
  homEquiv (K L) := by
    refine Equiv.trans ?_ (unitHomEquiv _).symm
    sorry
  homEquiv_id := sorry
  homEquiv_comp := sorry

which yields a goal (K ⟶ L) ≃ EnrichedCategory.Hom K L _[0] but I can't get EnrichedCategory.Hom to unfold (or otherwise reveal its definition).

[Adam Topaz]

You could enter tactic mode, and use dsimp [EnrichedCategory.Hom] to explore around at how things are defined. In this case it's defined as docs#CategoryTheory.Functor.functorHom under the hood.

[Adam Topaz]

HEre is the instance done in a not so ideal way because of the tactic mode:

import Mathlib

open CategoryTheory Simplicial MonoidalCategory

noncomputable
instance : SimplicialCategory SSet where
  toEnrichedCategory := inferInstanceAs (EnrichedCategory (_ ⥤ Type _) (_ ⥤ Type _))
  homEquiv K L := by
    refine Equiv.trans ?_ (Functor.functorHomEquiv K L (𝟙_ SSet)).symm
    refine Equiv.trans ?_ (Functor.homObjEquiv _ _ _).symm
    fconstructor
    · intro f
      exact (ρ_ _).hom ≫ f
    · intro f
      exact (ρ_ _).inv ≫ f
    · aesop_cat
    · aesop_cat

[Adam Topaz]

Here it is cleaned up a bit:

import Mathlib

open CategoryTheory Simplicial MonoidalCategory

noncomputable
instance : SimplicialCategory SSet where
  toEnrichedCategory := inferInstanceAs (EnrichedCategory (_ ⥤ Type _) (_ ⥤ Type _))
  homEquiv K L :=
    letI e : (K ⟶ L) ≃ (K ⊗ 𝟙_ SSet ⟶ L) :=
      ⟨fun f => (ρ_ _).hom ≫ f, fun f => (ρ_ _).inv ≫ f, by aesop_cat, by aesop_cat⟩
    e.trans (Functor.homObjEquiv _ _ _).symm |>.trans (Functor.functorHomEquiv K L (𝟙_ SSet)).symm

[Adam Topaz]

My guess is that there isn't much of an API for EnrichedCategory.Hom in the special case of simplicial sets, so by starting off with docs#SSet.unitHomEquiv may leave you in a state that's a bit more difficult.

[Emily Riehl]

Thanks @Adam Topaz. I see the point that we should argue from the definitions that Mathlib knows about.

[Joël Riou]

From the draft code I already had, I have just PRed (to mathlib) the more general simplicial category structure on simplicial objects in any category #16861.

[Adam Topaz]

IMO a slightly more optimal way to break up this more general instance is as follows:

import Mathlib.CategoryTheory.Functor.FunctorHom
import Mathlib.AlgebraicTopology.SimplicialCategory.Basic

namespace CategoryTheory

universe w v' v u u'

open CategoryTheory MonoidalCategory

variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]

def foo (K L : C ⥤ D) :
    (𝟙_ _ ⟶  EnrichedCategory.Hom (V := C ⥤ Type (max v' v u)) K L) ≃ (K ⟶ L) :=
  Functor.functorHomEquiv _ _ _ |>.trans {
    toFun := fun f => {
      app := fun X => f.app _ PUnit.unit
      naturality := by intros ; simp [← f.naturality] }
    invFun := fun f => { app := fun X _ => f.app _ }
    left_inv := by aesop_cat
    right_inv := by aesop_cat
  }

noncomputable instance : SimplicialCategory (SimplicialObject D) where
  toEnrichedCategory := inferInstanceAs <| EnrichedCategory (_ ⥤ Type _) (_ ⥤ _)
  homEquiv K L := foo K L |>.symm

noncomputable instance : SimplicialCategory SSet.{v} :=
  inferInstanceAs (SimplicialCategory (SimplicialObject (Type v)))

@Jack McKoen is the equiv foo available in mathlib? If not, then I think it's worthwhile adding in some form.

[Jack McKoen]

This should be https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Functor/FunctorHom.html#CategoryTheory.Functor.natTransEquiv

[Joël Riou]

Yes, indeed, I had just made the change in my PR in order to use natTransEquiv instead!

[Adam Topaz]

Perfect. So @Joël Riou ‘s PR can be simplified down to just a few lines!

[Emily Riehl]

Just bumped mathlib into the infinity-cosmos repository so we could use the merged version of @Jack McKoen's PR to get the monoidal closed structure on SSet. This is all in the basic file under SimplicialCategories for anyone who wants to have a look.

[Emily Riehl]

I'm now looking for a general lemma about closed monoidal categories to prove for MonoidalClosed C that

fromUnit.equiv (X : C) : iHom (𝟙_ C) X ≃ X

Does anyone know whether this exists?

[Dagur Asgeirsson]

I didn't find this either, feel free to use/PR the following if useful:

import Mathlib

open CategoryTheory MonoidalCategory MonoidalClosed

variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C]

def fromUnit.hom (X : C) : (X ⟶ (ihom (𝟙_ C)).obj X) :=
  ((ihom.adjunction (𝟙_ C)).unit.app _) ≫ (ihom (𝟙_ C)).map (λ_ X).hom

instance : (tensorLeft (𝟙_ C)).Full where
  map_surjective a := ⟨(λ_ _).inv ≫ a ≫ (λ_ _).hom, by simp⟩

instance : (tensorLeft (𝟙_ C)).Faithful where
  map_injective h := by simpa using h

instance (X : C) : IsIso (fromUnit.hom X) := by
  have := (ihom.adjunction (𝟙_ C)).unit_isIso_of_L_fully_faithful
  dsimp only [fromUnit.hom]
  infer_instance

noncomputable def fromUnit.equiv (X : C) : (ihom (𝟙_ C)).obj X ≅ X := (asIso (fromUnit.hom X)).symm

[Adam Topaz]

I think in this case making things explicit for the inverse might be better, but it seems that we're missing some simp lemmas to help out aesop_cat with one (or both) of the following approaches:

import Mathlib

open CategoryTheory MonoidalCategory

variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C]

example (X : C) : ((𝟙_ C) ⟶[C] X) ≅ X where
  hom := (λ_ _).inv ≫ (ihom.ev (𝟙_ C) |>.app X)
  inv := (ihom.coev (𝟙_ C) |>.app X) ≫ (ihom (𝟙_ C)).map (λ_ _).hom
  --hom_inv_id := _ -- fine.
  inv_hom_id := sorry

example (X : C) : ((𝟙_ C) ⟶[C] X) ≅ X where
  hom := (λ_ _).inv ≫ (ihom.ev (𝟙_ C) |>.app X)
  inv := MonoidalClosed.curry <| (λ_ _).hom
  hom_inv_id := sorry
  inv_hom_id := sorry

[Emily Riehl]

My thought was just to use conjugateIsoEquiv to define this to be the mate of leftUnitorNatIso.

Update: see #17065.

[Emily Riehl]

Though in the special case we care about (the chosen finite product structure on SSet) I'm not sure we know that the 0-simplex is the monoidal unit!

[Adam Topaz]

Emily Riehl said:

Though in the special case we care about (the chosen finite product structure on SSet) I'm not sure we know that the 0-simplex is the monoidal unit!

This should be okay assuming the monoidal structure comes from docs#CategoryTheory.ChosenFiniteProducts

[Adam Topaz]

But @Jack McKoen should be able to confirm

[Jack McKoen]

I think the terminal object comes from docs#CategoryTheory.Functor.chosenTerminal, so we don't know that the 0-simplex is the unit

[Jack McKoen]

I recently had to show the 0-simplex is terminal, so I don't even think we have that in mathlib

[Emily Riehl]

@Jack McKoen great. I figured that was the issue.

[Emily Riehl]

I'm about to merge some stuff from the coherent-iso branch with a sorry that needs this.

[Jack McKoen]

here's some ungolfed code that might accomplish what you need:

Edit: I have now golfed it a bit

import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

open CategoryTheory Simplicial Limits

namespace SSet

def isTerminalZero : IsTerminal ([0] : SimplexCategory) :=
  letI : ∀ (k : SimplexCategory), Unique (k ⟶ [0]) := fun k => {
    default := SimplexCategory.Hom.mk <| OrderHom.const _ 0
    uniq := fun m => SimplexCategory.Hom.ext _ _ <| OrderHom.ext _ _ <|
      funext fun _ => Fin.ext <| by simp }
  IsTerminal.ofUnique _

def ptIsTerminal : IsTerminal Δ[0] := by
  letI : ∀ (X : SSet), Unique (X ⟶ Δ[0]) := fun X ↦ {
    default := { app := fun n _ ↦ ULift.up <| Limits.IsTerminal.from isTerminalZero n.unop }
    uniq := fun f ↦ by
      ext n
      exact ULift.up_inj.2 <| Limits.IsTerminal.hom_ext isTerminalZero _ _}
  refine IsTerminal.ofUnique Δ[0]

open MonoidalCategory in
noncomputable
def unitIso : Δ[0] ≅ (𝟙_ SSet) :=
  Limits.IsTerminal.uniqueUpToIso ptIsTerminal (Functor.chosenTerminalIsTerminal _ _)