mathlibdocumentation

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:

• A family of elements x for P at R is an element x_f of P Y for every f : Y ⟶ X in R. See family_of_elements.
• The family x is compatible if, for any f₁ : Y₁ ⟶ X and f₂ : Y₂ ⟶ X both in R, and any g₁ : Z ⟶ Y₁ and g₂ : Z ⟶ Y₂ such that g₁ ≫ f₁ = g₂ ≫ f₂, the restriction of x_f₁ along g₁ agrees with the restriction of x_f₂ along g₂. See family_of_elements.compatible.
• An amalgamation t for the family is an element of P X such that for every f : Y ⟶ X in R, the restriction of t on f is x_f. See family_of_elements.is_amalgamation. We then say P is separated for R if every compatible family has at most one amalgamation, and it is a sheaf for R if every compatible family has a unique amalgamation. See is_separated_for and is_sheaf_for.

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

• The family x is compatible if, for any f : Y ⟶ X in R and g : Z ⟶ Y, the restriction of x_f along g agrees with x_(g ≫ f) (which is well defined since g ≫ f is in R). See family_of_elements.sieve_compatible and compatible_iff_sieve_compatible.

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

• The family x is compatible if, for any f : Y ⟶ X and g : Z ⟶ X both in R, the restriction of x_f along π₁ : pullback f g ⟶ Y agrees with the restriction of x_g along π₂ : pullback f g ⟶ Z. See family_of_elements.pullback_compatible and pullback_compatible_iff.

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.

• Stacks: In equalizer.presieve.sheaf_condition, the sheaf condition at a presieve is shown to be equivalent to that of https://stacks.math.columbia.edu/tag/00VM (and combined with is_sheaf_pretopology, this shows the notions of is_sheaf are exactly equivalent.)

The condition of https://stacks.math.columbia.edu/tag/00Z8 is virtually identical to the statement of yoneda_condition_iff_sheaf_condition (since the bijection described there carries the same information as the unique existence.)

• Maclane-Moerdijk [MM92]: Using compatible_iff_sieve_compatible, the definitions of is_sheaf are equivalent. There are also alternate definitions given:

• Yoneda condition: Defined in yoneda_sheaf_condition and equivalence in yoneda_condition_iff_sheaf_condition.
• Equalizer condition (Equation 3): Defined in the equalizer.sieve namespace, and equivalence in equalizer.sieve.sheaf_condition.
• Matching family for presieves with pullback: pullback_compatible_iff.
• Sheaf for a pretopology (Prop 1): is_sheaf_pretopology combined with the previous.
• Sheaf for a pretopology as equalizer (Prop 1, bis): equalizer.presieve.sheaf_condition combined with the previous.

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₁} {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
@[protected, instance]
def category_theory.presieve.family_of_elements.inhabited {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} :
Equations
def category_theory.presieve.family_of_elements.restrict {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R₁ R₂ : category_theory.presieve X} (h : R₁ R₂) :

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

Equations
• = λ (x : (Y : C) (f : Y X) (hf : R₁ f), x f _
def category_theory.presieve.family_of_elements.compatible {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X}  :
Prop

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₂)
def category_theory.presieve.family_of_elements.pullback_compatible {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X}  :
Prop

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
• x.pullback_compatible = ∀ ⦃Y₁ Y₂ : C⦄ ⦃f₁ : Y₁ X⦄ ⦃f₂ : Y₂ X⦄ (h₁ : R f₁) (h₂ : R f₂), (x f₁ h₁) = (x f₂ h₂)
theorem category_theory.presieve.pullback_compatible_iff {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X}  :
theorem category_theory.presieve.family_of_elements.compatible.restrict {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R₁ R₂ : category_theory.presieve X} (h : R₁ R₂)  :

The restriction of a compatible family is compatible.

noncomputable def category_theory.presieve.family_of_elements.sieve_extend {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X}  :

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₁} {P : Cᵒᵖ Type w} {X Y : C} {R : category_theory.presieve X} (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]
theorem category_theory.presieve.restrict_extend {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (t : x.compatible) :

The restriction of an extension is the original.

def category_theory.presieve.family_of_elements.sieve_compatible {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {S : category_theory.sieve X}  :
Prop

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
theorem category_theory.presieve.compatible_iff_sieve_compatible {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {S : category_theory.sieve X}  :
@[simp]
theorem category_theory.presieve.extend_restrict {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (t : x.compatible) :

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.

theorem category_theory.presieve.restrict_inj {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (t₁ : x₁.compatible) (t₂ : x₂.compatible) :

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

@[simp]
noncomputable def category_theory.presieve.compatible_equiv_generate_sieve_compatible {C : Type u₁} {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₁} {P : Cᵒᵖ Type w} {X Y : C} (S : category_theory.sieve X) (t : x.compatible) {f : Y X} (hf : S f) {Z : C} (g : Z Y) :
x (g f) _ = P.map g.op (x f hf)
def category_theory.presieve.family_of_elements.functor_pullback {C : Type u₁} {P : Cᵒᵖ Type w} {D : Type u₂} (F : D C) {Z : D} {T : category_theory.presieve (F.obj Z)}  :

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
• = λ (Y : D) (f : Y Z) (hf : , x (F.map f) hf
theorem category_theory.presieve.family_of_elements.compatible.functor_pullback {C : Type u₁} {P : Cᵒᵖ Type w} {D : Type u₂} (F : D C) {Z : D} {T : category_theory.presieve (F.obj Z)} (h : x.compatible) :
noncomputable def category_theory.presieve.family_of_elements.functor_pushforward {C : Type u₁} {P : Cᵒᵖ Type w} {D : Type u₂} (F : D C) {X : D} {T : category_theory.presieve X} (x : T) :

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
• = λ (Y : C) (f : Y F.obj X) (h : , (λ (Z : D) (g : Z X) (h : Y F.obj Z) (h₁ : T g) (fac : f = h F.map g), P.map h.op (x g h₁))
def category_theory.presieve.family_of_elements.pullback {C : Type u₁} {P : Cᵒᵖ Type w} {X Y : C} {S : category_theory.sieve X} (f : Y X)  :

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
• = λ (_x : C) (g : _x Y) (hg : g), x (g f) hg
theorem category_theory.presieve.family_of_elements.compatible.pullback {C : Type u₁} {P : Cᵒᵖ Type w} {X Y : C} {S : category_theory.sieve X} (f : Y X) (h : x.compatible) :
def category_theory.presieve.family_of_elements.comp_presheaf_map {C : Type u₁} {P Q : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (f : P Q)  :

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
@[simp]
@[simp]
theorem category_theory.presieve.family_of_elements.comp_prersheaf_map_comp {C : Type u₁} {P Q U : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (f : P Q) (g : Q U) :
theorem category_theory.presieve.family_of_elements.compatible.comp_presheaf_map {C : Type u₁} {P Q : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (f : P Q) (h : x.compatible) :
def category_theory.presieve.family_of_elements.is_amalgamation {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (t : P.obj (opposite.op X)) :
Prop

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
• = ∀ ⦃Y : C⦄ (f : Y X) (h : R f), P.map f.op t = x f h
theorem category_theory.presieve.family_of_elements.is_amalgamation.comp_presheaf_map {C : Type u₁} {P Q : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} {t : P.obj (opposite.op X)} (f : P Q) (h : x.is_amalgamation t) :
theorem category_theory.presieve.is_compatible_of_exists_amalgamation {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (h : ∃ (t : P.obj (opposite.op X)), ) :
theorem category_theory.presieve.is_amalgamation_restrict {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R₁ R₂ : category_theory.presieve X} (h : R₁ R₂) (t : P.obj (opposite.op X)) (ht : x.is_amalgamation t) :
theorem category_theory.presieve.is_amalgamation_sieve_extend {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (t : P.obj (opposite.op X)) (ht : x.is_amalgamation t) :
def category_theory.presieve.is_separated_for {C : Type u₁} {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₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} {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₂
theorem category_theory.presieve.is_separated_for_iff_generate {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} :
theorem category_theory.presieve.is_separated_for_top {C : Type u₁} {X : C} (P : Cᵒᵖ Type w) :
def category_theory.presieve.is_sheaf_for {C : Type u₁} {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₁} {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
def category_theory.presieve.nat_trans_equiv_compatible_family {C : Type u₁} {X : C} {S : category_theory.sieve X} {P : Cᵒᵖ Type v₁} :
(S.functor P) {x // x.compatible}

(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
theorem category_theory.presieve.extension_iff_amalgamation {C : Type u₁} {X : C} {S : category_theory.sieve X} {P : Cᵒᵖ Type v₁} (x : S.functor P) (g : P) :

(Implementation). A lemma useful to prove yoneda_condition_iff_sheaf_condition.

theorem category_theory.presieve.is_sheaf_for_iff_yoneda_sheaf_condition {C : Type u₁} {X : C} {S : category_theory.sieve X} {P : Cᵒᵖ Type v₁} :

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

C2.1.4 of [Joh02].

noncomputable def category_theory.presieve.is_sheaf_for.extend {C : Type u₁} {X : C} {S : category_theory.sieve X} {P : Cᵒᵖ Type v₁} (f : S.functor P) :

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]
theorem category_theory.presieve.is_sheaf_for.functor_inclusion_comp_extend_assoc {C : Type u₁} {X : C} {S : category_theory.sieve X} {P : Cᵒᵖ Type v₁} (f : S.functor P) {X' : Cᵒᵖ Type v₁} (f' : P X') :
theorem category_theory.presieve.is_sheaf_for.unique_extend {C : Type u₁} {X : C} {S : category_theory.sieve X} {P : Cᵒᵖ Type v₁} {f : S.functor P} (t : P) (ht : = f) :
t = h.extend f

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

theorem category_theory.presieve.is_sheaf_for.hom_ext {C : Type u₁} {X : C} {S : category_theory.sieve X} {P : Cᵒᵖ Type v₁} (t₁ t₂ : P) (ht : = ) :
t₁ = t₂

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.

theorem category_theory.presieve.is_separated_for_and_exists_is_amalgamation_iff_sheaf_for {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} :
∀ (x : , x.compatible(∃ (t : P.obj (opposite.op X)), x.is_amalgamation t))

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

theorem category_theory.presieve.is_separated_for.is_sheaf_for {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X}  :
(∀ (x : , x.compatible(∃ (t : P.obj (opposite.op X)), x.is_amalgamation t))

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

theorem category_theory.presieve.is_sheaf_for.is_separated_for {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} :

If P is a sheaf for R, it is separated for R.

noncomputable def category_theory.presieve.is_sheaf_for.amalgamate {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} (hx : x.compatible) :

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

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

C2.1.3 in [Joh02]

theorem category_theory.presieve.is_sheaf_for_singleton_iso {C : Type u₁} {X : C} (P : Cᵒᵖ Type w) :

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

[Joh02] C2.1.5(i)

theorem category_theory.presieve.is_sheaf_for_top_sieve {C : Type u₁} {X : C} (P : Cᵒᵖ Type w) :

Every presheaf is a sheaf for the maximal sieve.

[Joh02] C2.1.5(ii)

theorem category_theory.presieve.is_sheaf_for_iso {C : Type u₁} {P : Cᵒᵖ Type w} {X : C} {R : category_theory.presieve X} {P' : Cᵒᵖ Type w} (i : P P') :

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.

theorem category_theory.presieve.is_sheaf_for_subsieve_aux {C : Type u₁} {X : C} (P : Cᵒᵖ Type w) {S : category_theory.sieve X} {R : category_theory.presieve X} (h : S R) (trans : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, ) :

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

theorem category_theory.presieve.is_sheaf_for_subsieve {C : Type u₁} {X : C} (P : Cᵒᵖ Type w) {S : category_theory.sieve X} {R : category_theory.presieve X} (h : S R) (trans : ∀ ⦃Y : C⦄ (f : Y X), ) :

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.

def category_theory.presieve.is_separated {C : Type u₁} (P : Cᵒᵖ Type w) :
Prop

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

Equations
• = ∀ {X : C} (S : , S J X
def category_theory.presieve.is_sheaf {C : Type u₁} (P : Cᵒᵖ Type w) :
Prop

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
• = ∀ ⦃X : C⦄ (S : , S J X
theorem category_theory.presieve.is_sheaf.is_sheaf_for {C : Type u₁} {X : C} {P : Cᵒᵖ Type w} (hp : P) (R : category_theory.presieve X) (hr : J X) :
theorem category_theory.presieve.is_sheaf_of_le {C : Type u₁} (P : Cᵒᵖ Type w) {J₁ J₂ : category_theory.grothendieck_topology C} :
J₁ J₂
theorem category_theory.presieve.is_separated_of_is_sheaf {C : Type u₁} (P : Cᵒᵖ Type w)  :
theorem category_theory.presieve.is_sheaf_iso {C : Type u₁} {P : Cᵒᵖ Type w} {P' : Cᵒᵖ Type w} (i : P P')  :

The property of being a sheaf is preserved by isomorphism.

theorem category_theory.presieve.is_sheaf_of_yoneda {C : Type u₁} {P : Cᵒᵖ Type v₁} (h : ∀ {X : C} (S : , ) :
theorem category_theory.presieve.is_sheaf_pretopology {C : Type u₁} {P : Cᵒᵖ Type w}  :
∀ {X : C} (R : , R K X

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

theorem category_theory.presieve.is_sheaf_bot {C : Type u₁} {P : Cᵒᵖ Type w} :

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

def category_theory.equalizer.first_obj {C : Type u₁} (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
noncomputable def category_theory.equalizer.first_obj_eq_family {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X) :

Show that first_obj is isomorphic to family_of_elements.

Equations
@[simp]
theorem category_theory.equalizer.first_obj_eq_family_inv {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X)  :
= category_theory.limits.pi.lift (λ (f : Σ (Y : C), {f // R f}) (x : , x f.snd.val _)
@[simp]
theorem category_theory.equalizer.first_obj_eq_family_hom {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X) (Y : C) (f : Y X) (hf : R f) :
hf = category_theory.limits.pi.π (λ (f : Σ (Y : C), {f // R f}), P.obj (opposite.op f.fst)) Y, f, hf⟩ t
@[protected, instance]
noncomputable def category_theory.equalizer.first_obj.inhabited {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} :
Equations
noncomputable def category_theory.equalizer.fork_map {C : Type u₁} (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₁} (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
noncomputable def category_theory.equalizer.sieve.first_map {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (S : category_theory.sieve X) :

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

Equations
@[protected, instance]
noncomputable def category_theory.equalizer.sieve.second_obj.inhabited {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} :
Equations
noncomputable def category_theory.equalizer.sieve.second_map {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (S : category_theory.sieve X) :

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

Equations
theorem category_theory.equalizer.sieve.w {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (S : category_theory.sieve X) :
theorem category_theory.equalizer.sieve.compatible_iff {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (S : category_theory.sieve X)  :

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.

theorem category_theory.equalizer.sieve.equalizer_sheaf_condition {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (S : category_theory.sieve X) :

P is a sheaf for S, iff the fork given by w is an equalizer.

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₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X)  :
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
noncomputable def category_theory.equalizer.presieve.first_map {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X)  :

The map pr₀* of https://stacks.math.columbia.edu/tag/00VL.

Equations
@[protected, instance]
noncomputable def category_theory.equalizer.presieve.second_obj.inhabited {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C}  :
Equations
noncomputable def category_theory.equalizer.presieve.second_map {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X)  :

The map pr₁* of https://stacks.math.columbia.edu/tag/00VL.

Equations
theorem category_theory.equalizer.presieve.w {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X)  :
theorem category_theory.equalizer.presieve.compatible_iff {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X)  :

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.

theorem category_theory.equalizer.presieve.sheaf_condition {C : Type u₁} (P : Cᵒᵖ Type (max v₁ u₁)) {X : C} (R : category_theory.presieve X)  :

P is a sheaf for R, iff the fork given by w is an equalizer. See https://stacks.math.columbia.edu/tag/00VM.

structure category_theory.SheafOfTypes {C : Type u₁}  :
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_iff {C : Type u₁} {_inst_1 : category_theory.category C} {X Y : category_theory.SheafOfTypes J} (x y : X.hom Y) :
x = y x.val = y.val
theorem category_theory.SheafOfTypes.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {X Y : category_theory.SheafOfTypes J} (x y : X.hom Y) (h : x.val = y.val) :
x = y
@[ext]
structure category_theory.SheafOfTypes.hom {C : Type u₁} (X Y : category_theory.SheafOfTypes J) :
Type (max u_1 u₁)

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

Instances for category_theory.SheafOfTypes.hom
@[simp]
theorem category_theory.SheafOfTypes.category_theory.category_comp_val {C : Type u₁} (X Y Z : category_theory.SheafOfTypes J) (f : X Y) (g : Y Z) :
(f g).val = f.val g.val
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
def category_theory.SheafOfTypes_to_presheaf {C : Type u₁}  :
Cᵒᵖ Type w

The inclusion functor from sheaves to presheaves.

Equations
Instances for category_theory.SheafOfTypes_to_presheaf
@[simp]
theorem category_theory.SheafOfTypes_to_presheaf_map {C : Type u₁} (X Y : category_theory.SheafOfTypes J) (f : X Y) :
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem category_theory.SheafOfTypes_bot_equiv_counit_iso {C : Type u₁}  :
category_theory.SheafOfTypes_bot_equiv.counit_iso = category_theory.iso.refl ({obj := λ (P : Cᵒᵖ Type w), {val := P, cond := _}, map := λ (P₁ P₂ : Cᵒᵖ Type w) (f : P₁ P₂), , map_id' := _, map_comp' := _}
@[simp]
theorem category_theory.SheafOfTypes_bot_equiv_unit_iso_inv_app_val {C : Type u₁}  :
= 𝟙 {obj := λ (P : Cᵒᵖ Type w), {val := P, cond := _}, map := λ (P₁ P₂ : Cᵒᵖ Type w) (f : P₁ P₂), , map_id' := _, map_comp' := _}).obj _x).val
@[simp]
theorem category_theory.SheafOfTypes_bot_equiv_inverse_obj_val {C : Type u₁} (P : Cᵒᵖ Type w) :
def category_theory.SheafOfTypes_bot_equiv {C : Type u₁}  :
Cᵒᵖ Type w

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

Equations
@[simp]
theorem category_theory.SheafOfTypes_bot_equiv_inverse_map {C : Type u₁} (P₁ P₂ : Cᵒᵖ Type w) (f : P₁ P₂) :
@[simp]
@[protected, instance]
def category_theory.SheafOfTypes.inhabited {C : Type u₁}  :
Equations