[0015] Sheaves on $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$

The category $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ is type-theoretically not nice because it is not locally cartesian closed. We consider embedding it into a logos (in a larger universe).

[0016] Definition

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . We say a presheaf $A:{(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow V$ is a sheaf if it takes étale colimits in $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ to limits in $$V$$ .

[0019] Definition

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . We define $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ to be the full subcategory of $\mathord {\textnormal {\textsf {Fun}}}({(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}},V)$ spanned by the sheaves in the sense of [0016].

[001A] Exercise

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . Then $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ is a $$V$$ -logos.

[001B] Proposition

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . Then the Yoneda embedding $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\rightarrow \mathord {\textnormal {\textsf {Fun}}}({(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}},V)$ factors through $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ .

Proof

This is because representable presheaves preserve arbitrary limits.

[001C] Proposition

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . Then the Yoneda embedding $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\rightarrow \mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ preserves finite limits and $$U$$ -small products.

Proof

This is because the Yoneda embedding preserves arbitrary limits.

[001D] Proposition

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . Then the Yoneda embedding $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\rightarrow \mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ takes étale colimits to colimits.

Proof

This follows from the Yoneda lemma and the definition of sheaves on $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ .

[002Z] Exercise

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . Then the Yoneda embedding exhibits $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ as the completion of $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ under $$V$$ -small colimits preserving étale colimits.

The object $\mathbb {A}$ in $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ classifies $$U$$ -small sheaves by [000Z]. In $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ , we can construct objects that classify large sheaves.

[001E] Definition

Let $$U$$ be a universe, let $$V$$ be a universe greater than or equal to $$U$$ , and let $$W$$ be a universe strictly greater than $$V$$ . The forgetful functor $\mathord {\textnormal {\textsf {LexCocomp}}}(V,W)\rightarrow \mathord {\textnormal {\textsf {LexCocomp}}}(U,W)$ has a left adjoint. This left adjoint takes $$U$$ -compact objects in $\mathord {\textnormal {\textsf {LexCocomp}}}(U,W)$ to $$V$$ -compact objects in $\mathord {\textnormal {\textsf {LexCocomp}}}(V,W)$ and thus induces a functor $C\mapsto \mathop {\Uparrow ^{V}}C:\mathord {\textnormal {\textsf {Logos}}}(U)\rightarrow \mathord {\textnormal {\textsf {Logos}}}(V)$ . For a $$U$$ -logos $$C$$ , the $$V$$ -logos $\mathop {\Uparrow ^{V}}C$ is called the $$V$$ -enlargement of $$C$$ . Notice that the choice of $$W$$ does not matter.

[001F] Exercise

Let $$U$$ be a universe and let $$V$$ be a universe greater than or equal to $$U$$ . For any $$U$$ -logos $$C$$ , the unit $C\rightarrow \mathop {\Uparrow ^{V}}C$ , which is a morphism in $\mathord {\textnormal {\textsf {LexCocomp}}}(U,W)$ for some universe $$W$$ strictly greater than $$V$$ , is fully faithful. We thus regard $$C$$ as a full subcategory of $\mathop {\Uparrow ^{V}}C$ .

[001G] Exercise

Let $$U$$ be a universe and let $$V$$ be a universe greater than or equal to $$U$$ . Then the functor $C\mapsto \mathop {\Uparrow ^{V}}C:\mathord {\textnormal {\textsf {Logos}}}(U)\rightarrow \mathord {\textnormal {\textsf {Logos}}}(V)$ preserves étale morphisms. More precisely, for any $$U$$ -logos $$C$$ and any object $$A:C$$ , the embedding $C/A\rightarrow \mathop {\Uparrow ^{V}}C/A$ induces an equivalence $\mathop {\Uparrow ^{V}}(C/A)\simeq \mathop {\Uparrow ^{V}}C/A$ .

[001H] Proposition

Let $$U$$ be a universe and let $$V$$ be a universe greater than or equal to $$U$$ . Then the functor $C\mapsto \mathop {\Uparrow ^{V}}C:\mathord {\textnormal {\textsf {Logos}}}(U)\rightarrow \mathord {\textnormal {\textsf {Logos}}}(V)$ takes étale limits in $\mathord {\textnormal {\textsf {Logos}}}(U)$ to étale limits in $\mathord {\textnormal {\textsf {Logos}}}(V)$ .

Proof

Let $$C$$ be a $$U$$ -logos, let $$I$$ be a $$U$$ -small category, and let $A:I\rightarrow C$ be a functor. Let $$B:C$$ denote the colimit of $$A$$ . By [0011], the étale limit of the diagram induced by $$A$$ is $$C/B$$ . Then apply [001G].

[001I] Definition

Let $$U$$ be a universe, let $$V$$ be a universe greater than or equal to $$U$$ , and let $$W$$ be a universe strictly greater than $$V$$ . We define presheaves

\mathbb {A}^{(V)},\mathbb {A}_{\bullet }^{(V)}:{(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow W

\mathbb {A}^{(V)}(X)=\mathord {\textnormal {\textsf {Obj}}}(\mathop {\Uparrow ^{V}}(\mathord {\textnormal {\textsf {Sh}}}(X)))

and

\mathbb {A}_{\bullet }^{(V)}(X)=\mathord {\textnormal {\textsf {Obj}}}(\mathop {\Uparrow ^{V}}(\mathord {\textnormal {\textsf {Sh}}}(X))\backslash \mathord {\textnormal {\textsf {1}}})

. We also define a morphism

\mathord {\textnormal {\textsf {p}}}^{(V)}:\mathbb {A}_{\bullet }^{(V)}\rightarrow \mathbb {A}^{(V)}

by the codomain projection.

[001J] Proposition

Let $$U$$ be a universe, let $$V$$ be a universe greater than or equal to $$U$$ , and let $$W$$ be a universe strictly greater than $$W$$ . Then the presheaves $\mathbb {A}^{(V)},\mathbb {A}_{\bullet }^{(V)}:{(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow W$ are sheaves.

Proof

$\mathbb {A}^{(V)}$ is a sheaf by [001H]. $\mathbb {A}_{\bullet }^{(V)}$ is a sheaf because coslicing commutes with limits.

[001K] Exercise

Let $$U$$ be a universe, let $$V$$ be a universe greater than or equal to $$U$$ , and let $$W$$ be a universe strictly greater than $$V$$ . Then the morphism $\mathord {\textnormal {\textsf {p}}}^{(V)}:\mathbb {A}_{\bullet }^{(V)}\rightarrow \mathbb {A}^{(V)}$ in $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),W)$ is univalent.

We can restore part of the $$2$$ -categorical structure of $\mathord {\textnormal {\textsf {Topos}}}(U)$ .

[0053] Definition

Let $$U$$ be a universe. We define a functor $\mathord {\textnormal {\textsf {Q}}}:\mathord {\textnormal {\textsf {Cat}}}(U)\rightarrow \mathord {\textnormal {\textsf {Topos}}}(U)$ by $\mathord {\textnormal {\textsf {Q}}}(C)=C\bullet \mathord {\textnormal {\textsf {1}}}$ .

[0054] Exercise

Let $$U$$ be a universe.

- $(\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {s}}}^{1}),\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {s}}}^{0})):\mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 2\rbrack )\rightarrow \mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 1\rbrack )\times \mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 1\rbrack )$ determines a partial order in $\mathord {\textnormal {\textsf {Topos}}}(U)$ . We refer to this partially ordered object in $\mathord {\textnormal {\textsf {Topos}}}(U)$ as $\mathbb {I}$ .
- $\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {d}}}^{1}):\mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 0\rbrack )\rightarrow \mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 1\rbrack )$ determines the least element of $\mathbb {I}$ .
- $\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {d}}}^{0}):\mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 0\rbrack )\rightarrow \mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 1\rbrack )$ determines the greatest element of $\mathbb {I}$ .
- $\mathord {\textnormal {\textsf {0}}}\simeq \mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 0\rbrack )\mathbin {{}_{\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {d}}}^{1})}\mathord {\times _{\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {d}}}^{0})}}}\mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 0\rbrack )$
-Let $n\ge 3$ be an integer. Then the morphism $(\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {s}}}^{n-1}),{(\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {s}}}^{0}))}^{n-2}):\mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack n\rbrack )\rightarrow \mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack n-1\rbrack )\mathbin {{}_{{(\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {s}}}^{0}))}^{n-2}}\mathord {\times _{\mathord {\textnormal {\textsf {Q}}}(\mathord {\textnormal {\textsf {s}}}^{1})}}}\mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack 2\rbrack )$ is an equivalence. (This means that $\mathord {\textnormal {\textsf {Q}}}(\Delta \lbrack n\rbrack )$ is the object of increasing sequences in $\mathbb {I}$ of length $$n$$ ).

One can also show that $\mathbb {I}$ is totally ordered in $\mathord {\textnormal {\textsf {Topos}}}(U)$ , but that property would not be preserved by the embedding $\mathord {\textnormal {\textsf {Topos}}}(U)\rightarrow \mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ .

[0055] Definition

Let $$U$$ be a universe, let $$C$$ be a $$U$$ -logos, let $$I$$ be a partially ordered object in $$C$$ , and let $$n$$ be a natural number. We define $\Delta _{I}\lbrack n\rbrack$ to be the object in $$C$$ that classifies (non-strictly) increasing sequences in $$I$$ of length $$n$$ . When $$I$$ has least and greatest elements, face maps and degeneracy maps between $\Delta _{I}\lbrack n\rbrack$ 's can also be defined.

[0032] Definition

Let $$U$$ be a universe, let $$C$$ be a $$U$$ -logos, and let $$I$$ be a partially ordered object in $$C$$ with least and greatest elements. We say an object in $$C$$ is $$I$$ -categorically fibrant if it is internally local for the following morphisms.

- $(\mathord {\textnormal {\textsf {d}}}^{2},\mathord {\textnormal {\textsf {d}}}^{0}):\Delta _{I}\lbrack 1\rbrack \mathbin {{}_{\mathord {\textnormal {\textsf {d}}}^{0}}\mathord {+_{\mathord {\textnormal {\textsf {d}}}^{1}}}}\Delta _{I}\lbrack 1\rbrack \rightarrow \Delta _{I}\lbrack 2\rbrack$
- $\Delta _{I}\lbrack 3\rbrack \mathbin {{}_{(\mathord {\textnormal {\textsf {d}}}^{3}\circ \mathord {\textnormal {\textsf {d}}}^{1},\mathord {\textnormal {\textsf {d}}}^{0}\circ \mathord {\textnormal {\textsf {d}}}^{1})}\mathord {+_{\mathord {\textnormal {\textsf {s}}}^{0}+\mathord {\textnormal {\textsf {s}}}^{0}}}}(\Delta _{I}\lbrack 0\rbrack +\Delta _{I}\lbrack 0\rbrack )\rightarrow \Delta _{I}\lbrack 0\rbrack$
- $((\mathord {\textnormal {\textsf {s}}}^{0},\mathord {\textnormal {\textsf {s}}}^{1}),(\mathord {\textnormal {\textsf {s}}}^{1},\mathord {\textnormal {\textsf {s}}}^{0})):\Delta _{I}\lbrack 2\rbrack \mathbin {{}_{\mathord {\textnormal {\textsf {d}}}^{1}}\mathord {+_{\mathord {\textnormal {\textsf {d}}}^{1}}}}\Delta _{I}\lbrack 2\rbrack \rightarrow \Delta _{I}\lbrack 1\rbrack \times \Delta _{I}\lbrack 1\rbrack$

The locality for the first two morphisms in [0032] is the Segal condition and the Rezk condition, respectively. We add the third morphism because $$I$$ is not assumed to be totally ordered. Local objects for the third morphism “believe that $$I$$ is totally ordered”.

[005A] Definition

Let $$U$$ be a universe, let $$C$$ be a $$U$$ -logos, and let $$I$$ be a partially ordered object in $$C$$ with least and greatest elements. We say a morphism in $$C$$ is a $$I$$ -left fibration if it is internally right orthogonal to $\mathord {\textnormal {\textsf {d}}}^{1}:\Delta _{I}\lbrack 0\rbrack \rightarrow \Delta _{I}\lbrack 1\rbrack$ .

[0034] Exercise

Let $$U$$ be a universe, let $$V$$ be a universe greater than or equal to $$U$$ , and let $$W$$ be a universe strictly greater than $$V$$ . Then $\mathbb {A}^{(V)}:\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),W)$ is $\mathbb {I}$ -categorically fibrant.

[0035] Exercise

$\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$ itself appears in $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ as a universe.

[0050] Notation

Let $$C$$ be a lex category. We write $\rho (C):\mathord {\textnormal {\textsf {R}}}_{\bullet }(C)\rightarrow \mathord {\textnormal {\textsf {R}}}(C)$ for the universal representable map of presheaves on $$C$$ ; see Definition 5.2 of [Nguyen--Uemura--2022-0000].

[0051] Exercise

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . Then $\mathord {\textnormal {\textsf {R}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))$ and $\mathord {\textnormal {\textsf {R}}}_{\bullet }(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))$ are in $\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)$ .

[0056] Exercise

Let $$U$$ be a universe and let $$V$$ be a universe strictly greater than $$U$$ . Then $\mathord {\textnormal {\textsf {R}}}_{\bullet }(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)):\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)/\mathord {\textnormal {\textsf {R}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))$ is $\mathbb {I}$ -categorically fibrant.

[0015] Sheaves on \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\)

[0015] Sheaves on $\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)$