commaMapEquivalenceUnitIso

Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

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

Lean4

/-- The unit establishing the equivalence `StructuredArrow.commaMapEquivalence`. -/
@[simps!]
def commaMapEquivalenceUnitIso [IsIso β] (X : Comma L' R') :
    𝟭 (StructuredArrow X (Comma.map α β)) ≅ commaMapEquivalenceFunctor α β X ⋙ commaMapEquivalenceInverse α β X :=
  NatIso.ofComponents (fun _ => isoMk (Iso.refl _))

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

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

Разделы

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

Аффилиация

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