delta_naturality

Mathlib.CategoryTheory.Monad.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comonad.delta_naturality

English

For a comonad G and f: X → Y, map f followed by δ_Y equals δ_X followed by map of map f.

Русский

Для ко́монда G и f: X → Y выполняется: map f ∘ δ_Y = δ_X ∘ map(map f).

LaTeX

$$$T.map f \\\\circ T.\\\\delta_{Y} = T.\\\\delta_{X} \\\\circ T.map(T.map f).$$$

Lean4

@[reassoc]
theorem delta_naturality (T : Comonad C) ⦃X Y : C⦄ (f : X ⟶ Y) : T.map f ≫ T.δ.app Y = T.δ.app X ≫ T.map (T.map f) :=
  T.δ.naturality _

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

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

Разделы

Аффилиация

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