instFaithfulFunctorOppositeTypeUliftYoneda

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ULiftYoneda.instFaithfulFunctorOppositeTypeUliftYoneda

English

The uliftYoneda construction yields a faithful functor.

Русский

Конструкция ULift Yoneda образует верный функтор.

LaTeX

$$The functor $\mathrm{uliftYoneda}$ is faithful.$$

Lean4

instance : (uliftYoneda.{w} (C := C)).Faithful :=
  (fullyFaithful C).faithful

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

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

Разделы

Аффилиация

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