costructuredArrowIso

Mathlib.CategoryTheory.Comma.Presheaf.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.OverPresheafAux.OverArrows.costructuredArrowIso

Lean4

/-- If `η` is also `yoneda`-costructured, then `OverArrows η s` is just morphisms of costructured
arrows. -/
def costructuredArrowIso (s t : CostructuredArrow yoneda A) : OverArrows s.hom t.hom ≅ t ⟶ s
    where
  hom p := CostructuredArrow.homMk p.val (by simp)
  inv f := yonedaArrow f.left f.w

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

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

Разделы

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

Аффилиация

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