epi_of_isLocallySurjective' — Mathlib

English

If f is locally surjective, then f is epi.

Русский

Если f локально сюрьективен, то f эпиморфизм.

LaTeX

$$$\text{IsLocallySurjective}_J(f) \Rightarrow \text{Epi}(f)$$$

Lean4

instance epi_of_isLocallySurjective' {F₁ F₂ : Sheaf J (Type w)} (φ : F₁ ⟶ F₂) [IsLocallySurjective φ] : Epi φ where
  left_cancellation {Z} f₁ f₂
    h := by
    ext X x
    apply (((isSheaf_iff_isSheaf_of_type _ _).1 Z.2).isSeparated _ (Presheaf.imageSieve_mem J φ.val x)).ext
    rintro Y f ⟨s : F₁.val.obj (op Y), hs : φ.val.app _ s = F₂.val.map f.op x⟩
    dsimp
    have h₁ := congr_fun (f₁.val.naturality f.op) x
    have h₂ := congr_fun (f₂.val.naturality f.op) x
    dsimp at h₁ h₂
    rw [← h₁, ← h₂, ← hs]
    exact congr_fun (congr_app ((sheafToPresheaf J _).congr_map h) (op Y)) s

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