Quasicategory (nerve C)

Stream: Infinity-Cosmos

[Nick Ward]

Hi, all. I am working on refactoring the proof by @Johan Commelin in #16458 that the nerve of a category is a quasicategory. The tentative direction (suggested by @Emily Riehl) is to use the material in #18499 and show that any simplicial set satisfying the StrictSegal condition is a quasicategory. Any thoughts on this endeavor are very welcome, and I'm sure I will have some more concrete questions once I have a chance to dig into things.

[Emily Riehl]

One paper, I would prove this by appealing also to the fact that the StrictSegal condition implies that the simplicial set $X$ is 2-coskeletal. In particular you get an isomorphism cosk2Iso between $X$ and (cosk 2).obj X; warning the meaning of cosk depends on whether or not you are in the Truncated namespace.

What this means is that a lifting problem into $X$ transposes to a lifting problem where you apply the left adjoint (sk 2).map (hornInclusion n i). On paper it is "obvious" this this map is an isomorphism whenever $n > 3$ so now you only have to fill inner horns in three cases: (2,1), (3,1), and (3,2).

[Emily Riehl]

The "obvious" fact might not be so easy to prove here, so I suspect it's better to forget about 2-coskeletality and just use the StrictSegal condition. This will produce an argument that's much closer to what Johan has currently.

[Emily Riehl]

By the Yoneda lemma, to solve a lifting problem against hornInclusion n i your task is just to define an n-simplex in $X$ and then check a bunch of coherence conditions. (I forget how much infrastructure for this exists; maybe others can weigh in.)

The data of the inner horn Λ[n, i] ⟶ X will give you what you need to define the $n$-simplex: it will be a spineToSimplex of a path of arrows you can extract from the image of the spine of the horn Λ[n, i]. [Aside: we should show that maps of simplicial sets induce maps of paths in a simplicial set.]

[Emily Riehl]

For the coherence conditions, since $X$ is StrictSegal, you can apply (segal _).injective to reduce the question of whether two simplices are equal to the question of whether the paths along their spines are equal. @Joël Riou created an ext lemma for paths, which hopefully won't be too hard to apply.

Perhaps you can formulate an ext lemma for simplices in a StrictSegal simplicial set along these lines?

[Emily Riehl]

A quick heads up for @Nick Ward and anyone else following this discussion: the material on StrictSegal simplicial sets is now in mathlib and can be found here:

file#Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal

Note that StrictSegal is now a typeclass which contains an explicit equivalence inverse for spine : X _[n] -> Path X n.

[Nick Ward]

Thanks for the heads up, and for the helpful sketch above.

[Nick Ward]

Is it best to open a PR against the infinity-cosmos repo first so that folks here can take a look, or should I just open a mathlib PR and link to it here?

[Emily Riehl]

Unless your formalization needs some stuff we haven't yet ported to mathlib, it's probably most efficient to just open this as a mathlib PR and then alert the Infinity-Cosmos channel of its existence.

In general I'm happy to streamline the process of getting things that are of general interest into mathlib sooner rather than later.

[Emily Riehl]

But whatever workflow makes sense to you is fine with me.

[Nick Ward]

So far I have a rough proof (here) that constructs the extension. It remains "only" to prove that it restricts to the appropriate map on the horn.

[Nick Ward]

(which I suspect will be much harder)

[Emily Riehl]

@Nick Ward could you go ahead and open this PR? There's a way to mark this as a draft pull request (I forget how exactly, but I believe it's fairly intuitive) so that no one will review it just yet.

But (I believe) by creating the PR, it will make it easier for others (or at least me) to check out your code and play around with it.

[Emily Riehl]

Or maybe the correct thing to do is add the label "WIP" to indicate a work in progress.

[Nick Ward]

@Emily Riehl I've just realized I still need to get a mathlib branch before I can open a PR. In the meantime, the following git commands should give you a local copy of my (or anyone else's) mathlib fork.

git remote add gio https://github.com/gio256/mathlib4
git fetch gio
git checkout gio/develop

[Nick Ward]

I should have specified that the commands above should be run from an existing mathlib repo directory.

[Dagur Asgeirsson]

Emily Riehl said:

Or maybe the correct thing to do is add the label "WIP" to indicate a work in progress.

Either is fine, draft PRs and PRs labeled "WIP" don't show up on the #queue and thus won't get reviewed in detail

[Nick Ward]

Thanks @Dagur Asgeirsson. I'm still getting the hang of the mathlib contribution guidelines.

[Nick Ward]

@Emily Riehl I opened a WIP PR at #19270. Any suggestions are very welcome!

[Nick Ward]

I've pushed a working proof to #19270, though there is still quite a bit of clean-up to do.

[Emily Riehl]

Alerting @Johan Commelin.

I'm sure the experts will have feedback for you, but this looks really great. Congrats!

[Emily Riehl]

Just a heads up: the above the line comment on the PR will become the official commit message after merge, so it should be more straightforwardly descriptive of what happened in the commit and who the contributors are.

Your name will be attached automatically as the commit author, but I believe the correct syntax for your collaborator would be

Co-Authored-By: [Johan Commelin](link)

[Emily Riehl]

One other thought is that perhaps the proofs that both strict segal simplicial sets and nerve of categories are quasi-categories should appear in the quasi-category file? That way the imports would be Nerve imported to StrictSegal imported to Quasicategory. But we should have an expert like @Joël Riou weigh in.

[Nick Ward]

Thank you @Emily Riehl, that's very helpful to know. I also realize that I took quite a lot of work in Wombat.lean and split the ideas up into several different files. Should I credit Johan in those files in some way?

[Johan Commelin]

You can add me to the Authors line.

[Johan Commelin]

@Emily Riehl I suggest having a file with just the basic defs of quasicat, and then a separate file that builds the examples

[Johan Commelin]

Maybe we need a directory Quasicategory, with files Defs.lean, Nerve.lean, Segal.lean

[Nick Ward]

@Johan Commelin I'm happy to make such a PR. Should we keep the Quasicategory/ directory in AlgebraicTopology/SimplicialSet, or does it ultimately belong somewhere in CategoryTheory/?

[Johan Commelin]

I don't have an opinion on that

[Johan Commelin]

I'm really happy to see how much cleaner the new approach is, compared to my old wombat approach.

[Nick Ward]

It really mapped very well from the proof sketch @Emily Riehl provided. It never fails to surprise me how much a bit of extra machinery can simplify a proof.

[Nick Ward]

By the way @Emily Riehl, you will have to pardon my ignorance of the convention here, but I have listed you as PR co-author as well given that it was ultimately your proof that I implemented. Please let me know if you would prefer not to be listed as such.

[Emily Riehl]

No objections ;) Though I'm still learning the conventions too...

[Emily Riehl]

I'll be really pleased to have this in mathlib because we might now have enough to prove that ordinary categories define an oo-cosmos. I'm hoping to have some time next week to expand the blueprint a bit.

[Nick Ward]

@Emily Riehl, relatedly, I'd be keen to pick up work on another proof as this one gets close to crossing the finish line. Unfortunately, I don't yet know my way around the project (or the topic) well enough to know what needs to be done. Please let me know if you think of anything that might make sense to take on next.

[Nick Ward]

Merged in mathlib4#19270!

[Emily Riehl]

Just saw this! Congrats. Tomorrow sometime I'll bump mathlib into the infinity-cosmos branch, delete wombat, and update the blueprint to point to this (unless someone else beats me to it).

[Emily Riehl]

I'll also write back soon with some new suggested projects.

[Nick Ward]

@Emily Riehl much appreciated!

I can work on the mathlib bump and the blueprint, as I suspect there will be some changes to make as a result of mathlib4#19472.

On deleting Wombat.lean -- I probably should first go through the file to look for any nerve-related lemmas that might still be useful to have.

[Emily Riehl]

Whoops. I didn't see this and was working on the same thing at basically the same time. I didn't think to see what should be salvaged from Wombat, though, so if you could do that, this would be great.

[Emily Riehl]

Btw should your Nerve.quasicategory be in the CategoryTheory namespace, where Nerve itself is found?

[Nick Ward]

Yes, I think it's fine to delete Wombat.lean and I will go back and see what I can glean from it.

I think you're probably right. I think maybe the old instance was in the Nerve namespace and that's why I put it there. I will see if I can't move it to CategoryTheory.Nerve namespace.
edit: The current instance is Nerve.quasicategory, not SSet.Nerve.quasicategory.

[Nick Ward]

It looks like we have CategoryTheory.nerve, do we want the instance to be CategoryTheory.Nerve.quasicategory?

[Nick Ward]

Currently the instance of type StrictSegal (nerve C) is Nerve.strictSegal. Assuming we decide on CategoryTheory.Nerve.quasicategory, we probably also want to move this to CategoryTheory.Nerve.strictSegal.

[Emily Riehl]

This sort of question is above my paygrade but maybe one of the mathlib experts will weigh in.

[Nick Ward]

I think I will just open a PR and ask for some feedback there.

[Nick Ward]

mathlib4#19521