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 (max u v))) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => IsEmpty.elim instIsEmptyEmpty 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))

noncomputable def CategoryTheory.Presieve.preservesTerminalOfIsSheafForEmpty {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => IsEmpty.elim instIsEmptyEmpty 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.

Equations

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

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

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.piComparison_fac {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) {α : 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 (CategoryTheory.Limits.Cofan.inj c))

noncomputable def CategoryTheory.Presieve.preservesProductOfIsSheafFor {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => IsEmpty.elim instIsEmptyEmpty a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Presieve.hasPullbacks (CategoryTheory.Presieve.ofArrows X (CategoryTheory.Limits.Cofan.inj c))] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (CategoryTheory.Limits.Cofan.inj c i)] (hd : Pairwise fun (i j : α) => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (CategoryTheory.Limits.Cofan.inj c i) (CategoryTheory.Limits.Cofan.inj c j)) (hF' : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X (CategoryTheory.Limits.Cofan.inj c))) : 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.

Equations

• CategoryTheory.Presieve.preservesProductOfIsSheafFor F hF hI c hc hd hF' = let_fun this := ⋯; CategoryTheory.Limits.PreservesProduct.ofIsoComparison F fun (x : α) => Opposite.op (X x)

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

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

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