pullbackAssocSymmIsPullback

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.pullbackAssocSymmIsPullback

Lean4

/-- `X₁ ×[Y₁] (X₂ ×[Y₂] X₃)` is the pullback `(X₁ ×[Y₁] X₂) ×[Y₂] X₃`. -/
def pullbackAssocSymmIsPullback [HasPullback f₁ (g₃ ≫ f₂)] :
    IsLimit
      (PullbackCone.mk l₁' (l₂' ≫ g₄)
        (show l₁' ≫ g₂ ≫ f₃ = (l₂' ≫ g₄) ≫ f₄ by
          rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition])) :=
  by
  simpa [PullbackCone.pasteHoriz] using
    pasteHorizIsPullback rfl (pullbackIsPullback f₃ f₄) (pullbackPullbackRightIsPullback _ _ _ _)

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

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

Разделы

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

Аффилиация

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