faithful_linearYoneda

Mathlib.CategoryTheory.Linear.Yoneda

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

English

The linear Yoneda functor is faithful; its forgetful whiskering is faithful as a functor to ModuleCat.

Русский

Линейный Yoneda-функтор верен; забывающий whiskering верен как функтор в ModuleCat.

LaTeX

$$$\\text{linearYoneda}_R(C) \\text{ is faithful}.$$$

Lean4

instance faithful_linearYoneda : (linearYoneda R C).Faithful :=
  Functor.Faithful.of_comp_eq (whiskering_linearYoneda R C)

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

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

Разделы

Аффилиация

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