welcome!

Stream: Infinity-Cosmos

[Emily Riehl]

I'm writing to launch the ∞-Cosmos Project which aims to formalize the basic formal theory of ∞-categories in Lean.

The term ∞-cosmos refers to an axiomatization of the universe in which ∞-categories live as objects. The axioms are somewhat ad-hoc and chosen for largely pragmatic reasons. In particular, the axioms are stated in the language of 1-category theory and simplicially enriched category theory, rather than in the language of ∞-category theory itself. The notion of ∞-cosmoi enables a "model-independent" development of the theory of ∞-categories, since various models such as quasi-categories and complete Segal spaces assemble into ∞-cosmoi.

Much of the development of the theory of ∞-categories takes place not in the full ∞-cosmos but in a quotient 2-category whose objects are ∞-categories, whose morphisms are ∞-functors, and whose 2-cells are ∞-natural transformations. We call this the homotopy 2-category since it is a quotient of the ∞-cosmos (which is an (∞,2)-category of a particular form) much like an (∞,1)-category has a quotient homotopy (1-)category. For instance, the existing Mathlib notions of equivalences and adjunctions in a bicategory specialize to define equivalences and adjunctions between ∞-categories when interpreted in the homotopy 2-category.

The initial aims of this project are relatively modest, though with sufficient interest its ambitions could expand considerably. In particular, our initial intention is not to attempt the difficult theorem of proving that the cartesian closed category of quasi-categories defines an example of an ∞-cosmos (among other things, the cartesian closure of this subcategory has not yet been proven) but rather create a large "bounty" to reward anyone who succeeds in this task in the form of a large cache of ∞-categorical theorems that will follow immediately.

This project is being co-lead by @Dom Verity and @Mario Carneiro, though my hope is to spare them some of the day-to-day burdens by serving as project manager. I'm relatively new to Lean, however, so advice from more experienced folks is especially welcome.

If you're interesting in hearing more or contributing to the development of this project, please join us in the thread below.

[Emily Riehl]

To get the project started, here is a preliminary task list. We can use the thread below to discuss each task in more detail. I'll update this post periodically as tasks get fleshed out, claimed, and completed:

Warm-up definitions:

D1 (:check: by the JHU category theory seminar, but others should feel free to work on this in parallel). Define the homotopy coherent isomorphism. We may later opt to work with different models of this simplicial set.

D2 (:check: by @Nima Rasekh and @Matej Penciak ). Define the notion of isofibration between quasi-categories.

D3 (:check: by the JHU CT seminar). Define the notion of equivalence between quasi-categories.

D4 (:check: by @Jack McKoen). Define the notion of trivial fibration between quasi-categories.
Tasks involving simplicial sets:

S1 (:check: by @Kunhong Du and @Nick Ward). Define the homotopy relation on 1-simplices in a simplicial set. Note a draft of this exists written by @Joseph Tooby-Smith in a mathlib PR, though it's not obvious to me which version of this definition will be the most useful.

S2 (incoming from @Kunhong Du). Prove the simpler form of the homotopy relation, under the hypothesis that the ambient simplicial set is a quasi-category. This is really a sequence of lemmas, some of which are already proven in the PR mentioned above.

S3 (possibly in progress by @Nick Ward?). Characterize the homotopy category of a quasi-category. The general homotopy category functor on simplicial sets has a simplified description on quasi-categories.

S4 (incoming from @Rida Hamadani and Dalton Sakthivadivel) Prove that the homotopy category functor preserves equivalences.

S5. A particularly hard task: prove that the homotopy category functor preserves products. There are two lemmas here, both of which we will eventually need. I suspect the easier will be to show that the homotopy category functor, when restricted to the subcategory of quasi-categories preserves all products, though this relies on task 3. The harder result, which could be attempted now, would be to show that this functor preserves finite products (binary products and the terminal object) of arbitrary simplicial sets.

S6 (work in progress by @Amelia Livingston). Give a "generators and relations" presentation of the simplex category.

Tasks involving simplicially enriched limits:

L1. (:check: by @Daniel Carranza) Define simplicial cotensors. While the current definition of "has cotensors" is mathematically correct, it is likely not in the most useful form, as it does not give us direct access to the simplicially enriched adjunction or include the associativity isomorphisms.

L2. (:check: by @Daniel Carranza) Prove that simplicial cotensors define a bifunctor.

L3 (:check: by @Dagur Asgeirsson ). Define simplicial conical limits.
Tasks involving ∞-cosmoi:

C1 (:check: by a team effort). Using all of the above, complete the definition of an ∞-cosmos.

C2. Define cartesian closed ∞-cosmoi.

[Jack McKoen]

I've done D2 and D4 in my quasi-category repo, as well as some API surrounding them. I believe @Joël Riou has a branch of mathlib concerning L1 and L2 (cotensor stuff).

[Jack McKoen]

(I will send some links in a bit)

[Jack McKoen]

here is some relevant code by Joël

edit: sent wrong links

[Nima Rasekh]

Hey! Very happy to see this is up and running now, after following it's development in Bonn these past months.

Two questions:

• Would there be value/room for having "math answerers" as part of the project/channel? I am by no means the expert on ∞-cosmoi (that's of course @Emily Riehl ), but with the assumption that Emily cannot be around 24/7 and some Lean people join who have a different mathematical background, it might make sense to have a place for basic ∞-cosmos questions that will come up.
• There is now a list of definitions/results that need to be tackled, but is there or will there be some sub-list more suitable for people with less experience (me) interested in contributing in some form?

[Emily Riehl]

@Nima Rasekh it would be awesome to have you contribute in the way you expect.

One issue with the blueprint in its current form is that the proofs are not well specced out. It would be a great help if an expert could supply a carefully-written paper proofs (written with an eye on which results currently exist or not in Mathlib) for someone to try to formalize.

The TeX source for the blueprint is here. Please make any elaborations directly in this document! It's very similar to a standard LaTeX file (ignoring the Lean codes, which you can ignore at first) except that

• macros live in three different files (in the "macros" folder) depending on whether they will render on both the PDF and HTML versions or are just for print or just for the web
• tikzcd diagrams only work if they are inside \begin{center} and \end{center} (and not in an equation environment)
• definitions, theorems, lemmas, etc need to be called that to appear in the blueprint (there's some code that would recognize shorthands such as "thm" but I don't know how it works and don't have it set up).

Alternatively, proofs can be sketched here and someone else can write up more details (or perhaps they won't be needed in the blueprint). I'll try and contribute further proof elaborations myself, but as you note, time is something lacking...

[Emily Riehl]

Nima Rasekh said:

• There is now a list of definitions/results that need to be tackled, but is there or will there be some sub-list more suitable for people with less experience (me) interested in contributing in some form?

The warmup definitions were supposed to be this: good beginner exercises. Otherwise, I think my best suggestion would be to try to form a team with a more experienced user. Based on my own experience as a Lean newcomer myself, this seemed like the most efficient way to learn more.

[Amelia Livingston]

Has anybody's work so far involved showing you can define a simplicial object via face and degeneracy maps? I'm tentatively assuming no since it looks like 1.2.4 is unticked - I've been messing around trying to do this, but will stop if it's already done.

[Emily Riehl]

Amelia Livingston said:

Has anybody's work so far involved showing you can define a simplicial object via face and degeneracy maps? I'm tentatively assuming no since it looks like 1.2.4 is unticked - I've been messing around trying to do this, but will stop if it's already done.

Not that I'm aware of and this would definitely be helpful!

[Emily Riehl]

Jack McKoen said:

here is some relevant code by Joël

edit: sent wrong links

Thanks @Jack McKoen. @Joël Riou we should discuss the best way to formalize this definition.

I think this Lean definition is mathematically correct but doesn't give direct access to all the structure that you want. Am I right that it's best to give some redundant fields of this typeclass and later prove theorems that show that they can be built from less data?

On the other hand, I produced the code above by mimicking the way that unenriched limits are set up. It wasn't clear to me whether this case was so different...

[Nima Rasekh]

Emily Riehl said:

Nima Rasekh it would be awesome to have you contribute in the way you expect.

One issue with the blueprint in its current form is that the proofs are not well specced out. It would be a great help if an expert could supply a carefully-written paper proofs (written with an eye on which results currently exist or not in Mathlib) for someone to try to formalize.

The TeX source for the blueprint is here. Please make any elaborations directly in this document! It's very similar to a standard LaTeX file (ignoring the Lean codes, which you can ignore at first) except that

• macros live in three different files (in the "macros" folder) depending on whether they will render on both the PDF and HTML versions or are just for print or just for the web
• tikzcd diagrams only work if they are inside \begin{center} and \end{center} (and not in an equation environment)
• definitions, theorems, lemmas, etc need to be called that to appear in the blueprint (there's some code that would recognize shorthands such as "thm" but I don't know how it works and don't have it set up).

Alternatively, proofs can be sketched here and someone else can write up more details (or perhaps they won't be needed in the blueprint). I'll try and contribute further proof elaborations myself, but as you note, time is something lacking...

Cool, sounds like a very reasonable idea to start with. I'll take a look and see if I have meaningful suggestions.

[Nima Rasekh]

Emily Riehl said:

Nima Rasekh said:

• There is now a list of definitions/results that need to be tackled, but is there or will there be some sub-list more suitable for people with less experience (me) interested in contributing in some form?

The warmup definitions were supposed to be this: good beginner exercises. Otherwise, I think my best suggestion would be to try to form a team with a more experienced user. Based on my own experience as a Lean newcomer myself, this seemed like the most efficient way to learn more.

I agree, but unfortunately we can't all hang out in Bonn anymore. Maybe there can be ways to form groups online through this channel.

[Emily Riehl]

Jack McKoen said:

I've done D2 and D4 in my quasi-category repo, as well as some API surrounding them. I believe Joël Riou has a branch of mathlib concerning L1 and L2 (cotensor stuff).

Could you remind me where your repo is? I also suspect other readers might appreciate having this linked from here.

[Emily Riehl]

If you want to add D2 and D4 to the infinity-cosmos repo, I think perhaps "trivial fibration" belongs in the simplicial sets file (in the local "Mathlib" folder under "InfinityCosmos") while "isofibration" belongs in the quasicategories file (since the definition isn't correct between arbitrary simplicial sets).

[Jack McKoen]

The repo is https://github.com/mckoen/quasicategory (it's not very organised but I've written a lot of comments). I'll create a PR today or tomorrow to add both definitions

[Dagur Asgeirsson]

I completed L3 at https://github.com/emilyriehl/infinity-cosmos/pull/9

[Emily Riehl]

Thanks @Dagur Asgeirsson; just merged. I'm wondering what API we might need. For instance:

noncomputable def limitComparisonIso (X : A) (h : IsSLimit c) :
    sHom X c.pt ≅ (limit (K ⋙ (sHomFunctor A).obj (op X))) := by
  have := isIso_limitComparison c X h
  exact (asIso (SimplicialCategory.limitComparison c X))

???

[Emily Riehl]

Eg in the special case of simplicial products, I suspect we'll want the isomorphism sHom X (A × B) ≅ (sHom X A) x (sHom X B)

[Emily Riehl]

Also should the lemma isIso_limitComparison be an instance?

[Emily Riehl]

Tomorrow I'm introducing Lean to some new users who are regular attendees of the Johns Hopkins category theory seminar. If no one else objects, we'll work on D1, which is probably the most straightforward.

[Jack McKoen]

I made a quick PR for D4 here: https://github.com/emilyriehl/infinity-cosmos/pull/10

I'm not certain about the file locations- I made a MorphismProperty.lean file but wasn't sure where to put it. I also only added a bare minimum of API here. If there's something someone thinks I should add in relation to right/left lifting properties or trivial fibrations, just let me know.

I will make another PR for isofibrations a bit later.

[Emily Riehl]

Jack McKoen said:

I made a quick PR for D4 here: https://github.com/emilyriehl/infinity-cosmos/pull/10

I'm not certain about the file locations- I made a MorphismProperty.lean file but wasn't sure where to put it. I also only added a bare minimum of API here. If there's something someone thinks I should add in relation to right/left lifting properties or trivial fibrations, just let me know.

This looks great @Jack McKoen. I'd love to go ahead and merge so that others can play around with it.

Regarding your question, my understanding based on a conversation with @Pietro Monticone is that we should put augmentations of existing mathlib files like CategoryTheory.MorphismProperty in a local copy in the local Mathlib folder (rather than as a new file in the ForMathlib folder). But this also seems dangerous because of potential import conflicts: if one of our files transitively imports external mathlib's CategoryTheory.MorphismProperty then we'll get duplicate definition errors.

So I don't know what the best practice is. Thoughts anyone?

[Kim Morrison]

I think you should just be putting such material in ForMathlib. Anything else seems unnecessarily complicated, and I'm uncertain what the benefit would be.

[Pietro Monticone]

Another approach would be to create a dedicated InfinityCosmos branch in Mathlib, where all relevant augmentations can be added to the corresponding files. Afterward, you would only need to replace:

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "InfinityCosmos"

Additionally, it is important to periodically merge the master branch into the InfinityCosmos branch to stay up to date with upstream changes.

[Kim Morrison]

What benefit would that have?

[Kim Morrison]

It seems a lot of overhead for contributors to maintain that branch.

[Kim Morrison]

I guess it could, if done well, make it easier to PR to Mathlib because one could just do a squash merge of that branch and then select the subset of files you want to PR?

[Kim Morrison]

But I think it is better to have a clear distinction between "code that is not up to Mathlib standards" and "code that is". Code that isn't up to standard lives in ForMathlib. Code that is up to standard also lives in ForMathlib, but has a comment at the top of the file saying "This material has been PR'd to Mathlib as #12345."

[Kim Morrison]

Maintaining an InfinityCosmos branch of Mathlib just seems like an invitation to dump unpolished code into that branch.

[Pietro Monticone]

Kim Morrison said:

I guess it could, if done well, make it easier to PR to Mathlib because one could just do a squash merge of that branch and then select the subset of files you want to PR?

Yes, I believe it can make it quite easier to then PR to Mathlib (after polishing, generalizing, golfing, etc.).

[Pietro Monticone]

Kim Morrison said:

Maintaining an InfinityCosmos branch of Mathlib just seems like an invitation to dump unpolished code into that branch.

I see what you mean… I would have guessed the exact opposite: it would incentivize to push cleaner code. I might be completely wrong of course.

[Kim Morrison]

Worth experimenting! I think in the past people have not maintained such a branch, but perhaps that is a reason to do it, rather than a reason not to.

[Pietro Monticone]

Totally agree. Let’s see how it goes.

I’ll try to do my best to keep the code in that branch as clean as possible.

[Kevin Buzzard]

So it did occur to me to make an FLT branch of mathlib, with the idea being that I could just add random things to it which I felt were in good shape, and then have FLT depend on that branch. But I decided not to, because I was scared that it would just end up overflowing and be un-PRable. I'm not sure that having a branch with loads of stuff on it is any easier than having another repo with a ForMathlib directory, when it comes to making PRs. Maybe it's worth experimenting but I guess other projects I've worked on (specifically perfectoid and LTE) just had a ForMathlib directory and these worked out fine. The thing which I learnt from perfectoid is not just to keep filling up ForMathlib and not PRing anything, but I suspect that the same thing could happen with a mathlib branch.

[Mario Carneiro]

the advantage of a ForMathlib directory over a mathlib branch is that you can merge changes to it simultaneously with changes to the rest of the project

[Kim Morrison]

I think the critical thing, wherever the material actually lives, is that there is a project manager (Emily here, Kevin at FLT?) who considers it part of their job to be anxious and dissatisfied whenever there is material in that place without knowing who specifically is currently working on moving it out to Mathlib.

[Kim Morrison]

Hopefully they don't actually have to move it themselves, but it is a high priority to recruit/cajole/nerd-snipe participants into doing so.

[Emily Riehl]

@Kim Morrison your point is as project manager I should encourage folks to frequently ship things out of ForMathlib and into actual mathlib (as they're ready of course)? If so, noted.

[Kim Morrison]

Yes, exactly. (I realize my message above maybe had the wrong tone; sorry.)

[Emily Riehl]

No need for apology :) Just making sure I got the point. These sorts of tips are very helpful.

[Emily Riehl]

Jack McKoen said:

I made a quick PR for D4 here: https://github.com/emilyriehl/infinity-cosmos/pull/10

I'm not certain about the file locations- I made a MorphismProperty.lean file but wasn't sure where to put it. I also only added a bare minimum of API here. If there's something someone thinks I should add in relation to right/left lifting properties or trivial fibrations, just let me know.

I will make another PR for isofibrations a bit later.

Merged.

[Jack McKoen]

I actually got isofibrations (which I don't have) mixed up with inner fibrations (which I do have). So the PR for D2 will take a bit longer (and I invite others to also work on it).

[Kunhong Du]

Hello, really excited to learn about this project! Actually, I've been working on formalizing the simplcial model of HoTT for my master's thesis. so I have done some work on simplcial sets, including proving homotopy of maps from a simplcial set to a Kan complex is an equivalence relation and defining simplicial homotopy groups. Would they be useful for this project? Also, how is S2 going now? Since it's closely related to what I've done, would it be possible for me to help out with it?"

[Emily Riehl]

@Kunhong Du welcome aboard. We'd be delighted to have you contribute.

[Emily Riehl]

We need work on homotopy-related stuff at two different levels: inside a quasi-category and between quasi-categories.

[Emily Riehl]

S2 is about a homotopy relation for 1-simplices inside a quasi-category. One way to define it is a parallel pair of 1-simplices in a quasi-category are homotopic iff they map to the same 1-simplex along the unit of the homotopy category -| nerve adjunction. That's probably not the most useful definition to start with, though, since that adjunction is currently being PRed into mathlib (but an earlier version of this code can be found in the HomotopyCat.lean file in our repository).

[Emily Riehl]

There's a lemma in the statement of S2 that doesn't explicitly refer to the homotopy category functor which could be attacked directly by someone with your sort of background. If you want to work on it, it's yours!

[Emily Riehl]

You might also want to look at the file Homotopy.lean which experiments with an encoding of homotopy between simplicial sets parametrized by an arbitrary interval. The idea is that the choice you would make for Kan complexes Δ^1, is different from the choice you would make for quasi-categories (something we're calling CoherentIso).

This code is very experimental and might not be structured optimally. If you have suggestions for it, or want to add structure to the interval to allow you to prove some of the lemmas you've done in your repository, that would be helpful.

Note there's a reason for the slightly strange choice to define a homotopy in curried form: this will generalize better to develop analogous structures internally to an oo-cosmos.

[Emily Riehl]

Let me know if you have any questions/suggestions or want to chat about this more.

[Kunhong Du]

@Emily Riehl
Thanks for the informative reply. So the desired approach of S2 is to first define homotopy on 1-simplices via 2-simplex and then show it coincides with the definition using homotopy category? I'll work on the first part and see if I can handle the second part.

The file Homtopy.lean is very insightful. I'll think about how to make use of it and incorporate it into my repository.

[Emily Riehl]

@Kunhong Du I don't have a strong sense of which definition is most desirable, but 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.

[Emily Riehl]

Then we definitely want to show that this is the same as being identified in the homotopy category, but hopefully the construction of that functor will be stable by then!