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. - A 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.
Equations
- CategoryTheory.Presheaf.IsSheaf J P = ∀ (E : A), CategoryTheory.Presieve.IsSheaf J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))
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.
Equations
- One or more equations did not get rendered due to their size.
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 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
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 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
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 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
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 (Pretopology.toGrothendieck C K) 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.
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 Ps 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).
Equations
- hP.amalgamate S x hx = ⋯.amalgamate (fun (Y : C) (f : Y ⟶ X) (hf : (↑S).arrows f) => x { Y := Y, f := f, hf := hf }) ⋯
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)
:
@[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))
:
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))
:
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))
:
@[deprecated CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows (since := "2024-12-17")]
theorem
CategoryTheory.Presheaf.IsSheaf.exists_unique_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))
:
Alias of CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows.
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)).
Equations
- hP.amalgamateOfArrows f hf x hx = Exists.choose ⋯
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)
:
@[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)
structure
CategoryTheory.Sheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
Type (max (max (max u₁ u₂) v₁) v₂)
The category of sheaves taking values in A on a grothendieck topology.
the underlying presheaf
- cond : Presheaf.IsSheaf J self.val
the condition that the presheaf is a sheaf
Instances For
structure
CategoryTheory.Sheaf.Hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(X Y : Sheaf J A)
:
Type (max u₁ v₂)
Morphisms between sheaves are just morphisms of presheaves.
a morphism between the underlying presheaves
Instances For
theorem
CategoryTheory.Sheaf.Hom.ext_iff
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{J : GrothendieckTopology C}
{A : Type u₂}
{inst✝¹ : Category.{v₂, u₂} A}
{X Y : Sheaf J A}
{x y : X.Hom Y}
:
theorem
CategoryTheory.Sheaf.Hom.ext
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{J : GrothendieckTopology C}
{A : Type u₂}
{inst✝¹ : Category.{v₂, u₂} A}
{X Y : Sheaf J A}
{x y : X.Hom Y}
(val : x.val = y.val)
:
instance
CategoryTheory.Sheaf.instCategorySheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Sheaf.instCategorySheaf_comp_val
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{X✝ Y✝ Z✝ : Sheaf J A}
(f : X✝.Hom Y✝)
(g : Y✝.Hom Z✝)
:
@[simp]
theorem
CategoryTheory.Sheaf.instCategorySheaf_id_val
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(x✝ : Sheaf J A)
:
instance
CategoryTheory.Sheaf.instInhabitedHom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
(X : Sheaf J A)
:
Equations
- X.instInhabitedHom = { default := CategoryTheory.CategoryStruct.id X }
theorem
CategoryTheory.Sheaf.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{X Y : Sheaf J A}
(x y : X ⟶ Y)
(h : x.val = y.val)
:
theorem
CategoryTheory.Sheaf.hom_ext_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
{X Y : Sheaf J A}
{x y : X ⟶ Y}
:
def
CategoryTheory.sheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
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
@[simp]
theorem
CategoryTheory.sheafToPresheaf_map
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
{X✝ Y✝ : Sheaf J A}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.sheafToPresheaf_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
(self : Sheaf J A)
:
@[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).
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
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)
:
@[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)
:
def
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.fullyFaithfulSheafToPresheaf_preimage_val
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
{X✝ Y✝ : Sheaf J A}
(f : (sheafToPresheaf J A).obj X✝ ⟶ (sheafToPresheaf J A).obj Y✝)
:
@[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
instance
CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
(sheafToPresheaf J A).Full
instance
CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} A]
:
(sheafToPresheaf J A).Faithful
instance
CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(A : Type u₂)
[Category.{v₂, u₂} 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.val]
:
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.val]
:
Epi f
theorem
CategoryTheory.isSheaf_iff_isSheaf_of_type
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : GrothendieckTopology C)
(P : Functor Cᵒᵖ (Type w))
:
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.
Equations
- CategoryTheory.sheafOver ℱ E = { val := ℱ.val.comp (CategoryTheory.coyoneda.obj (Opposite.op E)), cond := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.sheafOver_val
{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)
:
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
:
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_inverse_map_val
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
{X✝ Y✝ : Functor Cᵒᵖ A}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
:
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_inverse_obj_val
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
(P : Functor Cᵒᵖ A)
:
@[simp]
theorem
CategoryTheory.sheafBotEquivalence_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
(A : Type u₂)
[Category.{v₂, u₂} A]
:
instance
CategoryTheory.instInhabitedSheafBotGrothendieckTopologyType
{C : Type u₁}
[Category.{v₁, u₁} C]
:
Equations
- One or more equations did not get rendered due to their size.
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.val.obj (Opposite.op X))
If the empty sieve is a cover of X, then F(X) is terminal.
Equations
Instances For
instance
CategoryTheory.sheafHomHasZSMul
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
:
instance
CategoryTheory.instSubHomSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
:
instance
CategoryTheory.instNegHomSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
:
instance
CategoryTheory.sheafHomHasNSMul
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
:
instance
CategoryTheory.instZeroHomSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
:
instance
CategoryTheory.instAddHomSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
:
@[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ᵒᵖ)
:
instance
CategoryTheory.Sheaf.Hom.addCommGroup
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
{P Q : Sheaf J A}
:
AddCommGroup (P ⟶ Q)
Equations
- CategoryTheory.Sheaf.Hom.addCommGroup = Function.Injective.addCommGroup (fun (f : P.Hom Q) => f.val) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
CategoryTheory.instPreadditiveSheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{A : Type u₂}
[Category.{v₂, u₂} A]
[Preadditive A]
:
Preadditive (Sheaf J A)
Equations
- CategoryTheory.instPreadditiveSheaf = { homGroup := fun (x x_1 : CategoryTheory.Sheaf J A) => CategoryTheory.Sheaf.Hom.addCommGroup, add_comp := ⋯, comp_add := ⋯ }
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.
Equations
- CategoryTheory.Presheaf.isLimitOfIsSheaf J P S hP = { lift := fun (E : CategoryTheory.Limits.Multifork (S.index P)) => hP.amalgamate S (fun (x : S.Arrow) => E.ι x) ⋯, fac := ⋯, uniq := ⋯ }
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)
:
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.
Equations
- hP.isLimitMultifork S = ⋯.some
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)]
:
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 [MLM92], as well as the fork diagram of the Stacks entry.
Stacks Tag 00VM (The middle object of the fork diagram there.)
Equations
Instances For
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 [MLM92], as well as the fork diagram of the Stacks entry.
Stacks Tag 00VM (The left morphism the fork diagram there.)
Equations
Instances For
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.
Stacks Tag 00VM (The rightmost object of the fork diagram there.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Stacks Tag 00VM (The map pr₀* there.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Stacks Tag 00VM (The map pr₁* there.)
Equations
- One or more equations did not get rendered due to their size.
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'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
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, eg groups, abelian groups and rings, but not for the category of topological spaces, topological rings, etc since reflecting isomorphisms doesn't hold.