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 #
- This is the definition Lurie uses in Spectral Algebraic Geometry.
The category of open sets contained in some element of the cover.
Equations
- Top.presheaf.sheaf_condition.opens_le_cover U = {V // ∃ (i : ι), V ≤ U i}
Equations
- Top.presheaf.sheaf_condition.opens_le_cover.category_theory.category U = category_theory.full_subcategory (λ (V : topological_space.opens ↥X), ∃ (i : ι), V ≤ U i)
An arbitrarily chosen index such that V ≤ U i.
Equations
- V.index = Exists.some _
The morphism from V to U i for some i.
Equations
supr U as a cocone over the opens sets contained in some element of the cover.
(In fact this is a colimit cocone.)
Equations
- Top.presheaf.sheaf_condition.opens_le_cover_cocone U = {X := supr U, ι := {app := λ (V : Top.presheaf.sheaf_condition.opens_le_cover U), V.hom_to_index ≫ topological_space.opens.le_supr U V.index, naturality' := _}}
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
- F.is_sheaf_opens_le_cover = ∀ ⦃ι : Type v⦄ (U : ι → topological_space.opens ↥X), nonempty (category_theory.limits.is_limit (category_theory.functor.map_cone F (Top.presheaf.sheaf_condition.opens_le_cover_cocone U).op))
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
- Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_map U (category_theory.pairwise.hom.right i j) = category_theory.hom_of_le _
- Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_map U (category_theory.pairwise.hom.left i j) = category_theory.hom_of_le _
- Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_map U (category_theory.pairwise.hom.id_pair i j) = 𝟙 (Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_obj U (category_theory.pairwise.pair i j))
- Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_map U (category_theory.pairwise.hom.id_single i) = 𝟙 (Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_obj U (category_theory.pairwise.single i))
The category of single and double intersections of the U i maps into the category
of open sets below some U i.
Equations
- Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover U = {obj := Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_obj U, map := λ (V W : category_theory.pairwise ι) (i : V ⟶ W), Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover_map U i, map_id' := _, map_comp' := _}
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.
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
- Top.presheaf.sheaf_condition.pairwise_diagram_iso U = {hom := {app := λ (X_1 : category_theory.pairwise ι), X_1.cases_on (λ (i : ι), 𝟙 ((category_theory.pairwise.diagram U).obj (category_theory.pairwise.single i))) (λ (i j : ι), 𝟙 ((category_theory.pairwise.diagram U).obj (category_theory.pairwise.pair i j))), naturality' := _}, inv := {app := λ (X_1 : category_theory.pairwise ι), X_1.cases_on (λ (i : ι), 𝟙 ((Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover U ⋙ category_theory.full_subcategory_inclusion (λ (V : topological_space.opens ↥X), ∃ (i : ι), V ≤ U i)).obj (category_theory.pairwise.single i))) (λ (i j : ι), 𝟙 ((Top.presheaf.sheaf_condition.pairwise_to_opens_le_cover U ⋙ category_theory.full_subcategory_inclusion (λ (V : topological_space.opens ↥X), ∃ (i : ι), V ≤ U i)).obj (category_theory.pairwise.pair i j))), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
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.
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.
The sheaf condition in terms of an equalizer diagram is equivalent
to the reformulation in terms of a limit diagram over all { V : opens X // ∃ i, V ≤ U i }.