map_one

Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_

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

English

For a monoidal functor F, F.map preserves the multiplication of arrows: F.map (f * g) = F.map f * F.map g.

Русский

Для мономодульной функторной F отображение F сохраняет умножение морфизмов: F.map (f * g) = F.map f * F.map g.

LaTeX

$$$F.map(f * g) = F.map f * F.map g$$$

Lean4

@[simp]
protected theorem map_one : F.map (1 : X ⟶ M) = 1 := by simp [Hom.one_def]

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

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

Разделы

Аффилиация

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