structuredArrowEquiv

Mathlib.CategoryTheory.Join.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Join.structuredArrowEquiv

Lean4

/-- The category of `Join.inclRight C D`-structured arrows with source `left c` is equivalent to
`D`. -/
def structuredArrowEquiv (c : C) : StructuredArrow (left c) (inclRight C D) ≌ D
    where
  functor := StructuredArrow.proj (left c) (inclRight C D)
  inverse :=
    { obj d := .mk (edge c d)
      map f := StructuredArrow.homMk f }
  unitIso := NatIso.ofComponents (fun _ ↦ StructuredArrow.isoMk (Iso.refl _))
  counitIso := NatIso.ofComponents (fun _ ↦ Iso.refl _)

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

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

Разделы

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

Аффилиация

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