# Documentation

Mathlib.CategoryTheory.Sites.Preserves

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

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
Instances For

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.
Instances For
theorem CategoryTheory.Presieve.firstMap_eq_secondMap {C : Type u} {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => )) (hI : ) {α : Type} {X : αC} (c : ) [∀ (i : α), ] (hd : ∀ (i j : α), i j) :

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

noncomputable def CategoryTheory.Presieve.preservesProductOfIsSheafFor {C : Type u} {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => )) (hI : ) {α : Type} {X : αC} (c : ) (hc : ) [∀ (i : α), ] (hd : ∀ (i j : α), i j) :

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
• One or more equations did not get rendered due to their size.
Instances For

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

theorem CategoryTheory.Presieve.isSheafFor_iff_preservesProduct {C : Type u} {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun (a : Empty) => )) (hI : ) {α : Type} {X : αC} (c : ) (hc : ) [∀ (i : α), ] (hd : ∀ (i j : α), i j) :