towards the homotopy category of a quasi-category

Stream: Infinity-Cosmos

[Emily Riehl]

@Kunhong Du are you still working on defining the various homotopy relations on 1-simplices via a 2-simplex? If you've made any preliminary progress, would you mind sharing your code (even if incomplete)?

[Kunhong Du]

@Emily Riehl Sure, please see here. I have only finished the definition and showed the reflexivity holds. Compared from this pr, I define the homotopy on morphisms rather than on objects, I think it is more consistent with other notions of homotopy. Also, I define the homotopy as sturcture rather than class as recommended by this comment.

I guess for further properties we need a complete api for horn filling. The pr mentioned before already did some work on that. Maybe I should first merge them into our repository?

[Emily Riehl]

This looks great. Would you mind creating a PR for us (it's okay to still have sorries; we have several in the repository) to review? There are various things that aren't obvious to me that are worth discussing, e.g.:

• should the 1-simplices be terms of type f g : Δ[1] ⟶ A or of type f g : A _[1]?
• If the latter should the 1-simplices be parametrized over zero simplices x y : A _[0] and come already with proofs that they are parallel from x to y?

[Emily Riehl]

Part of the reason I ask is that @Nick Ward is looking for something new to do and one thought was to suggest he work on re-defining the homotopy category functor in the special case where the simplicial set is a quasi-category.

[Emily Riehl]

While @Kunhong Du is working on something like this

Emily Riehl said:

... since the hoFunctor PR is still being reviewed (#16783), I think it makes sense to start with results that don't require it.

Maybe we call the thing where the degenerate 1-simplex is the 0-th face of a 2-simplex a left homotopy; "left" because it defines a 1-simplex in Hom^L(x,y). The other case, where the degenerate 1-simplex is the 2nd face of a 2-simplex is then a right homotopy.

Your first task would be to show that if the ambient simplicial set is a quasi-category then left and right homotopy are each equivalence relations and moreover coincide.

Perhaps @Nick Ward could work on defining a functor from QCat to Cat that sends a quasi-category X to the category whose type of objects is X _[0] and whose type of morphisms is a further question of the homs defined in #16783:

/-- A simplicial set `S` has an underlying refl quiver with `S _[0]` as its underlying type.-/
def SSet.OneTruncation (S : SSet) := S _[0]

/-- The source vertex of `f : S _[1]` for use in defining the underlying refl quiver.-/
def SSet.OneTruncation.src {S : SSet} (f : S _[1]) : OneTruncation S := S.δ 1 f

/-- The target vertex of `f : S _[1]` for use in defining the underlying refl quiver.-/
def SSet.OneTruncation.tgt {S : SSet} (f : S _[1]) : OneTruncation S := S.δ 0 f

/-- The hom-types of the refl quiver underlying a simplicial set `S` are subtypes of `S _[1]`.-/
def SSet.OneTruncation.Hom {S : SSet} (X Y : OneTruncation S) :=
  {p : S _[1] // src p = X ∧ tgt p = Y}

[Emily Riehl]

The further quotienting is then by the homotopy relation.

Unlike the construction of def SSet.hoFunctor' : SSet.{u} ⥤ Cat.{u,u} which first forms a free category on a ReflQuiver and then quotients by a hom relation, in this case once can show directly that the quotiented homs defined above have a well-defined composition function.

[Emily Riehl]

The proof would require several lemmas about the homotopy relation that @Kunhong Du could state sooner (and then prove later) so that @Nick Ward could work on this in parallel.

[Emily Riehl]

If this sounds vaguely interesting, let me know, and I'll see if I can whip up a blueprint with more details about all of the above. One thing that should be achievable once this is done is the proof that if X is StrictSegal, then an explicit map η from X to the nerve of its homotopy category (via the construction above) is an isomorphism.

[Nick Ward]

@Emily Riehl sounds great!

@Kunhong Du if it's alright I might bother you with some questions as I try to get a feel for the interface here. I'm also happy to work at the same time on some of the background stuff that might be needed (e.g. the more complete api for horn filling that you mentioned).

[Emily Riehl]

In the meanwhile @Nick Ward, if you have any suggestions for #16783 they would be very welcome.

[Kunhong Du]

@Emily Riehl I just opened a PR.

For your question, I think A _[1] might be easier to work with when we want to prove the properties of homotopy relations, but is it the case that in the context of $\infty$-category, we talk about morphisms more frequently? If so, maybe it would be helpful to define two versions of homotopy and state that they are somehow equivalent via Yoneda.

For the second question, I did require the 1-simplicies to be parametrized by 0-simplcies in my first approach.

structure ParallelPair {A : SSet.{u}} (x y : Δ[0] ⟶ A) where
  hom : Δ[1] ⟶ A
  src : Interval.src ≫ hom = x
  tgt : Interval.tgt ≫ hom = y

variable {A : SSet.{u}} {x y : Δ[0] ⟶ A} (f g : ParallelPair x y)

structure HomotopyL where
  homotopy : Δ[2] ⟶ A
  face0 : standardSimplex.map (δ 0) ≫ homotopy = standardSimplex.map (σ 0) ≫ y
  face1 : standardSimplex.map (δ 1) ≫ homotopy = g.hom
  face2 : standardSimplex.map (δ 2) ≫ homotopy = f.hom

Bad thing about this is being redundant, but we do have that f and g are parallel definitionally, rather than propositional equalities for the correpsonding vertices. And I believe not being equal definitionally may cause many problems when working on catgeories in Lean. Under this consideration, maybe an explicit parametrization may be better.

[Kunhong Du]

@Nick Ward Feel free to ask me any questions. I'm glad that I could help. You can tell me what lemmas you may want for your proof and I can state them. And we can discuss about the API for horn fillings, which should be interesting :big_smile:

[Emily Riehl]

@Nick Ward it occurred to me to also suggest that as a warmup you define this simpler version of the homotopy category first for StrictSegal simplicial sets. I don't know that we'll want that version in mathlib but you could PR it to the Infinity-Cosmos repository for folks to play around with.

[Emily Riehl]

For StrictSegal things two 1-simplices will be related by @Kunhong Du's homotopy relation iff they are equal so the homotopy category doesn't have any quotienting. Instead you are showing that the underlying reflQuiver of a strict segal simplicial set already has a category structure with composition defined by taking the diagonal of the 2-simplex formed by a path of length 2.

[Emily Riehl]

By request @Kunhong Du opened up an early PR containing the following definitions

open SimplexCategory

variable {A : SSet.{u}} (f g : Δ[1] ⟶ A)

structure HomotopyL where
  homotopy : Δ[2] ⟶ A
  face0 : standardSimplex.map (δ 0) ≫ homotopy =
    standardSimplex.map (σ 0) ≫ standardSimplex.map (δ 0) ≫ f
  face1 : standardSimplex.map (δ 1) ≫ homotopy = g
  face2 : standardSimplex.map (δ 2) ≫ homotopy = f

structure HomotopyR where
  homotopy : Δ[2] ⟶ A
  face0 : standardSimplex.map (δ 0) ≫ homotopy = f
  face1 : standardSimplex.map (δ 1) ≫ homotopy = g
  face2 : standardSimplex.map (δ 2) ≫ homotopy =
    standardSimplex.map (σ 0) ≫ standardSimplex.map (δ 1) ≫ f

def HomotopicL : Prop :=
    Nonempty (HomotopyL f g)

def HomotopicR : Prop :=
    Nonempty (HomotopyR f g)

Now we'd be grateful for some advice on the best way to handle these structures and relations.

[Emily Riehl]

A few that aren't obvious to me that are worth discussing, e.g.:

• should the 1-simplices be terms of type f g : Δ[1] ⟶ A or of type f g : A _[1]?
• If the latter should the 1-simplices be parametrized over zero simplices x y : A _[0] and come already with proofs that they are parallel from x to y?

[Emily Riehl]

Future theorems will show, for instance, that when A is a quasi-category:

• HomotopicL and HomotopyR are equivalence relations
• in fact they are the same equivalence relation
• moreover, these relations precisely capture the class of 1-simplices that are sent to the same arrow in the homotopy category of A.

[Dean Young]

@Jack McKoen's code had some of these things, right?

[Jack McKoen]

I had some early sketches of things like this, but nothing worth digging up

[Emily Riehl]

@Kunhong Du I think the easiest thing might be to just merge your branch now and just do some experiments on the main branch. Do you have any objections?

[Nick Ward]

Maybe we can open a github issue to organize any discussion? Alternatively, I think keeping all of the discussion here has its benefits as well.

[Emily Riehl]

Seems like a good idea to me. Go for it, if you like!

[Kunhong Du]

Please do the merge. I think the further experiments can tell which of the possible definitions is better.

[Nick Ward]

Nick Ward said:

Maybe we can open a github issue to organize any discussion?

cosmos#60

[Pietro Monticone]

Let me know if you want me to port the dashboard-based workflow into InfinityCosmos (see #FLT > Project Dashboard for more info).

It will just require a few steps for @Emily Riehl, but it would allow us to have have an issue per task, claim tasks directly on GitHub and having technical discussions within the same issue and / or related PR which is supposed to close it.

I'll be able to assist with that tomorrow.

[Nick Ward]

Emily Riehl said:

Nick Ward it occurred to me to also suggest that as a warmup you define this simpler version of the homotopy category first for StrictSegal simplicial sets.

cosmos#61 includes a (partial) definition of the homotopy category for StrictSegal simplicial sets. I don't know that we'll actually want to merge this one. My intention is to open a competing PR that uses @Kunhong Du's definition of the homotopy relations in cosmos#51 for comparison. Hopefully this will provide some insight into which version of the homotopy relations might be easier to work with.

[Nick Ward]

Emily Riehl said:

• should the 1-simplices be terms of type f g : Δ[1] ⟶ A or of type f g : A _[1]?

I will try to better express this opinion on the github issue once I have a bit more evidence to back it up, but so far working on cosmos#61 I have strongly preferred the definition of the homotopy relations using 1-simplices f g : A _[1]. I believe this is primarily because the Path structure and StrictSegal class are defined on arrows of the same type. It has proven fairly tedious translating back and forth between these definitions.

That being said, it's possible that this will start to matter less once the basics of quasicategories are out of the way. Additionally, there is always the option of altering the definition of Path to use 1-simplices f : Δ[1] ⟶ A if there are advantages to this approach. But, my opinion would be that it's best to pick a preferred form for 1-simplices and use it consistently in definitions.

[Kunhong Du]

I opened a PR, where I redefined HomotopyL and HomotopyR according to @Nick Ward 's suggestions.

[Kunhong Du]

I noticed that my commits include [Merge remote-tracking branch 'upstream/main'], which seems a little messy. Do I need to clean it?

[Kevin Buzzard]

In FLT we're squash merging when merging PRs to main

[Nick Ward]

This is great @Kunhong Du! I would be curious to know if anyone else thinks working with 1-simplices f g : Δ[1] ⟶ A might be easier in the long run. It's possible my opinion is influenced by mostly working with StrictSegal things thus far rather than Quasicategory.

It looks to me like the infinity-cosmos repo is also set up for squash merging, so I wouldn't worry about altering your commits.

[Nick Ward]

@Kunhong Du have you made any progress toward an improved api for defining maps from the horn? I have also found myself blocked by this while sketching out the construction of the homotopy category of a quasicategory here.

I'm happy to work on this, but don't want to duplicate efforts too much.

[Kunhong Du]

@Nick Ward Ah I happen to be working with it right now. I actually sort of finished the framework months ago but it's a total mess and probably only understandable to myself. It'd be great if we could work on it together.

[Nick Ward]

Yeah sounds great! I think the best way is probably either opening an infinity-cosmos PR or we could collaborate directly on a mathlib branch. Depending on where your work so far is maybe there's another way that's easier for you, though.

[Nick Ward]

No need to clean things up for my sake, but also no rush if it's a hassle to move your existing work over to infinity-cosmos or mathlib.

[Emily Riehl]

I see I've missed a lot of work from @Kunhong Du and @Nick Ward while I've been offline. Congrats to both of you.

Do you have advice on the correct order to review and integrate your respective PRs?

[Nick Ward]

@Emily Riehl I won't speak for @Kunhong Du, but I think cosmos#63 is fairly independent and probably just a matter of deciding which form of the homotopy relations are best to have on main for the time being.

cosmos#61 is probably not ready to be merged at this point (with inevitable merge conflicts being among the reasons). The two things of interest are StrictSegal.homotopic_iff_eq and the anonymous Category (OneTruncation S) instance. My guess is that StrictSegal.homotopic_iff_eq is worth cleaning up and merging, possibly in a separate PR. I'm not as sure about the StrictSegal homotopy category instance. I have a complete proof scattered across two branches at this point, but I am unsure whether to clean it up now or just view it as a warm-up for the homotopy category of a quasicategory.

[Kunhong Du]

Nick Ward said:

I won't speak for Kunhong Du, but I think cosmos#63 is fairly independent and probably just a matter of deciding which form of the homotopy relations are best to have on main for the time being.

I agree. I think it can be merged to main now.

[Emily Riehl]

Just left a review (finally). The code looks good but I think style conventions suggest we need more evocative names for the fields of the structure. I like "simplex" and then perhaps something like δ₀_eq which is a conventional way to name equalities.

[Emily Riehl]

But modulo a name change to something like the above I agree this is ready to merge.

[Emily Riehl]

@Kunhong Du I suggested a name change on your PR. How do you feel about it?

[Kunhong Du]

@Emily Riehl Changed. Sorry for the delay. I've been a little busy.

[Emily Riehl]

No rush and no need to apologize. It just occurred to me that perhaps you missed the comments from earlier. Anyway, merged!

[Nick Ward]

mathlib4#20448 provides a description of the boundary ∂Δ[n] as a colimit of the standard simplices.

The tentative plan is to use this as the basis for an api that makes it easier to define maps out of the horn / boundary. We will presumably need a very similar proof for the colimit description of Λ[n, i], so any feedback is very appreciated.

[Joël Riou]

Nick Ward said:

The tentative plan is to use this as the basis for an api that makes it easier to define maps out of the horn / boundary. We will presumably need a very similar proof for the colimit description of Λ[n, i], so any feedback is very appreciated.

I had not planned to make this public as early, but I am currently working on constructing the standard model category structures on TopCat and SSet, and as part of this work (which is at an early stage, following my work on the small object argument), I have thought about the following design. In https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Sites/Subsheaf.html we have the notion of a Subpresheaf of a presheaf of types (the presheaf part of this file should be moved to a better place), and I have verified that it is a complete lattice. In this file https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/Boundary.lean I define the faces of the standard simplex (face S for S : Set (Fin (n + 1))) and show the following lemmas:

lemma face_inter_face (S₁ S₂ : Set (Fin (n + 1))) :
    face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂) := by
  aesop

lemma subcomplexBoundary_eq_iSup :
    subcomplexBoundary.{u} n = ⨆ (i : Fin (n + 1)), standardSimplex.face {i}ᶜ  := ...

lemma subcomplexHorn_eq_iSup (i : Fin (n + 1)) :
    subcomplexHorn.{u} n i =
      ⨆ (j : ({i}ᶜ : Set (Fin (n + 1)))), standardSimplex.face {j.1}ᶜ := ...

In general, if a subcomplex is the ⨆ of subcomplexes Z i, then it should be easy to show there is a multicoequalizer diagram involving the Z i and the Z i ⊓ Z j (it suffices to show this in a category of sets instead of the category of presheaves). In the situation above, the subcomplexes Z i and their intersections are (empty or) representable in the simplex category.

[Nick Ward]

@Joël Riou very neat, thanks for sharing!

[Nick Ward]

If I understand correctly, this would subsume the work in mathlib4#20448 and perhaps even provide a better "backend" for a horn filling api. Do you have an opinion on the best place to draw the interface between your work and such an api?

[Joël Riou]

Yes, from the colimit cocone I suggest, yours should be obtained (up to reindexing) by excluding i = j and focusing on i < j (which is obviously possible). I will test a little bit my API while working on the various descriptions of the Gabriel-Zisman anodyne extensions, and then I will PR the basic subcomplexes API. It may take a few weeks before I start PRing this.

[Nick Ward]

@Joël Riou do you see any reason to push mathlib4#20448 forward in the meantime (or anything that should be salvaged into a separate PR)? If not, I will close it.

[Nick Ward]

Also, I'm happy to help port the subcomplexes api when the time comes, although I assume it is still evolving along with the other work you shared.

[Joël Riou]

I think it is better to wait for the subcomplexes API. (I just want to prove a few basic lemmas using it so that it stabilizes before PRing it; it should not be too long.)

[Nick Ward]

I'm inclined to agree. No rush of course!

[Joël Riou]

See #mathlib4 > Name suggestions for lattice/category theory notions? for a call for suggestions for the name of some new definitions related to the above discussion.

[Joël Riou]

I would like to mention that while working on the homotopy theory of simplicial sets, I have done significant steps towards the construction of the fundamental groupoid of a Kan complex. It seems (?) that the homotopy category of a quasi-category https://emilyriehl.github.io/infinity-cosmos/blueprint/sec-simplicial-sets.html#lem:htpy-cat-of-qcat is obtained using the same arguments. For the fundamental groupoid, we use outer horns in order to obtain left and right inverses, but otherwise, it would suffice to check the argumentation only requires inner horns. For example, when showing the associativity of the composition, I use an (inner) horn in Δ[3]. The uniqueness of path composition up to homotopy is more tricky as it uses the inclusion of the union of {0, 1} × Δ[2] and Δ[1] × Λ[2, 1] in Δ[1] × Δ[2], which requires general results on anodyne extensions. I have reduced one of the most technical lemmas about anodyne extensions (as initially defined by Gabriel and Zisman) to an equality of two subcomplexes (hopefully, I did not do mistakes with the indices...), but this will need some more work. (And Jack is working specifically on inner anodyne extensions.) I do not intend to work on quasi-categories (as I am very much focusing on the model category structure on topological spaces and simplicial sets), but there are significant chunks of code that will be useful for the infinity-cosmos project.
This is https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FundamentalGroupoid.lean and https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/AnodyneExtensions.lean
I will do mathlib PRs about some general API about subpresheaves and gluing as it was mentionned above (see for example https://github.com/joelriou/topcat-model-category/blob/e6e1c795171ab4e27551eaf433d004202aa553e9/TopCatModelCategory/SSet/Horn.lean#L310 ).

[Nick Ward]

@Joël Riou let me know if I can be of any help in the mathlib port.

[Emily Riehl]

Thanks for sharing @Joël Riou. This does sound very helpful.

Getting this construction of the homotopy of a quasi-category and proving that the homotopy category functor preserves products are high priorities as far as I'm concerned that I was hoping to renew interest in as soon as some current PRs are merged.

[Nick Ward]

@Emily Riehl I think interest is still high! It's just that @Joël Riou has come up with a much better solution to our problems than I managed to, so we are patiently awaiting these fancy new tools.

[Emily Riehl]

I'm grateful also that you've fixed all the truncated segal stuff so that maybe one day I'll finally be able to merge that PR from september...

[Joël Riou]

Modulo a very mild sorry, I have obtained that the inclusion of the union of {1} ⊗ Δ[n] and Δ[1] ⊗ ∂Δ[n] in Δ[1] ⊗ Δ[n] is an anodyne extension (here it is a finite composition of pushouts of horn inclusions) (and the proof for {0} ⊗ Δ[n] instead of {1} ⊗ Δ[n] should be very similar) https://github.com/joelriou/topcat-model-category/blob/28ae20d3b8b50b2f379a17d112c8745d19a5bcdd/TopCatModelCategory/SSet/AnodyneExtensions.lean#L319-L321
This is one of main technical results towards the description of anodyne extensions (not inner anodyne extensions), and this uses heavily the API that I have started to PR to mathlib, see #20840, #21090, #21096, #21098, #21103, #21174, and which should be soon usable for the infinity cosmos project...

[Jack McKoen]

This is great, I think I'll also be able to use some of this!

[Nick Ward]

@Joël Riou my only complaint is that I can't keep up! I will try to work my way through your recent PRs, but please don't hesitate to flag any that need more (unsophisticated) opinions or review.

[Joël Riou]

I have mostly formalized the fundamental groupoid of a Kan complex, and it turns out the proofs can be done by using very directly the lifting with respect to horn inclusions (instead of more intricate anodyne extensions).

[Joël Riou]

The most useful tool in this work is the following definition CompStruct, where FundamentalGroupoid X is a type synonym for X and Edge x₀ x₁ is a 1-simplex "from x₀ to x₁":

variable {x₀ x₁ x₂ x₃ : FundamentalGroupoid X}

structure CompStruct (p₀₁ : Edge x₀ x₁) (p₁₂ : Edge x₁ x₂) (p₀₂ : Edge x₀ x₂) where
  map : Δ[2] ⟶ X
  h₀₁ : stdSimplex.δ 2 ≫ map = p₀₁.map := by aesop_cat
  h₁₂ : stdSimplex.δ 0 ≫ map = p₁₂.map := by aesop_cat
  h₀₂ : stdSimplex.δ 1 ≫ map = p₀₂.map := by aesop_cat

(https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FundamentalGroupoid.lean)

[Joël Riou]

This structure expresses that the homotopy class of p₀₂ is the composition of p₀₁ and p₁₂. That there is such a structure for some p₀₂ when p₀₁ and p₁₂ are given uses the inner horn inclusion in Δ[2]. The homotopy relation HomotopyL and HomotopyR mentionned above in this thread are special cases of CompStruct. Then, two "associativity" lemmas using the two inner horns in Δ[3] can be used in order to show the equivalence of HomotopyL/R and to prove the compatibilities required in order to get the category structure on homotopy classes of "paths". The outer horns are used only in order to get the groupoid structure. (I have also mostly formalized the higher dimensional analogues of this in order to define the homotopy groups of a Kan complex.)

[Joël Riou]

(In this ongoing formalization work of simplicial homotopy theory, I found that details about the homotopy relation(s) on simplices are left under the carpet in the reference book I am mostly following. Here, the homotopy relation on paths may also be defined as a particular case of the general homotopy relation using homotopies X ⊗ Δ[1] ⟶ Y, i.e. as maps from the square Δ[1] ⊗ Δ[1], which contains two non degenerate 2-simplices. I do not see how to prove certain results without using CompStruct or HomotopyL/R...)

[Joël Riou]

As the construction of the category structure only use inner horns, the definition of the fundamental groupoid of a Kan complex should be done as a particular case of the homotopy category of a quasi-category.

[Nick Ward]

Joël Riou said:

The homotopy relation HomotopyL and HomotopyR mentionned above in this thread are special cases of CompStruct.

@Kunhong Du just flagging this as something that we will need.

[Nick Ward]

@Joël Riou thanks for all this work, and for your patience in explaining it to us.

[Nick Ward]

Would you be willing to share more info on the reference book you mentioned?

[Joël Riou]

I am using Simplicial homotopy theory by Goerss-Jardine. They define the homotopy relation by using maps X ⊗ Δ[1] ⟶ Y, but when we need a more precise result (Lemma I.7.4: an n-simplex s of a pointed Kan complex (X, x) represents the trivial element of the homotopy group iff there is a n+1-simplex whose faces are (x, ...,x, s) [Actually, s can be put in any place in the list]), they just left this as an exercice without any hint (this appears when doing the homotopy sequence of a fibration between Kan complexes). I could fill in the details only by looking at the original paper by Daniel Kan, Ann. of Math. 67 (1958).

[Nick Ward]

Thanks, these should be helpful resources in my efforts to follow along here.

[Joël Riou]

Given X : Type u, A : Set X, U : ι → Set X and V : ι → ι → Set X such that A is the union of the U i, and the V i j are the intersections (this is CompleteLattice.MulticoequalizerDiagram A U V), I show in #23872 that the type A is the multicoequalizer of the U is along the V i js. This depends on a few other PRs: #23364, #23339, #22205, #21032, #22203, #21026. In a subsequent PR, a similar result will be deduced for SSet.Subcomplex instead of Set, and this will allow the construction of maps from horns.