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

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

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