homotopies and equivalences for both qCats and Kan

Stream: Infinity-Cosmos

[Emily Riehl]

I've just added a new file Homotopy.lean with the following

namespace SSet

open CategoryTheory Simplicial SimplicialCategory

/-- An interval is a simplicial set equipped with two endpoints.-/
class Interval (I : SSet.{u}) : Type u where
  src : Δ[0] ⟶ I
  tgt : Δ[0] ⟶ I

/-- The interval relevant to the theory of Kan complexes.-/
instance arrowInterval : Interval Δ[1] where
  src := standardSimplex.map (SimplexCategory.δ (n := 0) (1))
  tgt := standardSimplex.map (SimplexCategory.δ (n := 0) (0))

/-- The interval relevant to the theory of quasi-categories. -/
instance isoInterval : Interval coherentIso where
  src :=   (yonedaEquiv coherentIso [0]).symm (WalkingIso.coev WalkingIso.zero)
  tgt :=   (yonedaEquiv coherentIso [0]).symm (WalkingIso.coev WalkingIso.one)

/-- Once we've proven that `Δ[0]` is terminal, this will follow from something just PRed to mathlib.-/
def expPointIsoSelf (X : SSet) : sHom Δ[0] X ≅ X := sorry

section

variable {I : SSet.{u}} [Interval I]

noncomputable def pathSpace {I : SSet.{u}} [Interval I] (X : SSet.{u}) : SSet.{u} := sHom I X

open MonoidalClosed

noncomputable def pathSpace.src (X : SSet.{u}) : pathSpace (I := I) X ⟶ X :=
  ((MonoidalClosed.pre Interval.src).app X ≫ X.expPointIsoSelf.hom)

noncomputable def pathSpace.tgt (X : SSet.{u}) : pathSpace (I := I) X ⟶ X :=
  ((MonoidalClosed.pre Interval.tgt).app X ≫ X.expPointIsoSelf.hom)


/-- TODO: Figure out how to allow `I` to be an a different universe from `A` and `B`?-/
structure Homotopy {A B : SSet.{u}} (f g : A ⟶ B) : Type u
    where
  homotopy : A ⟶ sHom I B
  source_eq : homotopy ≫ pathSpace.src B = f
  target_eq : homotopy ≫ pathSpace.tgt B = g

/-- For the correct interval, this defines a good notion of equivalences for both Kan complexes
and quasi-categories.-/
structure Equiv (A B : SSet.{u}) : Type u where
  toFun : A ⟶ B
  invFun : B ⟶ A
  left_inv : Homotopy (I := I) (toFun ≫ invFun) (𝟙 A)
  right_inv : Homotopy (I := I) (invFun ≫ toFun) (𝟙 B)

end

[Emily Riehl]

(This file imports CoherentIso.lean; alternatively just comment out that example.)

[Emily Riehl]

Some questions:

1. Is it better to define Interval as a class or a structure? Most often we'll use one particular interval structure on a given simplicial set, but perhaps not always.
2. Is it better to have the interval as an implicit or explicit variable? You can see I needed to specify it a few times.
3. Is there a way to define pathSpace to make it computable?

If someone else has done something similar in a better way I'd be happy to hear about it.

[Zeyi Zhao]

Hello everyone! Emily @Emily Riehl and I are working on the theorem proving that Δ[0] is terminal in the category of simplicial sets. We want to use the theorem that the Yoneda embedding preserves limits and a simple proof(already done) that [0] is terminal in the simplex category. However, we have encountered a problem with the uliftFunctor and a problem at the level of universe. How should we solve these problems?

import mathlib
import Mathlib.AlgebraicTopology.SimplicialSet.Basic
import Mathlib.CategoryTheory.Limits.Shapes.Types
import Mathlib.CategoryTheory.Yoneda
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic.FinCases
import mathlib.tactic
import Mathlib.CategoryTheory.Limits.Shapes.Terminal

open CategoryTheory Simplicial SimplicialCategory Limits

def d0_terminal : IsTerminal ([0] : SimplexCategory) := by
  refine IsTerminal.ofUniqueHom (fun _ ↦ SimplexCategory.const _ [0] 0) ?_
  · apply SimplexCategory.eq_const_to_zero

noncomputable def delta0_terminal : IsTerminal (Δ[0] : SSet) := by
  have lem : SSet.standardSimplex = (yoneda : SimplexCategory ⥤ SSet) := by
    unfold SSet.standardSimplex
    sorry
  let thm := yonedaFunctorPreservesLimits (C := SimplexCategory)
  let case := thm.preservesLimitsOfShape (J := Discrete PEmpty)
  let guess := case.preservesLimit (K := Functor.empty SimplexCategory)
  rw [← lem] at guess
  refine IsTerminal.isTerminalObj SSet.standardSimplex [0] ?l
  exact d0_terminal

noncomputable def delta0_terminal' : IsTerminal (Δ[0] : SSet) := by
  have lem1 : PreservesLimit (Functor.empty SimplexCategory ⋙ yoneda) SSet.uliftFunctor := by
    sorry
  have lem2 : PreservesLimit (Functor.empty SimplexCategory) SSet.standardSimplex := by
    unfold SSet.standardSimplex
    refine compPreservesLimit yoneda SSet.uliftFunctor
  refine IsTerminal.isTerminalObj SSet.standardSimplex [0] ?l
  exact d0_terminal

[Jack McKoen]

I'm not sure about the universe issues--but if all you need is a proof that Δ[0] is terminal, I've done it already

[Jack McKoen]

The code in https://leanprover.zulipchat.com/#narrow/channel/455414-Infinity-Cosmos/topic/Cartesian.2Fmonoidal.20closed.20structure.20on.20.60SSet.60/near/472340429 still appears to work

[Jack McKoen]

I seem to recall running into some universe issues but I guess I figured it out

[Kunhong Du]

I think your first sorry holds only if standardSimplex lies in Type 1. So even if you assume the sorry, what you prove is Δ[0].{0} is terminal.

For the second sorry, you only need whiskeringRightPreservesLimits and Types.instPreservesLimitsOfSizeUliftFunctor.

[Adam Topaz]

This is probably not the most useful way to break this down, but it's relatively straightforward to prove this by hand using your proof that [0] is terminal in the simplex category:

import Mathlib

open CategoryTheory Limits

open Simplicial

def SimplexCategory.isTerminalZero : IsTerminal ([0] : SimplexCategory) := by
  refine IsTerminal.ofUniqueHom (fun _ ↦ SimplexCategory.const _ [0] 0) ?_
  · apply SimplexCategory.eq_const_to_zero

def SSet.isTerminal : IsTerminal (Δ[0] : SSet.{u}) where
  lift S := { app := fun X _ => ULift.up <| SimplexCategory.isTerminalZero.from _ }
  uniq := by intros ; ext ; apply ULift.ext ; apply SimplexCategory.isTerminalZero.hom_ext

[Adam Topaz]

This also has the "benefit" of being computable.

[Adam Topaz]

(deleted)

[Emily Riehl]

Thanks all for weighing in. This is very similar to the proof that @Jack McKoen had originally.

I'm very curious about understanding, though, why the "direct" approach seems to work so much better than the one I find more aesthetic. Does all of the limit preservation results really have to be non-computable?

[Jack McKoen]

I think the limit preservation approach isn't as easy to do (regardless of noncomputability) just because the standard simplex is defined as yoneda ⋙ uliftFunctor, and the uliftFunctor bit is annoying to work around.

[Emily Riehl]

@Zeyi Zhao do you want to add the following code to the Infinity Cosmos repository? Or would you like me to do this for you?

Adam Topaz said:

This is probably not the most useful way to break this down, but it's relatively straightforward to prove this by hand using your proof that [0] is terminal in the simplex category:

import Mathlib

open CategoryTheory Limits

open Simplicial

def SimplexCategory.isTerminalZero : IsTerminal ([0] : SimplexCategory) := by
  refine IsTerminal.ofUniqueHom (fun _ ↦ SimplexCategory.const _ [0] 0) ?_
  · apply SimplexCategory.eq_const_to_zero

def SSet.isTerminal : IsTerminal (Δ[0] : SSet.{u}) where
  lift S := { app := fun X _ => ULift.up <| SimplexCategory.isTerminalZero.from _ }
  uniq := by intros ; ext ; apply ULift.ext ; apply SimplexCategory.isTerminalZero.hom_ext

[Zeyi Zhao]

Adam Topaz said:

This is probably not the most useful way to break this down, but it's relatively straightforward to prove this by hand using your proof that [0] is terminal in the simplex category:

import Mathlib

open CategoryTheory Limits

open Simplicial

def SimplexCategory.isTerminalZero : IsTerminal ([0] : SimplexCategory) := by
  refine IsTerminal.ofUniqueHom (fun _ ↦ SimplexCategory.const _ [0] 0) ?_
  · apply SimplexCategory.eq_const_to_zero

def SSet.isTerminal : IsTerminal (Δ[0] : SSet.{u}) where
  lift S := { app := fun X _ => ULift.up <| SimplexCategory.isTerminalZero.from _ }
  uniq := by intros ; ext ; apply ULift.ext ; apply SimplexCategory.isTerminalZero.hom_ext

Thanks for your help!

[Zeyi Zhao]

Emily Riehl said:

Zeyi Zhao do you want to add the following code to the Infinity Cosmos repository? Or would you like me to do this for you?

Adam Topaz said:

This is probably not the most useful way to break this down, but it's relatively straightforward to prove this by hand using your proof that [0] is terminal in the simplex category:

import Mathlib

open CategoryTheory Limits

open Simplicial

def SimplexCategory.isTerminalZero : IsTerminal ([0] : SimplexCategory) := by
  refine IsTerminal.ofUniqueHom (fun _ ↦ SimplexCategory.const _ [0] 0) ?_
  · apply SimplexCategory.eq_const_to_zero

def SSet.isTerminal : IsTerminal (Δ[0] : SSet.{u}) where
  lift S := { app := fun X _ => ULift.up <| SimplexCategory.isTerminalZero.from _ }
  uniq := by intros ; ext ; apply ULift.ext ; apply SimplexCategory.isTerminalZero.hom_ext

Can I do it after the seminar on Monday since I am not sure how to add stuff to the repository?