Sheaves taking values in a category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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, seecategory_theory.presheaf.is_sheaf. - When
A = Type, this recovers the basic definition of sheaves of sets, seecategory_theory.is_sheaf_iff_is_sheaf_of_type. - An alternate definition when
Cis small, has pullbacks andAhas products is given by an equalizer conditioncategory_theory.presheaf.is_sheaf'. This is equivalent to the earlier definition, shown incategory_theory.presheaf.is_sheaf_iff_is_sheaf'. - When
A = Type, this is definitionally equal to the equalizer condition for presieves incategory_theory.sites.sheaf_of_types. - 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 (category_theory.presheaf.is_sheaf_iff_is_sheaf_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.
def
category_theory.presheaf.is_sheaf
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A) :
Prop
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
- category_theory.presheaf.is_sheaf J P = ∀ (E : A), category_theory.presieve.is_sheaf J (P ⋙ category_theory.coyoneda.obj (opposite.op E))
@[simp]
theorem
category_theory.presheaf.cones_equiv_sieve_compatible_family_symm_apply_app
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : category_theory.sieve X)
(E : Aᵒᵖ)
(x : {x // x.sieve_compatible})
(f : (category_theory.full_subcategory (λ (f : category_theory.over X), S.arrows f.hom))ᵒᵖ) :
(⇑((category_theory.presheaf.cones_equiv_sieve_compatible_family P S E).symm) x).app f = x.val (opposite.unop f).obj.hom _
@[simp]
theorem
category_theory.presheaf.cones_equiv_sieve_compatible_family_apply_coe
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : category_theory.sieve X)
(E : Aᵒᵖ)
(π : (S.arrows.diagram.op ⋙ P).cones.obj E)
(Y : C)
(f : Y ⟶ X)
(h : ⇑S f) :
↑(⇑(category_theory.presheaf.cones_equiv_sieve_compatible_family P S E) π) f h = π.app (opposite.op {obj := category_theory.over.mk f, property := h})
def
category_theory.presheaf.cones_equiv_sieve_compatible_family
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : category_theory.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
- category_theory.presheaf.cones_equiv_sieve_compatible_family P S E = {to_fun := λ (π : (S.arrows.diagram.op ⋙ P).cones.obj E), ⟨λ (Y : C) (f : Y ⟶ X) (h : ⇑S f), π.app (opposite.op {obj := category_theory.over.mk f, property := h}), _⟩, inv_fun := λ (x : {x // x.sieve_compatible}), {app := λ (f : (category_theory.full_subcategory (λ (f : category_theory.over X), S.arrows f.hom))ᵒᵖ), x.val (opposite.unop f).obj.hom _, naturality' := _}, left_inv := _, right_inv := _}
@[simp]
def
category_theory.presieve.family_of_elements.sieve_compatible.cone
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{P : Cᵒᵖ ⥤ A}
{X : C}
{S : category_theory.sieve X}
{E : Aᵒᵖ}
{x : category_theory.presieve.family_of_elements (P ⋙ category_theory.coyoneda.obj E) ⇑S}
(hx : x.sieve_compatible) :
The cone corresponding to a sieve_compatible family of elements, dot notation enabled.
Equations
- hx.cone = {X := opposite.unop E, π := (category_theory.presheaf.cones_equiv_sieve_compatible_family P S E).inv_fun ⟨x, hx⟩}
def
category_theory.presheaf.hom_equiv_amalgamation
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{P : Cᵒᵖ ⥤ A}
{X : C}
{S : category_theory.sieve X}
{E : Aᵒᵖ}
{x : category_theory.presieve.family_of_elements (P ⋙ category_theory.coyoneda.obj E) ⇑S}
(hx : x.sieve_compatible) :
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.
theorem
category_theory.presheaf.is_limit_iff_is_sheaf_for
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : category_theory.sieve X) :
nonempty (category_theory.limits.is_limit (P.map_cone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), category_theory.presieve.is_sheaf_for (P ⋙ category_theory.coyoneda.obj E) ⇑S
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
category_theory.presheaf.subsingleton_iff_is_separated_for
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : category_theory.sieve X) :
(∀ (c : category_theory.limits.cone (S.arrows.diagram.op ⋙ P)), subsingleton (c ⟶ P.map_cone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), category_theory.presieve.is_separated_for (P ⋙ category_theory.coyoneda.obj E) ⇑S
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
category_theory.presheaf.is_sheaf_iff_is_limit
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A) :
category_theory.presheaf.is_sheaf J P ↔ ∀ ⦃X : C⦄ (S : category_theory.sieve X), S ∈ ⇑J X → nonempty (category_theory.limits.is_limit (P.map_cone S.arrows.cocone.op))
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
category_theory.presheaf.is_separated_iff_subsingleton
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A) :
(∀ (E : A), category_theory.presieve.is_separated J (P ⋙ category_theory.coyoneda.obj (opposite.op E))) ↔ ∀ ⦃X : C⦄ (S : category_theory.sieve X), S ∈ ⇑J X → ∀ (c : category_theory.limits.cone (S.arrows.diagram.op ⋙ P)), subsingleton (c ⟶ P.map_cone 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
category_theory.presheaf.is_limit_iff_is_sheaf_for_presieve
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(P : Cᵒᵖ ⥤ A)
{X : C}
(R : category_theory.presieve X) :
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
category_theory.presheaf.is_sheaf_iff_is_limit_pretopology
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_pullbacks C]
(K : category_theory.pretopology C) :
category_theory.presheaf.is_sheaf (category_theory.pretopology.to_grothendieck C K) P ↔ ∀ ⦃X : C⦄ (R : category_theory.presieve X), R ∈ ⇑K X → nonempty (category_theory.limits.is_limit (P.map_cone (category_theory.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
category_theory.presheaf.is_sheaf.amalgamate
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
{E : A}
{X : C}
{P : Cᵒᵖ ⥤ A}
(hP : category_theory.presheaf.is_sheaf J P)
(S : J.cover X)
(x : Π (I : S.arrow), E ⟶ P.obj (opposite.op I.Y))
(hx : ∀ (I : S.relation), x I.fst ≫ P.map I.g₁.op = x I.snd ≫ P.map I.g₂.op) :
E ⟶ P.obj (opposite.op X)
This is a wrapper around presieve.is_sheaf_for.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 (λ (Y : C) (f : Y ⟶ X) (hf : ⇑↑S f), x {Y := Y, f := f, hf := hf}) _
@[simp]
theorem
category_theory.presheaf.is_sheaf.amalgamate_map
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
{E : A}
{X : C}
{P : Cᵒᵖ ⥤ A}
(hP : category_theory.presheaf.is_sheaf J P)
(S : J.cover X)
(x : Π (I : S.arrow), E ⟶ P.obj (opposite.op I.Y))
(hx : ∀ (I : S.relation), x I.fst ≫ P.map I.g₁.op = x I.snd ≫ P.map I.g₂.op)
(I : S.arrow) :
@[simp]
theorem
category_theory.presheaf.is_sheaf.amalgamate_map_assoc
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
{E : A}
{X : C}
{P : Cᵒᵖ ⥤ A}
(hP : category_theory.presheaf.is_sheaf J P)
(S : J.cover X)
(x : Π (I : S.arrow), E ⟶ P.obj (opposite.op I.Y))
(hx : ∀ (I : S.relation), x I.fst ≫ P.map I.g₁.op = x I.snd ≫ P.map I.g₂.op)
(I : S.arrow)
{X' : A}
(f' : P.obj (opposite.op I.Y) ⟶ X') :
theorem
category_theory.presheaf.is_sheaf.hom_ext
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
{E : A}
{X : C}
{P : Cᵒᵖ ⥤ A}
(hP : category_theory.presheaf.is_sheaf J P)
(S : J.cover X)
(e₁ e₂ : E ⟶ P.obj (opposite.op X))
(h : ∀ (I : S.arrow), e₁ ≫ P.map I.f.op = e₂ ≫ P.map I.f.op) :
e₁ = e₂
theorem
category_theory.presheaf.is_sheaf_of_iso_iff
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
{P P' : Cᵒᵖ ⥤ A}
(e : P ≅ P') :
theorem
category_theory.presheaf.is_sheaf_of_is_terminal
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
{X : A}
(hX : category_theory.limits.is_terminal X) :
structure
category_theory.Sheaf
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A] :
Type (max u₁ u₂ v₁ v₂)
- val : Cᵒᵖ ⥤ A
- cond : category_theory.presheaf.is_sheaf J self.val
The category of sheaves taking values in A on a grothendieck topology.
Instances for category_theory.Sheaf
- category_theory.Sheaf.has_sizeof_inst
- category_theory.Sheaf.category_theory.category
- category_theory.Sheaf.inhabited
- category_theory.Sheaf.preadditive
- category_theory.Sheaf.category_theory.limits.has_limits_of_shape
- category_theory.Sheaf.category_theory.limits.has_limits
- category_theory.Sheaf.category_theory.limits.has_colimits_of_shape
- category_theory.Sheaf.category_theory.limits.has_colimits
- category_theory.Sheaf.limits.has_finite_products
- category_theory.Sheaf_is_abelian
- category_theory.grothendieck_topology.category_theory.Sheaf.category_theory.limits.has_images
theorem
category_theory.Sheaf.hom.ext_iff
{C : Type u₁}
{_inst_1 : category_theory.category C}
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
{_inst_2 : category_theory.category A}
{X Y : category_theory.Sheaf J A}
(x y : X.hom Y) :
@[ext]
structure
category_theory.Sheaf.hom
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
(X Y : category_theory.Sheaf J A) :
Type (max u₁ v₂)
Morphisms between sheaves are just morphisms of presheaves.
Instances for category_theory.Sheaf.hom
- category_theory.Sheaf.hom.has_sizeof_inst
- category_theory.Sheaf.hom.inhabited
theorem
category_theory.Sheaf.hom.ext
{C : Type u₁}
{_inst_1 : category_theory.category C}
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
{_inst_2 : category_theory.category A}
{X Y : category_theory.Sheaf J A}
(x y : X.hom Y)
(h : x.val = y.val) :
x = y
@[simp]
theorem
category_theory.Sheaf.category_theory.category_id_val
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
(X : category_theory.Sheaf J A) :
@[simp]
theorem
category_theory.Sheaf.category_theory.category_comp_val
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
(X Y Z : category_theory.Sheaf J A)
(f : X ⟶ Y)
(g : Y ⟶ Z) :
@[protected, instance]
def
category_theory.Sheaf.category_theory.category
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A] :
Equations
- category_theory.Sheaf.category_theory.category = {to_category_struct := {to_quiver := {hom := category_theory.Sheaf.hom _inst_2}, id := λ (X : category_theory.Sheaf J A), {val := 𝟙 X.val}, comp := λ (X Y Z : category_theory.Sheaf J A) (f : X ⟶ Y) (g : Y ⟶ Z), {val := f.val ≫ g.val}}, id_comp' := _, comp_id' := _, assoc' := _}
@[protected, instance]
def
category_theory.Sheaf.hom.inhabited
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
(X : category_theory.Sheaf J A) :
Equations
@[simp]
theorem
category_theory.Sheaf_to_presheaf_map
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A]
(_x _x_1 : category_theory.Sheaf J A)
(f : _x ⟶ _x_1) :
(category_theory.Sheaf_to_presheaf J A).map f = f.val
def
category_theory.Sheaf_to_presheaf
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A] :
category_theory.Sheaf J A ⥤ Cᵒᵖ ⥤ A
The inclusion functor from sheaves to presheaves.
Equations
- category_theory.Sheaf_to_presheaf J A = {obj := category_theory.Sheaf.val _inst_2, map := λ (_x _x_1 : category_theory.Sheaf J A) (f : _x ⟶ _x_1), f.val, map_id' := _, map_comp' := _}
Instances for category_theory.Sheaf_to_presheaf
- category_theory.Sheaf_to_presheaf.full
- category_theory.Sheaf_to_presheaf.faithful
- category_theory.Sheaf_to_presheaf_is_right_adjoint
- category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limit
- category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits_of_shape
- category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits
- category_theory.Sheaf_to_presheaf.creates_limits
@[simp]
theorem
category_theory.Sheaf_to_presheaf_obj
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A]
(self : category_theory.Sheaf J A) :
(category_theory.Sheaf_to_presheaf J A).obj self = self.val
@[protected, instance]
def
category_theory.Sheaf_to_presheaf.full
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A] :
Equations
- category_theory.Sheaf_to_presheaf.full J A = {preimage := λ (X Y : category_theory.Sheaf J A) (f : (category_theory.Sheaf_to_presheaf J A).obj X ⟶ (category_theory.Sheaf_to_presheaf J A).obj Y), {val := f}, witness' := _}
@[protected, instance]
def
category_theory.Sheaf_to_presheaf.faithful
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A] :
theorem
category_theory.Sheaf.hom.mono_of_presheaf_mono
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A]
{F G : category_theory.Sheaf J A}
(f : F ⟶ G)
[h : category_theory.mono f.val] :
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).
@[protected, instance]
def
category_theory.Sheaf.hom.epi_of_presheaf_epi
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(A : Type u₂)
[category_theory.category A]
{F G : category_theory.Sheaf J A}
(f : F ⟶ G)
[h : category_theory.epi f.val] :
def
category_theory.sheaf_over
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
(ℱ : category_theory.Sheaf J A)
(E : A) :
The sheaf of sections guaranteed by the sheaf condition.
Equations
- category_theory.sheaf_over ℱ E = {val := ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op E), cond := _}
@[simp]
theorem
category_theory.sheaf_over_val
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{J : category_theory.grothendieck_topology C}
(ℱ : category_theory.Sheaf J A)
(E : A) :
(category_theory.sheaf_over ℱ E).val = ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op E)
theorem
category_theory.is_sheaf_iff_is_sheaf_of_type
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ Type w) :
@[simp]
theorem
category_theory.Sheaf_equiv_SheafOfTypes_counit_iso
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C) :
(category_theory.Sheaf_equiv_SheafOfTypes J).counit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.SheafOfTypes J), {hom := {val := 𝟙 (({obj := λ (S : category_theory.SheafOfTypes J), {val := S.val, cond := _}, map := λ (S T : category_theory.SheafOfTypes J) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _} ⋙ {obj := λ (S : category_theory.Sheaf J (Type w)), {val := S.val, cond := _}, map := λ (S T : category_theory.Sheaf J (Type w)) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _}).obj X).val}, inv := {val := 𝟙 ((𝟭 (category_theory.SheafOfTypes J)).obj X).val}, hom_inv_id' := _, inv_hom_id' := _}) _
def
category_theory.Sheaf_equiv_SheafOfTypes
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C) :
The category of sheaves taking values in Type is the same as the category of set-valued sheaves.
Equations
- category_theory.Sheaf_equiv_SheafOfTypes J = {functor := {obj := λ (S : category_theory.Sheaf J (Type w)), {val := S.val, cond := _}, map := λ (S T : category_theory.Sheaf J (Type w)) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _}, inverse := {obj := λ (S : category_theory.SheafOfTypes J), {val := S.val, cond := _}, map := λ (S T : category_theory.SheafOfTypes J) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _}, unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.Sheaf J (Type w)), {hom := {val := 𝟙 ((𝟭 (category_theory.Sheaf J (Type w))).obj X).val}, inv := {val := 𝟙 (({obj := λ (S : category_theory.Sheaf J (Type w)), {val := S.val, cond := _}, map := λ (S T : category_theory.Sheaf J (Type w)) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _} ⋙ {obj := λ (S : category_theory.SheafOfTypes J), {val := S.val, cond := _}, map := λ (S T : category_theory.SheafOfTypes J) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _}).obj X).val}, hom_inv_id' := _, inv_hom_id' := _}) _, counit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.SheafOfTypes J), {hom := {val := 𝟙 (({obj := λ (S : category_theory.SheafOfTypes J), {val := S.val, cond := _}, map := λ (S T : category_theory.SheafOfTypes J) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _} ⋙ {obj := λ (S : category_theory.Sheaf J (Type w)), {val := S.val, cond := _}, map := λ (S T : category_theory.Sheaf J (Type w)) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _}).obj X).val}, inv := {val := 𝟙 ((𝟭 (category_theory.SheafOfTypes J)).obj X).val}, hom_inv_id' := _, inv_hom_id' := _}) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.Sheaf_equiv_SheafOfTypes_functor_obj_val
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(S : category_theory.Sheaf J (Type w)) :
@[simp]
theorem
category_theory.Sheaf_equiv_SheafOfTypes_inverse_obj_val
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(S : category_theory.SheafOfTypes J) :
@[simp]
theorem
category_theory.Sheaf_equiv_SheafOfTypes_functor_map_val
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(S T : category_theory.Sheaf J (Type w))
(f : S ⟶ T) :
@[simp]
theorem
category_theory.Sheaf_equiv_SheafOfTypes_unit_iso
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C) :
(category_theory.Sheaf_equiv_SheafOfTypes J).unit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.Sheaf J (Type w)), {hom := {val := 𝟙 ((𝟭 (category_theory.Sheaf J (Type w))).obj X).val}, inv := {val := 𝟙 (({obj := λ (S : category_theory.Sheaf J (Type w)), {val := S.val, cond := _}, map := λ (S T : category_theory.Sheaf J (Type w)) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _} ⋙ {obj := λ (S : category_theory.SheafOfTypes J), {val := S.val, cond := _}, map := λ (S T : category_theory.SheafOfTypes J) (f : S ⟶ T), {val := f.val}, map_id' := _, map_comp' := _}).obj X).val}, hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
theorem
category_theory.Sheaf_equiv_SheafOfTypes_inverse_map_val
{C : Type u₁}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(S T : category_theory.SheafOfTypes J)
(f : S ⟶ T) :
@[protected, instance]
def
category_theory.Sheaf.inhabited
{C : Type u₁}
[category_theory.category C] :
inhabited (category_theory.Sheaf ⊥ (Type w))
noncomputable
def
category_theory.Sheaf.is_terminal_of_bot_cover
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
(F : category_theory.Sheaf J A)
(X : C)
(H : ⊥ ∈ ⇑J X) :
If the empty sieve is a cover of X, then F(X) is terminal.
Equations
@[protected, instance]
def
category_theory.Sheaf_hom_has_zsmul
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A} :
@[protected, instance]
def
category_theory.quiver.hom.has_sub
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A} :
@[protected, instance]
def
category_theory.quiver.hom.has_neg
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A} :
@[protected, instance]
def
category_theory.Sheaf_hom_has_nsmul
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A} :
@[protected, instance]
def
category_theory.quiver.hom.has_zero
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A} :
@[protected, instance]
def
category_theory.quiver.hom.has_add
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A} :
@[simp]
theorem
category_theory.Sheaf.hom.add_app
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A}
(f g : P ⟶ Q)
(U : Cᵒᵖ) :
@[protected, instance]
def
category_theory.quiver.hom.add_comm_group
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A]
{P Q : category_theory.Sheaf J A} :
add_comm_group (P ⟶ Q)
Equations
- category_theory.quiver.hom.add_comm_group = function.injective.add_comm_group (λ (f : P.hom Q), f.val) category_theory.quiver.hom.add_comm_group._proof_1 category_theory.quiver.hom.add_comm_group._proof_2 category_theory.quiver.hom.add_comm_group._proof_3 category_theory.quiver.hom.add_comm_group._proof_4 category_theory.quiver.hom.add_comm_group._proof_5 category_theory.quiver.hom.add_comm_group._proof_6 category_theory.quiver.hom.add_comm_group._proof_7
@[protected, instance]
def
category_theory.Sheaf.preadditive
{C : Type u₁}
[category_theory.category C]
{J : category_theory.grothendieck_topology C}
{A : Type u₂}
[category_theory.category A]
[category_theory.preadditive A] :
Equations
- category_theory.Sheaf.preadditive = {hom_group := λ (P Q : category_theory.Sheaf J A), infer_instance, add_comp' := _, comp_add' := _}
noncomputable
def
category_theory.presheaf.is_limit_of_is_sheaf
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : J.cover X)
(hP : category_theory.presheaf.is_sheaf J P) :
When P is a sheaf and S is a cover, the associated multifork is a limit.
Equations
- category_theory.presheaf.is_limit_of_is_sheaf J P S hP = {lift := λ (E : category_theory.limits.multifork (S.index P)), hP.amalgamate S (λ (I : S.arrow), E.ι I) _, fac' := _, uniq' := _}
theorem
category_theory.presheaf.is_sheaf_iff_multifork
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A) :
category_theory.presheaf.is_sheaf J P ↔ ∀ (X : C) (S : J.cover X), nonempty (category_theory.limits.is_limit (S.multifork P))
theorem
category_theory.presheaf.is_sheaf_iff_multiequalizer
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A)
[∀ (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] :
category_theory.presheaf.is_sheaf J P ↔ ∀ (X : C) (S : J.cover X), category_theory.is_iso (S.to_multiequalizer P)
noncomputable
def
category_theory.presheaf.first_obj
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{U : C}
(R : category_theory.presieve U)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_products A] :
A
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.presheaf.first_obj R P = ∏ λ (f : Σ (V : C), {f // R f}), P.obj (opposite.op f.fst)
noncomputable
def
category_theory.presheaf.fork_map
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{U : C}
(R : category_theory.presieve U)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_products A] :
P.obj (opposite.op U) ⟶ category_theory.presheaf.first_obj R P
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.presheaf.fork_map R P = category_theory.limits.pi.lift (λ (f : Σ (V : C), {f // R f}), P.map f.snd.val.op)
noncomputable
def
category_theory.presheaf.second_obj
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{U : C}
(R : category_theory.presieve U)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_products A]
[category_theory.limits.has_pullbacks C] :
A
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.
noncomputable
def
category_theory.presheaf.first_map
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{U : C}
(R : category_theory.presieve U)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_products A]
[category_theory.limits.has_pullbacks C] :
The map pr₀* of https://stacks.math.columbia.edu/tag/00VM.
Equations
- category_theory.presheaf.first_map R P = category_theory.limits.pi.lift (λ (fg : (Σ (V : C), {f // R f}) × Σ (W : C), {g // R g}), category_theory.limits.pi.π (λ (f : Σ (V : C), {f // R f}), P.obj (opposite.op f.fst)) fg.fst ≫ P.map category_theory.limits.pullback.fst.op)
noncomputable
def
category_theory.presheaf.second_map
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{U : C}
(R : category_theory.presieve U)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_products A]
[category_theory.limits.has_pullbacks C] :
The map pr₁* of https://stacks.math.columbia.edu/tag/00VM.
Equations
- category_theory.presheaf.second_map R P = category_theory.limits.pi.lift (λ (fg : (Σ (V : C), {f // R f}) × Σ (W : C), {g // R g}), category_theory.limits.pi.π (λ (f : Σ (V : C), {f // R f}), P.obj (opposite.op f.fst)) fg.snd ≫ P.map category_theory.limits.pullback.snd.op)
theorem
category_theory.presheaf.w
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{U : C}
(R : category_theory.presieve U)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_products A]
[category_theory.limits.has_pullbacks C] :
def
category_theory.presheaf.is_sheaf'
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
[category_theory.limits.has_products A]
[category_theory.limits.has_pullbacks C]
(P : Cᵒᵖ ⥤ A) :
Prop
An alternative definition of the sheaf condition in terms of equalizers. This is shown to be
equivalent in category_theory.presheaf.is_sheaf_iff_is_sheaf'.
Equations
noncomputable
def
category_theory.presheaf.is_sheaf_for_is_sheaf_for'
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
[category_theory.limits.has_products A]
[category_theory.limits.has_pullbacks C]
(P : Cᵒᵖ ⥤ A)
(s : A ⥤ Type (max v₁ u₁))
[Π (J : Type (max v₁ u₁)), category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) s]
(U : C)
(R : category_theory.presieve U) :
(Implementation). An auxiliary lemma to convert between sheaf conditions.
Equations
- category_theory.presheaf.is_sheaf_for_is_sheaf_for' P s U R = (category_theory.limits.is_limit_map_cone_fork_equiv s _).trans ((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.nat_iso.of_components (λ (X : category_theory.limits.walking_parallel_pair), X.cases_on (category_theory.limits.preserves_product.iso s (λ (f : Σ (V : C), {f // R f}), P.obj (opposite.op f.fst))) (category_theory.limits.preserves_product.iso s (λ (fg : (Σ (V : C), {f // R f}) × Σ (W : C), {g // R g}), P.obj (opposite.op (category_theory.limits.pullback fg.fst.snd.val fg.snd.snd.val))))) _) (category_theory.limits.fork.of_ι (s.map (category_theory.presheaf.fork_map R P)) _)).symm.trans (category_theory.limits.is_limit.equiv_iso_limit (category_theory.limits.fork.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.nat_iso.of_components (λ (X : category_theory.limits.walking_parallel_pair), X.cases_on (category_theory.limits.preserves_product.iso s (λ (f : Σ (V : C), {f // R f}), P.obj (opposite.op f.fst))) (category_theory.limits.preserves_product.iso s (λ (fg : (Σ (V : C), {f // R f}) × Σ (W : C), {g // R g}), P.obj (opposite.op (category_theory.limits.pullback fg.fst.snd.val fg.snd.snd.val))))) _).hom).obj (category_theory.limits.fork.of_ι (s.map (category_theory.presheaf.fork_map R P)) _)).X) _)))
theorem
category_theory.presheaf.is_sheaf_iff_is_sheaf'
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_products A]
[category_theory.limits.has_pullbacks C] :
The equalizer definition of a sheaf given by is_sheaf' is equivalent to is_sheaf.
theorem
category_theory.presheaf.is_sheaf_iff_is_sheaf_forget
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
(J : category_theory.grothendieck_topology C)
(P : Cᵒᵖ ⥤ A)
[category_theory.limits.has_pullbacks C]
(s : A ⥤ Type (max v₁ u₁))
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_limits s]
[category_theory.reflects_isomorphisms s] :
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.