isLocallySurjective_iff_isIso — Mathlib

English

For a morphism of presheaves f: F → G in Type w, IsLocallySurjective f is equivalent to IsIso (imageι f).

Русский

Для отображения f: F → G типа Type w локальная сюрьктивность эквивалентна тому, что imageι f изоморфен

LaTeX

$$$\text{IsLocallySurjective}_J(f) \iff \text{IsIso}(\mathrm{Sheaf.image\,ι}(f))$$$

Lean4

theorem isLocallySurjective_iff_isIso {F G : Sheaf J (Type w)} (f : F ⟶ G) :
    IsLocallySurjective f ↔ IsIso (Sheaf.imageι f) :=
  by
  dsimp only [IsLocallySurjective]
  rw [Sheaf.imageι, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', Subpresheaf.eq_top_iff_isIso]
  exact isIso_iff_of_reflects_iso (f := Sheaf.imageι f) (F := sheafToPresheaf J (Type w))

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