mathlib3 documentation

category_theory.sites.sheaf

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.

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

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

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

Given sieve S and presheaf P : Cᵒᵖ ⥤ A, their natural associated cone is a limit cone iff Hom (E, P -) is a sheaf of types for the sieve S and all E : A.

Given sieve S and presheaf P : Cᵒᵖ ⥤ A, their natural associated cone admits at most one morphism from every cone in the same category (i.e. over the same diagram), iff Hom (E, P -)is separated for the sieve S and all E : A.

A presheaf P is a sheaf for the Grothendieck topology J iff for every covering sieve S of J, the natural cone associated to P and S is a limit cone.

A presheaf P is separated for the Grothendieck topology J iff for every covering sieve S of J, the natural cone associated to P and S admits at most one morphism from every cone in the same category.

Given presieve R and presheaf P : Cᵒᵖ ⥤ A, the natural cone associated to P and the sieve sieve.generate R generated by R is a limit cone iff Hom (E, P -) is a sheaf of types for the presieve R and all E : A.

A presheaf P is a sheaf for the Grothendieck topology generated by a pretopology K iff for every covering presieve R of K, the natural cone associated to P and sieve.generate R is a limit cone.

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) :

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
@[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) :
hP.amalgamate S x hx P.map I.f.op = x I
@[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') :
hP.amalgamate S x hx P.map I.f.op f' = x I f'
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.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) :
x = y x.val = y.val
@[ext]

Morphisms between sheaves are just morphisms of presheaves.

Instances for category_theory.Sheaf.hom
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

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).

The sheaf of sections guaranteed by the sheaf condition.

Equations

The category of sheaves taking values in Type is the same as the category of set-valued sheaves.

Equations
@[protected, instance]
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

When P is a sheaf and S is a cover, the associated multifork is a limit.

Equations

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

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

The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which contains the data used to check a family of elements for a presieve is compatible.

Equations

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

(Implementation). An auxiliary lemma to convert between sheaf conditions.

Equations

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.