faithful_ι

Mathlib.CategoryTheory.ObjectProperty.FullSubcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.faithful_ι

English

The inclusion ι of the P-full subcategory is faithful.

Русский

Включение ι полносвязной подкатегории P верно/показывает инъективность на гомоморфизмах.

LaTeX

$$$P.\iota.Faithful$$$

Lean4

instance faithful_ι : P.ι.Faithful :=
  P.fullyFaithfulι.faithful

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

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

Разделы

Аффилиация

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