I'm trying to use this comment that @Denis-CharlesCisinski made a while back about how the fat join ♦ allows me to think of Fun(X,C/c) as Fun_c(X♦{0},C) and that an object of this last thing really is honestly the same data as a natural transformation from a functor out of X to the constant functor at c. I.e. Fun_c(X♦{0},C)≃Fun(X,C)/const(c).

And I can't tell if there's actually anything to prove??

Doesn't look like it to me

except for the fact that the fat join and the (skinny?) join are equivalent

But I'm sure someone else can point out a subtlety about that last point if one exists

Yeah I guess I was hoping there would be a really explicit equivalence of simplicial sets Fun_c(X♦{0},C)→{some kind of slice in the functor category}

Again I guess this is all sort of obvious. But it's mostly "obvious" to me because I'm drawing pictures in my brain, which aren't really all that trustworthy.

Ah yes, if you're looking for something very explicit then the model you use for the join might matter

Like by playing around with the definitions you get two different things. On one hand you have maps of simplicial sets $(\Delta^n\Diamond \Delta^0)\times X\to C$ that have to take $X\times \Delta^0\subset (\Delta^n\Diamond \Delta^0)\times X$ to a single object $c$. On the other hand you get maps $(X\Diamond\Delta^0)\times \Delta^n\to C$ that have to do something like takes $(\Delta^n\times\Delta^0)\subset \Delta^n\times(X\Diamond\Delta^0)$ to $c$. I think...

Well, two different things for what the $n$-simplices of each of these categories are, that is.

Mapping in a simplicial set K you get for Fun(X,C/c) the same thing as maps (K x X) ^\triangleright taking the cone point to c, i.e. maps out of K x X x Delta^1 that take K x X x {1} to c, while for Fun(X,C)/const(c) you get maps K^\triangleright x X that take {cone point} x X to c, ie.e. maps out of (K x Delta^1) x X that take (K x {1}) x X to c. And those are the same.

If I have an adjunction of infinity-categories, I get a unit and a counit map. Am I correct in thinking that to prove that these two maps satisfy the triangle identities, one can, with some extremely minor changes, just copy the proof given here? en.wikipedia.org/wiki/…

Basically, just replace the requirement that morphisms are equal with the conditions that the morphisms are homotopic.

@Dedalus There are actually interesting questions related to what it "means" to give an adjunction of oo-categories, and so the deduction of the triangle identities will depend on your chosen definition.

I see. Let us say that an adjunction is a bicartesian fibration over \Delta^1, then. Then we can lift to get unit / counit maps.

@Dedalus Yes, but you need to be careful. In 1-category land it is enough to show that the diagram commutes, in ∞-categroy land you have to provide a 2-cell which varies naturally in the source (i.e. a functor C×Δ²→D), so you cannot just do it pointwise

@DenisNardin Thanks. Yes, that is a subtle but important point. I think one should be able to proceed by using naturality properties of mapping spaces?

Yes, indeed. One just has to be careful about it :)

Hi @BryanShih, I don't understand your first confusion. [26, Cor 6] exactly says that if an infinite direct sum of copies of M_r has vanishing lim^1 then M_r is Mittag-Leffler.

For 2.21 A, you're right the Postnikov section is unnecessary there. For 2.21 B, the problem with the sketch you give is that a map of spectra can be nonzero even if it induces 0 on all homotopy groups, e.g. consider the map HF_p ---> HF_p[1] classifying the short exact sequence F_p --> Z/p^2 --> F_p. That's why we run the Postnikov argument there

@RuneHaugseng Thanks Rune, that's helpful. Would it be incorrect to make this rigorous by representing the join $X\Diamond \Delta^0$ as a pushout, then crossing the whole diagram with K and saying something like crossing with $K$ preserves the pushout because one leg of the pushout, $X\times\Delta^0\times\Delta^1\to X$ is an equivalence?

*unnecessarily rigorous probably

@JonathanBeardsley If you're working with simplicial sets then products always commute with pushouts

(That map isn't an equivalence, but one leg of the pushouts is a monomorphism, so that they are homotopy pushouts.)

@RuneHaugseng Oh the map I wrote down isn't an equivalence?

I thought it was just the projection onto one end of the cylinder on X?

@RuneHaugseng ah right of course, because products are the tensor product here

I think I've been drawing the wrong diagram for the definition of the join...

Oh.... hm maybe here's a more elegant way to see this. We can define $C/c$ as a comma object, i.e. a homotopy pullback in $(\infty,2)$-categories I think, and then by applying $Fun(X,-)$ to this diagram and using the fact that this functor preserves pullbacks we get a new pullback diagram, but that diagram is exactly the one defining the comma object $Fun(X,C)_{/const(c)}$ I think?

Oh gosh, the thing I wanted to say earlier, that "cones over f are equivalent to natural transformations from f to constant functors" is literally the definition of "cones over f" in Riehl and Verity's work.

Yeah, seems like the thing I want to say is even MORE trivial in Riehl and Verity's framework.

I will be giving a course this spring on chromatic homotopy theory, starting next week, with the idea to put more focus on the algebra of formal groups. It might be possible to audit this course, so if you know someone who might be interested please encourage them to contact me directly.

@JonathanBeardsley The pullback defining the comma object is just what the pushout defining the join turns into when you map out of it, so it's really the same argument

@RuneHaugseng Yeah, I'm starting to see that.