toArrow

Mathlib.AlgebraicTopology.SimplicialObject.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CosimplicialObject.Augmented.toArrow

Lean4

/-- The functor from augmented objects to arrows. -/
@[simps!]
def toArrow : Augmented C ⥤ Arrow C
    where
  obj
    X :=
    { left := point.obj X
      right := (drop.obj X) ^⦋0⦌
      hom := X.hom.app _ }
  map
    η :=
    { left := point.map η
      right := (drop.map η).app _
      w := by
        dsimp
        rw [← NatTrans.comp_app]
        erw [← η.w]
        rfl }

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

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

Разделы

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

Аффилиация

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