mathlib documentation

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 #

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

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

The isomorphism first_obj_iso_pi_opens is compatible with canonical projections out of the product.

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

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

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

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.

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

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

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

The empty component of a sheaf is terminal

Equations

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

Equations
theorem Top.sheaf.hom_ext {C : Type u} [category_theory.category C] {X : Top} {ι : Type u_1} {B : ι → topological_space.opens X} (F : Top.presheaf C X) (F' : Top.sheaf C X) (h : topological_space.opens.is_basis (set.range B)) {α β : F F'.val} (he : ∀ (i : ι), α.app (opposite.op (B i)) = β.app (opposite.op (B i))) :
α = β