equivalences of quasi-categories

Stream: Infinity-Cosmos

[Rida Hamadani]

Is anybody working on defining equivalences of quasi-categories and proving Lemma 1.2.36? I plan to formalize this with help from Dalton Sakthivadivel and we want to check that nobody is working on it to avoid effort duplication.

[Emily Riehl]

Hi @Rida Hamadani; sorry to be slow.

We have an experimental definition of equivalence (of sorts) that can be found here. The idea of it would be to specialize to a particular interval (the coherent iso) and to the case where A and B are quasi-categories.

Whether it is a good idea to factor that specific notion of equivalence through this general framework is unclear to me, so feel free to ignore and start from scratch.

No one is working on lemma 1.2.36 I believe so that's all yours! Good luck and let us know if there's anything you want to discuss.

[Rida Hamadani]

I've started formalizing the first part (the equivalence) of the lemma and there are a few issues:

First, SSet.Homotopy is missing a basic API, in particular I'll need a Homotopy.symm lemma.

Second, I will need something of the form:

def Homotopy.hoFunctorIso {A B : SSet.{u}} {f g : A ⟶ B} (h : Homotopy (I := I) f g) :
    hoFunctor.map f ≅ hoFunctor.map g := by
  sorry

I think this could follow from Lemma 1.2.24, but please let me know if you have other ideas.

There is also an issue regarding functor_unitIso_comp but I haven't thought about it yet.

Should I start working on Lemma 1.2.24 or is someone else working on it?

Note: The lemma name in the blueprint was changed to 1.3.16. The initial code can be found here: https://github.com/emilyriehl/infinity-cosmos/pull/134/files.

[Rida Hamadani]

Regarding the first issue, do you have suggestions to make working with Homotopy easier? For example, you can see in the draft PR that I've tried proving that it is reflexive, but honestly I have no idea how to do that using the homotopy I've constructed (maybe I should be using a different homotopy?).

[Joël Riou]

Note that the homotopy relation on arbitrary simplicial sets is reflexive, but not symmetric nor transitive in general. I have formalized the fact it is an equivalence relation when the target simplicial set is a Kan complex. For the coherentIso interval, the symmetry should hold though.
About Homotopy.hoFunctorIso, you cannot prove it using Quotient.lift_unique': the functors hoFunctor.map f and hoFunctor.map g are not equal. You should probably use NatIso.ofComponents: for each 0-simplex, the homotopy gives a "double-sided path" between the images by both f and g (which should give an iso in the homotopy category), and then you need to check it is natural. I have shown a similar result at https://github.com/joelriou/topcat-model-category/blob/e5705bfcc6944a0f8119f7b1cf717b686f39fbfd/TopCatModelCategory/SSet/KanComplexWHomotopy.lean#L143

[Rida Hamadani]

Thanks Joël! I proved that the simplicial homotopy relation is symmetric when using the coherentIso interval, it is line 275 of:
https://github.com/emilyriehl/infinity-cosmos/pull/134/files
However, for some reason, now the file makes my computer crash every time I open it. I don't understand why that is happening. :sob:

[Rida Hamadani]

It just keeps compiling at this lemma:
image.png
Note that rfl was suggested by exact?, so it is supposed to close the goal correctly right?

[Aaron Liu]

do you have a mwe

[Aaron Liu]

ideas:

• try extracting the goal at rfl as a separate theorem
• try extracting source_eq and target_eq as a separate theorem
• try putting change _ before simp_rw
• try putting change _ after simp_rw
• try extracting homotopy as a separate definition
• try making homotopy an irreducible_def

[Rida Hamadani]

Aaron Liu said:

do you have a mwe

I've tried making one, but there are far many prerequisites, sorry.

[Rida Hamadani]

Here is my attempt for an mwe, sorry since its lengthy, but it demonstrates the issue on Lean4 web:

import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
import Mathlib.CategoryTheory.Closed.FunctorToTypes
import Mathlib.Combinatorics.Quiver.ReflQuiver

universe u v w

open CategoryTheory Simplicial SimplicialCategory Limits MonoidalCategory

namespace CategoryTheory

inductive WalkingIso : Type u where
  | zero : WalkingIso
  | one : WalkingIso

namespace WalkingIso

instance : Category (WalkingIso) where
  Hom _ _ := Unit
  id _ := ⟨⟩
  comp _ _ := ⟨⟩

def coev (i : WalkingIso) : Fin 1 ⥤ WalkingIso := ComposableArrows.mk₀ i

end WalkingIso

end CategoryTheory

namespace SimplexCategory

def isTerminalZero : IsTerminal (⦋0⦌ : SimplexCategory) :=
  IsTerminal.ofUniqueHom (fun _ ↦ const _ ⦋0⦌ 0) (fun _ _ => eq_const_to_zero _)

def δ_zero_mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) : SimplexCategory.δ 0 ≫ mkOfLe i j h =
  (SimplexCategory.mk 0).const (SimplexCategory.mk n) j := by
  ext x
  fin_cases x
  aesop

def δ_one_mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) : SimplexCategory.δ 1 ≫ mkOfLe i j h =
  (SimplexCategory.mk 0).const (SimplexCategory.mk n) i := by
  ext x
  fin_cases x
  aesop

end SimplexCategory

namespace SSet

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
  homEquiv_id := by aesop_cat
  homEquiv_comp := by aesop_cat

noncomputable instance : MonoidalClosed SSet where
  closed A := {
    rightAdj := (sHomFunctor _).obj ⟨A⟩
    adj := FunctorToTypes.adj _
  }

def coherentIso : SSet.{u} := nerve WalkingIso

def coherentIso.pt (i : WalkingIso) : Δ[0] ⟶ coherentIso :=
  yonedaEquiv.symm (WalkingIso.coev i)

class Interval (I : SSet.{u}) : Type u where
  src : Δ[0] ⟶ I
  tgt : Δ[0] ⟶ I

instance isoInterval : Interval coherentIso where
  src := coherentIso.pt WalkingIso.zero
  tgt := coherentIso.pt WalkingIso.one

/-- The object `Δ[0]` is terminal in `SSet`.-/
def isTerminalDeltaZero : 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


noncomputable def pointIsUnit : Δ[0] ≅ (𝟙_ SSet) :=
  IsTerminal.uniqueUpToIso isTerminalDeltaZero (IsTerminal.ofUnique (𝟙_ SSet))

noncomputable def expUnitNatIso : CategoryTheory.ihom (𝟙_ SSet) ≅ 𝟭 SSet :=
  MonoidalClosed.unitNatIso.symm

noncomputable def expPointNatIso : ihom Δ[0] ≅ 𝟭 SSet := by
  refine ?_ ≪≫ expUnitNatIso
  exact {
    hom := MonoidalClosed.pre pointIsUnit.inv
    inv := MonoidalClosed.pre pointIsUnit.hom
    hom_inv_id := by
      rw [← MonoidalClosed.pre_map, pointIsUnit.hom_inv_id]
      exact MonoidalClosed.pre_id _
    inv_hom_id := by
      rw [← MonoidalClosed.pre_map, pointIsUnit.inv_hom_id]
      exact MonoidalClosed.pre_id _
  }

noncomputable def expPointIsoSelf (X : SSet) : sHom Δ[0] X ≅ X := expPointNatIso.app X

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

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

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)

def WalkingIso.swap : WalkingIso ⟶ WalkingIso
| WalkingIso.zero => WalkingIso.one
| WalkingIso.one => WalkingIso.zero

def WalkingIso.swapFunctor : WalkingIso ⥤ WalkingIso where
  obj := WalkingIso.swap
  map := id

def coherentIso.swap : coherentIso ⟶ coherentIso :=
  nerveMap WalkingIso.swapFunctor

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

/- doesn't stop compiling, note that `rfl` is suggested by `exact?`. -/
noncomputable def Homotopy.coherentIso_symm {A B : SSet.{u}} {f g : A ⟶ B}
    (h : Homotopy (I := coherentIso) f g) :
    Homotopy (I := coherentIso) g f where
  homotopy := h.homotopy ≫ (MonoidalClosed.pre coherentIso.swap).app B
  source_eq := by
    simp_rw [← h.target_eq, Category.assoc]
    rfl
  target_eq := by
    simp_rw [← h.source_eq, Category.assoc]
    rfl

end SSet

[Joël Riou]

Adding a few lemmas fixes the issue:

@[reassoc (attr := simp)]
lemma coherentIso.src_swap : Interval.src ≫ coherentIso.swap = Interval.tgt := rfl

@[reassoc (attr := simp)]
lemma coherentIso.tgt_swap : Interval.tgt ≫ coherentIso.swap = Interval.src := rfl

@[reassoc (attr := simp)]
lemma coherentIso.pre_swap_app_comp_src (B : SSet.{u}) :
    (MonoidalClosed.pre coherentIso.swap).app B ≫ pathSpace.src B =
      pathSpace.tgt B := by
  dsimp [pathSpace.src, pathSpace.tgt, pathSpace]
  rw [← NatTrans.comp_app_assoc, ← MonoidalClosed.pre_map, src_swap]

@[reassoc (attr := simp)]
lemma coherentIso.pre_swap_app_comp_tgt (B : SSet.{u}) :
    (MonoidalClosed.pre coherentIso.swap).app B ≫ pathSpace.tgt B =
      pathSpace.src B := by
  dsimp [pathSpace.src, pathSpace.tgt, pathSpace]
  rw [← NatTrans.comp_app_assoc, ← MonoidalClosed.pre_map, tgt_swap]

noncomputable def Homotopy.coherentIso_symm {A B : SSet.{u}} {f g : A ⟶ B}
    (h : Homotopy (I := coherentIso) f g) :
    Homotopy (I := coherentIso) g f where
  homotopy := h.homotopy ≫ (MonoidalClosed.pre coherentIso.swap).app B
  source_eq := by simp [← h.target_eq]
  target_eq := by simp [← h.source_eq]

[Rida Hamadani]

Wow, thank you!

[Rida Hamadani]

Should the previous behavior be reported as an issue somewhere? I feel like lean shouldn't get stuck on a proof that exact? suggests.

[Joël Riou]

I would assume that the issue comes from MonoidalClosed.pre_map which may be rfl in case of SSet? but the cost of the verification that it is indeed rfl is extremely high!? It is unclear to me whether this is a bug.

[Rida Hamadani]

I'm following this plan:
Joël Riou said:

You should probably use NatIso.ofComponents: for each 0-simplex, the homotopy gives a "double-sided path" between the images by both f and g (which should give an iso in the homotopy category), and then you need to check it is natural.

I've searched a bit for a lemma/def that takes a double-sided path and gives out an Iso in the homotopy category, but couldn't find any. Do we have it yet?

Another question: I believe the following to be the desired path, but I'm not sure how to get the "two-sidedness", is pre-composing with a hom I ⟶ I that swaps the endpoints enough?

noncomputable def pathOfHomotopy {X Y : SSet} {f g : X ⟶ Y} (h : Homotopy (I := I) f g)
  (x : X _⦋0⦌) : I ⟶ Y :=
  (homEquiv' I Y).invFun (h.homotopy.app (Opposite.op ⦋0⦌) x)

[Emily Riehl]

Could you push something to your draft PR so I can look at some code? I haven't been paying as close attention to what you've been up to as I should.

In particular, I don't get what question you're asking in relation to the code block displayed here...

[Rida Hamadani]

Pushed a new commit.
I'm asking about whether there is lemma I can use to turn this path into an Iso in the homotopy category, or if that's missing.

[Emily Riehl]

Thanks. I understand now.

I think there are some missing lemmas here. The first I'd try to prove is this result from category theory:

def missing {C D : Type} [Category C] [Category D] (F G : C ⥤ D) (H : C × WalkingIso ⥤ D) : F ≅ G := by
  sorry

Rather than using NatIso.ofComponents I'd curry the functor H then use WalkingIso.toIso to get an isomorphism in the functor category.

To get from your homotopy h : A -> sHom I B to a functor H as above you'll need (in addition to some currying/uncurrying):
(i) : the fact that hoFunctor (nerve walkingIso) is isomorphic to walkingIso (via nerveAdjunction.isIso_counit)
(ii) the fact that hoFunctor preserves binary products.

The latter is in a mathlib PR #25780. You could sorry this

instance hoFunctor.binaryProductIsIso (X Y : SSet):
    IsIso (prodComparison hoFunctor X Y) := sorry

which will be provided once that is merged.

[Rida Hamadani]

Thank you. Would this be assuming that I is CoherentIso?

[Joël Riou]

Both approaches are probably worth investigating. What I suggested is probably easier to implement. Emily's suggestion is more conceptual, but I guess that a lot of "invisible mathematics" will pop up (for example, once we get a functor WalkingIso ⥤ A.HomotopyCategory ⥤ B.HomotopyCategory out of an homotopy H, the image of the two objects of WalkingIso should identify to hoFunctor.map f and hoFunctor.map g, but probably not definitionally, etc).

[Emily Riehl]

Rida Hamadani said:

Thank you. Would this be assuming that I is CoherentIso?

Yes, sorry, I meant I as an abbreviation for CoherentIso.

@Joël Riou is right to point out that I'm not very good (yet) and anticipating or avoiding "invisible mathematics". I'm hopeful that as we collectively gain formalization experience we'll figure out a way to make the conceptual proofs more easily formalizable. But in the meanwhile, if you want to pick the route the experts suggest is more expedient of course you should feel free..

[Rida Hamadani]

I'm trying to follow Joël's advice construct an isomorphism in the homotopy category from the double-sided path, but at the moment I find the homotopy category part of the library confusing so I'll appreciate some help.
At first I thought it would be formalized this way:

noncomputable def homotopyCategory_iso {X Y : SSet} {f g : X ⟶ Y}
    (h : Homotopy (I := coherentIso) f g) :
    ((truncation 2).obj X).HomotopyCategory ≅ ((truncation 2).obj Y).HomotopyCategory

But then I'm not sure what hom and inv are supposed to be, I'd assume hom would be something like (mapHomotopyCategory ((truncation 2).map f)).obj but then how would we construct inv?

[Joël Riou]

My suggestion was to use NatIso.ofComponents in order to construct an isomorphism between the functors induced by f and g on the homotopy categories. For any 0-simplex x of X, we want to construct an isomorphism between f(x) and g(x) in the homotopy category of Y. The homotopy h induces a map from coherentIso to Y with sends zero to f(x) and one to g(x). Then, the hom field will be given by the 1-simplex obtained by evaluating at the unique map from zero to one in WalkingIso and similarly for inv. Checking the hom_inv_id/inv_hom_id relations are a little bit more tricky as it will require considering certain 2-simplices in coherentIso which correspond to suitable commutative triangles.
For the naturality with respect to a path x ⟶ y, you may restrict to the case of a "direct" path given by a 1-simplex of X. Then, you may have to prove a lemma in the homotopy category saying that if you have a map Δ[1] ⊗ Δ[1] ⟶ Y, then there is an induced commutative square in the homotopy category of Y. (This would be similar to https://github.com/joelriou/topcat-model-category/blob/e5705bfcc6944a0f8119f7b1cf717b686f39fbfd/TopCatModelCategory/SSet/KanComplexWHomotopy.lean#L48C48-L48C63 )