(infinity, 1)-categories

Stream: Is there code for X?

[Andrea Bourque]

What progress (if any) has been made towards infinity categories in Lean?

[Kevin Buzzard]

IIRC we have simplicial sets but nobody has needed infinity categories yet

[Joseph Tooby-Smith]

I am also interested in (infinity,1)-categories in lean.

[Kevin Buzzard]

I don't think there's any obstruction to making the quasicategory definition

[Johan Commelin]

Here's a start that I created some time ago.

• As you can see, the definition can be made in a few lines.
• The first minor objective would be to show that the nerve of a 1-category is a quasicategory. Back then this was quite annoying. But recently @Joël Riou has added quite some API for chains of arrows in categories. So with a bit of refactoring and gluing, this should now be quite doable.

import Mathlib.AlgebraicTopology.SimplicialSet
import Mathlib.AlgebraicTopology.Nerve

/-!
# Kan complexes and quasicategories

-/

universe v u

open CategoryTheory CategoryTheory.Limits Opposite

open Simplicial

namespace SSet

/-- A *Kan complex* is a simplicial set `S` if it satisfies the following horn-filling condition:
for every `n : ℕ` and `0 ≤ i ≤ n`,
every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `σ : Δ[n] → S`. -/
class Kan_complex (S : SSet) : Prop :=
  (hornFilling : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+1)⦄ (σ₀ : Λ[n, i] ⟶ S),
    ∃ σ : Δ[n] ⟶ S, σ₀ = hornInclusion n i ≫ σ)

/-- A *quasicategory* is a simplicial set `S` if it satisfies the following horn-filling condition:
for every `n : ℕ` and `0 < i < n`,
every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `σ : Δ[n] → S`.

[Kerodon, 003A] -/
class quasicategory (S : SSet) : Prop :=
  (hornFilling : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+1)⦄ (σ₀ : Λ[n, i] ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last n),
    ∃ σ : Δ[n] ⟶ S, σ₀ = hornInclusion n i ≫ σ)

/-- Every Kan complex is a quasicategory.

[Kerodon, 003C] -/
instance (S : SSet) [Kan_complex S] : quasicategory S where
  hornFilling _ _ σ₀ _ _ := Kan_complex.hornFilling σ₀

-- TODO: move
instance fin_two_zero_le_one : ZeroLEOneClass (Fin 2) where
  zero_le_one := by decide

section nerve

-- TODO: move
/-- A constructor for `n`-simplices of the nerve of a category,
by specifying `n+1` objects and a morphism between each of the `n` pairs of adjecent objects. -/
def nerve.mk (C : Type) [inst : Category C] (n : ℕ)
    (obj : Fin (n+1) → C) (mor : ∀ (i : Fin n), obj i.castSucc ⟶ obj i.succ) :
    (nerve C).obj (op [n]) := sorry

variable {C : Type} [inst : Category C]

-- TODO: move
def nerve.source (f : (nerve C).obj (op [1])) : C := f.obj (0 : Fin 2)

-- TODO: move
def nerve.target (f : (nerve C).obj (op [1])) : C := f.obj (1 : Fin 2)

-- TODO: move
def nerve.arrow (f : (nerve C).obj (op [1])) : source f ⟶ target f :=
  f.map (homOfLE (X := Fin 2) zero_le_one)

-- TODO: move
open SimplexCategory in
lemma nerve.source_eq (f : (nerve C).obj (op [1])) :
    source f = ((nerve C).map (δ (1 : Fin 2)).op f).obj (0 : Fin 1) := rfl

-- TODO: move
open SimplexCategory in
lemma nerve.target_eq (f : (nerve C).obj (op [1])) :
    target f = ((nerve C).map (δ (0 : Fin 2)).op f).obj (0 : Fin 1) := rfl

end nerve

/-- The nerve of a category is a quasicategory.

[Kerodon, 0032] -/
instance (C : Type) [Category C] : quasicategory (nerve C) where
  hornFilling n i σ₀ h₀ hₙ  := by
    let v : Fin (n+1) → (horn n i).obj (op [0]) :=
      fun j ↦ ⟨SimplexCategory.Hom.mk (OrderHom.const _ j), ?_⟩
    swap
    · simp only [unop_op, SimplexCategory.len_mk, asOrderHom, SimplexCategory.Hom.toOrderHom_mk,
        OrderHom.const_coe_coe, Set.union_singleton, ne_eq, ← Set.univ_subset_iff, Set.subset_def,
        Set.mem_univ, Set.mem_insert_iff, Set.mem_range, Function.const_apply, exists_const,
        forall_true_left, not_forall]
      by_cases h : j = 0
      · refine ⟨Fin.last n, ?_⟩
        simp [h, hₙ.ne', (h₀.trans hₙ).ne]
      · refine ⟨0, ?_⟩
        simp [h, h₀.ne]
    let σ : Δ[n] ⟶ nerve C :=
      yonedaEquiv.symm <| nerve.mk C n (fun j ↦ ?_) (fun j ↦ ?_)
    use σ
    swap
    · refine (σ₀.app (op [0]) (v j)).obj ⟨0, by simp⟩
    swap
    let e : (horn n i).obj (op [1]) := ⟨SimplexCategory.Hom.mk ⟨![j.castSucc, j.succ], ?_⟩, ?_⟩
    let f := σ₀.app (op [1]) e
    swap
    · rw [Fin.monotone_iff_le_succ]
      dsimp
      simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, Fin.le_iff_val_le_val, Fin.val_succ,
        Fin.forall_fin_one, Fin.castSucc_zero, Matrix.cons_val_zero, Fin.coe_castSucc,
        le_add_iff_nonneg_right]
    swap
    · simp only [unop_op, SimplexCategory.len_mk, asOrderHom, SimplexCategory.Hom.toOrderHom_mk,
        OrderHom.const_coe_coe, Set.union_singleton, ne_eq, ← Set.univ_subset_iff, Set.subset_def,
        Set.mem_univ, Set.mem_insert_iff, Set.mem_range, Function.const_apply, exists_const,
        forall_true_left, not_forall, not_or, unop_op, not_exists, Fin.forall_fin_two]
      dsimp
      by_cases h : j.castSucc = 0
      · refine ⟨Fin.last n, ?_⟩
        cases n with
        | zero => simp only [Nat.zero_eq, Fin.last, Fin.zero_eta, Fin.not_lt_zero] at hₙ
        | succ n =>
          simp only [hₙ.ne', not_false_eq_true, h, (h₀.trans hₙ).ne, Fin.succ_eq_last_succ, true_and]
          simp only [Fin.lt_iff_val_lt_val, Fin.val_last, Fin.val_zero] at h₀ hₙ
          simp only [Fin.castSucc_eq_zero_iff] at h
          simp only [h, Fin.last, Fin.ext_iff, Fin.val_zero]
          linarith only [h₀, hₙ]
      · refine ⟨0, ?_⟩
        simp [h, h₀.ne, Fin.succ_ne_zero j]
    · let φ := nerve.arrow f
      -- let δ := fun (i : Fin 2) ↦ (nerve C).map (SimplexCategory.δ i).op
      have := fun (k : Fin 2) (e : (horn n i).obj (op [1])) ↦
        congr_fun (σ₀.naturality (SimplexCategory.δ k).op) e
      dsimp only [types_comp, Function.comp] at this
      refine ?_ ≫ φ ≫ ?_
      · rw [nerve.source_eq, ← this]
        apply eqToHom
        suffices : (horn n i).map (SimplexCategory.δ 1).op e = v j.castSucc
        · rw [this]; rfl
        apply Subtype.ext
        apply SimplexCategory.Hom.ext'
        apply OrderHom.ext
        apply funext
        erw [Fin.forall_fin_one]
        rfl
      · rw [nerve.target_eq, ← this]
        apply eqToHom
        suffices : (horn n i).map (SimplexCategory.δ 0).op e = v j.succ
        · rw [this]; rfl
        apply Subtype.ext
        apply SimplexCategory.Hom.ext'
        apply OrderHom.ext
        apply funext
        erw [Fin.forall_fin_one]
        rfl
    apply NatTrans.ext; apply funext
    apply Opposite.rec
    apply SimplexCategory.rec
    intro m
    ext f
    refine CategoryTheory.Functor.ext ?_ ?_
    · intro (k : Fin (m+1))
      sorry
    · sorry

end SSet

[Adam Topaz]

Pinging @Jack McKoen who is working on related things right now

[Trebor Huang]

I think the best plan is to formalize lifting properties (the Joyal–Tierney calculus) and maybe weak factorization systems in general categories since they will be repeatedly used in quasicat theory. Are those in mathlib yet?

[Johan Commelin]

Several people have been working on WFS. I lost track of what the current status is...

[Joël Riou]

@Trebor Huang: the basic definitions of lifting properties are in mathlib (CategoryTheory.LiftingProperties).

[Trebor Huang]

Ah, when I typed in "lifting" in the docs searchbar the suggestions are dominated by liftRing so I thought there was none

[Trebor Huang]

Is this some search priority issue to be fixed?

[Johan Commelin]

The branch quasicat now contains a sorry-free proof that the nerve of a category is a quasicategory.

[Johan Commelin]

It was a pretty nasty fight with DTT.

[Adam Topaz]

What about DTT made it tough? Maybe we should rethink the simplicial API?

[Johan Commelin]

An n-simplex of the nerve is a functor from Fin (n+1) to C. Now you can map i -> (i+1) through such a functor to get a morphism in C. That same morphism will also be a 1-simplex. But not in a defeq way.

[Adam Topaz]

Aha. But if we use some inductive analogue of Fin (I don’t know if Fin’ will quite work) then we should get good defeq behavior

[Adam Topaz]

Using functors from Fin to talk about sequences of composable morphisms is a nice trick, but if it’s tedious to use, then perhaps we should come up with a bespoke inductive definition after all

[Johan Commelin]

Maybe. I think @Joël Riou already wrote a very good API for ComposableArrows

[Johan Commelin]

I think I rather want to explore playing out the whole proof in the arrow category of C. I think it would save on a whole lot of eqToHoms.

[Johan Commelin]

Anyway: #9357 is the first PR, containing the bare definitions of Kan complex and quasicategory.

[Adam Topaz]

Left a few comments

[Adam Topaz]

Let me ping @Jack McKoen again since he also had a def of a Kan complex on his branch

[Johan Commelin]

We should also write a delaborator for

scoped[Simplicial] notation "Λ[" n ", " i "]" => SSet.horn (n : ℕ) i

[Adam Topaz]

If we change notation to notation3 does it make things better? I seem to recall @Kyle Miller saying something along those lines.

[Johan Commelin]

Thanks! That worked: #9358

[Johan Commelin]

#9360 provides an alternative hornfilling condition

[Johan Commelin]

#9362 adds some trivial prerequisites on cardinalities of explicit finsets.

[Riccardo Brasca]

I left a minicomment and delegated it.

[Johan Commelin]

Thanks

[Johan Commelin]

#9363 is the next one in line. But it depends on the finset-cardinalities PR.

[Johan Commelin]

• #9357 basic definitions
• #9360 alternative horn filling condition
• #9362 bounds on cardinalities of explicit finsets
• #9363 constructors for subsimplices of horns

[Joseph Tooby-Smith]

deleted message

[Joseph Tooby-Smith]

(Sorry ignore the above, I missed a comment above)

[Joseph Tooby-Smith]

Maybe it would be nice to have a github project for quasicategories, to track progress in this direction and list the important steps that would need to be taken to develop their theory. Do people think this is an appropriate of these projects? If so I am happy to put some work into to developing one - although I think maintainers have to create them on Mathlib4.

[Adam Topaz]

I think this is a good idea. But we should select a good “target” to help coordinate work. The infinity categorical yoneda lemma is a possible target

[Joseph Tooby-Smith]

@Adam Topaz Agreed, and I think the infinity-cat Yoneda lemma seems a good target. Another possible one is the definition of a infinity-topos. But Yoneda is probably better.

[Adam Topaz]

I made an empty project here: https://github.com/orgs/leanprover-community/projects/18

[Joseph Tooby-Smith]

@Adam Topaz Thanks :)

[Joseph Tooby-Smith]

@Adam Topaz Could I possibly have write access for the project? Doesn't seem to let me edit it by default.

[Adam Topaz]

hmmm... I don't remember how to do that. Can another maintainer help out?

[Adam Topaz]

Oh ok I see how to do it now. What's your github username @Joseph Tooby-Smith ?

[Joseph Tooby-Smith]

jstoobysmith

[Adam Topaz]

you should have an invite in your inbox

[Joseph Tooby-Smith]

Yep that worked! Thanks @Adam Topaz

[Dagur Asgeirsson]

It's a nontrivial result that the functors between ∞-categories form an ∞-category (and, I guess, necessary for the statement of the Yoneda lemma). Maybe that can be added to the list in the github project

[Adam Topaz]

There’s also the question of managing universes… for example, maybe we want the category of anima to have zero cells in level 1, and all higher cells in level 0?

[Adam Topaz]

The current simplicial sets framework doesn’t make this easy

[Joseph Tooby-Smith]

@Dagur Asgeirsson I added this....on which note:

Do you (and @Adam Topaz ) think the format of the list is ok/have any suggestions?
I added Kerodon tags to make it easier to find references to things. Although I'm not sure about the stability of these tags.

[Adam Topaz]

Re functors: IIRC there’s an adjunction between quasicats and ssets and it’s useful for constructing the qcat structure on functors, right? I guess this adjunction could be part of the list as well.

[Adam Topaz]

Kerodon tags are a great idea!

[Matthew Ballard]

Can the Kerodon tags be linkified?

[Matthew Ballard]

It doesn't appear so in any nice way from the UI :(

[Dagur Asgeirsson]

The format of the list is fine I think, I guess it will evolve over time. This GitHub projects UI seems kind of limited though

[Joseph Tooby-Smith]

@Matthew Ballard You can link to them in the comments of the entry. E.g. if you click the title of the first entry Define: homotopy of morphisms in an infinity-cat, I've put a link there.

[Matthew Ballard]

Thanks!

It would make your life easier if you could make a template and access the fields as variables though

[Jack McKoen]

How can I "claim" one of these goals?

[Matthew Ballard]

Assign yourself?

[Adam Topaz]

@Jack McKoen you might need write access... if so, let me know.

[Jack McKoen]

I think I need write access (unless I just can't find the option on mobile)

[Adam Topaz]

you should have access now.

[Jack McKoen]

Thanks, works now

[Dean Young]

@Jack McKoen @Adam Topaz I'd like to mention that these efforts will help a lot with my work with Jiazhen Xia available here:

https://github.com/linlib/TheWhiteheadTheoremandTwoVariations/blob/main/TheWhiteheadTheoremandTwoVariations.pdf

Is it ok if I lobby for a few things?

I think it is a good idea to use a certain four categories:

1. ∞-Cat : Category quasicategory
2. ∞-Grpd : Category Kan_complex
3. D(∞-Cat) : Category quasicategory
4. D(∞-Grpd) : Category Kan_complex

The second two can be created from the first two using the work in Jack's presentation at Lean together. The repository I linked to contains a definition of the first two in the file of TheWhiteheadTheoremandTwoVariations.lean.

I wonder if down the road, having these categories and the definitions of functors and natural transformations that they allow for would save a lot of effort. I'm thinking about how the components of each of the functors on the first pages of the files here and here could be more cumbersome without forming these categories.

P.S. Jiazhen and I are excited to be submitting our definition of CW-complexes and proof of the Whitehead theorem within a few weeks. We are also working on two variations of the Puppe sequence. Together, these six theorems give an alternative definition of ∞-Cat.

[Dean Young]

https://github.com/linlib/ThePuppeSequenceandTwoVariations/blob/main/ThePuppeSequenceandTwoVariations.pdf

[Dean Young]

@Adam Topaz Jiazhen and I would also be greatly excited to join this project. Would it be ok if we get write privileges and tackle a few of these goals?

[Dean Young]

Can Jiazhen and I take 11 and 12? We were already going to show those in the Whitehead theorem repo. Maybe you could give write privileges to linlib and jzxia.

[Joseph Tooby-Smith]

@Jack McKoen I have already done some work in the defining homotopies direction. See:

https://github.com/leanprover-community/mathlib4/pull/10006

I'm fairly new to lean so it's a bit of a mess though. In particular, the above uses:

https://github.com/leanprover-community/mathlib4/pull/9935

which is now waiting on another pull-request (plus some tidying on my part).

[Joseph Tooby-Smith]

Unrelated to the above: All the goals in this project now have links to the appropriate Kerodon page in their comments (click the title of the goal to see the comments).

[Adam Topaz]

@Dean Young I'm happy to give you write access to the project, but I would need your (and Jiazhen's) github user name(s).

[Adam Topaz]

Oh, I just noticed your second message with the user names. I'll add those now.

[Jiazhen Xia]

@Adam Topaz Thank you! We have access now, and we are excited to work on 11 and 12 (space of morphisms).

[Johan Commelin]

Let me just mention here that there is a proof in the file Wombat.lean of the quasicat branch that the nerve of a category is a quasicategory. I currently don't have the time to PR this to mathlib (maybe sometime in the future?). But anybody interested should feel free to PR (parts of it). I don't claim any copyright etc yaddayadda

[Jack McKoen]

@Joseph Tooby-Smith Given what you already have done I think it makes sense for you to take care of 1 and 2. I'll work on something else :)

[Johan Commelin]

I created a draft PR: #16458
It contains ~460 lines of code, proving that the nerve of a category is a quasicategory.
It needs some massaging to make it mathlib ready, but I don't have much time for that atm.
If you like this topic, please feel free to adopt this PR.

[Adam Topaz]

Ping @Jack McKoen :up:

[Dagur Asgeirsson]

Johan Commelin said:

The branch quasicat now contains a sorry-free proof that the nerve of a category is a quasicategory.

Hopefully someone adopts it this time (this was in december)!

[Adam Topaz]

All those eqToHoms make me sad

[Johan Commelin]

FYI, I did merge today's master into the branch. So no need to do awkward bumping

[Johan Commelin]

The eqToHoms make me sad. But they are not the worst part. :see_no_evil:

[Emily Riehl]

@Johan Commelin what would you say the worst part is?

[Emily Riehl]

@Joseph Tooby-Smith after reading this old thread I wanted to let you and your collaborators (if you can help me find them) know about a new blueprint project I'm in the process of setting up (https://emilyriehl.github.io/infinity-cosmos) and will create a channel for here very soon. The aim is to develop some of the formal (read 2-categorical) theory of (oo,1)-categories which means that if someone wants to do the hard work of showing that quasi-categories satisfy a certain list of axioms (defining an "oo-cosmos") then a whole bunch of theorems will follow.

[Emily Riehl]

Most of the early formalization work will involve simplicially enriched categories or 2-categories stuff but there is a little bit of quasi-category theory needed too, and part of why I wanted to get in touch is to see whether you (or anyone else) has already done it.

[Emily Riehl]

BTW @Mario Carneiro and I recently completed a construction of the left adjoint to the nerve and a proof that this adjunction is reflective (and thus, as a corollary, that Cat has colimits). This is all contained in the file "HomotopyCat.lean" in the repository I just linked from (currently broken in a way I don't understand due to some attempted renaming; I'll fix this later today). We're in the process of moving everything into a mathlib branch currently here: https://github.com/leanprover-community/mathlib4/tree/CatHasColimits

[Joseph Tooby-Smith]

Hi @Emily Riehl ! I ended up dropping the ball on this (another Lean project I'm working on has taken most of my time) - so never really made any progress on quasi-categories. Your blueprint project looks great though! I'm excited to see where it goes, and I'm looking forward to having more about higher-categories in Lean.

[Jack McKoen]

Hi @Emily Riehl , I've been working on formalizing some quasi-category theory in this repo. What in particular do you think you will need?

My main goal at the moment is to formalize https://kerodon.net/tag/0066 (Fun(S, D) is a quasicat when D is), so if you need anything that goes into this proof, I might have already done it or will be doing it soon. In any case I'd be happy to help with the quasi-category bit of your project.

[Johan Commelin]

Emily Riehl said:

Johan Commelin what would you say the worst part is?

filler_succ_aux is pretty terrible

[Johan Commelin]

And when you need a doubly-primed name, that's also a bit of a smell that something isn't optimal

[Emily Riehl]

@Jack McKoen in general I'd be happy to know about anything that you've got. Your goal is :fire: so let me know in particular when you've got it :)

[Emily Riehl]

@Joseph Tooby-Smith a few months ago you mentioned you formalized something about the homotopy relation for 1-simplices. If so, and if you're willing to share your code, we'll take

https://emilyriehl.github.io/infinity-cosmos/blueprint/sec-simplicial-sets.html#defn:1-simplex-htpy

and perhaps some of the following lemmas off the initial to-do list.

[Joseph Tooby-Smith]

@Emily Riehl The stuff I did on 1-simplies can be found here:

• https://github.com/leanprover-community/mathlib4/pull/10006/files#diff-d9401595c03bcfddf1ecc22aa64fe6a62f82ae75b237ef92269c4c42f967f04f

Other stuff I've done for infinity categories are:

• Define the join of augmented simplicial sets:
  https://github.com/leanprover-community/mathlib4/pull/11021

And some stuff related to the augmented simplex category:

• https://github.com/leanprover-community/mathlib4/pull/10190

I did all of this stuff when I was still pretty new to lean, so I can't claim it is any good, and it definitely needs a refactor.

[Dean Young]

@Emily Riehl do your plans include model structures?

One of the cited papers is "K. S. Brown. Abstract homotopy theory and generalized sheaf cohomology. Trans. Amer. Math. Soc., 186:419–458, 1973."

[Emily Riehl]

@Dean Young not initially no but we likely will want proofs of related results. The citation is for Brown's axiomatization of a category of fibrant objects. Some proofs of results that hold in that setting would be great to have. (See Appendix C of "Element of oo-category theory" with @Dom Verity; this isn't yet part of the blueprint.)

[Dean Young]

@Emily Riehl ok thanks for this.

Previously we had these thoughts about how to define an internal hom:
• [I,Δⁿ] has the (inner) horn lifting condition
• [I.X] has the (inner) horn lifting condition when X does
• [X, Y] has the (inner) horn lifting condition when Y does

[Emily Riehl]

@Dean Young is "I" something special here?

[Dean Young]

@Emily Riehl Sorry, meant Δ¹!

[Emily Riehl]

That makes sense.

Some thoughts for the first point: once we know that the homotopy category functor preserves finite products (a pain to prove I fear but something we will need soon) it follows formally (using the fact that ho(N C) = C that the nerve preserves exponentials. So then [I,Δ^n] is a nerve of a category and thus a quasi-category (thanks to Johan).

Though actually this requires the observation that Δ^n is the nerve of Fin n+1, which might not have been proven yet.

[Emily Riehl]

@Joseph Tooby-Smith I'm still new to Lean so all my code needs lots of editing...

If you don't mind, I think the best thing to do would be to leave the homotopy category stuff on the to-do list but point to your PR. That might spur some attention to it and then revisions can happen there. Does this feel okay to you?

[Joseph Tooby-Smith]

@Emily Riehl That seems like a great idea! I'd be fine with this.

[Emily Riehl]

There is a new channel open to discuss this project here: #Infinity-Cosmos

[Emily Riehl]

@Jack McKoen over in the new #Infinity-Cosmos branch I've invited some golfing on some existing quasi-category theory code. I didn't put your work in progress on the list because I wasn't sure whether it was at the stage that you'd like some outside eyeballs. But if you'd like me to add it, I'd be very happy to. No pressure either way.

[Amelia Livingston]

(whoops, deleted, I didn't check the above channel)

[Jack McKoen]

Emily Riehl said:

I've invited some golfing on some existing quasi-category theory code. I didn't put your work in progress on the list because I wasn't sure whether it was at the stage that you'd like some outside eyeballs.

My code is definitely not ready for golfing :sweat_smile: I am actively working on it, but thanks Emily

[Dean Young]

@Emily Riehl Thanks for this insight!

[Mario Carneiro]

For those following along: The "cat has colimits" PR series is now up at #16784 :tada:. The unblocked PRs are #16779, #16780, #16781

[Kim Morrison]

:peace_sign: :writing: