Zulip Chat Archive
Stream: Is there code for X?
Topic: (infinity, 1)-categories
Andrea Bourque (Dec 19 2023 at 03:30):
What progress (if any) has been made towards infinity categories in Lean?
Kevin Buzzard (Dec 19 2023 at 05:29):
IIRC we have simplicial sets but nobody has needed infinity categories yet
Joseph Tooby-Smith (Dec 19 2023 at 13:24):
I am also interested in (infinity,1)-categories in lean.
Kevin Buzzard (Dec 19 2023 at 15:20):
I don't think there's any obstruction to making the quasicategory definition
Johan Commelin (Dec 19 2023 at 15:25):
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 (Dec 19 2023 at 16:07):
Pinging @Jack McKoen who is working on related things right now
Trebor Huang (Dec 20 2023 at 13:55):
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 (Dec 20 2023 at 14:08):
Several people have been working on WFS. I lost track of what the current status is...
Joël Riou (Dec 20 2023 at 18:05):
@Trebor Huang: the basic definitions of lifting properties are in mathlib (CategoryTheory.LiftingProperties
).
Trebor Huang (Dec 21 2023 at 04:46):
Ah, when I typed in "lifting" in the docs searchbar the suggestions are dominated by liftRing
so I thought there was none
Trebor Huang (Dec 21 2023 at 04:46):
Is this some search priority issue to be fixed?
Johan Commelin (Dec 30 2023 at 14:45):
The branch quasicat
now contains a sorry-free proof that the nerve of a category is a quasicategory.
Johan Commelin (Dec 30 2023 at 14:46):
It was a pretty nasty fight with DTT.
Adam Topaz (Dec 30 2023 at 15:09):
What about DTT made it tough? Maybe we should rethink the simplicial API?
Johan Commelin (Dec 30 2023 at 15:20):
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 (Dec 30 2023 at 15:24):
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 (Dec 30 2023 at 15:26):
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 (Dec 30 2023 at 15:31):
Maybe. I think @Joël Riou already wrote a very good API for ComposableArrows
Johan Commelin (Dec 30 2023 at 15:32):
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 eqToHom
s.
Johan Commelin (Dec 30 2023 at 15:32):
Anyway: #9357 is the first PR, containing the bare definitions of Kan complex and quasicategory.
Adam Topaz (Dec 30 2023 at 15:44):
Left a few comments
Adam Topaz (Dec 30 2023 at 15:46):
Let me ping @Jack McKoen again since he also had a def of a Kan complex on his branch
Johan Commelin (Dec 30 2023 at 15:49):
We should also write a delaborator for
scoped[Simplicial] notation "Λ[" n ", " i "]" => SSet.horn (n : ℕ) i
Adam Topaz (Dec 30 2023 at 15:51):
If we change notation
to notation3
does it make things better? I seem to recall @Kyle Miller saying something along those lines.
Johan Commelin (Dec 30 2023 at 16:03):
Thanks! That worked: #9358
Johan Commelin (Dec 30 2023 at 19:31):
#9360 provides an alternative hornfilling condition
Johan Commelin (Dec 30 2023 at 20:34):
#9362 adds some trivial prerequisites on cardinalities of explicit finsets.
Riccardo Brasca (Dec 30 2023 at 20:51):
I left a minicomment and delegated it.
Johan Commelin (Dec 30 2023 at 21:08):
Thanks
Johan Commelin (Dec 30 2023 at 21:08):
#9363 is the next one in line. But it depends on the finset-cardinalities PR.
Johan Commelin (Jan 01 2024 at 07:44):
#9357 basic definitions- #9360 alternative horn filling condition
#9362 bounds on cardinalities of explicit finsets- #9363 constructors for subsimplices of horns
Joseph Tooby-Smith (Jan 09 2024 at 19:14):
deleted message
Joseph Tooby-Smith (Jan 09 2024 at 19:18):
(Sorry ignore the above, I missed a comment above)
Joseph Tooby-Smith (Feb 14 2024 at 19:19):
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 (Feb 14 2024 at 19:23):
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 (Feb 14 2024 at 19:34):
@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 (Feb 14 2024 at 19:35):
I made an empty project here: https://github.com/orgs/leanprover-community/projects/18
Joseph Tooby-Smith (Feb 14 2024 at 19:36):
@Adam Topaz Thanks :)
Joseph Tooby-Smith (Feb 14 2024 at 19:42):
@Adam Topaz Could I possibly have write access for the project? Doesn't seem to let me edit it by default.
Adam Topaz (Feb 14 2024 at 19:43):
hmmm... I don't remember how to do that. Can another maintainer help out?
Adam Topaz (Feb 14 2024 at 19:44):
Oh ok I see how to do it now. What's your github username @Joseph Tooby-Smith ?
Joseph Tooby-Smith (Feb 14 2024 at 19:44):
jstoobysmith
Adam Topaz (Feb 14 2024 at 19:45):
you should have an invite in your inbox
Joseph Tooby-Smith (Feb 14 2024 at 19:47):
Yep that worked! Thanks @Adam Topaz
Dagur Asgeirsson (Feb 14 2024 at 21:02):
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 (Feb 14 2024 at 21:05):
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 (Feb 14 2024 at 21:06):
The current simplicial sets framework doesn’t make this easy
Joseph Tooby-Smith (Feb 14 2024 at 21:19):
@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 (Feb 14 2024 at 21:20):
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 (Feb 14 2024 at 21:21):
Kerodon tags are a great idea!
Matthew Ballard (Feb 14 2024 at 21:23):
Can the Kerodon tags be linkified?
Matthew Ballard (Feb 14 2024 at 21:30):
It doesn't appear so in any nice way from the UI :(
Dagur Asgeirsson (Feb 14 2024 at 21:31):
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 (Feb 14 2024 at 21:31):
@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 (Feb 14 2024 at 21:34):
Thanks!
It would make your life easier if you could make a template and access the fields as variables though
Jack McKoen (Feb 14 2024 at 22:06):
How can I "claim" one of these goals?
Matthew Ballard (Feb 14 2024 at 22:07):
Assign yourself?
Adam Topaz (Feb 14 2024 at 22:08):
@Jack McKoen you might need write access... if so, let me know.
Jack McKoen (Feb 14 2024 at 22:10):
I think I need write access (unless I just can't find the option on mobile)
Adam Topaz (Feb 14 2024 at 22:11):
you should have access now.
Jack McKoen (Feb 14 2024 at 22:12):
Thanks, works now
Dean Young (Feb 15 2024 at 07:31):
@Jack McKoen @Adam Topaz I'd like to mention that these efforts will help a lot with my work with Jiazhen Xia available here:
Is it ok if I lobby for a few things?
I think it is a good idea to use a certain four categories:
∞-Cat : Category quasicategory
∞-Grpd : Category Kan_complex
D(∞-Cat) : Category quasicategory
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 (Feb 15 2024 at 07:34):
Dean Young (Feb 15 2024 at 07:42):
@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 (Feb 15 2024 at 07:56):
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 (Feb 15 2024 at 11:59):
@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 (Feb 15 2024 at 12:11):
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 (Feb 15 2024 at 12:29):
@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 (Feb 15 2024 at 12:31):
Oh, I just noticed your second message with the user names. I'll add those now.
Jiazhen Xia (Feb 15 2024 at 12:45):
@Adam Topaz Thank you! We have access now, and we are excited to work on 11 and 12 (space of morphisms).
Johan Commelin (Feb 15 2024 at 12:54):
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 (Feb 15 2024 at 16:34):
@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 (Sep 03 2024 at 18:25):
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 (Sep 03 2024 at 18:28):
Ping @Jack McKoen :up:
Dagur Asgeirsson (Sep 03 2024 at 18:28):
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 (Sep 03 2024 at 18:29):
All those eqToHom
s make me sad
Johan Commelin (Sep 03 2024 at 18:33):
FYI, I did merge today's master into the branch. So no need to do awkward bumping
Johan Commelin (Sep 03 2024 at 18:34):
The eqToHom
s make me sad. But they are not the worst part. :see_no_evil:
Emily Riehl (Sep 04 2024 at 13:40):
@Johan Commelin what would you say the worst part is?
Emily Riehl (Sep 04 2024 at 13:46):
@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 (Sep 04 2024 at 13:47):
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 (Sep 04 2024 at 13:50):
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 (Sep 04 2024 at 13:58):
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 (Sep 04 2024 at 17:08):
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 (Sep 04 2024 at 17:10):
Emily Riehl said:
Johan Commelin what would you say the worst part is?
filler_succ_aux
is pretty terrible
Johan Commelin (Sep 04 2024 at 17:11):
And when you need a doubly-primed name, that's also a bit of a smell that something isn't optimal
Emily Riehl (Sep 04 2024 at 22:12):
@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 (Sep 04 2024 at 22:18):
@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 (Sep 04 2024 at 22:35):
@Emily Riehl The stuff I did on 1-simplies can be found here:
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:
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 (Sep 05 2024 at 18:00):
@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 (Sep 05 2024 at 19:23):
@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 (Sep 07 2024 at 18:11):
@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 (Sep 08 2024 at 21:25):
@Dean Young is "I" something special here?
Dean Young (Sep 08 2024 at 21:39):
@Emily Riehl Sorry, meant Δ¹!
Emily Riehl (Sep 08 2024 at 22:44):
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 (Sep 08 2024 at 22:46):
@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 (Sep 09 2024 at 09:33):
@Emily Riehl That seems like a great idea! I'd be fine with this.
Emily Riehl (Sep 09 2024 at 16:59):
There is a new channel open to discuss this project here: #Infinity-Cosmos
Emily Riehl (Sep 09 2024 at 17:49):
@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 (Sep 09 2024 at 20:31):
(whoops, deleted, I didn't check the above channel)
Jack McKoen (Sep 09 2024 at 21:04):
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 (Sep 09 2024 at 22:11):
@Emily Riehl Thanks for this insight!
Mario Carneiro (Sep 13 2024 at 21:05):
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 (Sep 14 2024 at 02:45):
:peace_sign: :writing:
Last updated: May 02 2025 at 03:31 UTC