representativeIso — Mathlib

English

For any X and A in MonoOver X, there exists an isomorphism in C between the chosen representative and A.

Русский

Для любого X и A в MonoOver X существует изоморфизм в C между выбранным представителем и A.

LaTeX

$$$\\forall A: MonoOver(X),\\; \\mathrm{representative.obj}((\\mathrm{toThinSkeleton}(\\mathrm{MonoOver}(X))).obj A) \\cong A$$$

Lean4

/-- Starting with `A : MonoOver X`, we can take its equivalence class in `Subobject X`
then pick an arbitrary representative using `representative.obj`.
This is isomorphic (in `MonoOver X`) to the original `A`.
-/
noncomputable def representativeIso {X : C} (A : MonoOver X) : representative.obj ((toThinSkeleton _).obj A) ≅ A :=
  (equivMonoOver X).counitIso.app A

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