English
In a finitary pre-extensive setting, presheaves are locally surjective iff they preserve finite products.
Русский
В условиях финитно-пред-extensive, презашифры локально сюръективны тогда и только тогда, когда сохраняют конечные произведения.
LaTeX
$$$\mathrm{IsLocallySurjective} \iff \mathrm{PreservesFiniteProducts}$$$
Lean4
theorem presheafIsLocallySurjective_iff [FinitaryPreExtensive C] {F G : Cᵒᵖ ⥤ D} (f : F ⟶ G) [PreservesFiniteProducts F]
[PreservesFiniteProducts G] [PreservesFiniteProducts (forget D)] :
Presheaf.IsLocallySurjective (extensiveTopology C) f ↔ ∀ (X : C), Function.Surjective (f.app (op X)) :=
by
constructor
· rw [Presheaf.isLocallySurjective_iff_whisker_forget (J := extensiveTopology C)]
exact fun h _ ↦ surjective_of_isLocallySurjective_sheaf_of_types (Functor.whiskerRight f (forget D)) h
· intro h
refine ⟨fun {X} y ↦ ?_⟩
obtain ⟨x, hx⟩ := h X y
convert (extensiveTopology C).top_mem' X
rw [← Sieve.id_mem_iff_eq_top]
simpa [Presheaf.imageSieve] using ⟨x, hx⟩
