underlyingIso_hom_comp_eq_mk — Mathlib

English

For any mono morphism f: X → Y, the image of f under the underlying isomorphism composed with f equals the arrow of mk f.

Русский

Для моно-морфизма f: X → Y композиция с образовoм подмножества даёт стрелку mk f.

LaTeX

$$$(\\underline{underlyingIso} f).hom \\; \\circ f = (\\text{Subobject.mk } f).arrow$$$

Lean4

@[reassoc (attr := simp)]
theorem underlyingIso_hom_comp_eq_mk {X Y : C} (f : X ⟶ Y) [Mono f] : (underlyingIso f).hom ≫ f = (mk f).arrow :=
  (Iso.eq_inv_comp _).1 (underlyingIso_arrow f).symm

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