mathlib documentation

category_theory.sites.sheaf_of_types

Sheaves of types on a Grothendieck topology #

Defines the notion of a sheaf of types (usually called a sheaf of sets by mathematicians) on a category equipped with a Grothendieck topology, as well as a range of equivalent conditions useful in different situations.

First define what it means for a presheaf P : Cᵒᵖ ⥤ Type v to be a sheaf for a particular presieve R on X:

In the special case where R is a sieve, the compatibility condition can be simplified:

In the special case where C has pullbacks, the compatibility condition can be simplified:

Now given a Grothendieck topology J, P is a sheaf if it is a sheaf for every sieve in the topology. See is_sheaf.

In the case where the topology is generated by a basis, it suffices to check P is a sheaf for every presieve in the pretopology. See is_sheaf_pretopology.

We also provide equivalent conditions to satisfy alternate definitions given in the literature.

Implementation #

The sheaf condition is given as a proposition, rather than a subsingleton in Type (max u₁ v). This doesn't seem to make a big difference, other than making a couple of definitions noncomputable, but it means that equivalent conditions can be given as statements rather than statements, which can be convenient.

References #

def category_theory.presieve.family_of_elements {C : Type u₁} [category_theory.category C] {X : C} (P : Cᵒᵖ Type w) (R : category_theory.presieve X) :
Type (max u₁ v₁ w)

A family of elements for a presheaf P given a collection of arrows R with fixed codomain X consists of an element of P Y for every f : Y ⟶ X in R. A presheaf is a sheaf (resp, separated) if every compatible family of elements has exactly one (resp, at most one) amalgamation.

This data is referred to as a family in [MM92], Chapter III, Section 4. It is also a concrete version of the elements of the middle object in https://stacks.math.columbia.edu/tag/00VM which is more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Joh02].

Equations
Instances for category_theory.presieve.family_of_elements

A family of elements for a presheaf on the presieve R₂ can be restricted to a smaller presieve R₁.

Equations

A family of elements for the arrow set R is compatible if for any f₁ : Y₁ ⟶ X and f₂ : Y₂ ⟶ X in R, and any g₁ : Z ⟶ Y₁ and g₂ : Z ⟶ Y₂, if the square g₁ ≫ f₁ = g₂ ≫ f₂ commutes then the elements of P Z obtained by restricting the element of P Y₁ along g₁ and restricting the element of P Y₂ along g₂ are the same.

In special cases, this condition can be simplified, see pullback_compatible_iff and compatible_iff_sieve_compatible.

This is referred to as a "compatible family" in Definition C2.1.2 of [Joh02], and on nlab: https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents

Equations
  • x.compatible = ∀ ⦃Y₁ Y₂ Z : C⦄ (g₁ : Z Y₁) (g₂ : Z Y₂) ⦃f₁ : Y₁ X⦄ ⦃f₂ : Y₂ X⦄ (h₁ : R f₁) (h₂ : R f₂), g₁ f₁ = g₂ f₂P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)

If the category C has pullbacks, this is an alternative condition for a family of elements to be compatible: For any f : Y ⟶ X and g : Z ⟶ X in the presieve R, the restriction of the given elements for f and g to the pullback agree. This is equivalent to being compatible (provided C has pullbacks), shown in pullback_compatible_iff.

This is the definition for a "matching" family given in [MM92], Chapter III, Section 4, Equation (5). Viewing the type family_of_elements as the middle object of the fork in https://stacks.math.columbia.edu/tag/00VM, this condition expresses that pr₀* (x) = pr₁* (x), using the notation defined there.

Equations

The restriction of a compatible family is compatible.

Extend a family of elements to the sieve generated by an arrow set. This is the construction described as "easy" in Lemma C2.1.3 of [Joh02].

Equations

The extension of a compatible family to the generated sieve is compatible.

theorem category_theory.presieve.extend_agrees {C : Type u₁} [category_theory.category C] {P : Cᵒᵖ Type w} {X Y : C} {R : category_theory.presieve X} {x : category_theory.presieve.family_of_elements P R} (t : x.compatible) {f : Y X} (hf : R f) :
x.sieve_extend f _ = x f hf

The extension of a family agrees with the original family.

@[simp]

The restriction of an extension is the original.

If the arrow set for a family of elements is actually a sieve (i.e. it is downward closed) then the consistency condition can be simplified. This is an equivalent condition, see compatible_iff_sieve_compatible.

This is the notion of "matching" given for families on sieves given in [MM92], Chapter III, Section 4, Equation 1, and nlab: https://ncatlab.org/nlab/show/matching+family. See also the discussion before Lemma C2.1.4 of [Joh02].

Equations
@[simp]

Given a family of elements x for the sieve S generated by a presieve R, if x is restricted to R and then extended back up to S, the resulting extension equals x.

Two compatible families on the sieve generated by a presieve R are equal if and only if they are equal when restricted to R.

noncomputable def category_theory.presieve.compatible_equiv_generate_sieve_compatible {C : Type u₁} [category_theory.category C] {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} :
{x // x.compatible} {x // x.compatible}

Compatible families of elements for a presheaf of types P and a presieve R are in 1-1 correspondence with compatible families for the same presheaf and the sieve generated by R, through extension and restriction.

Equations
theorem category_theory.presieve.family_of_elements.comp_of_compatible {C : Type u₁} [category_theory.category C] {P : Cᵒᵖ Type w} {X Y : C} (S : category_theory.sieve X) {x : category_theory.presieve.family_of_elements P S} (t : x.compatible) {f : Y X} (hf : S f) {Z : C} (g : Z Y) :
x (g f) _ = P.map g.op (x f hf)

Given a family of elements of a sieve S on F(X), we can realize it as a family of elements of S.functor_pullback F.

Equations

Given a family of elements of a sieve S on X whose values factors through F, we can realize it as a family of elements of S.functor_pushforward F. Since the preimage is obtained by choice, this is not well-defined generally.

Equations

Given a family of elements of a sieve S on X, and a map Y ⟶ X, we can obtain a family of elements of S.pullback f by taking the same elements.

Equations

Given a morphism of presheaves f : P ⟶ Q, we can take a family of elements valued in P to a family of elements valued in Q by composing with f.

Equations

The given element t of P.obj (op X) is an amalgamation for the family of elements x if every restriction P.map f.op t = x_f for every arrow f in the presieve R.

This is the definition given in https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents, and https://ncatlab.org/nlab/show/matching+family, as well as [MM92], Chapter III, Section 4, equation (2).

Equations
def category_theory.presieve.is_separated_for {C : Type u₁} [category_theory.category C] {X : C} (P : Cᵒᵖ Type w) (R : category_theory.presieve X) :
Prop

A presheaf is separated for a presieve if there is at most one amalgamation.

Equations
theorem category_theory.presieve.is_separated_for.ext {C : Type u₁} [category_theory.category C] {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (hR : category_theory.presieve.is_separated_for P R) {t₁ t₂ : P.obj (opposite.op X)} (h : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, R fP.map f.op t₁ = P.map f.op t₂) :
t₁ = t₂
def category_theory.presieve.is_sheaf_for {C : Type u₁} [category_theory.category C] {X : C} (P : Cᵒᵖ Type w) (R : category_theory.presieve X) :
Prop

We define P to be a sheaf for the presieve R if every compatible family has a unique amalgamation.

This is the definition of a sheaf for the given presieve given in C2.1.2 of [Joh02], and https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents. Using compatible_iff_sieve_compatible, this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4.

Equations
def category_theory.presieve.yoneda_sheaf_condition {C : Type u₁} [category_theory.category C] {X : C} (P : Cᵒᵖ Type v₁) (S : category_theory.sieve X) :
Prop

This is an equivalent condition to be a sheaf, which is useful for the abstraction to local operators on elementary toposes. However this definition is defined only for sieves, not presieves. The equivalence between this and is_sheaf_for is given in yoneda_condition_iff_sheaf_condition. This version is also useful to establish that being a sheaf is preserved under isomorphism of presheaves.

See the discussion before Equation (3) of [MM92], Chapter III, Section 4. See also C2.1.4 of [Joh02]. This is also a direct reformulation of https://stacks.math.columbia.edu/tag/00Z8.

Equations

(Implementation). This is a (primarily internal) equivalence between natural transformations and compatible families.

Cf the discussion after Lemma 7.47.10 in https://stacks.math.columbia.edu/tag/00YW. See also the proof of C2.1.4 of [Joh02], and the discussion in [MM92], Chapter III, Section 4.

Equations

(Implementation). A lemma useful to prove yoneda_condition_iff_sheaf_condition.

The yoneda version of the sheaf condition is equivalent to the sheaf condition.

C2.1.4 of [Joh02].

If P is a sheaf for the sieve S on X, a natural transformation from S (viewed as a functor) to P can be (uniquely) extended to all of yoneda.obj X.

  f

S → P ↓ ↗ yX

Equations
@[simp]

Show that the extension of f : S.functor ⟶ P to all of yoneda.obj X is in fact an extension, ie that the triangle below commutes, provided P is a sheaf for S

  f

S → P ↓ ↗ yX

@[simp]

The extension of f to yoneda.obj X is unique.

If P is a sheaf for the sieve S on X, then if two natural transformations from yoneda.obj X to P agree when restricted to the subfunctor given by S, they are equal.

P is a sheaf for R iff it is separated for R and there exists an amalgamation.

If P is separated for R and every family has an amalgamation, then P is a sheaf for R.

Get the amalgamation of the given compatible family, provided we have a sheaf.

Equations
@[simp]
theorem category_theory.presieve.is_sheaf_for.valid_glue {C : Type u₁} [category_theory.category C] {P : Cᵒᵖ Type w} {X Y : C} {R : category_theory.presieve X} (t : category_theory.presieve.is_sheaf_for P R) {x : category_theory.presieve.family_of_elements P R} (hx : x.compatible) (f : Y X) (Hf : R f) :
P.map f.op (t.amalgamate x hx) = x f Hf

Every presheaf is a sheaf for the family {𝟙 X}.

[Joh02] C2.1.5(i)

Every presheaf is a sheaf for the maximal sieve.

[Joh02] C2.1.5(ii)

If P is a sheaf for S, and it is iso to P', then P' is a sheaf for S. This shows that "being a sheaf for a presieve" is a mathematical or hygenic property.

If a presieve R on X has a subsieve S such that:

  • P is a sheaf for S.
  • For every f in R, P is separated for the pullback of S along f,

then P is a sheaf for R.

This is closely related to [Joh02] C2.1.6(i).

If P is a sheaf for every pullback of the sieve S, then P is a sheaf for any presieve which contains S. This is closely related to [Joh02] C2.1.6.

A presheaf is separated for a topology if it is separated for every sieve in the topology.

Equations

A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology.

If the given topology is given by a pretopology, is_sheaf_for_pretopology shows it suffices to check the sheaf condition at presieves in the pretopology.

Equations

The property of being a sheaf is preserved by isomorphism.

For a topology generated by a basis, it suffices to check the sheaf condition on the basis presieves only.

Any presheaf is a sheaf for the bottom (trivial) grothendieck topology.

def category_theory.equalizer.first_obj {C : Type u₁} [category_theory.category C] (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X) :
Type (max v₁ u₁)

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
Instances for category_theory.equalizer.first_obj

Show that first_obj is isomorphic to family_of_elements.

Equations
@[simp]
theorem category_theory.equalizer.first_obj_eq_family_hom {C : Type u₁} [category_theory.category C] (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X) (t : category_theory.equalizer.first_obj P R) (Y : C) (f : Y X) (hf : R f) :
(category_theory.equalizer.first_obj_eq_family P R).hom t f hf = category_theory.limits.pi.π (λ (f : Σ (Y : C), {f // R f}), P.obj (opposite.op f.fst)) Y, f, hf⟩ t
noncomputable def category_theory.equalizer.fork_map {C : Type u₁} [category_theory.category C] (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X) :

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

This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and the definition of is_sheaf_for.

def category_theory.equalizer.sieve.second_obj {C : Type u₁} [category_theory.category C] (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (S : category_theory.sieve X) :
Type (max v₁ u₁)

The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used to check a family is compatible.

Equations
Instances for category_theory.equalizer.sieve.second_obj

The map p of Equations (3,4) [MM92].

Equations

The map a of Equations (3,4) [MM92].

Equations

The family of elements given by x : first_obj P S is compatible iff first_map and second_map map it to the same point.

This section establishes the equivalence between the sheaf condition of https://stacks.math.columbia.edu/tag/00VM and the definition of is_sheaf_for.

def category_theory.equalizer.presieve.second_obj {C : Type u₁} [category_theory.category C] (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X) [category_theory.limits.has_pullbacks C] :
Type (max v₁ u₁)

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
Instances for category_theory.equalizer.presieve.second_obj

The family of elements given by x : first_obj P S is compatible iff first_map and second_map map it to the same point.

structure category_theory.SheafOfTypes {C : Type u₁} [category_theory.category C] (J : category_theory.grothendieck_topology C) :
Type (max u₁ v₁ (w+1))

The category of sheaves on a grothendieck topology.

Instances for category_theory.SheafOfTypes
theorem category_theory.SheafOfTypes.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {J : category_theory.grothendieck_topology C} {X Y : category_theory.SheafOfTypes J} (x y : X.hom Y) (h : x.val = y.val) :
x = y
@[ext]

Morphisms between sheaves of types are just morphisms between the underlying presheaves.

Instances for category_theory.SheafOfTypes.hom

The category of sheaves on the bottom (trivial) grothendieck topology is equivalent to the category of presheaves.

Equations