vInv

Mathlib.CategoryTheory.CatCommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatCommSq.vInv

Lean4

/-- Vertical inverse of a 2-commutative square -/
@[simps!]
def vInv (_ : CatCommSq T L.functor R.functor B) : CatCommSq B L.inverse R.inverse T where
  iso :=
    isoWhiskerRight
        (B.leftUnitor.symm ≪≫
          isoWhiskerRight L.counitIso.symm B ≪≫
            associator _ _ _ ≪≫ isoWhiskerLeft L.inverse (iso T L.functor R.functor B).symm)
        R.inverse ≪≫
      associator _ _ _ ≪≫
        isoWhiskerLeft _ (associator _ _ _) ≪≫
          (associator _ _ _).symm ≪≫ isoWhiskerLeft _ R.unitIso.symm ≪≫ rightUnitor _

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

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

Разделы

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

Аффилиация

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