instFaithfulIncl — Mathlib

English

Let C be a category. The inclusion functor incl: C → WithInitial(C) is faithful; i.e., for any objects X, Y in C, the map Hom_C(X, Y) → Hom_{WithInitial(C)}(incl(X), incl(Y)) is injective. In particular, if incl(f) = incl(g), then f = g.

Русский

Пусть C — категория. Включение incl: C → WithInitial(C) верно (faithful); т. е. для любых объектов X, Y в C отображение Hom_C(X, Y) → Hom_{WithInitial(C)}(incl(X), incl(Y)) инъективно. В частности, если incl(f) = incl(g), то f = g.

LaTeX

$$$$\mathrm{incl}: \mathcal{C} \to \mathrm{WithInitial}(\mathcal{C}) \text{ is faithful, i.e. }\forall X,Y\in \mathcal{C},\ \mathrm{Hom}_{\mathcal{C}}(X,Y) \to \mathrm{Hom}_{\mathrm{WithInitial}(\mathcal{C})}(\mathrm{incl}(X),\mathrm{incl}(Y)) \text{ is injective.}$$$$

Lean4

instance : (incl : C ⥤ _).Faithful where

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