graphFunctor

Mathlib.CategoryTheory.Category.RelCat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.RelCat.graphFunctor

Lean4

/-- The essentially surjective faithful embedding
from the category of types and functions into the category of types and relations. -/
@[simps obj map_rel]
def graphFunctor : Type u ⥤ RelCat.{u} where
  obj X := X
  map f := .ofRel f.graph

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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