faithful

Mathlib.CategoryTheory.InducedCategory

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

English

The induced functor induced by F is faithful.

Русский

Индуцированный функтор, порожденный F, сохраняет различимость морфизмов (верен).

LaTeX

$$$\\operatorname{Faithful}(\\operatorname{inducedFunctor}(F))$$$

Lean4

instance faithful : (inducedFunctor F).Faithful :=
  (fullyFaithfulInducedFunctor F).faithful

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

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

Разделы

Аффилиация

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