isLocallySurjective_iff_range_sheafify_eq_top'

English

For morphism f: F ⇢ G between presheaves valued in Type w, IsLocallySurjective J f is equivalent to the sheafification of its range being top.

Русский

Для отображения f между прешефами, значащими в Type w, локальная сюрьективность эквивалентна тому, что просеивка диапазона равна вершине.

LaTeX

$$$\text{IsLocallySurjective}_J(f) \iff (\operatorname{range} f).\mathrm{sheafify} J = \top$$$

Lean4

theorem isLocallySurjective_iff_range_sheafify_eq_top' {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G) :
    IsLocallySurjective J f ↔ (Subpresheaf.range f).sheafify J = ⊤ := by
  apply isLocallySurjective_iff_range_sheafify_eq_top

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