Showing changes from revision #12 to #13:
Added | Removed | Changed
Let be a space (an object of a category of spaces), let be the category of sheaves on the frame of opens on , let denote the wide subcategory of with only étale morphisms. Then there is an adjoint equivalence
where
sends an étale morphism to the sheaf of local sections of .
sends a sheaf on to its espace étale.
We wish to clarify in which sense also the - topos can be regarded as an -sheaftopos on . One formulation of this is to show that is a locally representable structured -topos - and that the representation is exhibited by formally étale morphisms.
We assume that is the admissible class defined by an infinitesimal modality on .
(1) A -structure on an -topos is called universal if for every -topos composition with induces an equivalence of -categories if
where denotes the geometric morphisms with inverse image .
(2) In this case we say exhibits as classifying -topos for -structures on .
, , and are -structured -toposes.
The classifying topos for -structures is and the -toposes in question are linked with by geometric morphisms. We obtain the required structures as the image of
respectively for and in place of “H/X”.
Let be an -category. We have . A pro object in in is a formal limit of a cofiltered diagram in . A cofiltered diagram is defined to be a finite diagram having a cone (i.e. a family of natural transformation for all , where denotes the constant functor having value ). So we have
and the hom sets are
We have (more or less) synonyms:
pro object, cofiltered, having a cone
ind object, filtered, having a cocone
(1) A morphisms is called étale if (1a) the underlying geometric morphism of -toposes is étale and (1b) the induced map is an equivalence in
(2) Condition (1b) is equivalent to the requirement that is -cocartesian for the projection.
(3) Being an étale geometric morphism of structured -toposes is a local property:
If there is an effective epimorphism to the terminal object of , and in a morphism such that
is étale, then is étale.
Let be a structured U\in X$ be an object.
(1) The restriction of to is defined to be the slice .
(2) The restriction of to is defined to be composite
where is base change along .
Let be a morphism of geometries. Let the restriction functor.
(1) Then there is an adjunction
where the left adjoint is called a relative spectrum functor.
(2) Let now be the discrete geometry underlying . Then
is called absolute spectrum functor; here denotes the inclusion of the ind objects of .
A -structured (∞,1)-topos is called locally representable (aka a -scheme) if
such that
the cover in that the canonical morphism (with the terminal object of ) is an effective epimorphism;
for every there exists an equivalence
of structured -toposes for some (in the (∞,1)-category of pro-objects in ). In other words is assumed to be locally equivalent to an absolute spectrum (aka affine scheme) of a pro object in .
is locally representable. representable-structured -topos.
The terminal object in is the identity on . The collection of all formally étale effective epimorphisms (in ) with codomain covers and hence the cover in the slice. Since our chosen-structure is the identity the cover is preserved by it.
Let We know that be is an a element reflective- and coreflective subcategory of the cover; i.e. an formally étale effective epimorphism . (if not argue is leftexact, then an adjoint functor theorem implies that is coreflective subcat.). We think of being the reflector
Now Let we consider : be an element of the cover; i.e. a formally étale effective epimorphism. Since is a coreflective subcategory is a cover of .
Objects The of restriction are of cocones where is given by: is formally étale. Morphisms are pyramids with four faces and tip .
Pro objects in are cofiltered diagrams in or -equivalently filtered diagrams in
Objects of are cocones where is formally étale. Morphisms are pyramids with four faces and tip .
The restriction of the -structure is given as follows:
where is base change along . Pro objects in are cofiltered diagrams in or -equivalently filtered diagrams in