isLocallySurjective_iff_range_sheafify_eq_top

English

For a morphism f: F → G in presheaves, J locally surjective iff the sheafification of the range presheaf of the whiskered map equals the top presheaf.

Русский

Для морфизма f: F → G в прешефах J локально сюрьективно тогда и только тогда, когда просеивка (рафа) диапазона отображения после обрамления равна верхнему пресхефу.

LaTeX

$$$\text{IsLocallySurjective}_J(f) \iff (\operatorname{Subpresheaf.range}(\mathrm{whiskerRight}(f, \mathrm{forget}\ A))).\mathrm{sheafify} J = \top$$$

Lean4

theorem isLocallySurjective_iff_range_sheafify_eq_top {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) :
    IsLocallySurjective J f ↔ (Subpresheaf.range (whiskerRight f (forget A))).sheafify J = ⊤ :=
  by
  simp only [Subpresheaf.ext_iff, funext_iff, Set.ext_iff, Subpresheaf.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]
  exact ⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩

Похожие утверждения