Sheaves of types on a Grothendieck topology #
Defines the notion of a sheaf of types (usually called a sheaf of sets by mathematicians) on a category equipped with a Grothendieck topology, as well as a range of equivalent conditions useful in different situations.
First 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
. Seefamily_of_elements
. - 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₂
. Seefamily_of_elements.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
. Seefamily_of_elements.is_amalgamation
. 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. Seeis_separated_for
andis_sheaf_for
.
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
). Seefamily_of_elements.sieve_compatible
andcompatible_iff_sieve_compatible
.
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
. Seefamily_of_elements.pullback_compatible
andpullback_compatible_iff
.
Now given a Grothendieck topology J
, P
is a sheaf if it is a sheaf for every sieve in the
topology. See is_sheaf
.
In the case where the topology is generated by a basis, it suffices to check P
is a sheaf for
every presieve in the pretopology. See is_sheaf_pretopology
.
We also provide equivalent conditions to satisfy alternate definitions given in the literature.
-
Stacks: In
equalizer.presieve.sheaf_condition
, the sheaf condition at a presieve is shown to be equivalent to that of https://stacks.math.columbia.edu/tag/00VM (and combined withis_sheaf_pretopology
, this shows the notions ofis_sheaf
are exactly equivalent.)The condition of https://stacks.math.columbia.edu/tag/00Z8 is virtually identical to the statement of
yoneda_condition_iff_sheaf_condition
(since the bijection described there carries the same information as the unique existence.) -
Maclane-Moerdijk [MM92]: Using
compatible_iff_sieve_compatible
, the definitions ofis_sheaf
are equivalent. There are also alternate definitions given:- Yoneda condition: Defined in
yoneda_sheaf_condition
and equivalence inyoneda_condition_iff_sheaf_condition
. - Equalizer condition (Equation 3): Defined in the
equalizer.sieve
namespace, and equivalence inequalizer.sieve.sheaf_condition
. - Matching family for presieves with pullback:
pullback_compatible_iff
. - Sheaf for a pretopology (Prop 1):
is_sheaf_pretopology
combined with the previous. - Sheaf for a pretopology as equalizer (Prop 1, bis):
equalizer.presieve.sheaf_condition
combined with the previous.
- 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 #
- [MM92]: 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 [MM92], 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
- category_theory.presieve.family_of_elements P R = Π ⦃Y : C⦄ (f : Y ⟶ X), R f → P.obj (opposite.op Y)
Instances for category_theory.presieve.family_of_elements
Equations
- category_theory.presieve.family_of_elements.inhabited = {default := λ (Y : C) (f : Y ⟶ X), false.elim}
A family of elements for a presheaf on the presieve R₂
can be restricted to a smaller presieve
R₁
.
Equations
- category_theory.presieve.family_of_elements.restrict h = λ (x : category_theory.presieve.family_of_elements P R₂) (Y : C) (f : Y ⟶ X) (hf : R₁ f), x f _
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 pullback_compatible_iff
and
compatible_iff_sieve_compatible
.
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
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
pullback_compatible_iff
.
This is the definition for a "matching" family given in [MM92], Chapter III, Section 4,
Equation (5). Viewing the type family_of_elements
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.
Equations
- x.pullback_compatible = ∀ ⦃Y₁ Y₂ : C⦄ ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : R f₁) (h₂ : R f₂), P.map category_theory.limits.pullback.fst.op (x f₁ h₁) = P.map category_theory.limits.pullback.snd.op (x f₂ h₂)
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.sieve_extend = λ (Z : C) (f : Z ⟶ X) (hf : ⇑(category_theory.sieve.generate R) f), P.map (Exists.some _).op (x (Exists.some _) _)
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_sieve_compatible
.
This is the notion of "matching" given for families on sieves given in [MM92], 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].
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
- category_theory.presieve.compatible_equiv_generate_sieve_compatible = {to_fun := λ (x : {x // x.compatible}), ⟨x.val.sieve_extend, _⟩, inv_fun := λ (x : {x // x.compatible}), ⟨category_theory.presieve.family_of_elements.restrict _ x.val, _⟩, left_inv := _, right_inv := _}
Given a family of elements of a sieve S
on F(X)
, we can realize it as a family of elements of
S.functor_pullback F
.
Equations
- category_theory.presieve.family_of_elements.functor_pullback F x = λ (Y : D) (f : Y ⟶ Z) (hf : category_theory.presieve.functor_pullback F T f), x (F.map f) hf
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.functor_pushforward F
. Since the preimage is obtained by
choice, this is not well-defined generally.
Equations
- category_theory.presieve.family_of_elements.functor_pushforward F x = λ (Y : C) (f : Y ⟶ F.obj X) (h : category_theory.presieve.functor_pushforward F T f), (category_theory.presieve.get_functor_pushforward_structure h).cases_on (λ (Z : D) (g : Z ⟶ X) (h : Y ⟶ F.obj Z) (h₁ : T g) (fac : f = h ≫ F.map g), P.map h.op (x g h₁))
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
- category_theory.presieve.family_of_elements.pullback f x = λ (_x : C) (g : _x ⟶ Y) (hg : ⇑(category_theory.sieve.pullback f S) g), x (g ≫ f) hg
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
- category_theory.presieve.family_of_elements.comp_presheaf_map f x = λ (Y : C) (g : Y ⟶ X) (hg : R g), f.app (opposite.op Y) (x g hg)
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 [MM92], Chapter III, Section 4, equation (2).
A presheaf is separated for a presieve if there is at most one amalgamation.
Equations
- category_theory.presieve.is_separated_for P R = ∀ (x : category_theory.presieve.family_of_elements P R) (t₁ t₂ : P.obj (opposite.op X)), x.is_amalgamation t₁ → x.is_amalgamation t₂ → t₁ = t₂
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_sieve_compatible
,
this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4.
Equations
- category_theory.presieve.is_sheaf_for P R = ∀ (x : category_theory.presieve.family_of_elements P R), x.compatible → (∃! (t : P.obj (opposite.op X)), x.is_amalgamation t)
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 is_sheaf_for
is given in yoneda_condition_iff_sheaf_condition
.
This version is also useful to establish that being a sheaf is preserved under isomorphism of
presheaves.
See the discussion before Equation (3) of [MM92], 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
- category_theory.presieve.yoneda_sheaf_condition P S = ∀ (f : S.functor ⟶ P), ∃! (g : category_theory.yoneda.obj X ⟶ P), S.functor_inclusion ≫ g = f
(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 [MM92], Chapter III, Section 4.
Equations
- category_theory.presieve.nat_trans_equiv_compatible_family = {to_fun := λ (α : S.functor ⟶ P), ⟨λ (Y : C) (f : Y ⟶ X) (hf : ⇑S f), α.app (opposite.op Y) ⟨f, hf⟩, _⟩, inv_fun := λ (t : {x // x.compatible}), {app := λ (Y : Cᵒᵖ) (f : S.functor.obj Y), t.val f.val _, naturality' := _}, left_inv := _, right_inv := _}
(Implementation). A lemma useful to prove yoneda_condition_iff_sheaf_condition
.
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
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 = _.some
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 hygenic 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 presheaf is separated for a topology if it is separated for every sieve in the topology.
Equations
- category_theory.presieve.is_separated J P = ∀ {X : C} (S : category_theory.sieve X), S ∈ ⇑J X → category_theory.presieve.is_separated_for P ⇑S
A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology.
If the given topology is given by a pretopology, is_sheaf_for_pretopology
shows it suffices to
check the sheaf condition at presieves in the pretopology.
Equations
- category_theory.presieve.is_sheaf J P = ∀ ⦃X : C⦄ (S : category_theory.sieve X), S ∈ ⇑J X → category_theory.presieve.is_sheaf_for P ⇑S
The property of being a sheaf is preserved by isomorphism.
For a topology generated by a basis, it suffices to check the sheaf condition on the basis presieves only.
Any presheaf is a sheaf for the bottom (trivial) grothendieck topology.
The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM.
Equations
- category_theory.equalizer.first_obj P R = ∏ λ (f : Σ (Y : C), {f // R f}), P.obj (opposite.op f.fst)
Instances for category_theory.equalizer.first_obj
Show that first_obj
is isomorphic to family_of_elements
.
Equations
- category_theory.equalizer.first_obj_eq_family P R = {hom := λ (t : category_theory.equalizer.first_obj P R) (Y : C) (f : Y ⟶ X) (hf : R f), category_theory.limits.pi.π (λ (f : Σ (Y : C), {f // R f}), P.obj (opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ t, inv := category_theory.limits.pi.lift (λ (f : Σ (Y : C), {f // R f}) (x : category_theory.presieve.family_of_elements P R), x f.snd.val _), hom_inv_id' := _, inv_hom_id' := _}
The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM.
Equations
- category_theory.equalizer.fork_map P R = category_theory.limits.pi.lift (λ (f : Σ (Y : C), {f // R f}), P.map f.snd.val.op)
This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and
the definition of is_sheaf_for
.
The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used to check a family is compatible.
Equations
- category_theory.equalizer.sieve.second_obj P S = ∏ λ (f : Σ (Y Z : C) (g : Z ⟶ Y), {f' // ⇑S f'}), P.obj (opposite.op f.snd.fst)
Instances for category_theory.equalizer.sieve.second_obj
The map p
of Equations (3,4) [MM92].
The map a
of Equations (3,4) [MM92].
The family of elements given by x : first_obj P S
is compatible iff first_map
and second_map
map it to the same point.
P
is a sheaf for S
, iff the fork given by w
is an equalizer.
This section establishes the equivalence between the sheaf condition of
https://stacks.math.columbia.edu/tag/00VM and the definition of is_sheaf_for
.
The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which contains the data used to check a family of elements for a presieve is compatible.
Equations
- category_theory.equalizer.presieve.second_obj P R = ∏ λ (fg : (Σ (Y : C), {f // R f}) × Σ (Z : C), {g // R g}), P.obj (opposite.op (category_theory.limits.pullback fg.fst.snd.val fg.snd.snd.val))
Instances for category_theory.equalizer.presieve.second_obj
The map pr₀*
of https://stacks.math.columbia.edu/tag/00VL.
Equations
- category_theory.equalizer.presieve.first_map P R = category_theory.limits.pi.lift (λ (fg : (Σ (Y : C), {f // R f}) × Σ (Z : C), {g // R g}), category_theory.limits.pi.π (λ (f : Σ (Y : C), {f // R f}), P.obj (opposite.op f.fst)) fg.fst ≫ P.map category_theory.limits.pullback.fst.op)
The map pr₁*
of https://stacks.math.columbia.edu/tag/00VL.
Equations
- category_theory.equalizer.presieve.second_map P R = category_theory.limits.pi.lift (λ (fg : (Σ (Y : C), {f // R f}) × Σ (Z : C), {g // R g}), category_theory.limits.pi.π (λ (f : Σ (Y : C), {f // R f}), P.obj (opposite.op f.fst)) fg.snd ≫ P.map category_theory.limits.pullback.snd.op)
The family of elements given by x : first_obj P S
is compatible iff first_map
and second_map
map it to the same point.
P
is a sheaf for R
, iff the fork given by w
is an equalizer.
See https://stacks.math.columbia.edu/tag/00VM.
- val : Cᵒᵖ ⥤ Type ?
- cond : category_theory.presieve.is_sheaf J self.val
The category of sheaves on a grothendieck topology.
Instances for category_theory.SheafOfTypes
- category_theory.SheafOfTypes.has_sizeof_inst
- category_theory.SheafOfTypes.category_theory.category
- category_theory.SheafOfTypes.inhabited
Morphisms between sheaves of types are just morphisms between the underlying presheaves.
Instances for category_theory.SheafOfTypes.hom
- category_theory.SheafOfTypes.hom.has_sizeof_inst
- category_theory.SheafOfTypes.hom.inhabited
Equations
- category_theory.SheafOfTypes.category_theory.category = {to_category_struct := {to_quiver := {hom := category_theory.SheafOfTypes.hom J}, id := λ (X : category_theory.SheafOfTypes J), {val := 𝟙 X.val}, comp := λ (X Y Z : category_theory.SheafOfTypes J) (f : X ⟶ Y) (g : Y ⟶ Z), {val := f.val ≫ g.val}}, id_comp' := _, comp_id' := _, assoc' := _}
Equations
The inclusion functor from sheaves to presheaves.
Equations
- category_theory.SheafOfTypes_to_presheaf J = {obj := category_theory.SheafOfTypes.val J, map := λ (X Y : category_theory.SheafOfTypes J) (f : X ⟶ Y), f.val, map_id' := _, map_comp' := _}
Instances for category_theory.SheafOfTypes_to_presheaf
Equations
- category_theory.SheafOfTypes_to_presheaf.full J = {preimage := λ (X Y : category_theory.SheafOfTypes J) (f : (category_theory.SheafOfTypes_to_presheaf J).obj X ⟶ (category_theory.SheafOfTypes_to_presheaf J).obj Y), {val := f}, witness' := _}
The category of sheaves on the bottom (trivial) grothendieck topology is equivalent to the category of presheaves.
Equations
- category_theory.SheafOfTypes_bot_equiv = {functor := category_theory.SheafOfTypes_to_presheaf ⊥, inverse := {obj := λ (P : Cᵒᵖ ⥤ Type w), {val := P, cond := _}, map := λ (P₁ P₂ : Cᵒᵖ ⥤ Type w) (f : P₁ ⟶ P₂), (category_theory.SheafOfTypes_to_presheaf ⊥).preimage f, map_id' := _, map_comp' := _}, unit_iso := {hom := {app := λ (_x : category_theory.SheafOfTypes ⊥), {val := 𝟙 ((𝟭 (category_theory.SheafOfTypes ⊥)).obj _x).val}, naturality' := _}, inv := {app := λ (_x : category_theory.SheafOfTypes ⊥), {val := 𝟙 ((category_theory.SheafOfTypes_to_presheaf ⊥ ⋙ {obj := λ (P : Cᵒᵖ ⥤ Type w), {val := P, cond := _}, map := λ (P₁ P₂ : Cᵒᵖ ⥤ Type w) (f : P₁ ⟶ P₂), (category_theory.SheafOfTypes_to_presheaf ⊥).preimage f, map_id' := _, map_comp' := _}).obj _x).val}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}, counit_iso := category_theory.iso.refl ({obj := λ (P : Cᵒᵖ ⥤ Type w), {val := P, cond := _}, map := λ (P₁ P₂ : Cᵒᵖ ⥤ Type w) (f : P₁ ⟶ P₂), (category_theory.SheafOfTypes_to_presheaf ⊥).preimage f, map_id' := _, map_comp' := _} ⋙ category_theory.SheafOfTypes_to_presheaf ⊥), functor_unit_iso_comp' := _}