freeReflNatTrans

Mathlib.CategoryTheory.Category.ReflQuiv

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

Lean4

/-- We will make use of the natural quotient map from the free category on the underlying
quiver of a refl quiver to the free category on the reflexive quiver. -/
def freeReflNatTrans : ReflQuiv.forgetToQuiv ⋙ Cat.free ⟶ freeRefl
    where
  app V := FreeRefl.quotientFunctor V
  naturality _ _ f := freeReflMap_naturality f

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

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

Разделы

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

Аффилиация

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