vComp

Mathlib.CategoryTheory.CatCommSq

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

Lean4

/-- Vertical composition of 2-commutative squares -/
@[simps!]
def vComp (L₁ : C₁ ⥤ C₂) (L₂ : C₂ ⥤ C₃) (H₁ : C₁ ⥤ C₄) (H₂ : C₂ ⥤ C₅) (H₃ : C₃ ⥤ C₆) (R₁ : C₄ ⥤ C₅) (R₂ : C₅ ⥤ C₆)
    [CatCommSq H₁ L₁ R₁ H₂] [CatCommSq H₂ L₂ R₂ H₃] : CatCommSq H₁ (L₁ ⋙ L₂) (R₁ ⋙ R₂) H₃ where
  iso :=
    (associator _ _ _).symm ≪≫
      isoWhiskerRight (iso H₁ L₁ R₁ H₂) R₂ ≪≫
        associator _ _ _ ≪≫ isoWhiskerLeft L₁ (iso H₂ L₂ R₂ H₃) ≪≫ (associator _ _ _).symm

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

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

Разделы

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

Аффилиация

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