map_μ_δ

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Monoidal.map_μ_δ

English

The composite of μ, after mapping, with δ yields identity on the mapped tensor.

Русский

Состав μ после отображения и δ дает тождество на отображенной тензоре.

LaTeX

$$$G.map(\\mu F X Y) \\circ G.map(\\delta F X Y) = \\mathrm{Id}$$$

Lean4

@[reassoc (attr := simp)]
theorem map_μ_δ (G : D ⥤ C') (X Y : C) : G.map (μ F X Y) ≫ G.map (δ F X Y) = 𝟙 _ :=
  (μIso F X Y).map_hom_inv_id G

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

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

Разделы

Аффилиация

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