app

Mathlib.CategoryTheory.Category.ReflQuiv

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ReflQuiv.adj.unit.app

Lean4

/-- The unit components are defined as the composite of the corresponding unit component for the
adjunction between categories and quivers with the map underlying the quotient functor. -/
@[simps! toPrefunctor obj map]
def app (V : Type u) [ReflQuiver V] : V ⥤rq forget.obj (Cat.freeRefl.obj (ReflQuiv.of V))
    where
  toPrefunctor := Paths.of V ⋙q (Cat.FreeRefl.quotientFunctor V).toPrefunctor
  map_id := fun _ => Quotient.sound _ ⟨⟩

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

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

Разделы

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

Аффилиация

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