« first day (2761 days earlier)      last day (642 days later) » 

Bryan Shih
Bryan Shih
6:20 AM
@DustinClausen Thanks, this explained it!
 
 
11 hours later…
Dedalus
Dedalus
5:11 PM
Suppose I have a functor f: C \to D of infinity categories and let p: E \to \Delta^1 be the associated cocartesian fibration. Suppose that p is bicartesian, so that f has an adjoint g: D \to C. I have seen the claim that the precomposition with a cartesian edge s_Z: g(z) \to z, z \in C = E_0 factors through the functor g. More precisely, precomposition with
s_Z defines a map map_{E_1}(z,w) \to map_E(g(z),w)). I have seen the claim that this is homotopic to:
map_{E_1}(z,w) \to map_{E_0}(g(z),g(w)) = map_E(g(z),g(w)) \to map_E(g(z),w) where the last map is postcomposition with s_w: g(w) \to w…
Obviously, this is some naturality property that is being stated about mapping spaces. So I think that choosing cartesian edges gives me a map E_1 \times \Delta^1 \to E where the restriction to 0 is g, and the restriction to 1 is the inclusion.
So this gives us some sort of natural transformation, and I would then expect this to follow from some properties of mapping spaces
But I can't seem to nail it down.
 
 
3 hours later…
Dedalus
Dedalus
8:34 PM
Here is another instance where something similar seems to be said dropbox.com/s/22b0yns1qls4xkw/… on pg. 16
A diagram is claimed to be homotopy commutative. Why?
 
Denis Nardin
Denis Nardin
9:03 PM
@Dedalus In HTT this is the definition of an adjunction. To see how it relates to the classical notion, maybe my answer here is helpful?
 
Dedalus
Dedalus
@DenisNardin Thanks, I will read it. This point has been bugging me all day.
@DenisNardin I am a bit confused, what do you mean by the pullback of the right bottom corner? Pullback along what? (This is referring to your answer)
 
Denis Nardin
Denis Nardin
I mean the pullback of the fragment of the diagram given by the left vertical arrow and the bottom horizontal arrow
 
Dedalus
Dedalus
Of course, thanks.
 
Rune Haugseng
Rune Haugseng
9:21 PM
@Dedalus If you unwind how the functor g is obtained from the fibration you should get that the morphism map_{E_1}(z,w) \to map_{E_0}(g(z),g(w)) is exactly given by composing with the cartesian morphism g(z) -> z and then inverting the equivalence map(gz, gw) -> map(gz, w) given by composition with the cartesian morphism gw -> w.
 
Dedalus
Dedalus
9:53 PM
@RuneHaugseng Thanks, this was very helpful. I think the following is then the correct explanation: The functor g is constructed by taking a lift of the cartesian fibration, giving a natural transformation E_1 \times \Delta^1 \to E, where the restriction to 0 is g.
Then we can use the map (E_1 \times \Delta^1)^{op}) \times (E_1 \times \Delta^1) \to E^{op} \times E together with the mapping space functor
map_E(-,-) to get a nice square, and this should give me everything I want. Does this seem correct to you? :-)
 

« first day (2761 days earlier)      last day (642 days later) »