Presheaves on punit #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Presheaves on punit satisfy sheaf condition iff its value at empty set is a terminal object.
theorem
Top.presheaf.is_sheaf_of_is_terminal_of_indiscrete
{C : Type u}
[category_theory.category C]
{X : Top}
(hind : X.str = ⊤)
(F : Top.presheaf C X)
(it : category_theory.limits.is_terminal (F.obj (opposite.op ⊥))) :
F.is_sheaf
theorem
Top.presheaf.is_sheaf_iff_is_terminal_of_indiscrete
{C : Type u}
[category_theory.category C]
{X : Top}
(hind : X.str = ⊤)
(F : Top.presheaf C X) :
theorem
Top.presheaf.is_sheaf_on_punit_of_is_terminal
{C : Type u}
[category_theory.category C]
(F : Top.presheaf C (Top.of punit))
(it : category_theory.limits.is_terminal (F.obj (opposite.op ⊥))) :
F.is_sheaf
theorem
Top.presheaf.is_sheaf_on_punit_iff_is_terminal
{C : Type u}
[category_theory.category C]
(F : Top.presheaf C (Top.of punit)) :