English
An equivalent formulation of local surjectivity in presheaves via stalk surjectivity.
Русский
Эквивалентная формулировка локальной сюръективности прешейфов через сюръективность стежков.
LaTeX
$$$ IsLocallySurjective T \\Leftrightarrow \\forall x, Surjective\\; (stalkFunctor\\; C\\ x).map\\; T$$$
Lean4
theorem isSheaf_of_isTerminal_of_indiscrete {X : TopCat.{w}} (hind : X.str = ⊤) (F : Presheaf C X)
(it : IsTerminal <| F.obj <| op ⊥) : F.IsSheaf := fun c U s hs =>
by
obtain rfl | hne := eq_or_ne U ⊥
· intro _ _
rw [@existsUnique_iff_exists _ ⟨fun _ _ => _⟩]
· refine ⟨it.from _, fun U hU hs => IsTerminal.hom_ext ?_ _ _⟩
rwa [le_bot_iff.1 hU.le]
· apply it.hom_ext
· convert Presieve.isSheafFor_top_sieve (F ⋙ coyoneda.obj (@op C c))
rw [← Sieve.id_mem_iff_eq_top]
have := (U.eq_bot_or_top hind).resolve_left hne
subst this
obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
· exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim
obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
obtain rfl | rfl := U.eq_bot_or_top hind
· cases hm
· convert hf
