connectedComponents

Mathlib.CategoryTheory.Category.Cat.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cat.connectedComponents

Lean4

/-- The connected components functor -/
def connectedComponents : Cat.{v, u} ⥤ Type u
    where
  obj C := ConnectedComponents C
  map F := Functor.mapConnectedComponents F
  map_id _ := funext fun x ↦ (Quotient.exists_rep x).elim (fun _ h ↦ by subst h; rfl)
  map_comp _ _ := funext fun x ↦ (Quotient.exists_rep x).elim (fun _ h => by subst h; rfl)

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

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

Разделы

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

Аффилиация

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