preimage_image_of_epi — Mathlib

English

If p is an epimorphism, then (G.preimage p).image p = G for any subpresheaf G of F.

Русский

Если p — эпиморфизм, то (G.preimage p).image p = G для любой подпрефеши G.

LaTeX

$$$ (G.\\mathrm{preimage} p).\\mathrm{image} p = G \\quad\\text{ if } \\text{epi}(p) $$$

Lean4

@[simp]
theorem preimage_image_of_epi (G : Subpresheaf F) (p : F' ⟶ F) [hp : Epi p] : (G.preimage p).image p = G :=
  by
  apply le_antisymm
  · rw [image_le_iff]
  · intro i x hx
    simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp
    obtain ⟨y, rfl⟩ := hp _ x
    exact ⟨y, hx, rfl⟩

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