commaMapEquivalence

Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

URI: https://scilib.ai/kg/mathlib#CategoryTheory.StructuredArrow.commaMapEquivalence

Lean4

/-- The structured arrow category on the functor `Comma.map α β`, with `β` a natural isomorphism,
is equivalent to a comma category on two instances of `StructuredArrow.map₂`. -/
def commaMapEquivalence [IsIso β] (X : Comma L' R') :
    StructuredArrow X (Comma.map α β) ≌ Comma (map₂ (𝟙 _) α) (map₂ X.hom (inv β))
    where
  functor := commaMapEquivalenceFunctor α β X
  inverse := commaMapEquivalenceInverse α β X
  unitIso := commaMapEquivalenceUnitIso α β X
  counitIso := commaMapEquivalenceCounitIso α β X

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

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

Разделы

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

Аффилиация

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