instFaithfulForget

Mathlib.CategoryTheory.Monoidal.CommMon_

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

English

The forgetful functor forget from C to D is faithful; morphisms are determined by their images under forget.

Русский

Забывающий функтор из C в D верен; морфизмы определяются их образами через забывание.

LaTeX

$$$\\text{forget} : C \\to D \\text{Faithful}$$$

Lean4

instance : (forget C).Faithful where

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

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

Разделы

Аффилиация

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