equivMonoOver — Mathlib

English

The functor representative: Subobject X ⥤ MonoOver X is an equivalence of categories.

Русский

Функтор representative: Subobject X ⥤ MonoOver X является эквивалентностью категорий.

LaTeX

$$$(\\text{representative}(X)) : Subobject(X) \\simeq MonoOver(X)$$$

Lean4

/-- The category of subobjects is equivalent to the `MonoOver` category. It is more convenient to
use the former due to the partial order instance, but oftentimes it is easier to define structures
on the latter. -/
noncomputable def equivMonoOver (X : C) : Subobject X ≌ MonoOver X :=
  ThinSkeleton.equivalence _

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