Sheaves preserve products

We prove that a presheaf which satisfies the sheaf condition with respect to certain presieves preserve "the corresponding products".

Main results

More precisely, given a presheaf F : Cᵒᵖ ⥤ Type*, we have:

• If F satisfies the sheaf condition with respect to the empty sieve on the initial object of C, then F preserves terminal objects. See preservesTerminalOfIsSheafForEmpty.

• If F furthermore satisfies the sheaf condition with respect to the presieve consisting of the inclusion arrows in a coproduct in C, then F preserves the corresponding product. See preservesProductOfIsSheafFor.

• If F preserves a product, then it satisfies the sheaf condition with respect to the corresponding presieve of arrows. See isSheafFor_of_preservesProduct.

noncomputable def CategoryTheory.Presieve.isTerminal_of_isSheafFor_empty_presieve {C : Type u} [CategoryTheory.Category.{v, u} C] (I : C) (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => instIsEmptyEmpty.elim a)) : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op I))

If F is a presheaf which satisfies the sheaf condition with respect to the empty presieve on any object, then F takes that object to the terminal object.

Equations

• CategoryTheory.Presieve.isTerminal_of_isSheafFor_empty_presieve I F hF = CategoryTheory.Limits.IsTerminal.ofUnique (F.obj (Opposite.op I))

theorem CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => instIsEmptyEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty Cᵒᵖ) F

If F is a presheaf which satisfies the sheaf condition with respect to the empty presieve on the initial object, then F preserves terminal objects.

theorem CategoryTheory.Presieve.piComparison_fac {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) : let_fun this := ⋯; (CategoryTheory.Limits.piComparison F fun (x : α) => Opposite.op (X x)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.opCoproductIsoProduct' hc (CategoryTheory.Limits.productIsProduct fun (x : α) => Opposite.op (X x))).inv) (CategoryTheory.Equalizer.Presieve.Arrows.forkMap F X c.inj)

theorem CategoryTheory.Presieve.isSheafFor_of_preservesProduct {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun (x : α) => Opposite.op (X x)) F] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)

If F preserves a particular product, then it IsSheafFor the corresponding presieve of arrows.

theorem CategoryTheory.Presieve.firstMap_eq_secondMap {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => instIsEmptyEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X) [(CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun (i j : α) => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Equalizer.Presieve.Arrows.firstMap F X c.inj = CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj

The two parallel maps in the equalizer diagram for the sheaf condition corresponding to the inclusion maps in a disjoint coproduct are equal.

theorem CategoryTheory.Presieve.preservesProduct_of_isSheafFor {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => instIsEmptyEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun (i j : α) => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) (hF' : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun (x : α) => Opposite.op (X x)) F

If F is a presheaf which IsSheafFor a presieve of arrows and the empty presieve, then it preserves the product corresponding to the presieve of arrows.

theorem CategoryTheory.Presieve.isSheafFor_iff_preservesProduct {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => instIsEmptyEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun (i j : α) => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) ↔ Nonempty (CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun (x : α) => Opposite.op (X x)) F)