Faithful

Mathlib.CategoryTheory.Category.ReflQuiv

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ReflQuiv.forget.Faithful

English

The forgetful functor forget from reflexive quivers to ordinary quivers is faithful.

Русский

Функтор забывания от рефлексивных квар к обычным квар-функтор лоялен (faithful).

LaTeX

$$$\forall f,g:\ x\to y,\; \text{forget}(f) = \text{forget}(g) \Rightarrow f = g.$$$

Lean4

instance Faithful : Functor.Faithful (forget) where map_injective := fun hyp ↦ forget_faithful _ _ hyp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru