Coverings and sieves; from sheaves on sites and sheaves on spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we connect coverings in a topological space to sieves in the associated Grothendieck topology, in preparation of connecting the sheaf condition on sites to the various sheaf conditions on spaces.
We also specialize results about sheaves on sites to sheaves on spaces; we show that the inclusion
functor from a topological basis to topological_space.opens is cover_dense, that open maps
induce cover_preserving functors, and that open embeddings induce compatible_preserving functors.
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
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.
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.
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 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 ι.