mapCommMon

Mathlib.CategoryTheory.Monoidal.CommMon_

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Full.mapCommMon

English

If a functor F is full, then the induced map on commutative monoids is full.

Русский

Если функтор F является полным, то индуцированное отображение на комм-группы также полно.

LaTeX

$$$\\text{mapCommMon}$ is full whenever $F$ is full$$

Lean4

protected instance mapCommMon [F.Full] [F.Faithful] : F.mapCommMon.Full where map_surjective := F.mapMon.map_surjective

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

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

Разделы

Аффилиация

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