representative — Mathlib

English

Use the equivalence to pick a canonical representative in MonoOver X for each Subobject X.

Русский

Используя эквивалентность, выбрать канонический представитель в MonoOver X для каждого Subobject X.

LaTeX

$$$\\text{representative} : Subobject(X) \\to MonoOver(X) \\text{ is a functor (inverse to the equivalence).}$$$

Lean4

/-- Use choice to pick a representative `MonoOver X` for each `Subobject X`.
-/
noncomputable def representative {X : C} : Subobject X ⥤ MonoOver X :=
  (equivMonoOver X).functor

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