underlyingIso — Mathlib

English

From a morphism f: X → Y that is mono, the canonical isomorphism identifies the chosen underlying object of Subobject.mk f with X.

Русский

Для моно-морфизма f: X → Y каноническое изоморфизмом сопоставляется выбранный подобъект Subobject.mk f с X.

LaTeX

$$$\\mathrm{underlyingIso}(f) : (\\mathrm{Subobject.mk} f : C) \\cong X$$$

Lean4

/-- If we construct a `Subobject Y` from an explicit `f : X ⟶ Y` with `[Mono f]`,
then pick an arbitrary choice of underlying object `(Subobject.mk f : C)` back in `C`,
it is isomorphic (in `C`) to the original `X`.
-/
noncomputable def underlyingIso {X Y : C} (f : X ⟶ Y) [Mono f] : (Subobject.mk f : C) ≅ X :=
  (MonoOver.forget _ ⋙ Over.forget _).mapIso (representativeIso (MonoOver.mk' f))

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