diag_δ — Mathlib

Русский

Для любой категории C с мономодульной структурой компонент μ моноидальной структуры диагонального функторa diag C является тождественным; т.е. ассоциативный морфизм равен единице для диагонального вложения.

LaTeX

$$$\\mu(\\operatorname{diag} C)_{X,Y} = \\mathrm{id}$$$

Lean4

@[simp]
theorem diag_δ (X Y : C) : δ (diag C) X Y = 𝟙 _ :=
  rfl

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