Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes science set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2018

    this evident concept maybe deserves an entry of its own, for ease of linking.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2018

    So the main point is to say that the right derived functor of a right Quillen functor is identified with the left derived functor of a left Quillen functor.

    It is immediate to say this a) on the level of homotopy categories and b) on the level of Kan-complex enriched simplicial localizations. Is there an intermediate, more purely model-category-theoretic way to express this?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJul 11th 2018

    Perhaps with the derived natural transformations of this paper?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2018

    These derived natural transformation go between (images under some derived Quillen functor of) left Quillen functors, right (p. 8)? The issue with the adjoint triples is to identify a left Quillen functor with a right Quillen functor, after deriving.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJul 11th 2018

    The ones on p8 do, but the more general ones on p20 live in a square composed of two left Quillen functors and two right Quillen functors (some of which could be identities).

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2018

    Now I see, thanks. That looks like what I’d need, yes.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJul 12th 2018

    okay, so in the double category of model categories, the “Quillen adjoint triple” for homotopy limit/colimit is incarnated by the diagram

    [𝒞 op,sSet Qu] proj AAidAA [𝒞 op,sSet Qu] proj lim η id [𝒞 op,sSet Qu] inj AlimA sSet Qu AconstA [𝒞 op,sSet Qu] proj id ε const id id [𝒞 op,sSet Qu] inj AAidAA [𝒞 op,sSet Qu] inj AAidAA [𝒞 op,sSet Qu] inj \array{ && [\mathcal{C}^{op}, sSet_{Qu}]_{proj} &\overset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& [\mathcal{C}^{op}, sSet_{Qu}]_{proj} \\ && {}^{\mathllap{ \underset{\longrightarrow}{\lim} }}\Big\downarrow &{}^{\mathllap{\eta}}\swArrow& \Big\downarrow{}^{\mathrlap{id}} \\ [\mathcal{C}^{op}, sSet_{Qu}]_{inj} &\overset{ \phantom{A}\underset{\longleftarrow}{\lim}\phantom{A} }{\longrightarrow}& sSet_{Qu} &\overset{\phantom{A}const\phantom{A}}{\longrightarrow}& [\mathcal{C}^{op}, sSet_{Qu}]_{proj} \\ {}^{\mathllap{ id }}\Big\downarrow & {}^{\mathllap{\epsilon}}\swArrow & {}^{\mathllap{const}} \big\downarrow &\swArrow_{\mathrlap{id}}& \big\downarrow{}^{ \mathrlap{ id } } \\ [\mathcal{C}^{op}, sSet_{Qu}]_{inj} &\underset{\phantom{AA}id\phantom{AA}}{\longrightarrow}& [\mathcal{C}^{op}, sSet_{Qu}]_{inj} &\underset{\phantom{AA}id\phantom{AA}}{\longrightarrow}& [\mathcal{C}^{op}, sSet_{Qu}]_{inj} }

    maybe that kind of diagram could be taken as the general definition of “Quillen adjoint triple”.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJul 12th 2018

    I have made that the definiton, and spelled out the Example of the Quillen adjoint quadruple over a site with terminal object:


    Let 𝒞 1,𝒞 2,𝒟\mathcal{C}_1, \mathcal{C}_2, \mathcal{D} be model categories, where 𝒞 1\mathcal{C}_1 and 𝒞 2\mathcal{C}_2 share the same underlying category 𝒞\mathcal{C}, and such that the identity functor on 𝒞\mathcal{C} constitutes a Quillen equivalence

    𝒞 2 Qu QuAAidAAAAidAA𝒞 1 \mathcal{C}_2 \underoverset {\underset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}} {\overset{ \phantom{AA}id\phantom{AA} }{\longleftarrow}} {{}_{\phantom{Qu}}\bot_{Qu}} \mathcal{C}_1

    Then

    1. a Quillen adjoint triple of the form

      𝒞 1/2 Qu QuL Qu QuC AARAA 𝒟 \mathcal{C}_{1/2} \array{ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{L}{\longrightarrow} \\ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{C}{\longleftarrow} \\ \overset{\phantom{AA}R\phantom{AA}}{\longrightarrow} \\ } \mathcal{D}

      is a diagram in the double category of model categories of the form

      𝒞 1 AAidAA 𝒞 2 L η id 𝒞 2 ARA 𝒟 ACA 𝒞 1 id ε C id id 𝒞 2 AAidAA 𝒞 2 AAidAA 𝒞 2 \array{ && \mathcal{C}_1 &\overset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& \mathcal{C}_2 \\ && {}^{\mathllap{ L }}\Big\downarrow &{}^{\mathllap{\eta}}\swArrow& \Big\downarrow{}^{\mathrlap{id}} \\ \mathcal{C}_2 &\overset{ \phantom{A}R\phantom{A} }{\longrightarrow}& \mathcal{D} &\overset{\phantom{A}C\phantom{A}}{\longrightarrow}& \mathcal{C}_1 \\ {}^{\mathllap{ id }}\Big\downarrow & {}^{\mathllap{\epsilon}}\swArrow & {}^{\mathllap{C}} \big\downarrow &\swArrow_{\mathrlap{id}}& \big\downarrow{}^{ \mathrlap{ id } } \\ \mathcal{C}_2 &\underset{\phantom{AA}id\phantom{AA}}{\longrightarrow}& \mathcal{C}_2 &\underset{\phantom{AA}id\phantom{AA}}{\longrightarrow}& \mathcal{C}_2 }

      such that η\eta is the unit of an adjunction and ε\epsilon the counit of an adjunction, thus exhibiting Quillen adjunctions

      𝒞 1 Qu QuCL𝒟 𝒞 2 Qu QuRC𝒟 \array{ \mathcal{C}_1 \underoverset {\underset{C}{\longleftarrow}} {\overset{L}{\longrightarrow}} {{}_{\phantom{Qu}}\bot_{Qu}} \mathcal{D} \\ \\ \mathcal{C}_2 \underoverset {\underset{R}{\longrightarrow}} {\overset{C}{\longleftarrow}} {{}_{\phantom{Qu}}\bot_{Qu}} \mathcal{D} }
    2. a Quillen adjoint triple of the form

      𝒞 1/2 Qu QuL Qu QuC AARAA 𝒟 \mathcal{C}_{1/2} \array{ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{L}{\longleftarrow} \\ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{C}{\longrightarrow} \\ \overset{\phantom{AA}R\phantom{AA}}{\longleftarrow} \\ } \mathcal{D}

      is a diagram in the double category of model categories of the form

      𝒞 2 AAidAA 𝒞 1 AAidAA 𝒞 1 id id C ε id 𝒞 2 ACA 𝒟 R 𝒞 1 id ε L 𝒞 2 AAidAA 𝒞 2 \array{ \mathcal{C}_2 &\overset{ \phantom{AA} id \phantom{AA} }{\longrightarrow}& \mathcal{C}_1 &\overset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& \mathcal{C}_1 \\ {}^{\mathllap{id}} \Big\downarrow &{}^{ \mathllap{ id } }\swArrow& \Big\downarrow{}^{ \mathrlap{ C } } & {}^{ \mathllap{\epsilon} }\swArrow & \Big\downarrow{}^{\mathrlap{id}} \\ \mathcal{C}_2 &\underset{ \phantom{A}C\phantom{A} }{\longrightarrow}& \mathcal{D} &\underset{R}{\longrightarrow}& \mathcal{C}_1 \\ {}^{\mathllap{id}}\Big\downarrow &{}^{\mathllap{ \epsilon }}\swArrow& \Big\downarrow{}^{\mathrlap{L}} \\ \mathcal{C}_2 &\underset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& \mathcal{C}_2 }

      such that η\eta is the unit of an adjunction and ε\epsilon the counit of an adjunction, thus exhibiting Quillen adjunctions

      𝒞 2 Qu QuCL𝒟 𝒞 1 Qu QuRC𝒟 \array{ \mathcal{C}_2 \underoverset {\underset{C}{\longrightarrow}} {\overset{L}{\longleftarrow}} {{}_{\phantom{Qu}}\bot_{Qu}} \mathcal{D} \\ \\ \mathcal{C}_1 \underoverset {\underset{R}{\longleftarrow}} {\overset{C}{\longrightarrow}} {{}_{\phantom{Qu}}\bot_{Qu}} \mathcal{D} }

    If a Quillen adjoint triple of the first kind overlaps with one of the second kind

    𝒞 1/2 Qu QuL 1=A a Qu QuC 1=L 2 Qu QuR 1=C 2 A a=R 2 𝒟 \mathcal{C}_{1/2} \array{ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{L_1 \phantom{= A_a}}{\longrightarrow} \\ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{C_1 = L_2}{\longleftarrow} \\ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{R_1 = C_2}{\longrightarrow} \\ \overset{\phantom{A_a = } R_2}{\longleftarrow} \\ } \mathcal{D}

    we speak of a Quillen adjoint quadruple, and so forth.

    diff, v6, current

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJul 12th 2018

    That doesn’t seem like enough: don’t you also need to require that the derived transformation of your square idid is an isomorphism?

    Also there doesn’t seem to be any point to including the unit and counit in your “diagram” (which is not even a composable diagram in the double category). So if this is what you want, I would phrase it as “two Quillen adjunctions

    𝒞 1 Qu QuCL𝒟 𝒞 2 Qu QuRC𝒟 \array{ \mathcal{C}_1 \underoverset {\underset{C}{\longleftarrow}} {\overset{L}{\longrightarrow}} {{}_{\phantom{Qu}}\bot_{Qu}} \mathcal{D} \\ \\ \mathcal{C}_2 \underoverset {\underset{R}{\longrightarrow}} {\overset{C}{\longleftarrow}} {{}_{\phantom{Qu}}\bot_{Qu}} \mathcal{D} }

    such that the derived natural transformation of that square idid is an isomorphism.”

    But it’s not really any harder to allow 𝒟\mathcal{D} to have two model structures as well, is it? And even to allow the underlying categories to be different and the Quillen equivalence to be a nonidentity adjunction?

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJul 12th 2018
    • (edited Jul 12th 2018)

    you also need to require that the derived transformation of your square idid is an isomorphism

    Sure, thanks, forgot the most important bit in all the editing. Fixed now. Also added check that this is the case in the two examples.

    there doesn’t seem to be any point to including the unit and counit in your “diagram” (which is not even a composable diagram in the double category).

    I enjoyed how the double category 2-cells allow me to display the structure involved in a “Quillen triple” as one single connected diagram (could we call it a “pasting diagram in the double category”), that’s what I tried to bring out. But the alternative that you suggest follows right after, after “thus exhibiting”.

    it’s not really any harder to allow 𝒟\mathcal{D} to have two model structures as well, is it? And even to allow the underlying categories to be different and the Quillen equivalence to be a nonidentity adjunction?

    That’s what I had initially. But the special case seems really neat, with the “2-cells with adjacent 1-identities” for the unit/counit being accompanied exactly by the remaining possible “2-cells with adjacent 1-identities” exhibiting the gluing of the two Quillen adjunction.

    This feels like it really deserves to be called “Quillen adjoint triple”. The more general version might rather go by “derivable adjoint triple” or the like.(?)

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJul 13th 2018

    No, I don’t think you could call it a pasting diagram in a double category, because it’s not composable. It wouldn’t even be a composable diagram in a 2-category. I think the more concise definition is much easier to understand than a big diagram, but YMMV I guess. I also think it obscures what’s going on, rather than being neat, to focus on the special case when certain functors happen to be identities.

    Regarding naming, one criterion of sensibility is that there ought to be a theorem like “any adjoint triple between locally presentable (,1)(\infty,1)-categories can be presented by some Quillen adjoint triple”. Is that true for the more restricted version? For that matter, is it true for the more general version?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJul 13th 2018
    • (edited Jul 13th 2018)

    “any adjoint triple between locally presentable (,1)(\infty,1)-categories can be presented by some Quillen adjoint triple”. Is that true for the more restricted version? For that matter, is it true for the more general version?

    Yeah, I was wondering, too, that’s what one should know.

    I suppose adjoint triples of left/right Kan extension between Bousfield localizations of simplicial presheaves will also fit the strict definition, by direct generalization of the limit/colimit example. That probably exhausts the class of examples of adjoint triples of presentable \infty-categories that I know of.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJul 13th 2018

    made explicit the example of left/right homotopy Kan extension (here)

    diff, v9, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJul 13th 2018
    • (edited Jul 13th 2018)

    made explicit the Quillen adjoint quadruple of homotopy Kan extension of simplicial presheaves along an adjoint pair of functors (here)

    diff, v10, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJul 13th 2018
    • (edited Jul 13th 2018)

    For what it’s worth, the restriction to changing the model structure only on one of the two sides also goes along well with the examples of “\infty-solid sites”

    *AAevenAA AAι infAA AAΠAA ADiscACartSpAAevenAA AAι infAA AAΠ infAA ADiscAFormalCartSpAAevenAA AAι supAA AAΠ supAA ADiscASuperFormalCartSp \ast \array{ \phantom{\underoverset{\bot}{\phantom{AA}even\phantom{AA}}{\longleftarrow}} \\ \phantom{\underoverset{\bot}{\phantom{AA}\iota_{inf}\phantom{AA}}{\hookrightarrow}} \\ \underoverset{\bot}{\phantom{AA}\Pi\phantom{AA}}{\longleftarrow} \\ \underoverset{}{\phantom{A}Disc\phantom{A}}{\hookrightarrow} } CartSp \array{ \phantom{\underoverset{\bot}{\phantom{AA}even\phantom{AA}}{\longleftarrow}} \\ \underoverset{\bot}{\phantom{AA}\iota_{inf}\phantom{AA}}{\hookrightarrow} \\ \underoverset{}{\phantom{AA}\Pi_{inf}\phantom{AA}}{\longleftarrow} \\ \phantom{\underoverset{}{\phantom{A}Disc\phantom{A}}{\hookrightarrow}} } FormalCartSp \array{ \underoverset{\bot}{\phantom{AA}even\phantom{AA}}{\longleftarrow} \\ \underoverset{\bot}{\phantom{AA}\iota_{sup}\phantom{AA}}{\hookrightarrow} \\ \underoverset{}{\phantom{AA}\Pi_{sup}\phantom{AA}}{\longleftarrow} \\ \phantom{\underoverset{}{\phantom{A}Disc\phantom{A}}{\hookrightarrow}} } SuperFormalCartSp

    This induces a progression of Quillen adjoint quadruples of the form

    sSet Qu Qu Queven Qu Quι inf Qu QuΠ Qu QuDisc Qu QuΓ coDisc[CartSp op,sSet Qu] proj/inj Qu Queven Qu Quι inf Qu QuΠ inf Qu QuDisc inf Qu QuΓ inf coDisc[FormalCartSp op,sSet Qu] proj Qu Queven Qu Quι sup Qu QuΠ sup Qu QuDisc sup Qu QuΓ sup coDisc[SuperFormalCartSp op,sSet Qu] proj/inj sSet_{Qu} \;\; \array{ \phantom{\underoverset{\phantom{{}_{Qu}}\bot_{Qu} }{ even }{\longleftarrow}} \\ \phantom{\underoverset{ \phantom{{}_{Qu}}\bot_{Qu} }{ \iota_{inf} }{\hookrightarrow}} \\ \underoverset{\phantom{{}_{Qu}}\bot_{Qu} }{ \Pi }{\longleftarrow} \\ \underoverset{ \phantom{{}_{Qu}}\bot_{Qu} }{ Disc }{\hookrightarrow} \\ \underoverset{ \phantom{{}_{Qu}}\bot_{Qu} }{ \Gamma }{\longleftarrow} \\ \overset{ coDisc }{\hookrightarrow} } \;\; [CartSp^{op}, sSet_{Qu}]_{proj/inj} \;\; \array{ \phantom{\underoverset{\phantom{{}_{Qu}}\bot_{Qu} }{ even }{\longleftarrow}} \\ \underoverset{ \phantom{{}_{Qu}}\bot_{Qu} }{ \iota_{inf} }{\hookrightarrow} \\ \underoverset{\phantom{{}_{Qu}}\bot_{Qu} }{ \Pi_{inf} }{\longleftarrow} \\ \underoverset{ \phantom{{}_{Qu}}\bot_{Qu} }{ Disc_{inf} }{\hookrightarrow} \\ \underoverset{ \phantom{\phantom{{}_{Qu}}\bot_{Qu}} }{ \Gamma_{inf} }{\longleftarrow} \\ \phantom{\overset{ coDisc }{\longrightarrow}} } \;\; [FormalCartSp^{op}, sSet_{Qu}]_{proj} \;\; \array{ \underoverset{\phantom{{}_{Qu}}\bot_{Qu} }{ even }{\longleftarrow} \\ \underoverset{ \phantom{{}_{Qu}}\bot_{Qu} }{ \iota_{sup} }{\hookrightarrow} \\ \underoverset{\phantom{{}_{Qu}}\bot_{Qu} }{ \Pi_{sup} }{\longleftarrow} \\ \underoverset{ \phantom{{}_{Qu}}\bot_{Qu} }{ Disc_{sup} }{\hookrightarrow} \\ \underoverset{ \phantom{\phantom{{}_{Qu}}\bot_{Qu}} }{ \Gamma_{sup} }{\longleftarrow} \\ \phantom{\overset{ coDisc }{\longrightarrow}} } \;\; [SuperFormalCartSp^{op}, sSet_{Qu}]_{proj/inj}

    and so the way that the topmost left adjoints between sites keep shifting up in position, in this example, matches the alternation between a single model structure (proj) and change of model structure (proj/inj).

    So at least I luck out, and the neat restrictive definition is sufficient for my current purpose.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJul 13th 2018

    I know that there are various theorems about how every geometric morphism between Grothendieck toposes can be induced by a morphism of sites as long as we choose appropriate sites for the two toposes. What sort of theorems are there like this for adjunctions between locally presentable categories? I feel like I should know the answer to that.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJul 13th 2018

    Let’s see, if CC and DD are locally presentable and U:CDU:C\to D is a right adjoint, then if D fDD_f\subseteq D is a small generating full subcategory, the restricted Yoneda embedding D[D f op,Set]D \to [D_f^{op},Set] is fully faithful and has a left adjoint. So the composite CD[D f op,Set]C \to D \to [D_f^{op},Set] is a right adjoint and lands inside DD, while its left adjoint restricts on DD to the left adjoint FF of UU. Now let C fCC_f\subseteq C be a small generating full subcategory that contains F(D f)F(D_f); then since every presheaf is the colimit of representables and left adjoints preserve colimits, the left adjoint [D f op,Set]C[D_f^{op},Set] \to C factors as left Kan extension [D f op,Set][C f op,Set][D_f^{op},Set] \to [C_f^{op},Set] along the restriction F f:D fC fF_f: D_f \to C_f followed by reflection into CC (i.e. weighted colimits). Thus, if we present CC and DD with model structures on these presheaf categories, the given adjunction should be presented by the left Kan extension Quillen adjunction.

    Not sure yet how to extend this to adjoint triples though.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJul 16th 2018

    Thanks, Mike, for the input!

    I’ll try to further think about this later. For the moment, I have a different kind of question:

    Can we see that a Quillen adjoint triple between combinatorial model categories maps to an adjunction under Renaudin’s 2-localization?

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJul 16th 2018

    That’s… a good question. It’s not obvious to me! Maybe his theorem needs to be extended to a localization of the double category of model categories.

    • CommentRowNumber20.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 17th 2018

    Naive quick question: could the diagram

    𝒞 2 AAidAA 𝒞 1 AAidAA 𝒞 1 id id C ε id 𝒞 2 ACA 𝒟 R 𝒞 1 id ε L 𝒞 2 AAidAA 𝒞 2 \array{ \mathcal{C}_2 &\overset{ \phantom{AA} id \phantom{AA} }{\longrightarrow}& \mathcal{C}_1 &\overset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& \mathcal{C}_1 \\ {}^{\mathllap{id}} \Big\downarrow &{}^{ \mathllap{ id } }\swArrow& \Big\downarrow{}^{ \mathrlap{ C } } & {}^{ \mathllap{\epsilon} }\swArrow & \Big\downarrow{}^{\mathrlap{id}} \\ \mathcal{C}_2 &\underset{ \phantom{A}C\phantom{A} }{\longrightarrow}& \mathcal{D} &\underset{R}{\longrightarrow}& \mathcal{C}_1 \\ {}^{\mathllap{id}}\Big\downarrow &{}^{\mathllap{ \epsilon }}\swArrow& \Big\downarrow{}^{\mathrlap{L}} \\ \mathcal{C}_2 &\underset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& \mathcal{C}_2 }

    be extended to some

    𝒞 2 AAidAA 𝒞 1 AAidAA 𝒞 1 id id C ε id 𝒞 2 ACA 𝒟 R 𝒞 1 id ε L ?? ?? 𝒞 2 AAidAA 𝒞 2 AA??AA 𝒞 1 \array{ \mathcal{C}_2 &\overset{ \phantom{AA} id \phantom{AA} }{\longrightarrow}& \mathcal{C}_1 &\overset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& \mathcal{C}_1 \\ {}^{\mathllap{id}} \Big\downarrow &{}^{ \mathllap{ id } }\swArrow& \Big\downarrow{}^{ \mathrlap{ C } } & {}^{ \mathllap{\epsilon} }\swArrow & \Big\downarrow{}^{\mathrlap{id}} \\ \mathcal{C}_2 &\underset{ \phantom{A}C\phantom{A} }{\longrightarrow}& \mathcal{D} &\underset{R}{\longrightarrow}& \mathcal{C}_1 \\ {}^{\mathllap{id}}\Big\downarrow &{}^{\mathllap{ \epsilon }}\swArrow& \Big\downarrow{}^{\mathrlap{L}} &{}^{\mathllap{?? }}\swArrow& \Big\downarrow{}^{\mathrlap{??}} \\ \mathcal{C}_2 &\underset{ \phantom{AA}id\phantom{AA} }{\longrightarrow}& \mathcal{C}_2 &\underset{ \phantom{AA}??\phantom{AA} }{\longrightarrow}& \mathcal{C}_1 }

    ?

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJul 17th 2018

    Quick answer: no? (-:

    • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 17th 2018

    @Mike - ah, ok :-) I had a stupidly wrong guess at first, then realised the didn’t work, but then couldn’t quickly see what would prevent some other filler for that gap.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJul 17th 2018
    • (edited Jul 17th 2018)

    Another thought:

    Given a Quillen adjoint triple LCRL \dashv C \dashv R, what we should really ask is if the derived unit of C𝕃L\mathbb{R}C \circ \mathbb{L}L satisfies its universal property for pre-composition on derived hom-spaces.

    This is easy to see if in additon to 𝒞 1idid𝒞 2\mathcal{C}_1 \underoverset{\underset{id}{\longrightarrow}}{\overset{id}{\longleftarrow}}{\bot} \mathcal{C}_2 being a Quillen equivalence, we also assume that 𝒞 1\mathcal{C}_1 and 𝒞 2\mathcal{C}_2 have the same class of weak equivalences. Of course this further assumption is again met for the case of left/right homotopy Kan extension. (Hm, or is this automatic, in general?)

    I made a simple note on this here.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeJul 18th 2018
    • (edited Jul 18th 2018)

    I have written out discussion (here) of how simplicial Quillen adjoint triples induce “derived adjoint modalities”, such that on suitably fibrant/cofibrant objects the derived modal operators are represented by the ordinary modal operators.

    Strangely, I can make this work only in 3 of 4 cases: For Quillen adjoint triples of the form

    𝒞 1/2 Qu QuL Qu QuC AARAA 𝒟 \mathcal{C}_{1/2} \array{ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{L}{\longleftarrow} \\ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{C}{\longrightarrow} \\ \overset{\phantom{AA}R\phantom{AA}}{\longleftarrow} \\ } \mathcal{D}

    it works for a) CC being fully faithful and b) LL and RR being fully faithful, but for Quillen adjoint triples of the form

    𝒞 1/2 Qu QuL Qu QuC AARAA 𝒟 \mathcal{C}_{1/2} \array{ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{L}{\longrightarrow} \\ \underoverset{{}_{\phantom{Qu}}\bot_{Qu}}{C}{\longleftarrow} \\ \overset{\phantom{AA}R\phantom{AA}}{\longrightarrow} \\ } \mathcal{D}

    it seems to work only for the case that CC is fully faithful.

    diff, v16, current

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeJul 18th 2018

    I don’t understand what you’re trying to do here. Once we know that we have an adjoint triple at the homotopy level, doesn’t everything we want follow from abstract nonsense there?

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeJul 18th 2018

    Here I am after control of the \infty-adjoint triple, whose properties are seen not by the set-valued hom in the homotopy category, but the simplicial-set valued derived hom.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeJul 18th 2018

    But the properties that you’re talking about look like they should follow by abstract nonsense of (,1)(\infty,1)-category theory once we have an \infty-adjoint triple, without needing to futz about with model categories any more.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeJul 18th 2018

    (By “homotopy” I meant \infty, sorry if that wasn’t clear.)

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJul 19th 2018

    I am trying to do without \infty-category theory here. Just model category theory.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeJul 19th 2018

    Why?

    In any case, it seems like it would be more nPOV to first do it with \infty-category theory, and then relegate the model-categorical version to a subsection or a sub-page.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeJul 19th 2018

    Why?

    To give readers a comprehensive account without sending them through the \infty-literature. To have a clean 1-category theoretic construction. To know how to build models of modal HoTT in model categories.

    it seems like it would be more nPOV to first do it with \infty-category theory, and then relegate the model-categorical version to a subsection or a sub-page.

    That would be for an entry with a different title. This here is titled “Quillen adjoint triple” and not “\infty-adjoint triple”.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeJul 19th 2018

    Well, but we should at least tell the reader on this page that these model-categorical shenanigans are not actually required, and in particular that any seeming-arbitrary restrictions like “having the same weak equivalences” or “only working in 3/4 cases” come only from the choice of machinery rather than being fundamental to the result.

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeJul 19th 2018

    Expand Idea section to mention other possibilities in the definition, and remark that we could just as well use (,1)(\infty,1)-categories.

    diff, v22, current

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeJul 20th 2018

    I had had a silly variance error in the discussion of adjoint quadruples. Have fixed this now. In the process I ended up pretty much rewriting large bits of the entry.

    diff, v28, current

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeJul 20th 2018
    • (edited Jul 20th 2018)

    Supposing that I have it right now, I can now say “solid model topos” to be a system of Quillen adjoint triples of this form:

    sSet Qu Qu QuΠ red[𝒞 red op,sSet Qu] projloc Qu Quidid[𝒞 red op,sSet Qu] projloc Qu Quι inf[𝒞 inf op,sSet Qu] projloc Qu Quid[𝒞 inf op,sSet Qu] projloc Qu Queven[𝒞 op,sSet Qu] projloc sSet Qu Qu QuΠ red[𝒞 red op,sSet Qu] projloc Qu Quidid[𝒞 red op,sSet Qu] projloc Qu Quι inf[𝒞 inf op,sSet Qu] projloc Qu Quid[𝒞 inf op,sSet Qu] projloc Qu Quι sup[𝒞 op,sSet Qu] injloc sSet Qu Qu QuΠ red[𝒞 red op,sSet Qu] projloc Qu Quid[𝒞 red op,sSet Qu] injloc Qu QuΠ inf[𝒞 inf op,sSet Qu] projloc Qu Quid[𝒞 inf op,sSet Qu] injloc Qu QuΠ sup[𝒞 op,sSet Qu] injloc sSet Qu Qu QuDisc red[𝒞 red op,sSet Qu] injloc Qu Quid[𝒞 inf op,sSet Qu] injloc Qu QuDisc inf[𝒞 inf op,sSet Qu] injloc Qu Quid[𝒞 inf op,sSet Qu] projloc Qu QuDisc sup[𝒞 op,sSet Qu] projloc sSet Qu Qu QucoDisc redΓ red[𝒞 red op,sSet Qu] injloc Qu Quidid[𝒞 inf op,sSet Qu] injloc Qu QuΓ inf[𝒞 inf op,sSet Qu] injloc Qu Quid[𝒞 inf op,sSet Qu] projloc Qu Quι sup[𝒞 op,sSet Qu] projloc \array{ \phantom{ sSet_{Qu} \underoverset {{\longrightarrow}} {\overset{\Pi_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {\underset{id}{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{\iota_{inf}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longrightarrow}} {\overset{id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longrightarrow}} {\overset{even}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{proj \atop loc} \\ \phantom{ sSet_{Qu} \underoverset {{\longrightarrow}} {\overset{\Pi_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {\underset{id}{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } } [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{\iota_{inf}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longrightarrow}} {\overset{id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{\iota_{sup}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{inj \atop loc} \\ sSet_{Qu} \underoverset {{\longrightarrow}} {\overset{\Pi_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{inj \atop loc} \underoverset {{\longrightarrow}} {\overset{ \Pi_{inf} }{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj \atop loc} \underoverset {{\longrightarrow}} {\overset{\Pi_{sup}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{inj \atop loc} \\ sSet_{Qu} \underoverset {{\longleftarrow}} {\overset{Disc_{red}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{inj \atop loc} \underoverset {{\longrightarrow}} {\overset{id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj \atop loc} \underoverset {{\longleftarrow}} {\overset{ Disc_{inf} }{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj \atop loc} \underoverset {\phantom{\longrightarrow}} {\overset{\;\;id}{\phantom{\longleftarrow}}} {\phantom{\phantom{{}_{Qu}}\simeq_{Qu}} } \phantom{[\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc}} \underoverset {\phantom{\longleftarrow}} {\overset{\;Disc_{sup}}{\phantom{\longrightarrow}}} {\phantom{\phantom{{}_{Qu}}\bot_{Qu}}} \phantom{[\mathcal{C}^{op}, sSet_{Qu}]_{proj \atop loc}} \\ sSet_{Qu} \underoverset {\underset{coDisc_{red}}{\longrightarrow}} {\overset{\Gamma_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{inj \atop loc} \underoverset {\phantom{\underset{id}{\longrightarrow}}} {\overset{id}{\phantom{\longleftarrow}}} {\phantom{\phantom{{}_{Qu}}\simeq_{Qu}} } \phantom{ [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj \atop loc} } \underoverset {\phantom{{\longleftarrow}}} {\overset{ \Gamma_{inf} }{\phantom{\longrightarrow}}} {\phantom{\phantom{{}_{Qu}}\bot_{Qu}}} \phantom{ [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj \atop loc} \underoverset {\underset{}{\longrightarrow}} {\overset{id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{\iota_{sup}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{proj \atop loc} } }

    Here Disc infDisc redΓ redΓ infDisc_{inf} \circ Disc_{red} \dashv \Gamma_{red} \circ \Gamma_{inf} composes to a Quillen adjunction, and we ask in addition that this extends to yet another Quillen adjoint triple one step down.

    Unfortunately Π infΠ supDisc supDisc inf\Pi_{inf}\circ \Pi_{sup} \dashv Disc_{sup} \circ Disc_{inf} is not manifestly a Quillen adjunction from just the above data. Maybe I made a mistake somewhare, or maybe it’s just not going to happen, and the right adjoint &\& to the \Im-modality will be the (only) one among the 12 which is not directly the derived functor of a Quillen functor.

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeJul 21st 2018
    • (edited Jul 21st 2018)

    added the example of Quillen adjoint quintuples on simplicial presheaves induced via Kan extension along adjoint triples (here). This has two realizations: either

    [𝒞 op,sSet Qu] projA Qu QuAL !A aA a[𝒟 op,sSet Qu] proj [\mathcal{C}^{op}, sSet_{Qu}]_{proj} \underoverset {{\longleftarrow}} {\overset{L_! \phantom{\simeq A_a \simeq A_a}}{\longrightarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{proj} [𝒞 op,sSet Qu] injA Qu QuAL *C !A a[𝒟 op,sSet Qu] proj [\mathcal{C}^{op}, sSet_{Qu}]_{inj} \underoverset {{\longrightarrow}} {\overset{L^\ast \simeq C_! \phantom{\simeq A_a}}{\longleftarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{proj} [𝒞 op,sSet Qu] injA Qu QuAL *C *R ![𝒟 op,sSet Qu] inj [\mathcal{C}^{op}, sSet_{Qu}]_{inj} \underoverset {\underset{}{\longleftarrow}} {\overset{L_\ast \simeq C^\ast \simeq R_!}{\longrightarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{inj} [𝒞 op,sSet Qu] injA Qu QuAA aA aR *A aC *R *[𝒟 op,sSet Qu] inj [\mathcal{C}^{op}, sSet_{Qu}]_{inj} \underoverset {\underset{ \phantom{ A_a \simeq A_a \simeq} R_\ast }{\longrightarrow}} {\overset{ \phantom{A_a \simeq} C_\ast \simeq R^\ast }{\longleftarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{inj}

    or

    [𝒞 op,sSet Qu] projA Qu QuAL !A aA a[𝒟 op,sSet Qu] proj [\mathcal{C}^{op}, sSet_{Qu}]_{proj} \underoverset {{\longleftarrow}} {\overset{L_! \phantom{\simeq A_a \simeq A_a}}{\longrightarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{proj} [𝒞 op,sSet Qu] projA Qu QuAL *C !A a[𝒟 op,sSet Qu] proj [\mathcal{C}^{op}, sSet_{Qu}]_{proj} \underoverset {{\longrightarrow}} {\overset{L^\ast \simeq C_! \phantom{\simeq A_a}}{\longleftarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{proj} [𝒞 op,sSet Qu] injA Qu QuAL *C *R ![𝒟 op,sSet Qu] proj [\mathcal{C}^{op}, sSet_{Qu}]_{inj} \underoverset {\underset{}{\longleftarrow}} {\overset{L_\ast \simeq C^\ast \simeq R_!}{\longrightarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{proj} [𝒞 op,sSet Qu] injA Qu QuAA aA aR *A aC *R *[𝒟 op,sSet Qu] inj [\mathcal{C}^{op}, sSet_{Qu}]_{inj} \underoverset {\underset{ \phantom{ A_a \simeq A_a \simeq} R_\ast }{\longrightarrow}} {\overset{ \phantom{A_a \simeq} C_\ast \simeq R^\ast }{\longleftarrow}} {\phantom{\phantom{A}{}_{Qu}}\bot_{Qu}\phantom{A}} [\mathcal{D}^{op}, sSet_{Qu}]_{inj}

    This pattern continues for homotopy Kan extension along adjoint (n+1)(n+1)-tuples: the resulting Quillen adjoint (n+3)(n+3)-ples have

    1. projective model structures “everywhere on top”

    2. injective model structure “everywhere at the bottom”

    3. a transition zone across a Quillen adjoint quadruple where projective turns into injective.

    diff, v29, current

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeJul 21st 2018
    • (edited Jul 21st 2018)

    With this I can fix the remaining problem in #35: Since in the examples of solid model toposes of interest we happen to have not just a Quillen adjoint quadruple but a Quillen adjoint quintuple on the “far right”:

    sSet Qu Qu QuΠ red[𝒞 red op,sSet Qu] projloc Qu Quidid[𝒞 red op,sSet Qu] projloc Qu Quι inf[𝒞 inf op,sSet Qu] projloc Qu Quid[𝒞 inf op,sSet Qu] projloc Qu Queven[𝒞 op,sSet Qu] projloc sSet Qu Qu QuΠ red[𝒞 red op,sSet Qu] projloc Qu Quidid[𝒞 red op,sSet Qu] projloc Qu Quι inf[𝒞 inf op,sSet Qu] projloc Qu Quid[𝒞 inf op,sSet Qu] projloc Qu Quι sup[𝒞 op,sSet Qu] injrloc sSet Qu Qu QuΠ red[𝒞 red op,sSet Qu] projloc Qu Quid[𝒞 red op,sSet Qu] injrloc Qu QuΠ inf[𝒞 inf op,sSet Qu] projloc Qu Quid[𝒞 inf op,sSet Qu] injrloc Qu QuΠ sup[𝒞 op,sSet Qu] injrloc sSet Qu Qu QuDisc red[𝒞 red op,sSet Qu] injrloc Qu Quid[𝒞 inf op,sSet Qu] injrloc Qu QuDisc inf[𝒞 inf op,sSet Qu] injrloc Qu Quid[𝒞 inf op,sSet Qu] injrloc Qu QuDisc sup[𝒞 op,sSet Qu] injrloc sSet Qu Qu QucoDisc redΓ red[𝒞 red op,sSet Qu] injrloc Qu Quidid[𝒞 inf op,sSet Qu] injrloc Qu QuΓ inf[𝒞 inf op,sSet Qu] injrloc Qu Quid[𝒞 inf op,sSet Qu] projloc Qu QuΓ sup[𝒞 op,sSet Qu] projloc \array{ \phantom{ sSet_{Qu} \underoverset {{\longrightarrow}} {\overset{\Pi_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {\underset{id}{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{\iota_{inf}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longrightarrow}} {\overset{id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longrightarrow}} {\overset{even}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{proj \atop loc} \\ \phantom{ sSet_{Qu} \underoverset {{\longrightarrow}} {\overset{\Pi_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {\underset{id}{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } } [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{\iota_{inf}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longrightarrow}} {\overset{id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{\iota_{sup}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \\ sSet_{Qu} \underoverset {{\longrightarrow}} {\overset{\Pi_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \underoverset {{\longrightarrow}} {\overset{ \Pi_{inf} }{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc} \underoverset {{\longleftarrow}} {\overset{id}{\longrightarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \underoverset {{\longrightarrow}} {\overset{\Pi_{sup}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \\ sSet_{Qu} \underoverset {{\longleftarrow}} {\overset{Disc_{red}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \underoverset {{\longrightarrow}} {\overset{id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \underoverset {{\longleftarrow}} {\overset{ Disc_{inf} }{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \underoverset {{\longrightarrow}} {\overset{\;\;id}{\longleftarrow}} {\phantom{{}_{Qu}}\simeq_{Qu} } [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \underoverset {{\longleftarrow}} {\overset{\;Disc_{sup}}{\longrightarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \\ sSet_{Qu} \underoverset {\underset{coDisc_{red}}{\longrightarrow}} {\overset{\Gamma_{red}}{\longleftarrow}} {\phantom{{}_{Qu}}\bot_{Qu}} [\mathcal{C}_{red}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} \underoverset {\phantom{\underset{id}{\longrightarrow}}} {\overset{id}{\phantom{\longleftarrow}}} {\phantom{\phantom{{}_{Qu}}\simeq_{Qu}} } \phantom{ [\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc} } \underoverset {\phantom{{\longleftarrow}}} {\overset{ \Gamma_{inf} }{\phantom{\longrightarrow}}} {\phantom{\phantom{{}_{Qu}}\bot_{Qu}}} \phantom{[\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{inj\phantom{r} \atop loc}} \underoverset {\underset{}{\phantom{\longrightarrow}}} {\overset{id}{\phantom{\longleftarrow}}} {\phantom{\phantom{{}_{Qu}}\simeq_{Qu} }} \phantom{[\mathcal{C}_{inf}^{op}, sSet_{Qu}]_{proj \atop loc}} \underoverset {\phantom{{\longleftarrow}}} {\overset{\Gamma_{sup}}{\phantom{\longrightarrow}}} {\phantom{\phantom{{}_{Qu}}\bot_{Qu}}} \phantom{[\mathcal{C}^{op}, sSet_{Qu}]_{proj \atop loc}} }

    This now implies all the 12 derived adjoint modalities, all by application of this prop..