instSubsingletonHom — Mathlib

English

If every Hom-set in the original category C is a subsingleton, then every Hom-set in the quotient category Quotient r is also a subsingleton.

Русский

Если для каждой пары объектов в исходной категории обобщенное множество гомоморфизмов является субодин, то аналогично и в квотной категории.

LaTeX

$$$\forall X,Y\in C\,\operatorname{Subsingleton}(X\to Y)\; \Rightarrow\; \forall x,y\in \mathrm{Quotient}(r),\; \operatorname{Subsingleton}((\mathrm{Quotient}.category\ r).Hom x y).$$$

Lean4

instance [∀ (x y : C), Subsingleton (x ⟶ y)] (x y : Quotient r) : Subsingleton (x ⟶ y) :=
  (full_functor r).map_surjective.subsingleton

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