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.

In Mathlib/CategoryTheory/Sites/IsSheafFor.lean it is defined what it means for a presheaf to be a sheaf for a particular sieve. 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 [MLM92]: Using compatible_iff_sieveCompatible, the definitions of IsSheaf are equivalent. There are also alternate definitions given:

  • Sheaf for a pretopology (Prop 1): isSheaf_pretopology combined with pullbackCompatible_iff.
  • Sheaf for a pretopology as equalizer (Prop 1, bis): Equalizer.Presieve.sheaf_condition combined with the previous.

References

• [MLM92]: Sheaves in geometry and logic, Saunders MacLane, and Ieke Moerdijk: Chapter III, Section 4.
• [Joh02]: 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.IsSeparated {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (P : Functor Cᵒᵖ (Type w)) : Prop

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

Equations

• CategoryTheory.Presieve.IsSeparated J P = ∀ ⦃X : C⦄, ∀ S ∈ J X, CategoryTheory.Presieve.IsSeparatedFor P S.arrows

def CategoryTheory.Presieve.IsSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (P : Functor 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, isSheaf_pretopology shows it suffices to check the sheaf condition at presieves in the pretopology.

Equations

• CategoryTheory.Presieve.IsSheaf J P = ∀ ⦃X : C⦄, ∀ S ∈ J X, CategoryTheory.Presieve.IsSheafFor P S.arrows

theorem CategoryTheory.Presieve.IsSheaf.isSheafFor {C : Type u} [Category.{v, u} C] {X : C} (J : GrothendieckTopology C) {P : Functor Cᵒᵖ (Type w)} (hp : IsSheaf J P) (R : Presieve X) (hr : Sieve.generate R ∈ J X) : IsSheafFor P R

theorem CategoryTheory.Presieve.isSheaf_of_le {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {J₁ J₂ : GrothendieckTopology C} : J₁ ≤ J₂ → IsSheaf J₂ P → IsSheaf J₁ P

theorem CategoryTheory.Presieve.isSeparated_of_le {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {J₁ J₂ : GrothendieckTopology C} : J₁ ≤ J₂ → IsSeparated J₂ P → IsSeparated J₁ P

theorem CategoryTheory.Presieve.IsSheaf.isSeparated {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P : Functor Cᵒᵖ (Type w)} (h : IsSheaf J P) : IsSeparated J P

@[deprecated CategoryTheory.Presieve.IsSheaf.isSeparated (since := "2025-08-28")]

theorem CategoryTheory.Presieve.isSeparated_of_isSheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P : Functor Cᵒᵖ (Type w)} (h : IsSheaf J P) : IsSeparated J P

Alias of CategoryTheory.Presieve.IsSheaf.isSeparated.

theorem CategoryTheory.Presieve.IsSeparated.isSheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P : Functor Cᵒᵖ (Type w)} (h : IsSeparated J P) (h' : ∀ (X : C), ∀ S ∈ J X, ∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃ (t : P.obj (Opposite.op X)), x.IsAmalgamation t) : IsSheaf J P

If P is separated and every compatible family of elements of P for a covering sieve has an amalgamation, P is a sheaf.

theorem CategoryTheory.Presieve.isSheaf_of_nat_equiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P₁ : Functor Cᵒᵖ (Type w)} {P₂ : Functor Cᵒᵖ (Type w')} (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)) (he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)) (hP₁ : IsSheaf J P₁) : IsSheaf J P₂

theorem CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {P₁ : Functor Cᵒᵖ (Type w)} {P₂ : Functor Cᵒᵖ (Type w')} (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)) (he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)) : IsSheaf J P₁ ↔ IsSheaf J P₂

theorem CategoryTheory.Presieve.isSheaf_iso {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} (J : GrothendieckTopology C) {P' : Functor Cᵒᵖ (Type w)} (i : P ≅ P') (h : IsSheaf J P) : IsSheaf J P'

The property of being a sheaf is preserved by isomorphism.

theorem CategoryTheory.Presieve.isSeparated_iso {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} (J : GrothendieckTopology C) {P' : Functor Cᵒᵖ (Type w)} (i : P ≅ P') (hP : IsSeparated J P) : IsSeparated J P'

The property of being separated is preserved under isomorphisms.

theorem CategoryTheory.Presieve.isSheaf_of_yoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {P : Functor Cᵒᵖ (Type v)} (h : ∀ {X : C}, ∀ S ∈ J X, YonedaSheafCondition P S) : IsSheaf J P

theorem CategoryTheory.Presieve.isSheaf_pretopology {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} [Limits.HasPullbacks C] (K : Pretopology C) : IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P 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} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} : IsSheaf ⊥ P

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

theorem CategoryTheory.Presieve.isSheaf_comp_uliftFunctor {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} (J : GrothendieckTopology C) (h : IsSheaf J P) : IsSheaf J (P.comp uliftFunctor.{w', w})

The composition of a sheaf with a ULift functor is still a sheaf.

def CategoryTheory.Presieve.compatibleYonedaFamily_toCocone {C : Type u} [Category.{v, u} C] {X : C} (R : Presieve X) (W : C) (x : FamilyOfElements (yoneda.obj W) R) (hx : x.Compatible) : Limits.Cocone R.diagram

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

Equations

• R.compatibleYonedaFamily_toCocone W x hx = { pt := W, ι := { app := fun (f : R.category) => x f.obj.hom ⋯, naturality := ⋯ } }

def CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone {C : Type u} [Category.{v, u} C] {X : C} (R : Presieve X) (s : Limits.Cocone R.diagram) : FamilyOfElements (yoneda.obj s.pt) R

Construct a family of elements from a cocone.

Equations

• R.yonedaFamilyOfElements_fromCocone s f hf = s.ι.app { obj := CategoryTheory.Over.mk f, property := hf }

theorem CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible {C : Type u} [Category.{v, u} C] {X : C} (S : Sieve X) (s : Limits.Cocone S.arrows.diagram) : (S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible

theorem CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit {C : Type u} [Category.{v, u} C] {X : C} (S : Sieve X) : (∀ (W : C), Presieve.IsSheafFor (yoneda.obj W) S.arrows) ↔ Nonempty (Limits.IsColimit S.arrows.cocone)

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