The sheaf condition for a presieve

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

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

• Stacks: 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.
  • Matching family for presieves with pullback: pullbackCompatible_iff.

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

Equations

• CategoryTheory.Presieve.FamilyOfElements P R = (⦃Y : C⦄ → (f : Y ⟶ X) → R f → P.obj (Opposite.op Y))

instance CategoryTheory.Presieve.instInhabitedFamilyOfElementsBot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} : Inhabited (CategoryTheory.Presieve.FamilyOfElements P ⊥)

Equations

• CategoryTheory.Presieve.instInhabitedFamilyOfElementsBot = { default := fun (x : C) (x_1 : x ⟶ X) => False.elim }

def CategoryTheory.Presieve.FamilyOfElements.restrict {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) : CategoryTheory.Presieve.FamilyOfElements P R₂ → CategoryTheory.Presieve.FamilyOfElements P R₁

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

Equations

• CategoryTheory.Presieve.FamilyOfElements.restrict h x✝ f hf = x✝ f ⋯

def CategoryTheory.Presieve.FamilyOfElements.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (p : CategoryTheory.Presieve.FamilyOfElements P R) (φ : P ⟶ Q) : CategoryTheory.Presieve.FamilyOfElements Q R

The image of a family of elements by a morphism of presheaves.

Equations

• p.map φ f hf = φ.app (Opposite.op x) (p f hf)

@[simp]

theorem CategoryTheory.Presieve.FamilyOfElements.map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (p : CategoryTheory.Presieve.FamilyOfElements P R) (φ : P ⟶ Q) {Y : C} (f : Y ⟶ X) (hf : R f) : p.map φ f hf = φ.app (Opposite.op Y) (p f hf)

theorem CategoryTheory.Presieve.FamilyOfElements.restrict_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (p : CategoryTheory.Presieve.FamilyOfElements P R) (φ : P ⟶ Q) {R' : CategoryTheory.Presieve X} (h : R' ≤ R) : (CategoryTheory.Presieve.FamilyOfElements.restrict h p).map φ = CategoryTheory.Presieve.FamilyOfElements.restrict h (p.map φ)

def CategoryTheory.Presieve.FamilyOfElements.Compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) : 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 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

For a more explicit version in the case where R is of the form Presieve.ofArrows, see CategoryTheory.Presieve.Arrows.Compatible.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Presieve.FamilyOfElements.PullbackCompatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) [R.hasPullbacks] : 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 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.

For a more explicit version in the case where R is of the form Presieve.ofArrows, see CategoryTheory.Presieve.Arrows.PullbackCompatible.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Presieve.pullbackCompatible_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) [R.hasPullbacks] : x.Compatible ↔ x.PullbackCompatible

theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) {x : CategoryTheory.Presieve.FamilyOfElements P R₂} : x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.restrict h x).Compatible

The restriction of a compatible family is compatible.

noncomputable def CategoryTheory.Presieve.FamilyOfElements.sieveExtend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows

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

Equations

• x✝¹.sieveExtend x hf = P.map ⋯.choose.op (x✝¹ ⋯.choose ⋯)

theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) : x.sieveExtend.Compatible

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

theorem CategoryTheory.Presieve.extend_agrees {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} (t : x.Compatible) {f : Y ⟶ X} (hf : R f) : x.sieveExtend f ⋯ = x f hf

The extension of a family agrees with the original family.

@[simp]

theorem CategoryTheory.Presieve.restrict_extend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} (t : x.Compatible) : CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x.sieveExtend = x

The restriction of an extension is the original.

def CategoryTheory.Presieve.FamilyOfElements.SieveCompatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {S : CategoryTheory.Sieve X} (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows) : 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_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].

Equations

• x.SieveCompatible = ∀ ⦃Y Z : C⦄ (f : Y ⟶ X) (g : Z ⟶ Y) (hf : S.arrows f), x (CategoryTheory.CategoryStruct.comp g f) ⋯ = P.map g.op (x f hf)

theorem CategoryTheory.Presieve.compatible_iff_sieveCompatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {S : CategoryTheory.Sieve X} (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows) : x.Compatible ↔ x.SieveCompatible

theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.to_sieveCompatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {S : CategoryTheory.Sieve X} {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (t : x.Compatible) : x.SieveCompatible

@[simp]

theorem CategoryTheory.Presieve.extend_restrict {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows} (t : x.Compatible) : (CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x).sieveExtend = 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₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x₁ x₂ : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows} (t₁ : x₁.Compatible) (t₂ : x₂.Compatible) : CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₁ = CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₂ → 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.

noncomputable def CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : { x : CategoryTheory.Presieve.FamilyOfElements P R // x.Compatible } ≃ { x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows // 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : { x : CategoryTheory.Presieve.FamilyOfElements P R // x.Compatible }) : ↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible x) = (↑x).sieveExtend

@[simp]

theorem CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : { x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows // x.Compatible }) : ↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible.symm x) = CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ ↑x

theorem CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} (S : CategoryTheory.Sieve X) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (t : x.Compatible) {f : Y ⟶ X} (hf : S.arrows f) {Z : C} (g : Z ⟶ Y) : x (CategoryTheory.CategoryStruct.comp g f) ⋯ = P.map g.op (x f hf)

def CategoryTheory.Presieve.FamilyOfElements.functorPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {Z : D} {T : CategoryTheory.Presieve (F.obj Z)} (x : CategoryTheory.Presieve.FamilyOfElements P T) : CategoryTheory.Presieve.FamilyOfElements (F.op.comp P) (CategoryTheory.Presieve.functorPullback F T)

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.

Equations

• CategoryTheory.Presieve.FamilyOfElements.functorPullback F x✝ f hf = x✝ (F.map f) hf

theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {Z : D} {T : CategoryTheory.Presieve (F.obj Z)} {x : CategoryTheory.Presieve.FamilyOfElements P T} (h : x.Compatible) : (CategoryTheory.Presieve.FamilyOfElements.functorPullback F x).Compatible

noncomputable def CategoryTheory.Presieve.FamilyOfElements.functorPushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {X : D} {T : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements (F.op.comp P) T) : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.functorPushforward F 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.functorPushforward F. Since the preimage is obtained by choice, this is not well-defined generally.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Presieve.FamilyOfElements.pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X) (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows) : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.pullback f S).arrows

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

• CategoryTheory.Presieve.FamilyOfElements.pullback f x✝ g hg = x✝ (CategoryTheory.CategoryStruct.comp g f) hg

theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (h : x.Compatible) : (CategoryTheory.Presieve.FamilyOfElements.pullback f x).Compatible

def CategoryTheory.Presieve.FamilyOfElements.compPresheafMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (f : P ⟶ Q) (x : CategoryTheory.Presieve.FamilyOfElements P R) : CategoryTheory.Presieve.FamilyOfElements Q R

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

• CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x g hg = f.app (Opposite.op Y) (x g hg)

@[simp]

theorem CategoryTheory.Presieve.FamilyOfElements.compPresheafMap_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) : CategoryTheory.Presieve.FamilyOfElements.compPresheafMap (CategoryTheory.CategoryStruct.id P) x = x

@[simp]

theorem CategoryTheory.Presieve.FamilyOfElements.compPresheafMap_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q U : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (f : P ⟶ Q) (g : Q ⟶ U) : CategoryTheory.Presieve.FamilyOfElements.compPresheafMap g (CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x) = CategoryTheory.Presieve.FamilyOfElements.compPresheafMap (CategoryTheory.CategoryStruct.comp f g) x

theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.compPresheafMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (f : P ⟶ Q) {x : CategoryTheory.Presieve.FamilyOfElements P R} (h : x.Compatible) : (CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x).Compatible

def CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (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

• x.IsAmalgamation t = ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : R f), P.map f.op t = x f h

theorem CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.compPresheafMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} {t : P.obj (Opposite.op X)} (f : P ⟶ Q) (h : x.IsAmalgamation t) : (CategoryTheory.Presieve.FamilyOfElements.compPresheafMap f x).IsAmalgamation (f.app (Opposite.op X) t)

theorem CategoryTheory.Presieve.is_compatible_of_exists_amalgamation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (h : ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation t) : x.Compatible

theorem CategoryTheory.Presieve.isAmalgamation_restrict {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) (x : CategoryTheory.Presieve.FamilyOfElements P R₂) (t : P.obj (Opposite.op X)) (ht : x.IsAmalgamation t) : (CategoryTheory.Presieve.FamilyOfElements.restrict h x).IsAmalgamation t

theorem CategoryTheory.Presieve.isAmalgamation_sieveExtend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (t : P.obj (Opposite.op X)) (ht : x.IsAmalgamation t) : x.sieveExtend.IsAmalgamation t

def CategoryTheory.Presieve.IsSeparatedFor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) (R : CategoryTheory.Presieve X) : Prop

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

Equations

• CategoryTheory.Presieve.IsSeparatedFor P R = ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R) (t₁ t₂ : P.obj (Opposite.op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

theorem CategoryTheory.Presieve.IsSeparatedFor.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (hR : CategoryTheory.Presieve.IsSeparatedFor P R) {t₁ t₂ : P.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P.map f.op t₁ = P.map f.op t₂) : t₁ = t₂

theorem CategoryTheory.Presieve.isSeparatedFor_iff_generate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : CategoryTheory.Presieve.IsSeparatedFor P R ↔ CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.generate R).arrows

theorem CategoryTheory.Presieve.isSeparatedFor_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSeparatedFor P ⊤

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

Equations

• CategoryTheory.Presieve.IsSheafFor P R = ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃! t : P.obj (Opposite.op X), x.IsAmalgamation t

def CategoryTheory.Presieve.YonedaSheafCondition {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (S : CategoryTheory.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 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.

Equations

• CategoryTheory.Presieve.YonedaSheafCondition P S = ∀ (f : S.functor ⟶ P), ∃! g : CategoryTheory.yoneda.obj X ⟶ P, CategoryTheory.CategoryStruct.comp S.functorInclusion g = f

def CategoryTheory.Presieve.natTransEquivCompatibleFamily {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} : (S.functor ⟶ P) ≃ { x : CategoryTheory.Presieve.FamilyOfElements P S.arrows // 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 [Elephant], and the discussion in [MM92], Chapter III, Section 4.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Presieve.extension_iff_amalgamation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : S.functor ⟶ P) (g : CategoryTheory.yoneda.obj X ⟶ P) : CategoryTheory.CategoryStruct.comp S.functorInclusion g = x ↔ (↑(CategoryTheory.Presieve.natTransEquivCompatibleFamily x)).IsAmalgamation (CategoryTheory.yonedaEquiv g)

(Implementation). A lemma useful to prove isSheafFor_iff_yonedaSheafCondition.

theorem CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} : CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ CategoryTheory.Presieve.YonedaSheafCondition P S

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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P) : 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

Equations

• h.extend f = ⋯.choose

@[simp]

theorem CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P) : CategoryTheory.CategoryStruct.comp S.functorInclusion (h.extend f) = 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

@[simp]

theorem CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P) {Z : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h✝ : P ⟶ Z) : CategoryTheory.CategoryStruct.comp S.functorInclusion (CategoryTheory.CategoryStruct.comp (h.extend f) h✝) = CategoryTheory.CategoryStruct.comp f h✝

theorem CategoryTheory.Presieve.IsSheafFor.unique_extend {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) {f : S.functor ⟶ P} (t : CategoryTheory.yoneda.obj X ⟶ P) (ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t = f) : t = h.extend f

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

theorem CategoryTheory.Presieve.IsSheafFor.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (t₁ t₂ : CategoryTheory.yoneda.obj X ⟶ P) (ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t₁ = CategoryTheory.CategoryStruct.comp S.functorInclusion t₂) : 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 CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : (CategoryTheory.Presieve.IsSeparatedFor P R ∧ ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation t) ↔ CategoryTheory.Presieve.IsSheafFor P R

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₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSeparatedFor P R) : (∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation t) → CategoryTheory.Presieve.IsSheafFor P 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₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSeparatedFor P R

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

noncomputable def CategoryTheory.Presieve.IsSheafFor.amalgamate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R) (x : CategoryTheory.Presieve.FamilyOfElements P R) (hx : x.Compatible) : P.obj (Opposite.op X)

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

Equations

• t.amalgamate x hx = ⋯.choose

theorem CategoryTheory.Presieve.IsSheafFor.isAmalgamation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R) {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) : x.IsAmalgamation (t.amalgamate x hx)

@[simp]

theorem CategoryTheory.Presieve.IsSheafFor.valid_glue {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R) {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) (f : Y ⟶ X) (Hf : R f) : P.map f.op (t.amalgamate x hx) = x f Hf

theorem CategoryTheory.Presieve.isSheafFor_iff_generate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} (R : CategoryTheory.Presieve X) : CategoryTheory.Presieve.IsSheafFor P R ↔ CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.generate R).arrows

C2.1.3 in [Elephant]

theorem CategoryTheory.Presieve.isSheafFor_singleton_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton (CategoryTheory.CategoryStruct.id X))

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

[Elephant] C2.1.5(i)

theorem CategoryTheory.Presieve.isSheafFor_top_sieve {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheafFor P ⊤.arrows

Every presheaf is a sheaf for the maximal sieve.

[Elephant] C2.1.5(ii)

theorem CategoryTheory.Presieve.isSheafFor_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P') : CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSheafFor P' R

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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X} (h : S.arrows ≤ R) (hS : CategoryTheory.Presieve.IsSheafFor P S.arrows) (trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f S).arrows) : CategoryTheory.Presieve.IsSheafFor P R

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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X} (h : S.arrows ≤ R) (trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) : CategoryTheory.Presieve.IsSheafFor P R

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.

def CategoryTheory.Presieve.Arrows.Compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) (x : (i : I) → P.obj (Opposite.op (X i))) : Prop

A more explicit version of FamilyOfElements.Compatible for a Presieve.ofArrows.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_iff_ofArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) (x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)) (t : P.obj (Opposite.op B)) : x.IsAmalgamation t ↔ ∀ (i : I), P.map (π i).op t = x (π i) ⋯

theorem CategoryTheory.Presieve.Arrows.Compatible.exists_familyOfElements {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type u_1} {X : I → C} {π : (i : I) → X i ⟶ B} {x : (i : I) → P.obj (Opposite.op (X i))} (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) : ∃ (x' : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)), ∀ (i : I), x' (π i) ⋯ = x i

noncomputable def CategoryTheory.Presieve.Arrows.Compatible.familyOfElements {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type u_1} {X : I → C} {π : (i : I) → X i ⟶ B} {x : (i : I) → P.obj (Opposite.op (X i))} (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)

A FamilyOfElements associated to an explicit family of elements.

Equations

• hx.familyOfElements = ⋯.choose

@[simp]

theorem CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_ofArrows_mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type u_1} {X : I → C} {π : (i : I) → X i ⟶ B} {x : (i : I) → P.obj (Opposite.op (X i))} (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) (i : I) : hx.familyOfElements (π i) ⋯ = x i

theorem CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type u_1} {X : I → C} {π : (i : I) → X i ⟶ B} {x : (i : I) → P.obj (Opposite.op (X i))} (hx : CategoryTheory.Presieve.Arrows.Compatible P π x) : hx.familyOfElements.Compatible

theorem CategoryTheory.Presieve.isSheafFor_arrows_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.Compatible P π x → ∃! t : P.obj (Opposite.op B), ∀ (i : I), P.map (π i).op t = x i

def CategoryTheory.Presieve.Arrows.PullbackCompatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).hasPullbacks] (x : (i : I) → P.obj (Opposite.op (X i))) : Prop

A more explicit version of FamilyOfElements.PullbackCompatible for a Presieve.ofArrows.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Presieve.Arrows.pullbackCompatible_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).hasPullbacks] (x : (i : I) → P.obj (Opposite.op (X i))) : CategoryTheory.Presieve.Arrows.Compatible P π x ↔ CategoryTheory.Presieve.Arrows.PullbackCompatible P π x

theorem CategoryTheory.Presieve.isSheafFor_arrows_iff_pullbacks {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).hasPullbacks] : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.PullbackCompatible P π x → ∃! t : P.obj (Opposite.op B), ∀ (i : I), P.map (π i).op t = x i