faithful

Mathlib.CategoryTheory.Functor.FullyFaithful

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.FullyFaithful.faithful

English

A functor F is faithful if F.map is injective on hom-sets: equal images imply equal morphisms.

Русский

Функтор F верный, если отображение F.map инъективно на множествах морфизмов: равные образы означают равные морфизмы.

LaTeX

$$$\forall X,Y:\; \text{If } F.map(f)=F.map(g) \text{ then } f=g$$$

Lean4

theorem faithful : F.Faithful where map_injective := hF.map_injective

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

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

Разделы

Аффилиация

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