hComp

Mathlib.CategoryTheory.CatCommSq

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

Lean4

/-- Horizontal composition of 2-commutative squares -/
@[simps!]
def hComp (T₁ : C₁ ⥤ C₂) (T₂ : C₂ ⥤ C₃) (V₁ : C₁ ⥤ C₄) (V₂ : C₂ ⥤ C₅) (V₃ : C₃ ⥤ C₆) (B₁ : C₄ ⥤ C₅) (B₂ : C₅ ⥤ C₆)
    [CatCommSq T₁ V₁ V₂ B₁] [CatCommSq T₂ V₂ V₃ B₂] : CatCommSq (T₁ ⋙ T₂) V₁ V₃ (B₁ ⋙ B₂) where
  iso :=
    associator _ _ _ ≪≫
      isoWhiskerLeft T₁ (iso T₂ V₂ V₃ B₂) ≪≫
        (associator _ _ _).symm ≪≫ isoWhiskerRight (iso T₁ V₁ V₂ B₁) B₂ ≪≫ associator _ _ _

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

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

Разделы

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

Аффилиация

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