pullbackAssocIsPullback

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

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

Lean4

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

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

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

Разделы

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

Аффилиация

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