The sheaf condition in terms of unique gluings #
We provide an alternative formulation of the sheaf condition in terms of unique gluings.
We work with sheaves valued in a concrete category C admitting all limits, whose forgetful
functor C ⥤ Type preserves limits and reflects isomorphisms. The usual categories of algebraic
structures, such as MonCat, AddCommGrp, RingCat, CommRingCat etc. are all examples of
this kind of category.
A presheaf F : Presheaf C X satisfies the sheaf condition if and only if, for every
compatible family of sections sf : Π i : ι, F.obj (op (U i)), there exists a unique gluing
s : F.obj (op (iSup U)).
Here, the family sf is called compatible, if for all i j : ι, the restrictions of sf i
and sf j to U i ⊓ U j agree. A section s : F.obj (op (iSup U)) is a gluing for the
family sf, if s restricts to sf i on U i for all i : ι
We show that the sheaf condition in terms of unique gluings is equivalent to the definition
in terms of pairwise intersections. Our approach is as follows: First, we show them to be equivalent
for Type-valued presheaves. Then we use that composing a presheaf with a limit-preserving and
isomorphism-reflecting functor leaves the sheaf condition invariant, as shown in
Mathlib/Topology/Sheaves/Forget.lean.
A family of sections sf is compatible, if the restrictions of sf i and sf j to U i ⊓ U j
agree, for all i and j
Equations
Instances For
A section s is a gluing for a family of sections sf if it restricts to sf i on U i,
for all i
Equations
- F.IsGluing U sf s = ∀ (i : ι), (F.map (TopologicalSpace.Opens.leSupr U i).op) s = sf i
Instances For
The sheaf condition in terms of unique gluings. A presheaf F : Presheaf C X satisfies this sheaf
condition if and only if, for every compatible family of sections sf : Π i : ι, F.obj (op (U i)),
there exists a unique gluing s : F.obj (op (iSup U)).
We prove this to be equivalent to the usual one below in
TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given sections over a family of open sets, extend it to include sections over pairwise intersections of the open sets.
Equations
- TopCat.Presheaf.objPairwiseOfFamily sf (Opposite.op (CategoryTheory.Pairwise.single i)) = sf i
- TopCat.Presheaf.objPairwiseOfFamily sf (Opposite.op (CategoryTheory.Pairwise.pair i j)) = F.map ((U i).infLELeft (U j)).op (sf i)
Instances For
Given a compatible family of sections over open sets, extend it to a
section of the functor (Pairwise.diagram U).op ⋙ F.
Equations
- h.sectionPairwise = ⟨TopCat.Presheaf.objPairwiseOfFamily sf, ⋯⟩
Instances For
For type-valued presheaves, the sheaf condition in terms of unique gluings is equivalent to the usual sheaf condition.
The usual sheaf condition can be obtained from the sheaf condition in terms of unique gluings.
For presheaves valued in a concrete category, whose forgetful functor reflects isomorphisms and preserves limits, the sheaf condition in terms of unique gluings is equivalent to the usual one.
A more convenient way of obtaining a unique gluing of sections for a sheaf.
In this version of the lemma, the inclusion homs iUV can be specified directly by the user,
which can be more convenient in practice.
In this version of the lemma, the inclusion homs iUV can be specified directly by the user,
which can be more convenient in practice.