Equivalent formulations of the sheaf condition #
We give an equivalent formulation of the sheaf condition.
Given any indexed type ι, we define overlap ι,
a category with objects corresponding to
- individual open sets,
single i, and - intersections of pairs of open sets,
pair i j, with morphisms frompair i jto bothsingle iandsingle j.
Any open cover U : ι → opens X provides a functor diagram U : overlap ι ⥤ (opens X)ᵒᵖ.
There is a canonical cone over this functor, cone U, whose cone point is supr U,
and in fact this is a limit cone.
A presheaf F : presheaf C X is a sheaf precisely if it preserves this limit.
We express this in two equivalent ways, as
is_limit (F.map_cone (cone U)), orpreserves_limit (diagram U) F
We show that this sheaf condition is equivalent to the opens_le_cover sheaf condition, and
thereby also equivalent to the default sheaf condition.
An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
is_sheaf_iff_is_sheaf_pairwise_intersections).
A presheaf is a sheaf if F sends the cone (pairwise.cocone U).op to a limit cone.
(Recall pairwise.cocone U has cone point supr U, mapping down to the U i and the U i ⊓ U j.)
Instances For
An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections).
A presheaf is a sheaf if F preserves the limit of pairwise.diagram U.
(Recall pairwise.diagram U is the diagram consisting of the pairwise intersections
U i ⊓ U j mapping into the open sets U i. This diagram has limit supr U.)
Instances For
Implementation detail:
the object level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U
Instances For
Implementation detail:
the morphism level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U
Instances For
The category of single and double intersections of the U i maps into the category
of open sets below some U i.
Instances For
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.
Instances For
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.
Instances For
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 U i and U i ⊓ U j.
The sheaf condition in terms of an equalizer diagram is equivalent
to the reformulation in terms of the presheaf preserving the limit of the diagram
consisting of the U i and U i ⊓ U j.
For a sheaf F, F(U ⊔ V) is the pullback of F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V).
This is the pullback cone.
Instances For
(Implementation).
Every cone over F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V) factors through F(U ⊔ V).
Instances For
For a sheaf F, F(U ⊔ V) is the pullback of F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V).
Instances For
If U, V are disjoint, then F(U ⊔ V) = F(U) × F(V).
Instances For
F(U ⊔ V) is isomorphic to the eq_locus of the two maps F(U) × F(V) ⟶ F(U ⊓ V).