CatCenter

Mathlib.CategoryTheory.Center.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatCenter

Lean4

/-- The center of a category `C` is the type `End (𝟭 C)` of the endomorphisms
of the identify functor of `C`. -/
abbrev CatCenter :=
  End (𝟭 C)

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

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

Разделы

Аффилиация

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