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 iSup 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).
Main statement #
TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover: for a presheaf on a topological space,
the sheaf condition in terms of Grothendieck topology is equivalent to the OpensLeCover
sheaf condition. This result will be used to further connect to other sheaf conditions on spaces,
like pairwise_intersections and equalizer_products.
References #
- This is the definition Lurie uses in Spectral Algebraic Geometry.
The category of open sets contained in some element of the cover.
Equations
- TopCat.Presheaf.SheafCondition.OpensLeCover U = CategoryTheory.FullSubcategory fun (V : TopologicalSpace.Opens ↑X) => ∃ (i : ι), V ≤ U i
Instances For
Equations
- TopCat.Presheaf.SheafCondition.instCategoryOpensLeCover U = CategoryTheory.FullSubcategory.category fun (V : TopologicalSpace.Opens ↑X) => ∃ (i : ι), V ≤ U i
Equations
- TopCat.Presheaf.SheafCondition.instInhabitedOpensLeCoverOfNonempty U = { default := { obj := ⊥, property := ⋯ } }
An arbitrarily chosen index such that V ≤ U i.
Equations
- V.index = ⋯.choose
Instances For
The morphism from V to U i for some i.
Equations
- V.homToIndex = ⋯.hom
Instances For
iSup U as a cocone over the opens sets contained in some element of the cover.
(In fact this is a colimit cocone.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
An equivalent formulation of the sheaf condition
(which we prove equivalent to the usual one below as
isSheaf_iff_isSheafOpensLeCover).
A presheaf is a sheaf if F sends the cone (opensLeCoverCocone U).op to a limit cone.
(Recall opensLeCoverCocone U, has cone point iSup U,
mapping down to any V which is contained in some U i.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 OpensLeCover U, the (poset)
category of opens contained in some U i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 OpensLeCover U, the (poset)
category of opens contained in some U i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 OpensLeCover U, the (poset)
category of opens contained in some U i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a family of opens opensLeCoverCocone 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
- F.whiskerIsoMapGenerateCocone U hY = { hom := { hom := F.map (CategoryTheory.eqToHom ⋯), w := ⋯ }, inv := { hom := F.map (CategoryTheory.eqToHom ⋯), w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
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.IsSheafOpensLeCover 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
- One or more equations did not get rendered due to their size.
Instances For
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
- F.isLimitOpensLeEquivGenerate₂ R hR = ⋯.mpr (F.isLimitOpensLeEquivGenerate₁ (TopCat.Presheaf.coveringOfPresieve Y R) ⋯)
Instances For
A presheaf (opens X)ᵒᵖ ⥤ C on a topological space X is a sheaf on the site opens X iff
it satisfies the IsSheafOpensLeCover 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.