toCat_faithful

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#MonCat.toCat_faithful

English

The forgetful functor toCat is faithful, i.e., distinct morphisms are detected by the underlying functor.

Русский

Функтор toCat является верным, то есть различия морфизмов заметны на уровне функторов.

LaTeX

$$MonCat.toCat.Faithful$$

Lean4

instance toCat_faithful : toCat.Faithful where
  map_injective h := MonCat.hom_ext <| by rwa [toCat, (SingleObj.mapHom _ _).apply_eq_iff_eq] at h

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

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

Разделы

Аффилиация

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