isIso_left_iff_subobjectMk_eq — Mathlib

English

An arrow f.left is iso if and only if the corresponding subobjects mk P.obj.hom and mk Q.obj.hom coincide.

Русский

Морофизм слева является изоморфизмом тогда и только тогда, когда mk P.obj.hom = mk Q.obj.hom.

LaTeX

$$$\text{IsIso } f.left \;\iff \; \operatorname{Subobject.mk} P.1.hom = \operatorname{Subobject.mk} Q.1.hom$$$

Lean4

theorem isIso_left_iff_subobjectMk_eq : IsIso f.left ↔ Subobject.mk P.1.hom = Subobject.mk Q.1.hom :=
  ⟨fun _ ↦ Subobject.mk_eq_mk_of_comm _ _ (asIso f.left) (by simp), fun h ↦
    ⟨Subobject.ofMkLEMk _ _ h.symm.le, by simp [← cancel_mono P.1.hom], by simp [← cancel_mono Q.1.hom]⟩⟩

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