instFaithfulForget

Mathlib.CategoryTheory.Action.Basic

URI: https://scilib.ai/kg/mathlib#Action.instFaithfulForget

English

The forgetful functor forget is faithful; it reflects distinct morphisms in Action(V,G) to distinct underlying morphisms in V.

Русский

Функтор forget внимателен: различные морфизмы сохраняются как разные отображения в V.

LaTeX

$$forget: \\mathrm{Action}(V,G) \\to V is faithful.$$

Lean4

instance : (forget V G).Faithful where map_injective w := Hom.ext w

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

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

Разделы

Аффилиация

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