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} [Category.{v, u} C] (I : C) (F : Functor Cᵒᵖ (Type w)) (hF : IsSheafFor F (ofArrows Empty.elim fun (a : Empty) => Empty.instIsEmpty.elim a)) : 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} [Category.{v, u} C] {I : C} (F : Functor Cᵒᵖ (Type w)) (hF : IsSheafFor F (ofArrows Empty.elim fun (a : Empty) => Empty.instIsEmpty.elim a)) (hI : Limits.IsInitial I) : Limits.PreservesLimit (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} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : Limits.Cofan X) (hc : Limits.IsColimit c) : have this := ⋯; (Limits.piComparison F fun (x : α) => Opposite.op (X x)) = CategoryStruct.comp (F.map (Limits.opCoproductIsoProduct' hc (Limits.productIsProduct fun (x : α) => Opposite.op (X x))).inv) (Equalizer.Presieve.Arrows.forkMap F X c.inj)

theorem CategoryTheory.Presieve.isSheafFor_of_preservesProduct {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : Limits.Cofan X) (hc : Limits.IsColimit c) [(ofArrows X c.inj).HasPairwisePullbacks] [Limits.PreservesLimit (Discrete.functor fun (x : α) => Opposite.op (X x)) F] : IsSheafFor F (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} [Category.{v, u} C] {I : C} (F : Functor Cᵒᵖ (Type w)) (hF : IsSheafFor F (ofArrows Empty.elim fun (a : Empty) => Empty.instIsEmpty.elim a)) (hI : Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : Limits.Cofan X) [(ofArrows X c.inj).HasPairwisePullbacks] [Limits.HasInitial C] [∀ (i : α), Mono (c.inj i)] (hd : Pairwise fun (i j : α) => IsPullback (Limits.initial.to (X i)) (Limits.initial.to (X j)) (c.inj i) (c.inj j)) : Equalizer.Presieve.Arrows.firstMap F X c.inj = 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} [Category.{v, u} C] {I : C} (F : Functor Cᵒᵖ (Type w)) (hF : IsSheafFor F (ofArrows Empty.elim fun (a : Empty) => Empty.instIsEmpty.elim a)) (hI : Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : Limits.Cofan X) (hc : Limits.IsColimit c) [(ofArrows X c.inj).HasPairwisePullbacks] [Limits.HasInitial C] [∀ (i : α), Mono (c.inj i)] (hd : Pairwise fun (i j : α) => IsPullback (Limits.initial.to (X i)) (Limits.initial.to (X j)) (c.inj i) (c.inj j)) (hF' : IsSheafFor F (ofArrows X c.inj)) : Limits.PreservesLimit (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} [Category.{v, u} C] {I : C} (F : Functor Cᵒᵖ (Type w)) (hF : IsSheafFor F (ofArrows Empty.elim fun (a : Empty) => Empty.instIsEmpty.elim a)) (hI : Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : Limits.Cofan X) (hc : Limits.IsColimit c) [(ofArrows X c.inj).HasPairwisePullbacks] [Limits.HasInitial C] [∀ (i : α), Mono (c.inj i)] (hd : Pairwise fun (i j : α) => IsPullback (Limits.initial.to (X i)) (Limits.initial.to (X j)) (c.inj i) (c.inj j)) : IsSheafFor F (ofArrows X c.inj) ↔ Limits.PreservesLimit (Discrete.functor fun (x : α) => Opposite.op (X x)) F