Presheaves on PUnit #
Presheaves on PUnit satisfy sheaf condition iff its value at empty set is a terminal object.
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.toPrefunctor.obj (Opposite.op ⊥)))
:
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)
:
TopCat.Presheaf.IsSheaf F ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.toPrefunctor.obj (Opposite.op ⊥)))
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.toPrefunctor.obj (Opposite.op ⊥)))
:
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} ))
:
TopCat.Presheaf.IsSheaf F ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.toPrefunctor.obj (Opposite.op ⊥)))