π

Mathlib.CategoryTheory.Elements

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CategoryOfElements.π

Lean4

/-- The functor out of the category of elements which forgets the element. -/
@[simps]
def π : F.Elements ⥤ C where
  obj X := X.1
  map f := f.val

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

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

Разделы

Аффилиация

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