English
A presheaf on a point (PUnit) is a sheaf iff the fiber over the bottom open is terminal.
Русский
Образ presheaf на точке (PUnit) является sheaf тогда и только тогда, когда фибер над нижним открытым множеством является терминальным.
LaTeX
$$$F.IsSheaf \iff Nonempty (IsTerminal (F.obj (op ⊥)))$$$
Lean4
/-- The `stalkToFiber` map is surjective at `x` if
every point in the fiber `T x` has an allowed section passing through it.
-/
theorem stalkToFiber_surjective (P : LocalPredicate T) (x : X)
(w : ∀ t : T x, ∃ (U : OpenNhds x) (f : ∀ y : U.1, T y) (_ : P.pred f), f ⟨x, U.2⟩ = t) :
Function.Surjective (stalkToFiber P x) := fun t ↦
by
rcases w t with ⟨U, f, h, rfl⟩
fconstructor
· exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩
· exact stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩
