faithful_linearCoyoneda

Mathlib.CategoryTheory.Linear.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.faithful_linearCoyoneda

English

The linear Coyoneda construction is faithful.

Русский

Линейная Coyoneda-конструкция верна.

LaTeX

$$$\\text{linearCoyoneda}_R(C)\\text{ is faithful}$$$

Lean4

instance faithful_linearCoyoneda : (linearCoyoneda R C).Faithful :=
  Functor.Faithful.of_comp_eq (whiskering_linearCoyoneda R C)

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

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

Разделы

Аффилиация

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