functorToDiscrete

Mathlib.CategoryTheory.ConnectedComponents

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ConnectedComponents.functorToDiscrete

Lean4

/-- Every function from connected components of a category gives a functor to discrete category -/
def functorToDiscrete (X : Type*) (f : ConnectedComponents J → X) : J ⥤ Discrete X
    where
  obj Y := Discrete.mk (f (Quotient.mk (Zigzag.setoid _) Y))
  map g := Discrete.eqToHom (congrArg f (Quotient.sound (Zigzag.of_hom g)))

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

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

Разделы

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

Аффилиация

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