# Documentation

Mathlib.CategoryTheory.Sites.SheafOfTypes

# 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 FamilyOfElements.
• 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 FamilyOfElements.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 FamilyOfElements.IsAmalgamation. 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 IsSeparatedFor and IsSheafFor.

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 FamilyOfElements.SieveCompatible and compatible_iff_sieveCompatible.

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 FamilyOfElements.PullbackCompatible and pullbackCompatible_iff.

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

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 isSheaf_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 isSheaf_pretopology, this shows the notions of IsSheaf are exactly equivalent.)

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

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

• Yoneda condition: Defined in yonedaSheafCondition and equivalence in isSheafFor_iff_yonedaSheafCondition.
• Equalizer condition (Equation 3): Defined in the Equalizer.Sieve namespace, and equivalence in Equalizer.Sieve.sheaf_condition.
• Matching family for presieves with pullback: pullbackCompatible_iff.
• Sheaf for a pretopology (Prop 1): isSheaf_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 #

• [MM92]: Sheaves in geometry and logic, Saunders MacLane, and Ieke Moerdijk: Chapter III, Section 4.
• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1.
• https://stacks.math.columbia.edu/tag/00VL (sheaves on a pretopology or site)
• https://stacks.math.columbia.edu/tag/00ZB (sheaves on a topology)
def CategoryTheory.Presieve.FamilyOfElements {C : Type u₁} [] {X : C} (P : ) (R : ) :
Type (max (max u₁ w) v₁)

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 [Elephant].

Instances For
def CategoryTheory.Presieve.FamilyOfElements.restrict {C : Type u₁} [] {P : } {X : C} {R₁ : } {R₂ : } (h : R₁ R₂) :

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

Instances For
def CategoryTheory.Presieve.FamilyOfElements.Compatible {C : Type u₁} [] {P : } {X : C} {R : } :

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 pullbackCompatible_iff and compatible_iff_sieveCompatible.

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

Instances For

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

This is the definition for a "matching" family given in [MM92], Chapter III, Section 4, Equation (5). Viewing the type FamilyOfElements 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.

Instances For
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict {C : Type u₁} [] {P : } {X : C} {R₁ : } {R₂ : } (h : R₁ R₂) {x : } :

The restriction of a compatible family is compatible.

noncomputable def CategoryTheory.Presieve.FamilyOfElements.sieveExtend {C : Type u₁} [] {P : } {X : C} {R : } :

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 [Elephant].

Instances For

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

theorem CategoryTheory.Presieve.extend_agrees {C : Type u₁} [] {P : } {X : C} {Y : C} {R : } {f : Y X} (hf : R Y f) :

The extension of a family agrees with the original family.

@[simp]
theorem CategoryTheory.Presieve.restrict_extend {C : Type u₁} [] {P : } {X : C} {R : } :

The restriction of an extension is the original.

def CategoryTheory.Presieve.FamilyOfElements.SieveCompatible {C : Type u₁} [] {P : } {X : C} {S : } (x : ) :

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

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 [Elephant].

Instances For
theorem CategoryTheory.Presieve.compatible_iff_sieveCompatible {C : Type u₁} [] {P : } {X : C} {S : } (x : ) :
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.to_sieveCompatible {C : Type u₁} [] {P : } {X : C} {S : } {x : } :
@[simp]
theorem CategoryTheory.Presieve.extend_restrict {C : Type u₁} [] {P : } {X : C} {R : } {x : } :

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 CategoryTheory.Presieve.restrict_inj {C : Type u₁} [] {P : } {X : C} {R : } {x₁ : } {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.

@[simp]
theorem CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe {C : Type u₁} [] {P : } {X : C} {R : } (x : ) :
↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible x) =
@[simp]
theorem CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe {C : Type u₁} [] {P : } {X : C} {R : } (x : ) :
↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible.symm x) = CategoryTheory.Presieve.FamilyOfElements.restrict (_ : R ().arrows) x
noncomputable def CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible {C : Type u₁} [] {P : } {X : C} {R : } :

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.

Instances For
theorem CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible {C : Type u₁} [] {P : } {X : C} {Y : C} (S : ) {x : } {f : Y X} (hf : S.arrows f) {Z : C} (g : Z Y) :
x Z () (_ : S.arrows ()) = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor () () g.op (x Y f hf)
def CategoryTheory.Presieve.FamilyOfElements.functorPullback {C : Type u₁} [] {P : } {D : Type u₂} [] (F : ) {Z : D} {T : CategoryTheory.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.functorPullback F.

Instances For
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPullback {C : Type u₁} [] {P : } {D : Type u₂} [] (F : ) {Z : D} {T : CategoryTheory.Presieve (F.obj Z)} :
noncomputable def CategoryTheory.Presieve.FamilyOfElements.functorPushforward {C : Type u₁} [] {P : } {D : Type u₂} [] (F : ) {X : D} {T : } (x : ) :

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.functorPushforward F. Since the preimage is obtained by choice, this is not well-defined generally.

Instances For
def CategoryTheory.Presieve.FamilyOfElements.pullback {C : Type u₁} [] {P : } {X : C} {Y : C} {S : } (f : Y X) (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.

Instances For
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.pullback {C : Type u₁} [] {P : } {X : C} {Y : C} {S : } (f : Y X) {x : } :
def CategoryTheory.Presieve.FamilyOfElements.compPresheafMap {C : Type u₁} [] {P : } {Q : } {X : C} {R : } (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.

Instances For
@[simp]
theorem CategoryTheory.Presieve.FamilyOfElements.compPresheafMap_id {C : Type u₁} [] {P : } {X : C} {R : } :
@[simp]
theorem CategoryTheory.Presieve.FamilyOfElements.compPresheafMap_comp {C : Type u₁} [] {P : } {Q : } {U : } {X : C} {R : } (f : P Q) (g : Q U) :
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.compPresheafMap {C : Type u₁} [] {P : } {Q : } {X : C} {R : } (f : P Q) :
def CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation {C : Type u₁} [] {P : } {X : C} {R : } (t : P.obj ()) :

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

Instances For
theorem CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.compPresheafMap {C : Type u₁} [] {P : } {Q : } {X : C} {R : } {t : P.obj ()} (f : P Q) :
CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation () (Cᵒᵖ.app CategoryTheory.Category.opposite (Type w) CategoryTheory.types P Q f () t)
theorem CategoryTheory.Presieve.is_compatible_of_exists_amalgamation {C : Type u₁} [] {P : } {X : C} {R : } (h : ) :
theorem CategoryTheory.Presieve.isAmalgamation_restrict {C : Type u₁} [] {P : } {X : C} {R₁ : } {R₂ : } (h : R₁ R₂) (x : ) (t : P.obj ()) :
theorem CategoryTheory.Presieve.isAmalgamation_sieveExtend {C : Type u₁} [] {P : } {X : C} {R : } (t : P.obj ()) :
def CategoryTheory.Presieve.IsSeparatedFor {C : Type u₁} [] {X : C} (P : ) (R : ) :

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

Instances For
theorem CategoryTheory.Presieve.IsSeparatedFor.ext {C : Type u₁} [] {P : } {X : C} {R : } (hR : ) {t₁ : P.obj ()} {t₂ : P.obj ()} (h : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, R Y fCᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor () () f.op t₁ = Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor () () f.op t₂) :
t₁ = t₂
theorem CategoryTheory.Presieve.isSeparatedFor_iff_generate {C : Type u₁} [] {P : } {X : C} {R : } :
theorem CategoryTheory.Presieve.isSeparatedFor_top {C : Type u₁} [] {X : C} (P : ) :
def CategoryTheory.Presieve.IsSheafFor {C : Type u₁} [] {X : C} (P : ) (R : ) :

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 [Elephant], and https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents. Using compatible_iff_sieveCompatible, this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4.

Instances For
def CategoryTheory.Presieve.YonedaSheafCondition {C : Type u₁} [] {X : C} (P : ) (S : ) :

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 IsSheafFor is given in isSheafFor_iff_yonedaSheafCondition. 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 [Elephant]. This is also a direct reformulation of https://stacks.math.columbia.edu/tag/00Z8.

Instances For
def CategoryTheory.Presieve.natTransEquivCompatibleFamily {C : Type u₁} [] {X : C} {S : } {P : } :

(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 [Elephant], and the discussion in [MM92], Chapter III, Section 4.

Instances For
theorem CategoryTheory.Presieve.extension_iff_amalgamation {C : Type u₁} [] {X : C} {S : } {P : } (x : ) (g : CategoryTheory.yoneda.obj X P) :
CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation (↑(CategoryTheory.Presieve.natTransEquivCompatibleFamily x)) (CategoryTheory.yonedaEquiv g)

(Implementation). A lemma useful to prove isSheafFor_iff_yonedaSheafCondition.

theorem CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition {C : Type u₁} [] {X : C} {S : } {P : } :

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

C2.1.4 of [Elephant].

noncomputable def CategoryTheory.Presieve.IsSheafFor.extend {C : Type u₁} [] {X : C} {S : } {P : } (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : ) :
CategoryTheory.yoneda.obj X 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

Instances For
@[simp]
theorem CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend_assoc {C : Type u₁} [] {X : C} {S : } {P : } (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : ) {Z : } (h : P Z) :
@[simp]
theorem CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend {C : Type u₁} [] {X : C} {S : } {P : } (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : ) :

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

theorem CategoryTheory.Presieve.IsSheafFor.unique_extend {C : Type u₁} [] {X : C} {S : } {P : } (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) {f : } (t : CategoryTheory.yoneda.obj X P) :

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

theorem CategoryTheory.Presieve.IsSheafFor.hom_ext {C : Type u₁} [] {X : C} {S : } {P : } (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (t₁ : CategoryTheory.yoneda.obj X P) (t₂ : CategoryTheory.yoneda.obj X P) :
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.

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

theorem CategoryTheory.Presieve.IsSeparatedFor.isSheafFor {C : Type u₁} [] {P : } {X : C} {R : } :
() →

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

theorem CategoryTheory.Presieve.IsSheafFor.isSeparatedFor {C : Type u₁} [] {P : } {X : C} {R : } :

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

noncomputable def CategoryTheory.Presieve.IsSheafFor.amalgamate {C : Type u₁} [] {P : } {X : C} {R : } (t : ) :
P.obj ()

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

Instances For
theorem CategoryTheory.Presieve.IsSheafFor.isAmalgamation {C : Type u₁} [] {P : } {X : C} {R : } (t : ) :
@[simp]
theorem CategoryTheory.Presieve.IsSheafFor.valid_glue {C : Type u₁} [] {P : } {X : C} {Y : C} {R : } (t : ) (f : Y X) (Hf : R Y f) :
Cᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver P.toPrefunctor () () f.op () = x Y f Hf
theorem CategoryTheory.Presieve.isSheafFor_iff_generate {C : Type u₁} [] {P : } {X : C} (R : ) :

C2.1.3 in [Elephant]

theorem CategoryTheory.Presieve.isSheafFor_singleton_iso {C : Type u₁} [] {X : C} (P : ) :

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

[Elephant] C2.1.5(i)

theorem CategoryTheory.Presieve.isSheafFor_top_sieve {C : Type u₁} [] {X : C} (P : ) :

Every presheaf is a sheaf for the maximal sieve.

[Elephant] C2.1.5(ii)

theorem CategoryTheory.Presieve.isSheafFor_iso {C : Type u₁} [] {P : } {X : C} {R : } {P' : } (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 hygienic property.

theorem CategoryTheory.Presieve.isSheafFor_subsieve_aux {C : Type u₁} [] {X : C} (P : ) {S : } {R : } (h : S.arrows R) (hS : CategoryTheory.Presieve.IsSheafFor P S.arrows) (trans : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, R Y f) :

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 [Elephant] C2.1.6(i).

theorem CategoryTheory.Presieve.isSheafFor_subsieve {C : Type u₁} [] {X : C} (P : ) {S : } {R : } (h : S.arrows 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 [Elephant] C2.1.6.

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

Instances For
def CategoryTheory.Presieve.IsSheaf {C : Type u₁} [] (P : ) :

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, isSheaf_pretopology shows it suffices to check the sheaf condition at presieves in the pretopology.

Instances For
theorem CategoryTheory.Presieve.IsSheaf.isSheafFor {C : Type u₁} [] {X : C} {P : } (hp : ) (R : ) :
theorem CategoryTheory.Presieve.isSheaf_of_le {C : Type u₁} [] (P : ) :
J₁ J₂
theorem CategoryTheory.Presieve.isSeparated_of_isSheaf {C : Type u₁} [] (P : ) (h : ) :
theorem CategoryTheory.Presieve.isSheaf_iso {C : Type u₁} [] {P : } {P' : } (i : P P') (h : ) :

The property of being a sheaf is preserved by isomorphism.

theorem CategoryTheory.Presieve.isSheaf_of_yoneda {C : Type u₁} [] {P : } (h : ∀ {X : C} (S : ), ) :
theorem CategoryTheory.Presieve.isSheaf_pretopology {C : Type u₁} [] {P : } (K : ) :
∀ {X : C} (R : ),

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

theorem CategoryTheory.Presieve.isSheaf_bot {C : Type u₁} [] {P : } :

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

def CategoryTheory.Presieve.compatibleYonedaFamily_toCocone {C : Type u₁} [] {X : C} (R : ) (W : C) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.yoneda.obj W) R) :

For a presheaf of the form yoneda.obj W, a compatible family of elements on a sieve is the same as a co-cone over the sieve. Constructing a co-cone from a compatible family works for any presieve, as does constructing a family of elements from a co-cone. Showing compatibility of the family needs the sieve condition. Note: This is related to CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily

Instances For
def CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone {C : Type u₁} [] {X : C} (R : ) :
CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.yoneda.obj s.pt) R
Instances For
theorem CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible {C : Type u₁} [] {X : C} (S : ) (s : ) :
theorem CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit {C : Type u₁} [] {X : C} (S : ) :
(∀ (W : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj W) S.arrows)

The base of a sieve S is a colimit of S iff all Yoneda-presheaves satisfy the sheaf condition for S.

def CategoryTheory.Equalizer.FirstObj {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :
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.

Instances For
theorem CategoryTheory.Equalizer.FirstObj.ext {C : Type u₁} [] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))} {X : C} {R : } (z₁ : ) (z₂ : ) (h : ∀ (Y : C) (f : Y X) (hf : R Y f), CategoryTheory.Limits.Pi.π ((Y : C) × { f // R Y f }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))) { fst := Y, snd := { val := f, property := hf } } z₁ = CategoryTheory.Limits.Pi.π ((Y : C) × { f // R Y f }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))) { fst := Y, snd := { val := f, property := hf } } z₂) :
z₁ = z₂
@[simp]
theorem CategoryTheory.Equalizer.firstObjEqFamily_inv {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :
∀ (a : ), ().inv a = CategoryTheory.Limits.Pi.lift (fun f x => x f.fst (f.snd) ()) a
@[simp]
theorem CategoryTheory.Equalizer.firstObjEqFamily_hom {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) (t : ) (Y : C) (f : Y X) (hf : R Y f) :
Type (max v₁ u₁).hom CategoryTheory.types () () () t Y f hf = CategoryTheory.Limits.Pi.π ((Y : C) × { f // R Y f }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))) { fst := Y, snd := { val := f, property := hf } } t
def CategoryTheory.Equalizer.firstObjEqFamily {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :

Show that FirstObj is isomorphic to FamilyOfElements.

Instances For
def CategoryTheory.Equalizer.forkMap {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :
P.obj ()

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.

Instances For

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

def CategoryTheory.Equalizer.Sieve.SecondObj {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (S : ) :
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.

Instances For
theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext {C : Type u₁} [] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))} {X : C} {S : } (z₁ : ) (z₂ : ) (h : ∀ (Y Z : C) (g : Z Y) (f : Y X) (hf : S.arrows f), CategoryTheory.Limits.Pi.π ((Y : C) × (Z : C) × (_ : Z Y) × { f' // S.arrows f' }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.snd.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.snd.fst))) { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } z₁ = CategoryTheory.Limits.Pi.π ((Y : C) × (Z : C) × (_ : Z Y) × { f' // S.arrows f' }) (Type (max v₁ u₁)) CategoryTheory.types (fun f => P.obj (Opposite.op f.snd.fst)) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.snd.fst))) { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } z₂) :
z₁ = z₂
def CategoryTheory.Equalizer.Sieve.firstMap {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (S : ) :

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

Instances For
def CategoryTheory.Equalizer.Sieve.secondMap {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (S : ) :

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

Instances For
theorem CategoryTheory.Equalizer.Sieve.w {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (S : ) :

The family of elements given by x : FirstObj P S is compatible iff firstMap and secondMap map it to the same point.

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

def CategoryTheory.Equalizer.Presieve.SecondObj {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :
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.

Instances For
def CategoryTheory.Equalizer.Presieve.firstMap {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :

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

Instances For
def CategoryTheory.Equalizer.Presieve.secondMap {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :

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

Instances For
theorem CategoryTheory.Equalizer.Presieve.w {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) :
theorem CategoryTheory.Equalizer.Presieve.compatible_iff {C : Type u₁} [] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ u₁))) {X : C} (R : ) (x : ) :

The family of elements given by x : FirstObj P S is compatible iff firstMap and secondMap map it to the same point.

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

structure CategoryTheory.SheafOfTypes {C : Type u₁} [] :
Type (max u₁ v₁ (w + 1))
• val :

the underlying presheaf

• cond :

the condition that the presheaf is a sheaf

The category of sheaves on a grothendieck topology.

Instances For
theorem CategoryTheory.SheafOfTypes.Hom.ext {C : Type u₁} :
∀ {inst : } {J : } {X Y : } (x y : ), x.val = y.valx = y
theorem CategoryTheory.SheafOfTypes.Hom.ext_iff {C : Type u₁} :
∀ {inst : } {J : } {X Y : } (x y : ), x = y x.val = y.val
structure CategoryTheory.SheafOfTypes.Hom {C : Type u₁} [] (X : ) (Y : ) :
Type (max u_1 u₁)
• val : X.val Y.val

a morphism between the underlying presheaves

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

Instances For
@[simp]
theorem CategoryTheory.SheafOfTypes.instCategorySheafOfTypes_comp_val {C : Type u₁} [] :
∀ {X Y Z : } (f : X Y) (g : Y Z), ().val = CategoryTheory.CategoryStruct.comp f.val g.val
theorem CategoryTheory.SheafOfTypes.Hom.ext' {C : Type u₁} [] {X : } {Y : } (f : X Y) (g : X Y) (w : f.val = g.val) :
f = g
@[simp]
theorem CategoryTheory.sheafOfTypesToPresheaf_map {C : Type u₁} [] :
∀ {X Y : } (f : X Y), = f.val
@[simp]
theorem CategoryTheory.sheafOfTypesToPresheaf_obj {C : Type u₁} [] (self : ) :
().obj self = self.val

The inclusion functor from sheaves to presheaves.

Instances For
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_inverse_map {C : Type u₁} [] :
∀ {X Y : } (f : X Y), CategoryTheory.sheafOfTypesBotEquiv.inverse.map f = ().preimage f
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_inverse_obj_val {C : Type u₁} [] (P : ) :
(CategoryTheory.sheafOfTypesBotEquiv.inverse.obj P).val = P
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_unitIso_hom_app_val {C : Type u₁} [] :
∀ (x : ), (CategoryTheory.sheafOfTypesBotEquiv.unitIso.hom.app x).val =
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_counitIso {C : Type u₁} [] :
CategoryTheory.sheafOfTypesBotEquiv.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp (CategoryTheory.Functor.mk { obj := fun P => { val := P, cond := (_ : ) }, map := fun {X Y} f => ().preimage f }) ())
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_functor {C : Type u₁} [] :
CategoryTheory.sheafOfTypesBotEquiv.functor =
@[simp]
theorem CategoryTheory.sheafOfTypesBotEquiv_unitIso_inv_app_val {C : Type u₁} [] :
∀ (x : ), (CategoryTheory.sheafOfTypesBotEquiv.unitIso.inv.app x).val = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp () (CategoryTheory.Functor.mk { obj := fun P => { val := P, cond := (_ : ) }, map := fun {X Y} f => ().preimage f })).obj x).val

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

Instances For