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 3 of 3
I am feeling a bit dense that I have trouble giving a formal proof of the following. Maybe someone can give me a nudge in the right direction.
A retract square of a pullback square is itself a pullback. Right? How to show this in the ∞-categorical context?
So here is what I am talking about in more detail: let S be the category with four objects and morphisms forming a square, so that functors S:S→D are precisely commuting square diagrams in D.
Consider a retract Id:S1→S2→S1 in the functor category [S,D]. If the square S2 is a pullback, then so should be S1. I want this statement for homotopy pullbacks / ∞-pullbacks.
This is easy with derivators. An object of D(S) is a pullback square iff it is in the image of r*:D(C)→D(S), where C is the walking cospan and r the inclusion. Since r* is a fully faithful right adjoint, this is equivalent to saying that the counit X→r*r*X is an isomorphism. But a retract of an isomorphism is also an isomorphism.
I expect one can say an up-to-homotopy version of this for ∞-categories.
Thanks, Mike! That’s very useful.
I have now added a discussion along these lines to retract.
I realize that I need to better include in my active repository of tools the fact that the (homotopy) limiting cone is equivalently the right Kan extension along the inclusion of the given diagram into its cone diagram.
1 to 3 of 3