underlying — Mathlib

English

This isomorphism is natural with respect to A, providing a canonical bridge between representative and any MonoOver object.

Русский

Этот изоморфизм естествен по отношению к A, обеспечивая канонический мост между представителем и любым объектом MonoOver.

LaTeX

$$$\\mathrm{representative\\_iso}_X(A) : \\mathrm{representative}((\\mathrm{toThinSkeleton} (A)).obj) \\cong A$$$

Lean4

/-- Use choice to pick a representative underlying object in `C` for any `Subobject X`.

Prefer to use the coercion `P : C` rather than explicitly writing `underlying.obj P`.
-/
noncomputable def underlying {X : C} : Subobject X ⥤ C :=
  representative ⋙ MonoOver.forget _ ⋙ Over.forget _

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