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ᵒᵖ ⥤ Ais 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. - An alternate definition in terms of limits, unconditionally equivalent to the original one:
see
CategoryTheory.Presheaf.isSheaf_iff_isLimit. - An alternate definition when
Cis small, has pullbacks andAhas 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
Ahas limits and there is a functors : A ⥤ Typewhich is faithful, reflects isomorphisms and preserves limits, thenP : Cᵒᵖ ⥤ Ais a sheaf iff the underlying presheaf of typesP ⋙ s : Cᵒᵖ ⥤ Typeis 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.
def
CategoryTheory.Presheaf.IsSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
:
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.
Instances For
def
CategoryTheory.Presheaf.IsSeparated
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
{FA : A → A → Type u_1}
{CA : A → Type u_2}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
:
Condition that a presheaf with values in a concrete category is separated for a Grothendieck topology.
Instances For
def
CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
{X : C}
(S : Sieve X)
(E : Aᵒᵖ)
:
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 SieveCompatible family of elements
for the sieve S and the presheaf of types Hom (E, P -).
Instances For
def
CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{P : Functor Cᵒᵖ A}
{X : C}
{S : Sieve X}
{E : Aᵒᵖ}
{x : FamilyOfElements (P.comp (coyoneda.obj E)) S.arrows}
(hx : x.SieveCompatible)
:
Limits.Cone (S.arrows.diagram.op.comp P)
The cone corresponding to a SieveCompatible family of elements, dot notation enabled.
Instances For
def
CategoryTheory.Presheaf.homEquivAmalgamation
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{P : Functor Cᵒᵖ A}
{X : C}
{S : Sieve X}
{E : Aᵒᵖ}
{x : Presieve.FamilyOfElements (P.comp (coyoneda.obj E)) S.arrows}
(hx : x.SieveCompatible)
:
Cone morphisms from the cone corresponding to a SieveCompatible family to the natural
cone associated to a sieve S and a presheaf P are in 1-1 correspondence with amalgamations
of the family.
Instances For
theorem
CategoryTheory.Presheaf.isLimit_iff_isSheafFor
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
{X : C}
(S : Sieve X)
:
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.
theorem
CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
{X : C}
(S : Sieve X)
:
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.
theorem
CategoryTheory.Presheaf.isSheaf_iff_isLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ 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.
theorem
CategoryTheory.Presheaf.isSeparated_iff_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
:
(∀ (E : A), Presieve.IsSeparated J (P.comp (coyoneda.obj (Opposite.op E)))) ↔ ∀ ⦃X : C⦄,
∀ S ∈ J X, ∀ (c : Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
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.
theorem
CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
{X : C}
(R : Presieve X)
:
Nonempty (Limits.IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), Presieve.IsSheafFor (P.comp (coyoneda.obj E)) R
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.
theorem
CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
[Limits.HasPullbacks C]
(K : Pretopology C)
:
IsSheaf K.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (Limits.IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))
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.
noncomputable def
CategoryTheory.Presheaf.IsSheaf.amalgamate
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{E : A}
{X : C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
(S : J.Cover X)
(x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
(hx :
∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryStruct.comp (x I₂) (P.map r.g₂.op))
:
This is a wrapper around Presieve.IsSheafFor.amalgamate to be used below.
If P is 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 xs to obtain a single morphism E ⟶ P.obj (op X).
Instances For
@[simp]
theorem
CategoryTheory.Presheaf.IsSheaf.amalgamate_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{E : A}
{X : C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
(S : J.Cover X)
(x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
(hx :
∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryStruct.comp (x I₂) (P.map r.g₂.op))
(I : S.Arrow)
:
CategoryStruct.comp (hP.amalgamate S x hx) (P.map I.f.op) = x I
@[simp]
theorem
CategoryTheory.Presheaf.IsSheaf.amalgamate_map_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{E : A}
{X : C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
(S : J.Cover X)
(x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
(hx :
∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryStruct.comp (x I₂) (P.map r.g₂.op))
(I : S.Arrow)
{Z : A}
(h : P.obj (Opposite.op I.Y) ⟶ Z)
:
CategoryStruct.comp (hP.amalgamate S x hx) (CategoryStruct.comp (P.map I.f.op) h) = CategoryStruct.comp (x I) h
theorem
CategoryTheory.Presheaf.IsSheaf.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{E : A}
{X : C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
(S : J.Cover X)
(e₁ e₂ : E ⟶ P.obj (Opposite.op X))
(h : ∀ (I : S.Arrow), CategoryStruct.comp e₁ (P.map I.f.op) = CategoryStruct.comp e₂ (P.map I.f.op))
:
e₁ = e₂
theorem
CategoryTheory.Presheaf.IsSheaf.hom_ext_ofArrows
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
{I : Type u_1}
{S : C}
{X : I → C}
(f : (i : I) → X i ⟶ S)
(hf : Sieve.ofArrows X f ∈ J S)
{E : A}
{x y : E ⟶ P.obj (Opposite.op S)}
(h : ∀ (i : I), CategoryStruct.comp x (P.map (f i).op) = CategoryStruct.comp y (P.map (f i).op))
:
x = y
theorem
CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
{I : Type u_1}
{S : C}
{X : I → C}
(f : (i : I) → X i ⟶ S)
(hf : Sieve.ofArrows X f ∈ J S)
{E : A}
(x : (i : I) → E ⟶ P.obj (Opposite.op (X i)))
(hx :
∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
CategoryStruct.comp a (f i) = CategoryStruct.comp b (f j) →
CategoryStruct.comp (x i) (P.map a.op) = CategoryStruct.comp (x j) (P.map b.op))
:
noncomputable def
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
{I : Type u_1}
{S : C}
{X : I → C}
(f : (i : I) → X i ⟶ S)
(hf : Sieve.ofArrows X f ∈ J S)
{E : A}
(x : (i : I) → E ⟶ P.obj (Opposite.op (X i)))
(hx :
∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
CategoryStruct.comp a (f i) = CategoryStruct.comp b (f j) →
CategoryStruct.comp (x i) (P.map a.op) = CategoryStruct.comp (x j) (P.map b.op))
:
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)).
Instances For
@[simp]
theorem
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
{I : Type u_1}
{S : C}
{X : I → C}
(f : (i : I) → X i ⟶ S)
(hf : Sieve.ofArrows X f ∈ J S)
{E : A}
(x : (i : I) → E ⟶ P.obj (Opposite.op (X i)))
(hx :
∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
CategoryStruct.comp a (f i) = CategoryStruct.comp b (f j) →
CategoryStruct.comp (x i) (P.map a.op) = CategoryStruct.comp (x j) (P.map b.op))
(i : I)
:
CategoryStruct.comp (hP.amalgamateOfArrows f hf x hx) (P.map (f i).op) = x i
@[simp]
theorem
CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
{I : Type u_1}
{S : C}
{X : I → C}
(f : (i : I) → X i ⟶ S)
(hf : Sieve.ofArrows X f ∈ J S)
{E : A}
(x : (i : I) → E ⟶ P.obj (Opposite.op (X i)))
(hx :
∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
CategoryStruct.comp a (f i) = CategoryStruct.comp b (f j) →
CategoryStruct.comp (x i) (P.map a.op) = CategoryStruct.comp (x j) (P.map b.op))
(i : I)
{Z : A}
(h : P.obj (Opposite.op (X i)) ⟶ Z)
:
CategoryStruct.comp (hP.amalgamateOfArrows f hf x hx) (CategoryStruct.comp (P.map (f i).op) h) = CategoryStruct.comp (x i) h
theorem
CategoryTheory.Presheaf.isSheaf_of_iso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{P P' : Functor Cᵒᵖ A}
(e : P ≅ P')
:
theorem
CategoryTheory.Presheaf.isSheaf_of_isTerminal
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
{X : A}
(hX : Limits.IsTerminal X)
:
IsSheaf J ((Functor.const Cᵒᵖ).obj X)
@[reducible, inline]
abbrev
CategoryTheory.Sheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
Type (max (max (max u₂ v₂) u₁) v₁)
The category of sheaves taking values in A on a Grothendieck topology.
Instances For
@[reducible, inline, deprecated "Use ObjectProperty.obj" (since := "2026-03-03")]
abbrev
CategoryTheory.Sheaf.val
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(F : Sheaf J A)
:
The underlying presheaf of a sheaf.
Instances For
@[deprecated "Use ObjectProperty.FullSubcategory.property" (since := "2026-03-03")]
theorem
CategoryTheory.Sheaf.cond
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(F : Sheaf J A)
:
Presheaf.IsSheaf J F.obj
@[deprecated CategoryTheory.ObjectProperty.homMk (since := "2026-03-03")]
def
CategoryTheory.Sheaf.Hom.mk
{C : Type u}
[Category.{v, u} C]
{P : ObjectProperty C}
{X Y : P.FullSubcategory}
(f : X.obj ⟶ Y.obj)
:
Alias of CategoryTheory.ObjectProperty.homMk.
Instances For
theorem
CategoryTheory.Sheaf.hom_ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{F G : Sheaf J A}
{f g : F ⟶ G}
:
theorem
CategoryTheory.Sheaf.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{F G : Sheaf J A}
{f g : F ⟶ G}
(h : f.hom = g.hom)
:
f = g
@[reducible, inline]
abbrev
CategoryTheory.sheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
The inclusion functor of the category of sheaves in the category of presheaves.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.sheafSections
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
The sections of a sheaf (i.e. evaluation as a presheaf on C).
Instances For
def
CategoryTheory.sheafSectionsNatIsoEvaluation
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
{X : C}
:
(sheafSections J A).obj (Opposite.op X) ≅ (sheafToPresheaf J A).comp ((evaluation Cᵒᵖ A).obj (Opposite.op X))
The sheaf sections functor on X is given by evaluation of presheaves on X.
Instances For
@[simp]
theorem
CategoryTheory.sheafSectionsNatIsoEvaluation_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
{X : C}
(X✝ : Sheaf J A)
:
(sheafSectionsNatIsoEvaluation J A).hom.app X✝ = CategoryStruct.id (X✝.obj.obj (Opposite.op X))
@[simp]
theorem
CategoryTheory.sheafSectionsNatIsoEvaluation_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
{X : C}
(X✝ : Sheaf J A)
:
(sheafSectionsNatIsoEvaluation J A).inv.app X✝ = CategoryStruct.id (X✝.obj.obj (Opposite.op X))
@[reducible, inline]
abbrev
CategoryTheory.fullyFaithfulSheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
(sheafToPresheaf J A).FullyFaithful
The functor Sheaf J A ⥤ Cᵒᵖ ⥤ A is fully faithful.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Sheaf.homEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{X Y : Sheaf J A}
:
The bijection (X ⟶ Y) ≃ (X.val ⟶ Y.val) when X and Y are sheaves.
Instances For
def
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
:
Sheaf.homEquiv as a natural isomorphism.
Instances For
@[simp]
theorem
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(X : Sheaf J A)
(X✝ : (Sheaf J A)ᵒᵖ)
(a✝ :
(((sheafToPresheaf J A).comp
(yoneda.comp
((Functor.whiskeringLeft (Sheaf J A)ᵒᵖ (Functor Cᵒᵖ A)ᵒᵖ (Type (max u₁ v₂))).obj
(sheafToPresheaf J A).op))).obj
X).obj
X✝)
:
((sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf.hom.app X).app X✝ a✝).hom = Equiv.ulift ((uliftYonedaIsoYoneda.inv.app X.obj).app (Opposite.op (Opposite.unop X✝).obj) a✝)
@[simp]
theorem
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(X : Sheaf J A)
(X✝ : (Sheaf J A)ᵒᵖ)
(a✝ : (yoneda.obj X).obj X✝)
:
(sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf.inv.app X).app X✝ a✝ = a✝.hom
theorem
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{X Y : Sheaf J A}
:
def
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
:
(sheafToPresheaf J A).op.comp
(coyoneda.comp
((Functor.whiskeringLeft (Sheaf J A) (Functor Cᵒᵖ A) (Type (max u₁ v₂))).obj (sheafToPresheaf J A))) ≅ coyoneda
Sheaf.homEquiv as a natural isomorphism, using coyoneda.
Instances For
@[simp]
theorem
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(X : (Sheaf J A)ᵒᵖ)
(X✝ : Sheaf J A)
(a✝ :
(((sheafToPresheaf J A).op.comp
(coyoneda.comp
((Functor.whiskeringLeft (Sheaf J A) (Functor Cᵒᵖ A) (Type (max u₁ v₂))).obj (sheafToPresheaf J A)))).obj
X).obj
X✝)
:
((sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.hom.app X).app X✝ a✝).hom = Equiv.ulift ((uliftCoyonedaIsoCoyoneda.inv.app (Opposite.op (Opposite.unop X).obj)).app X✝.obj a✝)
@[simp]
theorem
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(X : (Sheaf J A)ᵒᵖ)
(X✝ : Sheaf J A)
(a✝ : (coyoneda.obj X).obj X✝)
:
(sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app X).app X✝ a✝ = a✝.hom
theorem
CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{X Y : Sheaf J A}
:
theorem
CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
{F G : Sheaf J A}
(f : F ⟶ G)
[h : Mono f.hom]
:
Mono f
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).
instance
CategoryTheory.Sheaf.Hom.epi_of_presheaf_epi
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
{F G : Sheaf J A}
(f : F ⟶ G)
[h : Epi f.hom]
:
Epi f
theorem
CategoryTheory.isSheaf_iff_isSheaf_of_type
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ (Type w))
:
Presheaf.IsSheaf J P ↔ Presieve.IsSheaf J P
def
CategoryTheory.sheafOver
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
(ℱ : Sheaf J A)
(E : A)
:
The sheaf of sections guaranteed by the sheaf condition.
Instances For
@[simp]
theorem
CategoryTheory.sheafOver_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
(ℱ : Sheaf J A)
(E : A)
:
theorem
CategoryTheory.Presheaf.IsSheaf.isSheafFor
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{P : Functor Cᵒᵖ (Type w)}
(hP : IsSheaf J P)
{X : C}
(S : Sieve X)
(hS : S ∈ J X)
:
theorem
CategoryTheory.Presheaf.isSheaf_bot
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
:
theorem
CategoryTheory.Presheaf.IsSheaf.of_le
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{K : GrothendieckTopology C}
{F : Functor Cᵒᵖ A}
(hle : J ≤ K)
(h : IsSheaf K F)
:
IsSheaf J F
def
CategoryTheory.sheafBotEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
:
The category of sheaves on the bottom (trivial) Grothendieck topology is equivalent to the category of presheaves.
Instances For
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
:
(sheafBotEquivalence A).functor = sheafToPresheaf ⊥ A
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_inverse_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
{X✝ Y✝ : Functor Cᵒᵖ A}
(f : X✝ ⟶ Y✝)
:
((sheafBotEquivalence A).inverse.map f).hom = f
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_inverse_obj_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
:
((sheafBotEquivalence A).inverse.obj P).obj = P
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
:
(sheafBotEquivalence A).unitIso = Iso.refl (Functor.id (Sheaf ⊥ A))
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
:
@[implicit_reducible]
instance
CategoryTheory.instInhabitedSheafBotGrothendieckTopologyType
{C : Type u₁}
[Category.{v₁, u₁} C]
:
noncomputable def
CategoryTheory.Sheaf.isTerminalOfBotCover
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(F : Sheaf J A)
(X : C)
(H : ⊥ ∈ J X)
:
Limits.IsTerminal (F.obj.obj (Opposite.op X))
If the empty sieve is a cover of X, then F(X) is terminal.
Instances For
def
CategoryTheory.Sheaf.terminal
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{A : Type u₂}
[Category.{v₂, u₂} A]
{X : A}
(hX : Limits.IsTerminal X)
:
Sheaf J A
A terminal object in A gives rise to a terminal object in Sheaf J
Instances For
@[simp]
theorem
CategoryTheory.Sheaf.terminal_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{A : Type u₂}
[Category.{v₂, u₂} A]
{X : A}
(hX : Limits.IsTerminal X)
:
(terminal J hX).obj = (Functor.const Cᵒᵖ).obj X
def
CategoryTheory.Sheaf.isTerminalTerminal
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
{A : Type u₂}
[Category.{v₂, u₂} A]
{X : A}
(hX : Limits.IsTerminal X)
:
Limits.IsTerminal (terminal J hX)
The constant sheaf of a terminal object is indeed terminal
Instances For
@[simp]
theorem
CategoryTheory.Sheaf.isTerminalTerminal_from_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{X : A}
(hX : Limits.IsTerminal X)
(G : Sheaf J A)
:
((isTerminalTerminal J hX).from G).hom = (Functor.isTerminalConst Cᵒᵖ hX).from G.obj
noncomputable def
CategoryTheory.Sheaf.isTerminalOfEqTop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(H : J = ⊤)
(F : Sheaf J A)
:
If the topology is discrete, any sheaf is terminal.
Instances For
@[simp]
theorem
CategoryTheory.Sheaf.Hom.add_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
(f g : P ⟶ Q)
(U : Cᵒᵖ)
:
noncomputable def
CategoryTheory.Presheaf.isLimitOfIsSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X)
(hP : IsSheaf J P)
:
Limits.IsLimit (S.multifork P)
When P is a sheaf and S is a cover, the associated multifork is a limit.
Instances For
theorem
CategoryTheory.Presheaf.isSheaf_iff_multifork
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
:
IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), Nonempty (Limits.IsLimit (S.multifork P))
noncomputable def
CategoryTheory.Presheaf.IsSheaf.isLimitMultifork
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{P : Functor Cᵒᵖ A}
(hP : IsSheaf J P)
{X : C}
(S : J.Cover X)
:
Limits.IsLimit (S.multifork P)
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.
Instances For
theorem
CategoryTheory.Presheaf.isSheaf_iff_multiequalizer
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
[∀ (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
:
IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
noncomputable def
CategoryTheory.Presheaf.firstObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{U : C}
(R : Presieve U)
(P : Functor Cᵒᵖ A)
[Limits.HasProducts A]
:
A
The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of the Stacks entry.
Instances For
noncomputable def
CategoryTheory.Presheaf.forkMap
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{U : C}
(R : Presieve U)
(P : Functor Cᵒᵖ A)
[Limits.HasProducts A]
:
The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of the Stacks entry.
Instances For
noncomputable def
CategoryTheory.Presheaf.secondObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{U : C}
(R : Presieve U)
(P : Functor Cᵒᵖ A)
[Limits.HasProducts A]
[Limits.HasPullbacks C]
:
A
The rightmost object of the fork diagram of the Stacks entry, which contains the data used to check a family of elements for a presieve is compatible.
Instances For
noncomputable def
CategoryTheory.Presheaf.firstMap
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{U : C}
(R : Presieve U)
(P : Functor Cᵒᵖ A)
[Limits.HasProducts A]
[Limits.HasPullbacks C]
:
The map pr₀* of the Stacks entry.
Instances For
noncomputable def
CategoryTheory.Presheaf.secondMap
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{U : C}
(R : Presieve U)
(P : Functor Cᵒᵖ A)
[Limits.HasProducts A]
[Limits.HasPullbacks C]
:
The map pr₁* of the Stacks entry.
Instances For
theorem
CategoryTheory.Presheaf.w
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{U : C}
(R : Presieve U)
(P : Functor Cᵒᵖ A)
[Limits.HasProducts A]
[Limits.HasPullbacks C]
:
CategoryStruct.comp (forkMap R P) (firstMap R P) = CategoryStruct.comp (forkMap R P) (secondMap R P)
def
CategoryTheory.Presheaf.IsSheaf'
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
(J : GrothendieckTopology C)
[Limits.HasProducts A]
[Limits.HasPullbacks C]
(P : Functor Cᵒᵖ A)
:
An alternative definition of the sheaf condition in terms of equalizers. This is shown to be
equivalent in CategoryTheory.Presheaf.isSheaf_iff_isSheaf'.
Instances For
noncomputable def
CategoryTheory.Presheaf.isSheafForIsSheafFor'
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
[Limits.HasProducts A]
[Limits.HasPullbacks C]
(P : Functor Cᵒᵖ A)
(s : Functor A (Type (max v₁ u₁)))
[∀ (J : Type (max v₁ u₁)), Limits.PreservesLimitsOfShape (Discrete J) s]
(U : C)
(R : Presieve U)
:
Limits.IsLimit (s.mapCone (Limits.Fork.ofι (forkMap R P) ⋯)) ≃ Limits.IsLimit (Limits.Fork.ofι (Equalizer.forkMap (P.comp s) R) ⋯)
(Implementation). An auxiliary lemma to convert between sheaf conditions.
Instances For
theorem
CategoryTheory.Presheaf.isSheaf_iff_isSheaf'
{C : Type u₁}
[Category.{v₁, u₁} C]
{A' : Type u₂}
[Category.{max v₁ u₁, u₂} A']
(J : GrothendieckTopology C)
(P' : Functor Cᵒᵖ A')
[Limits.HasProducts A']
[Limits.HasPullbacks C]
:
The equalizer definition of a sheaf given by isSheaf' is equivalent to isSheaf.
theorem
CategoryTheory.Presheaf.isSheaf_of_isSheaf_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
(s : Functor A B)
[Limits.ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s]
(h : IsSheaf J (P.comp s))
:
IsSheaf J P
theorem
CategoryTheory.Presheaf.isSheaf_comp_of_isSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
(s : Functor A B)
[Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s]
(h : IsSheaf J P)
:
theorem
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ A)
(s : Functor A B)
[Limits.HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A]
[Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s]
[s.ReflectsIsomorphisms]
:
theorem
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget
{C : Type u₁}
[Category.{v₁, u₁} C]
{A' : Type u₂}
[Category.{max v₁ u₁, u₂} A']
(J : GrothendieckTopology C)
(P' : Functor Cᵒᵖ A')
(s : Functor A' (Type (max v₁ u₁)))
[Limits.HasLimits A']
[Limits.PreservesLimits s]
[s.ReflectsIsomorphisms]
:
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, e.g. groups, abelian groups and rings, but not for the category of topological spaces, topological rings, etc. since reflecting isomorphisms does not hold.