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 OpensLeCover 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
isSheaf_iff_isSheafPairwiseIntersections).
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.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
isSheaf_iff_isSheafPreservesLimitPairwiseIntersections).
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.)
Equations
- F.IsSheafPreservesLimitPairwiseIntersections = ∀ ⦃ι : Type w⦄ (U : ι → TopologicalSpace.Opens ↑X), Nonempty (CategoryTheory.Limits.PreservesLimit (CategoryTheory.Pairwise.diagram U).op F)
Instances For
Implementation detail:
the object level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation detail:
the morphism level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U
Equations
- One or more equations did not get rendered due to their size.
Instances For
The category of single and double intersections of the U i maps into the category
of open sets below some U i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
The diagram in opens X indexed by pairwise intersections from U is isomorphic
(in fact, equal) to the diagram factored through OpensLeCover U.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cocone Pairwise.cocone U with cocone point supr U over Pairwise.diagram U is isomorphic
to the cocone opensLeCoverCocone U (with the same cocone point)
after appropriate whiskering and postcomposition.
Equations
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.
Equations
- F.interUnionPullbackCone U V = CategoryTheory.Limits.PullbackCone.mk (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op) ⋯
Instances For
(Implementation).
Every cone over F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V) factors through F(U ⊔ V).
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a sheaf F, F(U ⊔ V) is the pullback of F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V).
Equations
- One or more equations did not get rendered due to their size.
Instances For
If U, V are disjoint, then F(U ⊔ V) = F(U) × F(V).
Equations
- One or more equations did not get rendered due to their size.
Instances For
F(U ⊔ V) is isomorphic to the eq_locus of the two maps F(U) × F(V) ⟶ F(U ⊓ V).
Equations
- One or more equations did not get rendered due to their size.