app

Mathlib.CategoryTheory.Category.ReflQuiv

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

Lean4

/-- The counit components are defined using the universal property of the quotient
from the corresponding counit component for the adjunction between categories and quivers. -/
@[simps!]
def app (C : Type u) [Category.{max u v} C] : Cat.freeRefl.obj (ReflQuiv.of C) ⥤ C :=
  Quotient.lift Cat.FreeReflRel (pathComposition C)
    (by
      intro x y f g rel
      cases rel
      unfold pathComposition
      simp only [composePath_toPath]
      rfl)

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

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

Разделы

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

Аффилиация

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