# mathlibdocumentation

topology.sheaves.sheaf_condition.opens_le_cover

# Another version of the sheaf condition. #

Given a family of open sets U : ι → opens X we can form the subcategory { V : opens X // ∃ i, V ≤ U i }, which has supr U as a cocone.

The sheaf condition on a presheaf F is equivalent to F sending the opposite of this cocone to a limit cone in C, for every U.

This condition is particularly nice when checking the sheaf condition because we don't need to do any case bashing (depending on whether we're looking at single or double intersections, or equivalently whether we're looking at the first or second object in an equalizer diagram).

## References #

def Top.presheaf.sheaf_condition.opens_le_cover {X : Top} {ι : Type w} (U : ι → ) :
Type w

The category of open sets contained in some element of the cover.

Equations
Instances for Top.presheaf.sheaf_condition.opens_le_cover
@[protected, instance]
def Top.presheaf.sheaf_condition.opens_le_cover.category {X : Top} {ι : Type w} (U : ι → ) :
@[protected, instance]
def Top.presheaf.sheaf_condition.opens_le_cover.inhabited {X : Top} {ι : Type w} (U : ι → ) [inhabited ι] :
Equations
noncomputable def Top.presheaf.sheaf_condition.opens_le_cover.index {X : Top} {ι : Type w} {U : ι → }  :
ι

An arbitrarily chosen index such that V ≤ U i.

Equations
noncomputable def Top.presheaf.sheaf_condition.opens_le_cover.hom_to_index {X : Top} {ι : Type w} {U : ι → }  :
V.obj U V.index

The morphism from V to U i for some i.

Equations
noncomputable def Top.presheaf.sheaf_condition.opens_le_cover_cocone {X : Top} {ι : Type w} (U : ι → ) :

supr U as a cocone over the opens sets contained in some element of the cover.

(In fact this is a colimit cocone.)

Equations
def Top.presheaf.is_sheaf_opens_le_cover {C : Type u} {X : Top} (F : X) :
Prop

An equivalent formulation of the sheaf condition (which we prove equivalent to the usual one below as is_sheaf_iff_is_sheaf_opens_le_cover).

A presheaf is a sheaf if F sends the cone (opens_le_cover_cocone U).op to a limit cone. (Recall opens_le_cover_cocone U, has cone point supr U, mapping down to any V which is contained in some U i.)

Equations
@[simp]
def Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_obj {X : Top} {ι : Type w} (U : ι → ) :

Implementation detail: the object level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U

Equations

Implementation detail: the morphism level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U

Equations
@[simp]
theorem Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_map_2 {X : Top} {ι : Type w} (U : ι → ) (V W : category_theory.pairwise ι) (i : V W) :
def Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover {X : Top} {ι : Type w} (U : ι → ) :

The category of single and double intersections of the U i maps into the category of open sets below some U i.

Equations
Instances for Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover
@[simp]
theorem Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_obj_2 {X : Top} {ι : Type w} (U : ι → ) (ᾰ : category_theory.pairwise ι) :
@[protected, instance]
@[protected, instance]

The diagram consisting of the U i and U i ⊓ U j is cofinal in the diagram of all opens contained in some U i.

def Top.presheaf.sheaf_condition.pairwise_diagram_iso {X : Top} {ι : Type w} (U : ι → ) :

The diagram in opens X indexed by pairwise intersections from U is isomorphic (in fact, equal) to the diagram factored through opens_le_cover U.

Equations

The cocone pairwise.cocone U with cocone point supr U over pairwise.diagram U is isomorphic to the cocone opens_le_cover_cocone U (with the same cocone point) after appropriate whiskering and postcomposition.

Equations

The sheaf condition in terms of a limit diagram over all { V : opens X // ∃ i, V ≤ U i } is equivalent to the reformulation in terms of a limit diagram over U i and U i ⊓ U j.

@[simp]
theorem Top.presheaf.generate_equivalence_opens_le_functor_obj_obj {X : Top} {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) (f : category_theory.full_subcategory (λ (f : , ) :
@[simp]
theorem Top.presheaf.generate_equivalence_opens_le_inverse_obj_obj {X : Top} {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U)  :
def Top.presheaf.generate_equivalence_opens_le {X : Top} {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) :

Given a family of opens U and an open Y equal to the union of opens in U, we may take the presieve on Y associated to U and the sieve generated by it, and form the full subcategory (subposet) of opens contained in Y (over Y) consisting of arrows in the sieve. This full subcategory is equivalent to opens_le_cover U, the (poset) category of opens contained in some U i.

Equations
@[simp]
theorem Top.presheaf.generate_equivalence_opens_le_counit_iso {X : Top} {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) :
@[simp]
theorem Top.presheaf.generate_equivalence_opens_le_functor_map {X : Top} {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) (_x _x_1 : category_theory.full_subcategory (λ (f : , ) (g : _x _x_1) :
@[simp]
theorem Top.presheaf.generate_equivalence_opens_le_inverse_map {X : Top} {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) (_x _x_1 : Top.presheaf.sheaf_condition.opens_le_cover U) (g : _x _x_1) :
@[simp]
theorem Top.presheaf.generate_equivalence_opens_le_unit_iso {X : Top} {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) :
@[simp]
theorem Top.presheaf.whisker_iso_map_generate_cocone_inv_hom {C : Type u} {X : Top} (F : X) {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) :
hY).inv.hom =
noncomputable def Top.presheaf.whisker_iso_map_generate_cocone {C : Type u} {X : Top} (F : X) {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) :

Given a family of opens opens_le_cover_cocone U is essentially the natural cocone associated to the sieve generated by the presieve associated to U with indexing category changed using the above equivalence.

Equations
@[simp]
theorem Top.presheaf.whisker_iso_map_generate_cocone_hom_hom {C : Type u} {X : Top} (F : X) {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) :
hY).hom.hom =
noncomputable def Top.presheaf.is_limit_opens_le_equiv_generate₁ {C : Type u} {X : Top} (F : X) {ι : Type w} (U : ι → ) {Y : topological_space.opens X} (hY : Y = supr U) :

Given a presheaf F on the topological space X and a family of opens U of X, the natural cone associated to F and U used in the definition of F.is_sheaf_opens_le_cover is a limit cone iff the natural cone associated to F and the sieve generated by the presieve associated to U is a limit cone.

Equations
noncomputable def Top.presheaf.is_limit_opens_le_equiv_generate₂ {C : Type u} {X : Top} (F : X) {Y : topological_space.opens X} (R : category_theory.presieve Y)  :

Given a presheaf F on the topological space X and a presieve R whose generated sieve is covering for the associated Grothendieck topology (equivalently, the presieve is covering for the associated pretopology), the natural cone associated to F and the family of opens associated to R is a limit cone iff the natural cone associated to F and the generated sieve is a limit cone. Since only the existence of a 1-1 correspondence will be used, the exact definition does not matter, so tactics are used liberally.

Equations
theorem Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover {C : Type u} {X : Top} (F : X) :

A presheaf (opens X)ᵒᵖ ⥤ C on a topological space X is a sheaf on the site opens X iff it satisfies the is_sheaf_opens_le_cover sheaf condition. The latter is not the official definition of sheaves on spaces, but has the advantage that it does not require has_products C.