English
For a coherent topology, a presheaf is locally surjective iff it is locally surjective after whiskering with forgetful functors.
Русский
Для когерентной топологии презашифр локально сюръективен тогда и только тогда, когда он локально сюръективен после whisker() с забыванием.
LaTeX
$$$\mathrm{IsLocallySurjective}(\mathrm{coherentTopology}(C), f) \iff \mathrm{IsLocallySurjective}(\mathrm{regularTopology}(C), f^{\mathrm{val}})$$$
Lean4
theorem presheafIsLocallySurjective_iff {F G : Cᵒᵖ ⥤ D} (f : F ⟶ G) [Preregular C] [FinitaryPreExtensive C]
[PreservesFiniteProducts F] [PreservesFiniteProducts G] [PreservesFiniteProducts (forget D)] :
Presheaf.IsLocallySurjective (coherentTopology C) f ↔ Presheaf.IsLocallySurjective (regularTopology C) f :=
by
constructor
· rw [Presheaf.isLocallySurjective_iff_whisker_forget,
Presheaf.isLocallySurjective_iff_whisker_forget (J := regularTopology C)]
exact regularTopology.isLocallySurjective_sheaf_of_types _
· refine Presheaf.isLocallySurjective_of_le (J := regularTopology C) ?_ _
rw [← extensive_regular_generate_coherent]
exact (Coverage.gi _).gc.monotone_l le_sup_right
