[0KF3]
Proof. For d = − 1 d=-1 , there is nothing to prove in (1)–(3) and so we assume that d ≥ 0 d\geq 0 .
(1) For d = 0 d=0 , it is clear that ( h 0 𝒪 ) ⊗ \left(h_{0}\mathcal{\mathcal{O}}\right)^{\otimes}
is a skeletal 1 1 -category, with p 0 p_{0} fully faithful; and for d ≥ 1 d\geq 1 ,
it is clear that ( h d 𝒪 ) ⊗ \left(h_{d}\mathcal{\mathcal{O}}\right)^{\otimes}
is a d d -category. Hence, we only need to show that ( h d 𝒪 ) ⊗ \left(h_{d}\mathcal{\mathcal{O}}\right)^{\otimes}
is an ∞ \infty -operad. For this we need to check the three conditions
of Definition A.2.1.1.10 .
•
Since p : 𝒪 ⊗ → 𝐅𝐢𝐧 ∗ p\colon\mathcal{O}^{\otimes}\to\mathbf{Fin}_{*} is an ∞ \infty -operad,
for every inert morphism f : ⟨ m ⟩ → ⟨ n ⟩ f\colon\left\langle m\right\rangle\to\left\langle n\right\rangle
and an object X ¯ ∈ h d 𝒪 ⟨ m ⟩ ⊗ \overline{X}\in h_{d}\mathcal{O}_{\left\langle m\right\rangle}^{\otimes} ,
we can lift X ¯ \overline{X} to X ∈ 𝒪 ⟨ m ⟩ ⊗ X\in\mathcal{O}_{\left\langle m\right\rangle}^{\otimes}
and find a coCartesian lift g : X → Y g\colon X\to Y of f f in 𝒪 ⊗ \mathcal{O}^{\otimes} .
For d ≥ 1 d\geq 1 , the image g ¯ \overline{g} of g g in ( h d 𝒪 ) ⊗ \left(h_{d}\mathcal{O}\right)^{\otimes}
is a coCartesian lift of f f by 3.3 . For d = 0 d=0 ,
we use the dual of T.2.4.4.3 to show that g ¯ \overline{g} is coCartesian.
( h 0 𝒪 ) ⊗ → 𝐅𝐢𝐧 ∗ \left(h_{0}\mathcal{O}\right)^{\otimes}\to\mathbf{Fin}_{*} is an inner fibration
(as the nerve of a functor of ordinary categories) and for every Z ¯ ∈ ( h 0 𝒪 ) ⟨ m ⟩ ⊗ \overline{Z}\in\left(h_{0}\mathcal{O}\right)_{\left\langle m\right\rangle}^{\otimes} ,
pre-composition with g ¯ \overline{g} induces a diagram
Map ( h 0 𝒪 ) ⊗ ( Y ¯ , Z ¯ ) Map ( h 0 𝒪 ) ⊗ ( X ¯ , Z ¯ ) Map 𝐅𝐢𝐧 ∗ ( ⟨ m ⟩ , ⟨ k ⟩ ) Map 𝐅𝐢𝐧 ∗ ( ⟨ n ⟩ , ⟨ k ⟩ ) , \lx@xy@svg{\hbox{\raise 2.5pt\hbox{\kern 42.02347pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\halign{\entry@#!@&&\entry@@#!@\cr&\cr&\crcr}}}\ignorespaces{\hbox{\kern-36.83408pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-2.5pt\hbox{$\textstyle{\operatorname{Map}_{\left(h_{0}\mathcal{O}\right)^{\otimes}}\left(\overline{Y},\overline{Z}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-24.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 69.82396pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 69.82396pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-2.5pt\hbox{$\textstyle{\operatorname{Map}_{\left(h_{0}\mathcal{O}\right)^{\otimes}}\left(\overline{X},\overline{Z}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 106.65804pt\raise-24.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-42.02347pt\raise-32.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-2.5pt\hbox{$\textstyle{\operatorname{Map}_{\mathbf{Fin}_{*}}\left(\left\langle m\right\rangle,\left\langle k\right\rangle\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 66.02347pt\raise-32.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 66.02347pt\raise-32.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-2.5pt\hbox{$\textstyle{\operatorname{Map}_{\mathbf{Fin}_{*}}\left(\left\langle n\right\rangle,\left\langle k\right\rangle\right)}$}}}}}}}\ignorespaces}}}}\ignorespaces,
and it is easy to verify that it is a homotopy pullback.
•
Let X ¯ ∈ ( h d 𝒪 ) ⟨ m ⟩ ⊗ \overline{X}\in\left(h_{d}\mathcal{O}\right)_{\left\langle m\right\rangle}^{\otimes}
and Y ¯ ∈ ( h d 𝒪 ) ⟨ n ⟩ ⊗ \overline{Y}\in\left(h_{d}\mathcal{O}\right)_{\left\langle n\right\rangle}^{\otimes}
and let
f : ⟨ m ⟩ → ⟨ n ⟩ f\colon\left\langle m\right\rangle\to\left\langle n\right\rangle
be a morphism in 𝐅𝐢𝐧 ∗ \mathbf{Fin}_{*} . We first observe that
Map ( h d 𝒪 ) ⊗ f ( X , Y ) ≃ h d − 1 ( Map 𝒪 ⊗ f ( X , Y ) ) . \operatorname{Map}_{\left(h_{d}\mathcal{O}\right)^{\otimes}}^{f}\left(X,Y\right)\simeq h_{d-1}\left(\operatorname{Map}_{\mathcal{O}^{\otimes}}^{f}\left(X,Y\right)\right).
For d ≥ 1 d\geq 1 this follows from 2.13 and
for d = 0 d=0 it follows directly from the definition. Hence,
Map ( h d 𝒪 ) ⊗ f ( X , Y ) \displaystyle\operatorname{Map}_{\left(h_{d}\mathcal{O}\right)^{\otimes}}^{f}\left(X,Y\right)
≃ \displaystyle\simeq
h d − 1 ( Map 𝒪 ⊗ f ( X , Y ) ) ≃ h d − 1 ( ∏ 1 ≤ i ≤ n Map 𝒪 ⊗ ρ i ∘ f ( X , Y i ) ) \displaystyle h_{d-1}\left(\operatorname{Map}_{\mathcal{O}^{\otimes}}^{f}\left(X,Y\right)\right)\simeq h_{d-1}\left(\prod_{1\leq i\leq n}\operatorname{Map}_{\mathcal{O}^{\otimes}}^{\rho^{i}\circ f}\left(X,Y_{i}\right)\right)
≃ \displaystyle\simeq
∏ 1 ≤ i ≤ n h d − 1 ( Map 𝒪 ⊗ ρ i ∘ f ( X , Y i ) ) ≃ ∏ 1 ≤ i ≤ n Map ( h d 𝒪 ) ⊗ ρ i ∘ f ( X , Y i ) . \displaystyle\prod_{1\leq i\leq n}h_{d-1}\left(\operatorname{Map}_{\mathcal{O}^{\otimes}}^{\rho^{i}\circ f}\left(X,Y_{i}\right)\right)\simeq\prod_{1\leq i\leq n}\operatorname{Map}_{\left(h_{d}\mathcal{O}\right)^{\otimes}}^{\rho^{i}\circ f}\left(X,Y_{i}\right).
Note that we use the fact that h d h_{d} preserves finite products of spaces.
•
For every finite collection of objects X ¯ 1 , … , X ¯ n ∈ ( h d 𝒪 ) ⟨ 1 ⟩ ⊗ \overline{X}_{1},\dots,\overline{X}_{n}\in\left(h_{d}\mathcal{O}\right)_{\left\langle 1\right\rangle}^{\otimes}
that are lifted to objects of 𝒪 ⟨ 1 ⟩ ⊗ \mathcal{O}_{\left\langle 1\right\rangle}^{\otimes} ,
there is an object X ∈ 𝒪 ⟨ n ⟩ ⊗ X\in\mathcal{O}_{\left\langle n\right\rangle}^{\otimes}
and coCartesian morphisms f i : X → X i f_{i}\colon X\to X_{i} covering ρ i : ⟨ n ⟩ → ⟨ 1 ⟩ \rho^{i}\colon\left\langle n\right\rangle\to\left\langle 1\right\rangle .
The images of those maps in h d 𝒪 ⊗ h_{d}\mathcal{O}^{\otimes} are coCartesian
as well and satisfy the analogous property.
(2) From the proof of (1), θ d \theta_{d} maps inert morphisms in 𝒪 ⊗ \mathcal{O}^{\otimes}
to inert morphisms in h d 𝒪 ⊗ h_{d}\mathcal{O}^{\otimes} .
(3) We need to show that h d F h_{d}F maps inert morphisms to inert morphisms.
For d = 0 d=0 , this is automatic. For d ≥ 1 d\geq 1 , let f ¯ : X → Y \overline{f}\colon X\to Y
be an inert morphism in ( h d 𝒪 ) ⊗ \left(h_{d}\mathcal{O}\right)^{\otimes} .
There is a coCartesian morphism f : X → Y ′ f\colon X\to Y^{\prime} in 𝒪 ⊗ \mathcal{O}^{\otimes}
with the same image as f ¯ \overline{f} in 𝐅𝐢𝐧 ∗ \mathbf{Fin}_{*} ; hence its image
in ( h d 𝒪 ) ⊗ \left(h_{d}\mathcal{O}\right)^{\otimes} is equivalent to f f .
Since the composition 𝒪 ⊗ → 𝒰 ⊗ → ( h d 𝒰 ) ⊗ \mathcal{O}^{\otimes}\to\mathcal{U}^{\otimes}\to\left(h_{d}\mathcal{U}\right)^{\otimes}
preserves inert morphisms, it follows that the image of f f in ( h d 𝒰 ) ⊗ \left(h_{d}\mathcal{U}\right)^{\otimes}
is inert and since the image of f ¯ \overline{f} in ( h d 𝒰 ) ⊗ \left(h_{d}\mathcal{U}\right)^{\otimes}
is equivalent to the image of f f , it is inert as well.
∎