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 j
to bothsingle i
andsingle 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)
.