isoStrongEpiMono_hom_comp_ι — Mathlib

English

For any e: X ⟶ I', m: I' ⟶ Y and comm: e ≫ m = f, the hom component of image.isoStrongEpiMono satisfies: its composition with image.ι f equals m.

Русский

Для любых e: X ⟶ I', m: I' ⟶ Y и comm: e ≫ m = f, композиция гомоморфизма image.isoStrongEpiMono с image.ι f равна m.

LaTeX

$$$\big(\mathrm{image.isoStrongEpiMono}(e,m,comm)\big).hom \circ \mathrm{image.\iota}(f) = m$$$

Lean4

@[simp]
theorem isoStrongEpiMono_hom_comp_ι {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [StrongEpi e] [Mono m] :
    (image.isoStrongEpiMono e m comm).hom ≫ image.ι f = m :=
  by
  dsimp [isoStrongEpiMono]
  apply IsImage.lift_fac

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