isLocallySurjective_iff_epi — Mathlib

English

For a morphism f: F → G of Sheaves of Type w with sheafification, IsLocallySurjective f is equivalent to epi f.

Русский

Для морфизма f: F → G Sheaf типа w с применением шейфификации IsLocallySurjective f эквивалентно epi f.

LaTeX

$$$\text{IsLocallySurjective} f \iff \text{Epi}(f)$$$

Lean4

theorem isLocallySurjective_iff_epi {F G : Sheaf J (Type w)} (φ : F ⟶ G) [HasSheafify J (Type w)] :
    IsLocallySurjective φ ↔ Epi φ := by
  constructor
  · intro
    infer_instance
  · intro
    have := epi_of_epi_fac (Sheaf.toImage_ι φ)
    rw [isLocallySurjective_iff_isIso φ]
    apply isIso_of_mono_of_epi

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