Sheaves taking values in a category #
If C is a category with a Grothendieck topology, we define the notion of a sheaf taking values in
an arbitrary category A
. We follow the definition in https://stacks.math.columbia.edu/tag/00VR,
noting that the presheaf of sets "defined above" can be seen in the comments between tags 00VQ and
00VR on the page https://stacks.math.columbia.edu/tag/00VL. The advantage of this definition is
that we need no assumptions whatsoever on A
other than the assumption that the morphisms in C
and A
live in the same universe.
- An
A
-valued presheafP : Cᵒᵖ ⥤ A
is defined to be a sheaf (for the topologyJ
) iff for everyE : A
, the type-valued presheaves of sets given by sendingU : Cᵒᵖ
toHom_{A}(E, P U)
are all sheaves of sets, seeCategoryTheory.Presheaf.IsSheaf
. - When
A = Type
, this recovers the basic definition of sheaves of sets, seeCategoryTheory.isSheaf_iff_isSheaf_of_type
. - A alternate definition in terms of limits, unconditionally equivalent to the original one:
see
CategoryTheory.Presheaf.isSheaf_iff_isLimit
. - An alternate definition when
C
is small, has pullbacks andA
has products is given by an equalizer conditionCategoryTheory.Presheaf.IsSheaf'
. This is equivalent to the earlier definition, shown inCategoryTheory.Presheaf.isSheaf_iff_isSheaf'
. - When
A = Type
, this is definitionally equal to the equalizer condition for presieves inCategoryTheory.Sites.SheafOfTypes
. - When
A
has limits and there is a functors : A ⥤ Type
which is faithful, reflects isomorphisms and preserves limits, thenP : Cᵒᵖ ⥤ A
is a sheaf iff the underlying presheaf of typesP ⋙ s : Cᵒᵖ ⥤ Type
is a sheaf (CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget
). Cf https://stacks.math.columbia.edu/tag/0073, which is a weaker version of this statement (it's only over spaces, not sites) and https://stacks.math.columbia.edu/tag/00YR (a), which additionally assumes filtered colimits.
Implementation notes #
Occasionally we need to take a limit in A
of a collection of morphisms of C
indexed
by a collection of objects in C
. This turns out to force the morphisms of A
to be
in a sufficiently large universe. Rather than use UnivLE
we prove some results for
a category A'
instead, whose morphism universe of A'
is defined to be max u₁ v₁
, where
u₁, v₁
are the universes for C
. Perhaps after we get better at handling universe
inequalities this can be changed.
A sheaf of A is a presheaf P : Cᵒᵖ => A such that for every E : A, the presheaf of types given by sending U : C to Hom_{A}(E, P U) is a sheaf of types.
https://stacks.math.columbia.edu/tag/00VR
Equations
- CategoryTheory.Presheaf.IsSheaf J P = ∀ (E : A), CategoryTheory.Presieve.IsSheaf J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))
Instances For
Condition that a presheaf with values in a concrete category is separated for a Grothendieck topology.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a sieve S
on X : C
, a presheaf P : Cᵒᵖ ⥤ A
, and an object E
of A
,
the cones over the natural diagram S.arrows.diagram.op ⋙ P
associated to S
and P
with cone point E
are in 1-1 correspondence with sieve_compatible family of elements
for the sieve S
and the presheaf of types Hom (E, P -)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cone corresponding to a sieve_compatible family of elements, dot notation enabled.
Equations
- hx.cone = { pt := Opposite.unop E, π := (CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily P S E).invFun ⟨x, hx⟩ }
Instances For
Cone morphisms from the cone corresponding to a sieve_compatible family to the natural
cone associated to a sieve S
and a presheaf P
are in 1-1 correspondence with amalgamations
of the family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given sieve S
and presheaf P : Cᵒᵖ ⥤ A
, their natural associated cone is a limit cone
iff Hom (E, P -)
is a sheaf of types for the sieve S
and all E : A
.
Given sieve S
and presheaf P : Cᵒᵖ ⥤ A
, their natural associated cone admits at most one
morphism from every cone in the same category (i.e. over the same diagram),
iff Hom (E, P -)
is separated for the sieve S
and all E : A
.
A presheaf P
is a sheaf for the Grothendieck topology J
iff for every covering sieve
S
of J
, the natural cone associated to P
and S
is a limit cone.
A presheaf P
is separated for the Grothendieck topology J
iff for every covering sieve
S
of J
, the natural cone associated to P
and S
admits at most one morphism from every
cone in the same category.
Given presieve R
and presheaf P : Cᵒᵖ ⥤ A
, the natural cone associated to P
and
the sieve Sieve.generate R
generated by R
is a limit cone iff Hom (E, P -)
is a
sheaf of types for the presieve R
and all E : A
.
A presheaf P
is a sheaf for the Grothendieck topology generated by a pretopology K
iff for every covering presieve R
of K
, the natural cone associated to P
and
Sieve.generate R
is a limit cone.
This is a wrapper around Presieve.IsSheafFor.amalgamate
to be used below.
If P
s a sheaf, S
is a cover of X
, and x
is a collection of morphisms from E
to P
evaluated at terms in the cover which are compatible, then we can amalgamate
the x
s to obtain a single morphism E ⟶ P.obj (op X)
.
Equations
Instances For
If P : Cᵒᵖ ⥤ A
is a sheaf and f i : X i ⟶ S
is a covering family, then
a morphism E ⟶ P.obj (op S)
can be constructed from a compatible family of
morphisms x : E ⟶ P.obj (op (X i))
.
Equations
- hP.amalgamateOfArrows f hf x hx = Exists.choose ⋯
Instances For
The category of sheaves taking values in A
on a grothendieck topology.
- val : CategoryTheory.Functor Cᵒᵖ A
the underlying presheaf
- cond : CategoryTheory.Presheaf.IsSheaf J self.val
the condition that the presheaf is a sheaf
Instances For
the condition that the presheaf is a sheaf
Morphisms between sheaves are just morphisms of presheaves.
- val : X.val ⟶ Y.val
a morphism between the underlying presheaves
Instances For
Equations
- CategoryTheory.Sheaf.instCategorySheaf = CategoryTheory.Category.mk ⋯ ⋯ ⋯
Equations
- X.instInhabitedHom = { default := CategoryTheory.CategoryStruct.id X }
The inclusion functor from sheaves to presheaves.
Equations
- CategoryTheory.sheafToPresheaf J A = { obj := CategoryTheory.Sheaf.val, map := fun {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y) => f.val, map_id := ⋯, map_comp := ⋯ }
Instances For
The sections of a sheaf (i.e. evaluation as a presheaf on C
).
Equations
- CategoryTheory.sheafSections J A = (CategoryTheory.sheafToPresheaf J A).flip
Instances For
The functor Sheaf J A ⥤ Cᵒᵖ ⥤ A
is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bijection (X ⟶ Y) ≃ (X.val ⟶ Y.val)
when X
and Y
are sheaves.
Equations
- CategoryTheory.Sheaf.homEquiv = (CategoryTheory.fullyFaithfulSheafToPresheaf J A).homEquiv
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
This is stated as a lemma to prevent class search from forming a loop since a sheaf morphism is monic if and only if it is monic as a presheaf morphism (under suitable assumption).
Equations
- ⋯ = ⋯
The sheaf of sections guaranteed by the sheaf condition.
Equations
- CategoryTheory.sheafOver ℱ E = { val := ℱ.val.comp (CategoryTheory.coyoneda.obj (Opposite.op E)), cond := ⋯ }
Instances For
The category of sheaves taking values in Type is the same as the category of set-valued sheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.instInhabitedSheafBotGrothendieckTopologyType = { default := (CategoryTheory.sheafEquivSheafOfTypes ⊥).inverse.obj default }
If the empty sieve is a cover of X
, then F(X)
is terminal.
Equations
- F.isTerminalOfBotCover X H = CategoryTheory.Limits.IsTerminal.ofUnique (F.val.obj (Opposite.op X))
Instances For
Equations
- CategoryTheory.instZeroHomSheaf = { zero := { val := 0 } }
Equations
- CategoryTheory.Sheaf.Hom.addCommGroup = Function.Injective.addCommGroup (fun (f : P.Hom Q) => f.val) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- CategoryTheory.instPreadditiveSheaf = { homGroup := fun (P Q : CategoryTheory.Sheaf J A) => CategoryTheory.Sheaf.Hom.addCommGroup, add_comp := ⋯, comp_add := ⋯ }
When P
is a sheaf and S
is a cover, the associated multifork is a limit.
Equations
- CategoryTheory.Presheaf.isLimitOfIsSheaf J P S hP = { lift := fun (E : CategoryTheory.Limits.Multifork (S.index P)) => hP.amalgamate S (fun (I : S.Arrow) => E.ι I) ⋯, fac := ⋯, uniq := ⋯ }
Instances For
If F : Cᵒᵖ ⥤ A
is a sheaf for a Grothendieck topology J
on C
,
and S
is a cover of X : C
, then the multifork S.multifork F
is limit.
Equations
- hP.isLimitMultifork S = ⋯.some
Instances For
The middle object of the fork diagram given in Equation (3) of [MLM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM.
Equations
- CategoryTheory.Presheaf.firstObj R P = ∏ᶜ fun (f : (V : C) × { f : V ⟶ U // R f }) => P.obj (Opposite.op f.fst)
Instances For
The left morphism of the fork diagram given in Equation (3) of [MLM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM.
Equations
- CategoryTheory.Presheaf.forkMap R P = CategoryTheory.Limits.Pi.lift fun (f : (V : C) × { f : V ⟶ U // R f }) => P.map (↑f.snd).op
Instances 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
- One or more equations did not get rendered due to their size.
Instances For
The map pr₀*
of https://stacks.math.columbia.edu/tag/00VM.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map pr₁*
of https://stacks.math.columbia.edu/tag/00VM.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An alternative definition of the sheaf condition in terms of equalizers. This is shown to be
equivalent in CategoryTheory.Presheaf.isSheaf_iff_isSheaf'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Implementation). An auxiliary lemma to convert between sheaf conditions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equalizer definition of a sheaf given by isSheaf'
is equivalent to isSheaf
.
For a concrete category (A, s)
where the forgetful functor s : A ⥤ Type v
preserves limits and
reflects isomorphisms, and A
has limits, an A
-valued presheaf P : Cᵒᵖ ⥤ A
is a sheaf iff its
underlying Type
-valued presheaf P ⋙ s : Cᵒᵖ ⥤ Type
is a sheaf.
Note this lemma applies for "algebraic" categories, eg groups, abelian groups and rings, but not for the category of topological spaces, topological rings, etc since reflecting isomorphisms doesn't hold.