Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 25 of 25
The second part of HTT Proposition 2.2.1.1 gives a certain functoriality property of the straightening functor with respect to left Kan extensions.
Here’s what Lurie said in an e-mail earlier today:
If is a simplicial category and is a simplicial functor, let denote the simplicial category obtained from by adjoining a new object , with , , and empty for in .
has the following universal property: to give a (simplicial) functor , you need to give a functor , and object in (which will be the image of ), and a natural transformation of functors .
From this universal property, you conclude that given a functor , you have a pushout square
So this resolves part of the problem, but in general, the category (in the definition of the straightening functor) is not exactly . Suppose we call the map , and we let where is the distinguished vertex. Then we have a factorization . Lurie’s email says that the big pushout factors as a pair of pushout squares, the pushout from the e-mail: juxtaposed with the pushout square .
That is, there seems to be a small bit more to prove. Presumably it suffices to show that the new object satisfies the universal property, but I’m not sure how to do that.
By Yoneda reduction, it suffices to show that where is the canonical map, and is the other canonical map.
(There may be a bunch of places where I forgot to put opposite categories. I have faith that you’ll figure it out!
Hi Harry,
I think it is great that you invest this energy into sorting these things out.
I’d be willing to help, even though have absolutely no time for it, but as a means for procrastinating what I really need to do.
But it is a bit hard for us to jump right into some nitty-gritty details of your technical discussion with Jacob Lurie. For instance I am not sure from the above what the remaining question is that you would like to have answered.
For instance that juxtaposition/pasting of two pushout squares. I trust you know that this implies on general grounds that the outer rectangle is itself again a pushout? Or is this the question?
Sorry, this must be frustrating for you, who has been concentrating on this, but: what exactly is your question now? :-)
The question is, why is (where and are the natural pushout maps) exactly the left Kan extension of along where is the induced map?
Notce that could reasonably be called for some , , and . The problem presented in my first post is a simplification of that case, but if need be, I can write out everything, including the definition, and then re-ask the question.
An affirmative answer to this question would resolve the problem above.
I’ll paste it here:
Let be a topos (a presheaf topos if necessary), and let , , and be -categories. Suppose is a strictly injective (on objects) and fully faithful -functor in the sense that it induces isomorphisms on Hom-objects.
Let be any -functor, and let be the strict pushout of along .
Is necessarily strictly injective (on objects) and fully faithful (in the sense above)?
The above conclusion holds in the face of the lemma above because the map is strictly injective and fully faithful, so its pushouts ( and ) are strictly injective and fully faithful, which implies that is an isomorphism of functors since is an isomorphism, as is .
This does not depend on the stuff from Lurie’s e-mail.
Mike and David, how do you compute the hom-spaces in the pushout V-category?
I don’t have time to write it out carefully, but just think about what the pushout would look like in Set-enrichment (all the morphisms in the categories being pushed out give you new ones, and then you have to throw in relatively free composites as necessary) and write that as a coend.
Mike, if you know of a reference that explains the pushout of V-categories (also ordinary categories), I would really appreciate it. Pushouts of categories are kinda mysterious to me.
All I know is that it’s like the amalgamation product of groups, but like a hundred times worse.
There might be something in Wolff’s paper “V-Cat and V-Graph”. But I really encourage you to just sit down and force yourself to figure out what it has to be.
if you know of a reference that explains the pushout of V-categories (also ordinary categories), I would really appreciate it.
This one here considers almost the situation you are looking at, but not quite,
Macdonald, Scull, Amalgamations of categories.
Urs, very nice! Not only that, but the paper in question confirmed exactly my suspicions on the necessary property (2-for 3) when I was toying around with it.
@Harry,
Notice that their counterexample is not of the form that you are considering (neither of their functors they are pushing out are fully faithful), so that you aren’t necessarily back to square one. You may be able to come up with a counterexample to your question, but if not, here are some ideas to check:
The results holds if and only the three following cases hold ( in this order):
I’ve made a random guess that your has epi-mono factorisation, to get the first two steps (instead of just is the identity on objects). Full here means is an epi in . Maybe check some of these for …
See also page 20 of this talk by Pronk.
I’m done with this problem, since the general thing that would resolve this is a pain in the butt, and I found a way to do it that will work.
Also, I just realized that Lurie’s comment resolves everything in one go, since I just realized now that the simplicial category is precisely where is some simplicial functor (dependent on the magic of , which is extremely annoying to describe explicitly but arises from a bar construction on the free category comonad restricted to then extended by the universal property of presheaves) , which resolves everything by an appeal to composition of adjoints in a certain way.
If you care about the formal proof, I have it written down.
Thanks for all the help, guys! I really appreciate it.
I’ll leave the question regarding the general case on mathoverflow open if anyone wants to give a proof at some point in the future (sometimes Todd likes to do this, and he reprimanded me for deleting other questions like this).
Here’s the proof:
First, let’s prove Lurie’s claim formally:
Let be any simplicial functor, and let be the simplicial category with objects consisting of the objects of and an extra object such that and for all , and such that . Let be the evident full and faithful embedding.
Then suppose we’re given a functor . Then a cone for the diagram consists of the following data: A simplicial category and a pair of simplicial functors and making the evident diagram commute.
Now, the functor consists of a functor , an object , and a natural transformation . However, it is clear from the definitions that , and therefore, we have a natural transformation , but this corresponds under the adjunction to a natural transformation .
So a cone on this diagram is identical to the data of a functor , an object , an extension such that , and a morphism of functors .
Then certainly if there exists a simplicial category with a distinguished object and a functor such that , it would be universal, but if we let , we’re done. Hooray!
Next, we show that for any simplicial set , for the simplicial functor .
Let be the class of simplicial sets for which the claim holds. Clearly is stable under isomorphisms, disjoint unions, and given a span is of the form with with the map monic, then the pushout is in (clear). It is left as an exercise to show that it is stable under (countable) sequential colimits of monomorphisms (this is easy).
Then it suffices to show that it holds for simplices, but this is immediately clear by the construction of .
(The part where I wrote (clear) is a part that I don’t actually know how to finish without computing the pushout. Is there an easier way to prove this? The whole part is geometrically obvious because the cone point is absolutely terminal in the simplicial set (the only edge such that is the cone point is degenerate).
But then we’re done, since in particular, given any and any , we have that:
Given any functor , then it follows from the first lemma that the pushout is precisely
(The part where I wrote (clear) is a part that I don’t actually know how to finish without computing the pushout. Is there an easier way to prove this?
It seems to me to be sufficient to observe that the pushout is by definition of . Because the pushout is clearly a category of the form and is defined to be that .
I have included your discussion of the proof into the the Lab page (infinity,1)-Grothendieck construction in the section For fibrations in oo-groupoids – model category presentation.
Dear Urs, the trouble is the following:
We must verify that is where for the cone point and where for being the canonical inclusion. To show this, it is enough to show the following: for all , that , and that for all .
I was trying to prove the statement by proving it for generators then proving stability under the usual things to show that .
The second two parts are sort of obviously true (there are no nondegenerate edges issuing from the cone point), but the first part, that the embedding is full and faithful is not obvious to me for general simplicial sets.
The second two parts are sort of obviously true
But then the first should be, too: is obtained from gluing cells, . So in there are extra morphisms to the new vertex point glued in, but no non-degenearate new morphism and no nontrivial composites with the new morphisms go from objects in to objects in . For they had to pass through the new object, but out of that is no nontrivial morphism.
Sure, it’s intuitively true, but I want to construct the following isomorphisms formally:
for all . I can see why it’s true, but I’m totally baffled regarding how to actually show it. For some reason, it’s very hard to manipulate the hom-objects in in terms of the simplices of . Sure, we have the coend formula, but that doesn’t tll us anything concrete about the hom-objects, which are a priori extremely complicated because colimits in are poorly behaved (they involve lots of crazy free composites).
I e-mailed Lurie, and he gave a very pretty proof:
Let be the terminal map, then this gives a map , but this becomes a map However, is empty, so this proves one of the claims.
The other claims follow by looking at the fibres over and .
More generally, this proof can be adapted to show that is a full and faithful embedding.
they involve lots of crazy free composites
But never one involving the new vertex, if that is not the codomain. So crazy as they may be, they are the same on both sides.
But if you have a proof now that satisfies you, all the better!
@Urs:
But never one involving the new vertex, if that is not the codomain. So crazy as they may be, they are the same on both sides.
Sure, but there’s a difference between a formal proof and knowing why the formal proof works. What you said is the reason why the proof works, but it’s not a proof. A full proof exhibits the isomorphisms without handwaving!
However, have you ever done the explicit construction of the unstraightening functor?
I just verified it, and I’ll put it on the lab page later:
Let be a simplicial functor. Then consider the diagram:
where is the vertex classifying the distinguished point on . Then the limit of this diagram is the simplicial set over called .
Interestingly enough, I think this implies that the unstraightening of a simplicial functor is always contravariantly fibrant.
The straightening and unstraightening functors are really elegant now that I look. There are some very subtle points about them that make things seem harder than they are.
In particular, straightening and unstraightening are the composite of three separate adjunctions.
I should also note that the explicit form of the unstraightening functor is quite literally a million times easier to compute with.
I just verified it, and I’ll put it on the lab page later:
You should really do that, if you have not already.
Wow, Harry is becoming quite a specialist.
I realize this thread is essentially finished but thought that participants might like to know about recent work of Dugger and Spivak which makes the simplicial categories much easier to compute. Explicitly, they characterize -simplices in as necklaces in from to , that is joins of the standard simplices which we call “beads” (where we identify the final vertex of a simplex with the initial vertex of the next) where the initial vertex of the entire necklace is and the final one is , together with some vertex data which determines the faces of the -simplex. I’ve found this description quite amenable to calculation. No colimits in simplicial categories required!
In particular it’s immediate that -simplices in are exactly -simplices in since the distinguished vertex only makes an appearance as the final vertex in a non-degenerate simplex of . Similarly, -simplices in are exactly necklaces all but the last bead of which land in and whose final bead can be thought of as a simplex of one dimension lower in .
The original paper is quite readable and has some other good stuff besides, but if you just want a quick introduction to the necklace characterization of hom-spaces in the simplicial categories associated to simplicial sets, I summarize their work in a just a couple pages in the second section of this paper.
1 to 25 of 25