map_unit_app

Mathlib.CategoryTheory.Monad.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monad.map_unit_app

English

For a monad T and any f: X → Y, T.map (T.map f) ≫ μ_Y = μ_X ≫ T.map f, i.e., μ is natural.

Русский

Для монадой T и любого f: X → Y выполняется: T.map(T.map f) ∘ μ_Y = μ_X ∘ T.map f.

LaTeX

$$$T.map(T.map f) \\\\circ T.\\\\mu_Y = T.\\\\mu_X \\\\circ T.map f.$$$

Lean4

theorem map_unit_app (T : Monad C) (X : C) [IsIso T.μ] : T.map (T.η.app X) = T.η.app (T.obj X) := by
  simp [← cancel_mono (T.μ.app _)]

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

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

Разделы

Аффилиация

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