diag

Mathlib.CategoryTheory.Products.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.diag

English

The diagonal functor diag: C ⥤ C × C sends X to (X,X) and f to (f,f).

Русский

Диагональный функтор diag: C ⥤ C × C отправляет X в (X,X) и f в (f,f).

LaTeX

$$$\\mathrm{diag}: C \\to C \\times C$, with $\\mathrm{diag}(X)=(X,X)$ and $\\mathrm{diag}(f)=(f,f)$.$$

Lean4

/-- The diagonal functor. -/
@[simps! obj map]
def diag : C ⥤ C × C :=
  (𝟭 C).prod' (𝟭 C)

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

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

Разделы

Аффилиация

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