essImage_overPost — Mathlib

English

For F full, the essImage of Under.post F on Y coincides with F.essImage on Y.right.

Русский

Для полного F, essImage в Under.post F на Y совпадает с essImage F на Y.right.

LaTeX

$$$\big(\mathrm{essImage}_{Under(post\ F)}(Y)\big) \iff \big(\mathrm{essImage}_F(Y.right)\big)$$$

Lean4

/-- The essential image of `Over.post F` where `F` is full is the same as the essential image of
`F`. -/
@[simp]
theorem essImage_overPost [F.Full] {Y : Over (F.obj X)} : (Over.post F (X := X)).essImage Y ↔ F.essImage Y.left
    where
  mp := .of_overPost
  mpr := fun ⟨Z, ⟨e⟩⟩ ↦
    let ⟨f, hf⟩ := F.map_surjective (e.hom ≫ Y.hom);
    ⟨.mk f, ⟨Over.isoMk e⟩⟩

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