mu_naturality

Mathlib.CategoryTheory.Monad.Basic

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

English

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

Русский

Для монадой 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

@[reassoc]
theorem mu_naturality (T : Monad C) ⦃X Y : C⦄ (f : X ⟶ Y) : T.map (T.map f) ≫ T.μ.app Y = T.μ.app X ≫ T.map f :=
  T.μ.naturality _

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

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

Разделы

Аффилиация

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