Documentation

Mathlib.Topology.Sheaves.PUnit

Presheaves on PUnit #

Presheaves on PUnit satisfy sheaf condition iff its value at empty set is a terminal object.

source
theorem TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscrete {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (hind : X.str = ⊤) (F : TopCat.Presheaf C X) (it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))) :
F.IsSheaf
source
theorem TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (hind : X.str = ⊤) (F : TopCat.Presheaf C X) :
F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))
source
theorem TopCat.Presheaf.isSheaf_on_punit_of_isTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] (F : TopCat.Presheaf C (TopCat.of PUnit.{u_1 + 1})) (it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))) :
F.IsSheaf
source
theorem TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] (F : TopCat.Presheaf C (TopCat.of PUnit.{u_1 + 1})) :
F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))