The sheaf condition in terms of sites. #
The theory of sheaves on sites was developed independently from sheaves on spaces in
category_theory/sites
. In this file, we connect the two theories: We show that for a topological
space X
, a presheaf F : (opens X)ᵒᵖ ⥤ C
is a sheaf on the site opens X
if and only if it is
a sheaf on X
in terms of is_sheaf_equalizer_products
.
Recall that a presheaf F : (opens X)ᵒᵖ ⥤ C
is called a sheaf on the space X
, if for every
family of opens U : ι → opens X
, the object F.obj (op (supr U))
is the limit of some fork
diagram. On the other hand, F
is called a sheaf on the site opens X
, if for every open set
U : opens X
and every presieve R : presieve U
, the object F.obj (op U)
is the limit of a
very similar fork diagram. In this file, we will construct the two functions covering_of_presieve
and presieve_of_covering
, which translate between the two concepts. We then prove a bunch of
naturality lemmas relating the two fork diagrams to each other.
Main statements #
is_sheaf_iff_is_sheaf_equalizer_products
. A presheafF : (opens X)ᵒᵖ ⥤ C
is a sheaf on the siteopens X
if and only if it is a sheaf on the spaceX
.
Given a presieve R
on U
, we obtain a covering family of open sets in X
, by taking as index
type the type of dependent pairs (V, f)
, where f : V ⟶ U
is in R
.
Equations
- Top.presheaf.covering_of_presieve U R = λ (f : Σ (V : topological_space.opens ↥X), {f // R f}), f.fst
In this section, we will relate two different fork diagrams to each other.
The first one is the defining fork diagram for the sheaf condition in terms of sites, applied to
the presieve R
. It will henceforth be called the sites diagram. Its objects are called
presheaf.first_obj
and presheaf.second_obj
and its morphisms are presheaf.first_map
and
presheaf.second_obj
. The fork map into this diagram is called presheaf.fork_map
.
The second one is the defining fork diagram for the sheaf condition in terms of spaces, applied to
the family of opens covering_of_presieve U R
. It will henceforth be called the spaces diagram.
Its objects are called pi_opens
and pi_inters
and its morphisms are left_res
and right_res
.
The fork map into this diagram is called res
.
If R
is a presieve in the grothendieck topology on opens X
, the covering family associated to
R
really is covering, i.e. the union of all open sets equals U
.
The first object in the sites diagram is isomorphic to the first object in the spaces diagram. Actually, they are even definitionally equal, but it is convenient to give this isomorphism a name.
The isomorphism first_obj_iso_pi_opens
is compatible with canonical projections out of the
product.
The second object in the sites diagram is isomorphic to the second object in the spaces diagram.
Equations
- Top.presheaf.covering_of_presieve.second_obj_iso_pi_inters F U R = category_theory.limits.has_limit.iso_of_nat_iso (category_theory.discrete.nat_iso (λ (i : category_theory.discrete ((Σ (V : topological_space.opens ↥X), {f // R f}) × Σ (W : topological_space.opens ↥X), {g // R g})), category_theory.functor.map_iso F (category_theory.eq_to_iso _).op))
The isomorphism second_obj_iso_pi_inters
is compatible with canonical projections out of the
product. Here, we have to insert an eq_to_hom
arrow to pass from
F.obj (op (pullback f.2.1 g.2.1))
to F.obj (op (f.1 ⊓ g.1))
.
Composing the fork map of the sites diagram with the isomorphism first_obj_iso_pi_opens
is the
same as the fork map of the spaces diagram (modulo an eq_to_hom
arrow).
First naturality condition. Under the isomorphisms first_obj_iso_pi_opens
and
second_obj_iso_pi_inters
, the map presheaf.first_map
corresponds to left_res
.
Second naturality condition. Under the isomorphisms first_obj_iso_pi_opens
and
second_obj_iso_pi_inters
, the map presheaf.second_map
corresponds to right_res
.
The natural isomorphism between the sites diagram and the spaces diagram.
Equations
Postcomposing the given fork of the sites diagram with the natural isomorphism between the diagrams gives us a fork of the spaces diagram. We construct a morphism from this fork to the given fork of the spaces diagram. This is shown to be an isomorphism below.
Equations
Instances for Top.presheaf.covering_of_presieve.postcompose_diagram_fork_hom
See postcompose_diagram_fork_hom
.
Given a family of opens U : ι → opens X
and any open Y : opens X
, we obtain a presieve
on Y
by declaring that a morphism f : V ⟶ Y
is a member of the presieve if and only if
there exists an index i : ι
such that V = U i
.
Equations
- Top.presheaf.presieve_of_covering_aux U Y = λ (V : topological_space.opens ↥X) (f : V ⟶ Y), ∃ (i : ι), V = U i
Take Y
to be supr U
and obtain a presieve over supr U
.
Equations
Given a presieve R
on Y
, if we take its associated family of opens via
covering_of_presieve
(which may not cover Y
if R
is not covering), and take
the presieve on Y
associated to the family of opens via presieve_of_covering_aux
,
then we get back the original presieve R
.
In this section, we will relate two different fork diagrams to each other.
The first one is the defining fork diagram for the sheaf condition in terms of spaces, applied to
the family of opens U
. It will henceforth be called the spaces diagram. Its objects are called
pi_opens
and pi_inters
and its morphisms are left_res
and right_res
. The fork map into this
diagram is called res
.
The second one is the defining fork diagram for the sheaf condition in terms of sites, applied to
the presieve presieve_of_covering U
. It will henceforth be called the sites diagram. Its objects
are called presheaf.first_obj
and presheaf.second_obj
and its morphisms are presheaf.first_map
and presheaf.second_obj
. The fork map into this diagram is called presheaf.fork_map
.
The sieve generated by presieve_of_covering U
is a member of the grothendieck topology.
An index i : ι
can be turned into a dependent pair (V, f)
, where V
is an open set and
f : V ⟶ supr U
is a member of presieve_of_covering U f
.
Equations
- Top.presheaf.presieve_of_covering.hom_of_index U i = ⟨U i, ⟨topological_space.opens.le_supr U i, _⟩⟩
By using the axiom of choice, a dependent pair (V, f)
where f : V ⟶ supr U
is a member of
presieve_of_covering U f
can be turned into an index i : ι
, such that V = U i
.
Equations
The canonical morphism from the first object in the sites diagram to the first object in the
spaces diagram. Note that this is not an isomorphism, as the product pi_opens F U
may contain
duplicate factors, i.e. U : ι → opens X
may not be injective.
Equations
- Top.presheaf.presieve_of_covering.first_obj_to_pi_opens F U = category_theory.limits.pi.lift (λ (i : ι), category_theory.limits.pi.π (λ (f : Σ (V : topological_space.opens ↥X), {f // Top.presheaf.presieve_of_covering U f}), F.obj (opposite.op f.fst)) (Top.presheaf.presieve_of_covering.hom_of_index U i))
The canonical morphism from the first object in the spaces diagram to the first object in the
sites diagram. Note that this is not an isomorphism, as the product pi_opens F U
may contain
duplicate factors, i.e. U : ι → opens X
may not be injective.
Equations
- Top.presheaf.presieve_of_covering.pi_opens_to_first_obj F U = category_theory.limits.pi.lift (λ (f : Σ (V : topological_space.opens ↥X), {f // Top.presheaf.presieve_of_covering U f}), category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) (Top.presheaf.presieve_of_covering.index_of_hom U f) ≫ F.map (category_theory.eq_to_hom _).op)
Even though first_obj_to_pi_opens
and pi_opens_to_first_obj
are not inverse to each other,
applying them both after a fork map s.ι
does nothing. The intuition here is that a compatible
family s : Π i : ι, F.obj (op (U i))
does not care about duplicate open sets:
If U i = U j
the compatible family coincides on the intersection U i ⊓ U j = U i = U j
,
hence s i = s j
(module an eq_to_hom
arrow).
The canonical morphism from the second object of the spaces diagram to the second object of the sites diagram.
Equations
- Top.presheaf.presieve_of_covering.pi_inters_to_second_obj F U = category_theory.limits.pi.lift (λ (f : (Σ (V : topological_space.opens ↥X), {f // Top.presheaf.presieve_of_covering U f}) × Σ (W : topological_space.opens ↥X), {g // Top.presheaf.presieve_of_covering U g}), category_theory.limits.pi.π (λ (p : ι × ι), F.obj (opposite.op (U p.fst ⊓ U p.snd))) (Top.presheaf.presieve_of_covering.index_of_hom U f.fst, Top.presheaf.presieve_of_covering.index_of_hom U f.snd) ≫ F.map (category_theory.eq_to_hom _).op)
The empty component of a sheaf is terminal
Equations
- F.is_terminal_of_empty = category_theory.Sheaf.is_terminal_of_bot_cover F ∅ Top.sheaf.is_terminal_of_empty._proof_1
A variant of is_terminal_of_empty
that is easier to apply
.
Equations
If a family B
of open sets forms a basis of the topology on X
, and if F'
is a sheaf on X
, then a homomorphism between a presheaf F
on X
and F'
is equivalent to a homomorphism between their restrictions to the indexing type
ι
of B
, with the induced category structure on ι
.