coyoneda_faithful

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Coyoneda.coyoneda_faithful

English

The Coyoneda functor is faithful.

Русский

Coyoneda-функтор верен.

LaTeX

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

Lean4

instance coyoneda_faithful : (coyoneda : Cᵒᵖ ⥤ C ⥤ Type v₁).Faithful :=
  fullyFaithful.faithful

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

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

Разделы

Аффилиация

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