The sheaf condition for a presieve #
We define what it means for a presheaf P : Cᵒᵖ ⥤ Type v
to be a sheaf for a particular
presieve R
on X
:
- A family of elements
x
forP
atR
is an elementx_f
ofP Y
for everyf : Y ⟶ X
inR
. SeeFamilyOfElements
. - The family
x
is compatible if, for anyf₁ : Y₁ ⟶ X
andf₂ : Y₂ ⟶ X
both inR
, and anyg₁ : Z ⟶ Y₁
andg₂ : Z ⟶ Y₂
such thatg₁ ≫ f₁ = g₂ ≫ f₂
, the restriction ofx_f₁
alongg₁
agrees with the restriction ofx_f₂
alongg₂
. SeeFamilyOfElements.Compatible
. - An amalgamation
t
for the family is an element ofP X
such that for everyf : Y ⟶ X
inR
, the restriction oft
onf
isx_f
. SeeFamilyOfElements.IsAmalgamation
. We then sayP
is separated forR
if every compatible family has at most one amalgamation, and it is a sheaf forR
if every compatible family has a unique amalgamation. SeeIsSeparatedFor
andIsSheafFor
.
In the special case where R
is a sieve, the compatibility condition can be simplified:
- The family
x
is compatible if, for anyf : Y ⟶ X
inR
andg : Z ⟶ Y
, the restriction ofx_f
alongg
agrees withx_(g ≫ f)
(which is well defined sinceg ≫ f
is inR
). SeeFamilyOfElements.SieveCompatible
andcompatible_iff_sieveCompatible
.
In the special case where C
has pullbacks, the compatibility condition can be simplified:
- The family
x
is compatible if, for anyf : Y ⟶ X
andg : Z ⟶ X
both inR
, the restriction ofx_f
alongπ₁ : pullback f g ⟶ Y
agrees with the restriction ofx_g
alongπ₂ : pullback f g ⟶ Z
. SeeFamilyOfElements.PullbackCompatible
andpullbackCompatible_iff
.
We also provide equivalent conditions to satisfy alternate definitions given in the literature.
Stacks: The condition of https://stacks.math.columbia.edu/tag/00Z8 is virtually identical to the statement of
isSheafFor_iff_yonedaSheafCondition
(since the bijection described there carries the same information as the unique existence.)Maclane-Moerdijk [MLM92]: Using
compatible_iff_sieveCompatible
, the definitions ofIsSheaf
are equivalent. There are also alternate definitions given:- Yoneda condition: Defined in
yonedaSheafCondition
and equivalence inisSheafFor_iff_yonedaSheafCondition
. - Matching family for presieves with pullback:
pullbackCompatible_iff
.
- Yoneda condition: Defined in
Implementation #
The sheaf condition is given as a proposition, rather than a subsingleton in Type (max u₁ v)
.
This doesn't seem to make a big difference, other than making a couple of definitions noncomputable,
but it means that equivalent conditions can be given as ↔
statements rather than ≃
statements,
which can be convenient.
References #
- [MLM92]: Sheaves in geometry and logic, Saunders MacLane, and Ieke Moerdijk: Chapter III, Section 4.
- [Joh02]: Sketches of an Elephant, P. T. Johnstone: C2.1.
- https://stacks.math.columbia.edu/tag/00VL (sheaves on a pretopology or site)
- https://stacks.math.columbia.edu/tag/00ZB (sheaves on a topology)
A family of elements for a presheaf P
given a collection of arrows R
with fixed codomain X
consists of an element of P Y
for every f : Y ⟶ X
in R
.
A presheaf is a sheaf (resp, separated) if every compatible family of elements has exactly one
(resp, at most one) amalgamation.
This data is referred to as a family
in [MLM92], Chapter III, Section 4. It is also a concrete
version of the elements of the middle object in https://stacks.math.columbia.edu/tag/00VM which is
more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Joh02].
Equations
- CategoryTheory.Presieve.FamilyOfElements P R = (⦃Y : C⦄ → (f : Y ⟶ X) → R f → P.obj (Opposite.op Y))
Instances For
A family of elements for a presheaf on the presieve R₂
can be restricted to a smaller presieve
R₁
.
Equations
- CategoryTheory.Presieve.FamilyOfElements.restrict h x✝ f hf = x✝ f ⋯
Instances For
The image of a family of elements by a morphism of presheaves.
Equations
- p.map φ f hf = φ.app (Opposite.op x) (p f hf)
Instances For
A family of elements for the arrow set R
is compatible if for any f₁ : Y₁ ⟶ X
and
f₂ : Y₂ ⟶ X
in R
, and any g₁ : Z ⟶ Y₁
and g₂ : Z ⟶ Y₂
, if the square g₁ ≫ f₁ = g₂ ≫ f₂
commutes then the elements of P Z
obtained by restricting the element of P Y₁
along g₁
and
restricting the element of P Y₂
along g₂
are the same.
In special cases, this condition can be simplified, see pullbackCompatible_iff
and
compatible_iff_sieveCompatible
.
This is referred to as a "compatible family" in Definition C2.1.2 of [Joh02], and on nlab: https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents
For a more explicit version in the case where R
is of the form Presieve.ofArrows
, see
CategoryTheory.Presieve.Arrows.Compatible
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If the category C
has pullbacks, this is an alternative condition for a family of elements to be
compatible: For any f : Y ⟶ X
and g : Z ⟶ X
in the presieve R
, the restriction of the
given elements for f
and g
to the pullback agree.
This is equivalent to being compatible (provided C
has pullbacks), shown in
pullbackCompatible_iff
.
This is the definition for a "matching" family given in [MLM92], Chapter III, Section 4,
Equation (5). Viewing the type FamilyOfElements
as the middle object of the fork in
https://stacks.math.columbia.edu/tag/00VM, this condition expresses that pr₀* (x) = pr₁* (x)
,
using the notation defined there.
For a more explicit version in the case where R
is of the form Presieve.ofArrows
, see
CategoryTheory.Presieve.Arrows.PullbackCompatible
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The restriction of a compatible family is compatible.
Extend a family of elements to the sieve generated by an arrow set. This is the construction described as "easy" in Lemma C2.1.3 of [Joh02].
Equations
- x✝¹.sieveExtend x hf = P.map ⋯.choose.op (x✝¹ ⋯.choose ⋯)
Instances For
The extension of a compatible family to the generated sieve is compatible.
The extension of a family agrees with the original family.
The restriction of an extension is the original.
If the arrow set for a family of elements is actually a sieve (i.e. it is downward closed) then the
consistency condition can be simplified.
This is an equivalent condition, see compatible_iff_sieveCompatible
.
This is the notion of "matching" given for families on sieves given in [MLM92], Chapter III, Section 4, Equation 1, and nlab: https://ncatlab.org/nlab/show/matching+family. See also the discussion before Lemma C2.1.4 of [Joh02].
Equations
- x.SieveCompatible = ∀ ⦃Y Z : C⦄ (f : Y ⟶ X) (g : Z ⟶ Y) (hf : S.arrows f), x (CategoryTheory.CategoryStruct.comp g f) ⋯ = P.map g.op (x f hf)
Instances For
Given a family of elements x
for the sieve S
generated by a presieve R
, if x
is restricted
to R
and then extended back up to S
, the resulting extension equals x
.
Two compatible families on the sieve generated by a presieve R
are equal if and only if they are
equal when restricted to R
.
Compatible families of elements for a presheaf of types P
and a presieve R
are in 1-1 correspondence with compatible families for the same presheaf and
the sieve generated by R
, through extension and restriction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a family of elements of a sieve S
on F(X)
, we can realize it as a family of elements of
S.functorPullback F
.
Equations
- CategoryTheory.Presieve.FamilyOfElements.functorPullback F x✝ f hf = x✝ (F.map f) hf
Instances For
Given a family of elements of a sieve S
on X
whose values factors through F
, we can
realize it as a family of elements of S.functorPushforward F
. Since the preimage is obtained by
choice, this is not well-defined generally.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a family of elements of a sieve S
on X
, and a map Y ⟶ X
, we can obtain a
family of elements of S.pullback f
by taking the same elements.
Equations
- CategoryTheory.Presieve.FamilyOfElements.pullback f x✝ g hg = x✝ (CategoryTheory.CategoryStruct.comp g f) hg
Instances For
Given a morphism of presheaves f : P ⟶ Q
, we can take a family of elements valued in P
to a
family of elements valued in Q
by composing with f
.
Equations
- CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x g hg = f.app (Opposite.op Y) (x g hg)
Instances For
The given element t
of P.obj (op X)
is an amalgamation for the family of elements x
if every
restriction P.map f.op t = x_f
for every arrow f
in the presieve R
.
This is the definition given in https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents, and https://ncatlab.org/nlab/show/matching+family, as well as [MLM92], Chapter III, Section 4, equation (2).
Instances For
A presheaf is separated for a presieve if there is at most one amalgamation.
Equations
- CategoryTheory.Presieve.IsSeparatedFor P R = ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R) (t₁ t₂ : P.obj (Opposite.op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Instances For
We define P
to be a sheaf for the presieve R
if every compatible family has a unique
amalgamation.
This is the definition of a sheaf for the given presieve given in C2.1.2 of [Joh02], and
https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents.
Using compatible_iff_sieveCompatible
,
this is equivalent to the definition of a sheaf in [MLM92], Chapter III, Section 4.
Equations
- CategoryTheory.Presieve.IsSheafFor P R = ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃! t : P.obj (Opposite.op X), x.IsAmalgamation t
Instances For
This is an equivalent condition to be a sheaf, which is useful for the abstraction to local
operators on elementary toposes. However this definition is defined only for sieves, not presieves.
The equivalence between this and IsSheafFor
is given in isSheafFor_iff_yonedaSheafCondition
.
This version is also useful to establish that being a sheaf is preserved under isomorphism of
presheaves.
See the discussion before Equation (3) of [MLM92], Chapter III, Section 4. See also C2.1.4 of [Joh02]. This is also a direct reformulation of https://stacks.math.columbia.edu/tag/00Z8.
Equations
- CategoryTheory.Presieve.YonedaSheafCondition P S = ∀ (f : S.functor ⟶ P), ∃! g : CategoryTheory.yoneda.obj X ⟶ P, CategoryTheory.CategoryStruct.comp S.functorInclusion g = f
Instances For
(Implementation). This is a (primarily internal) equivalence between natural transformations and compatible families.
Cf the discussion after Lemma 7.47.10 in https://stacks.math.columbia.edu/tag/00YW. See also the proof of C2.1.4 of [Joh02], and the discussion in [MLM92], Chapter III, Section 4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Implementation). A lemma useful to prove isSheafFor_iff_yonedaSheafCondition
.
The yoneda version of the sheaf condition is equivalent to the sheaf condition.
C2.1.4 of [Joh02].
If P
is a sheaf for the sieve S
on X
, a natural transformation from S
(viewed as a functor)
to P
can be (uniquely) extended to all of yoneda.obj X
.
f
S → P ↓ ↗ yX
Equations
- h.extend f = ⋯.choose
Instances For
Show that the extension of f : S.functor ⟶ P
to all of yoneda.obj X
is in fact an extension, ie
that the triangle below commutes, provided P
is a sheaf for S
f
S → P ↓ ↗ yX
The extension of f
to yoneda.obj X
is unique.
If P
is a sheaf for the sieve S
on X
, then if two natural transformations from yoneda.obj X
to P
agree when restricted to the subfunctor given by S
, they are equal.
P
is a sheaf for R
iff it is separated for R
and there exists an amalgamation.
If P
is separated for R
and every family has an amalgamation, then P
is a sheaf for R
.
If P
is a sheaf for R
, it is separated for R
.
Get the amalgamation of the given compatible family, provided we have a sheaf.
Equations
- t.amalgamate x hx = ⋯.choose
Instances For
C2.1.3 in [Joh02]
Every presheaf is a sheaf for the family {𝟙 X}.
[Joh02] C2.1.5(i)
Every presheaf is a sheaf for the maximal sieve.
[Joh02] C2.1.5(ii)
If P
is a sheaf for S
, and it is iso to P'
, then P'
is a sheaf for S
. This shows that
"being a sheaf for a presieve" is a mathematical or hygienic property.
If a presieve R
on X
has a subsieve S
such that:
P
is a sheaf forS
.- For every
f
inR
,P
is separated for the pullback ofS
alongf
,
then P
is a sheaf for R
.
This is closely related to [Joh02] C2.1.6(i).
If P
is a sheaf for every pullback of the sieve S
, then P
is a sheaf for any presieve which
contains S
.
This is closely related to [Joh02] C2.1.6.
A more explicit version of FamilyOfElements.Compatible
for a Presieve.ofArrows
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A FamilyOfElements
associated to an explicit family of elements.
Equations
- hx.familyOfElements = ⋯.choose
Instances For
A more explicit version of FamilyOfElements.PullbackCompatible
for a Presieve.ofArrows
.
Equations
- One or more equations did not get rendered due to their size.