essImage_underPost — Mathlib

English

If F is full, then essImage for Under.post F aligns with F.essImage on the corresponding side.

Русский

Если F полно, essImage для Under.post F согласуется с essImage F на соответствующей стороне.

LaTeX

$$$\mathsf{essImage}_{Under.post F} = \mathsf{essImage}_F$ on the appropriate side$$

Lean4

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

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