# mathlibdocumentation

topology.sheaves.sheaf_condition.sites

# 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 presheaf F : (opens X)ᵒᵖ ⥤ C is a sheaf on the site opens X if and only if it is a sheaf on the space X.
def Top.presheaf.covering_of_presieve {X : Top} (U : topological_space.opens X) (R : category_theory.presieve U) :
(Σ (V : , {f // R f})

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
• = λ (f : Σ (V : , {f // R f}), f.fst
@[simp]
theorem Top.presheaf.covering_of_presieve_apply {X : Top} (U : topological_space.opens X) (R : category_theory.presieve U) (f : Σ (V : , {f // R f}) :

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.

Equations
theorem Top.presheaf.covering_of_presieve.first_obj_iso_pi_opens_π {C : Type u} {X : Top} (F : X) (U : topological_space.opens X) (R : category_theory.presieve U) (f : Σ (V : , {f // R f}) :
category_theory.limits.pi.π (λ (i : Σ (V : , {f // R f}), F.obj (opposite.op i))) f = category_theory.limits.pi.π (λ (f : Σ (V : , {f // R f}), F.obj (opposite.op f.fst)) f

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
theorem Top.presheaf.covering_of_presieve.second_obj_iso_pi_inters_π {C : Type u} {X : Top} (F : X) (U : topological_space.opens X) (R : category_theory.presieve U) (f g : Σ (V : , {f // R f}) :
category_theory.limits.pi.π (λ (p : (Σ (V : , {f // R f}) × Σ (V : , {f // R f}), F.obj (opposite.op (f, g) = category_theory.limits.pi.π (λ (fg : (Σ (V : , {f // R f}) × Σ (W : , {g // R g}), F.obj (opposite.op fg.snd.snd.val))) (f, g)

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.

@[simp]
theorem Top.presheaf.covering_of_presieve.diagram_nat_iso_hom_app {C : Type u} {X : Top} (F : X) (U : topological_space.opens X) (R : category_theory.presieve U)  :
= (category_theory.limits.walking_parallel_pair.rec X_1).hom
@[simp]
theorem Top.presheaf.covering_of_presieve.diagram_nat_iso_inv_app {C : Type u} {X : Top} (F : X) (U : topological_space.opens X) (R : category_theory.presieve U)  :
= (category_theory.limits.walking_parallel_pair.rec X_1).inv
noncomputable def Top.presheaf.covering_of_presieve.diagram_nat_iso {C : Type u} {X : Top} (F : X) (U : topological_space.opens X) (R : category_theory.presieve U) :

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.

Equations
def Top.presheaf.presieve_of_covering_aux {X : Top} {ι : Type v} (U : ι → ) (Y : topological_space.opens X) :

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
• = λ (V : (f : V Y), ∃ (i : ι), V = U i
def Top.presheaf.presieve_of_covering {X : Top} {ι : Type v} (U : ι → ) :

Take Y to be supr U and obtain a presieve over supr U.

Equations
@[simp]

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.

theorem Top.presheaf.presieve_of_covering.mem_grothendieck_topology {X : Top} {ι : Type v} (U : ι → ) :

The sieve generated by presieve_of_covering U is a member of the grothendieck topology.

def Top.presheaf.presieve_of_covering.hom_of_index {X : Top} {ι : Type v} (U : ι → ) (i : ι) :
Σ (V : , {f //

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
noncomputable def Top.presheaf.presieve_of_covering.index_of_hom {X : Top} {ι : Type v} (U : ι → ) (f : Σ (V : , {f // ) :
ι

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
theorem Top.presheaf.presieve_of_covering.index_of_hom_spec {X : Top} {ι : Type v} (U : ι → ) (f : Σ (V : , {f // ) :
noncomputable def Top.presheaf.presieve_of_covering.first_obj_to_pi_opens {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :

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
noncomputable def Top.presheaf.presieve_of_covering.pi_opens_to_first_obj {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :

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

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).

noncomputable def Top.presheaf.presieve_of_covering.pi_inters_to_second_obj {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :

The canonical morphism from the second object of the spaces diagram to the second object of the sites diagram.

Equations
theorem Top.presheaf.presieve_of_covering.fork_map_comp_first_map_to_pi_opens_eq {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :
theorem Top.presheaf.presieve_of_covering.res_comp_pi_opens_to_first_obj_eq {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :
theorem Top.presheaf.is_sheaf_equalizer_products_of_is_sheaf {C : Type u} {X : Top} (F : X) (Fsh : F.is_sheaf) :
theorem Top.presheaf.is_sheaf_iff_is_sheaf_equalizer_products {C : Type u} {X : Top} (F : X) :
theorem Top.opens.cover_dense_iff_is_basis {X : Top} {ι : Type u_2} (B : ι ) :
theorem Top.opens.cover_dense_induced_functor {X : Top} {ι : Type u_2} {B : ι → }  :
noncomputable def Top.sheaf.is_terminal_of_empty {C : Type u} {X : Top} (F : X) :

The empty component of a sheaf is terminal

Equations
noncomputable def Top.sheaf.is_terminal_of_eq_empty {C : Type u} {X : Top} (F : X) {U : topological_space.opens X} (h : U = ) :

A variant of is_terminal_of_empty that is easier to apply.

Equations
noncomputable def Top.sheaf.restrict_hom_equiv_hom {C : Type u} {X : Top} {ι : Type u_1} {B : ι → } (F : X) (F' : X)  :
(F F'.val)

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 ι.

Equations
@[simp]
theorem Top.sheaf.extend_hom_app {C : Type u} {X : Top} {ι : Type u_1} {B : ι → } (F : X) (F' : X) (α : ) (i : ι) :
( h) α).app (opposite.op (B i)) = α.app (opposite.op i)
theorem Top.sheaf.hom_ext {C : Type u} {X : Top} {ι : Type u_1} {B : ι → } (F : X) (F' : X) {α β : F F'.val} (he : ∀ (i : ι), α.app (opposite.op (B i)) = β.app (opposite.op (B i))) :
α = β