Coverings and sieves; from sheaves on sites and sheaves on spaces

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 TopologicalSpace.Opens is CoverDense, that open maps induce CoverPreserving functors, and that open embeddings induce CompatiblePreserving functors.

def TopCat.Presheaf.coveringOfPresieve {X : TopCat} (U : TopologicalSpace.Opens ↑X) (R : CategoryTheory.Presieve U) : (V : TopologicalSpace.Opens ↑X) × { f // R V f } → TopologicalSpace.Opens ↑X

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.

@[simp]

theorem TopCat.Presheaf.coveringOfPresieve_apply {X : TopCat} (U : TopologicalSpace.Opens ↑X) (R : CategoryTheory.Presieve U) (f : (V : TopologicalSpace.Opens ↑X) × { f // R V f }) : TopCat.Presheaf.coveringOfPresieve U R f = f.fst

theorem TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck {X : TopCat} (U : TopologicalSpace.Opens ↑X) (R : CategoryTheory.Presieve U) (hR : CategoryTheory.Sieve.generate R ∈ CategoryTheory.GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U) : iSup (TopCat.Presheaf.coveringOfPresieve U R) = U

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.

def TopCat.Presheaf.presieveOfCoveringAux {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) (Y : TopologicalSpace.Opens ↑X) : CategoryTheory.Presieve Y

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.

def TopCat.Presheaf.presieveOfCovering {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Presieve (iSup U)

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

@[simp]

theorem TopCat.Presheaf.covering_presieve_eq_self {X : TopCat} {Y : TopologicalSpace.Opens ↑X} (R : CategoryTheory.Presieve Y) : TopCat.Presheaf.presieveOfCoveringAux (TopCat.Presheaf.coveringOfPresieve Y R) Y = R

Given a presieve R on Y, if we take its associated family of opens via coveringOfPresieve (which may not cover Y if R is not covering), and take the presieve on Y associated to the family of opens via presieveOfCoveringAux, then we get back the original presieve R.

theorem TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCovering U) ∈ CategoryTheory.GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)

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

def TopCat.Presheaf.presieveOfCovering.homOfIndex {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) : (V : TopologicalSpace.Opens ↑X) × { f // TopCat.Presheaf.presieveOfCovering U f }

An index i : ι can be turned into a dependent pair (V, f), where V is an open set and f : V ⟶ iSup U is a member of presieveOfCovering U f.

def TopCat.Presheaf.presieveOfCovering.indexOfHom {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) (f : (V : TopologicalSpace.Opens ↑X) × { f // TopCat.Presheaf.presieveOfCovering U f }) : ι

By using the axiom of choice, a dependent pair (V, f) where f : V ⟶ iSup U is a member of presieveOfCovering U f can be turned into an index i : ι, such that V = U i.

theorem TopCat.Presheaf.presieveOfCovering.indexOfHom_spec {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X) (f : (V : TopologicalSpace.Opens ↑X) × { f // TopCat.Presheaf.presieveOfCovering U f }) : f.fst = U (TopCat.Presheaf.presieveOfCovering.indexOfHom U f)

theorem TopCat.Opens.coverDense_iff_isBasis {X : TopCat} {ι : Type u_1} [CategoryTheory.Category.{u_2, u_1} ι] (B : CategoryTheory.Functor ι (TopologicalSpace.Opens ↑X)) : CategoryTheory.CoverDense (Opens.grothendieckTopology ↑X) B ↔ TopologicalSpace.Opens.IsBasis (Set.range B.obj)

theorem TopCat.Opens.coverDense_inducedFunctor {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X} (h : TopologicalSpace.Opens.IsBasis (Set.range B)) : CategoryTheory.CoverDense (Opens.grothendieckTopology ↑X) (CategoryTheory.inducedFunctor B)

theorem OpenEmbedding.compatiblePreserving {X : TopCat} {Y : TopCat} {f : X ⟶ Y} (hf : OpenEmbedding ↑f) : CategoryTheory.CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ↑f))

theorem IsOpenMap.coverPreserving {X : TopCat} {Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ↑f) : CategoryTheory.CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor hf)

theorem TopCat.Presheaf.isSheaf_of_openEmbedding {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {F : TopCat.Presheaf C Y} (h : OpenEmbedding ↑f) (hF : TopCat.Presheaf.IsSheaf F) : TopCat.Presheaf.IsSheaf (CategoryTheory.Functor.comp (IsOpenMap.functor (_ : IsOpenMap ↑f)).op F)

def TopCat.Sheaf.isTerminalOfEmpty {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Sheaf C X) : CategoryTheory.Limits.IsTerminal (F.val.obj (Opposite.op ⊥))

The empty component of a sheaf is terminal.

def TopCat.Sheaf.isTerminalOfEqEmpty {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Sheaf C X) {U : TopologicalSpace.Opens ↑X} (h : U = ⊥) : CategoryTheory.Limits.IsTerminal (F.val.obj (Opposite.op U))

A variant of isTerminalOfEmpty that is easier to apply.

def TopCat.Sheaf.restrictHomEquivHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X} (F : TopCat.Presheaf C X) (F' : TopCat.Sheaf C X) (h : TopologicalSpace.Opens.IsBasis (Set.range B)) : (CategoryTheory.Functor.comp (CategoryTheory.inducedFunctor B).op F ⟶ CategoryTheory.Functor.comp (CategoryTheory.inducedFunctor B).op F'.val) ≃ (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 ι.

@[simp]

theorem TopCat.Sheaf.extend_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X} (F : TopCat.Presheaf C X) (F' : TopCat.Sheaf C X) (h : TopologicalSpace.Opens.IsBasis (Set.range B)) (α : CategoryTheory.Functor.comp (CategoryTheory.inducedFunctor B).op F ⟶ CategoryTheory.Functor.comp (CategoryTheory.inducedFunctor B).op F'.val) (i : ι) : (↑(TopCat.Sheaf.restrictHomEquivHom F F' h) α).app (Opposite.op (B i)) = α.app (Opposite.op i)

theorem TopCat.Sheaf.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X} (F : TopCat.Presheaf C X) (F' : TopCat.Sheaf C X) (h : TopologicalSpace.Opens.IsBasis (Set.range B)) {α : F ⟶ F'.val} {β : F ⟶ F'.val} (he : ∀ (i : ι), α.app (Opposite.op (B i)) = β.app (Opposite.op (B i))) : α = β