instFaithfulFullSubcategoryLift

Mathlib.CategoryTheory.ObjectProperty.FullSubcategory

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

English

If F is faithful, then the lifted object property P.lift F hF is faithful.

Русский

Если F верно сохраняет морфизмы, то P.lift F hF верно по морфизмам.

LaTeX

$$$[F.\text{Faithful}] \Rightarrow (P.\lift F hF).\Faithful$$$

Lean4

instance [F.Faithful] : (P.lift F hF).Faithful :=
  Functor.Faithful.of_comp_iso (P.liftCompιIso F hF)

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

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

Разделы

Аффилиация

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