arrow — Mathlib

English

The morphism in C from the arbitrarily chosen underlying object to the ambient object is given by the arrow of the representative.

Русский

Морфизм в C от выбранного базового объекта к окружающему объекту задаётся стрелкой представителя.

LaTeX

$$$\\text{arrow}(Y) := (\\mathrm{representative.obj} Y).\\mathrm{obj}.\\mathrm{hom}$$$

Lean4

/-- The morphism in `C` from the arbitrarily chosen underlying object to the ambient object.
-/
noncomputable def arrow {X : C} (Y : Subobject X) : (Y : C) ⟶ X :=
  (representative.obj Y).obj.hom

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