Theorems · Theorem · category theory

CategoryTheory.IsPullback.paste_vert

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁ →
      CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
        (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁

Paste two pullback squares "vertically" to obtain another pullback square. The objects in the statement fit into the following diagram: `` X₁₁ - h₁₁ -> X₁₂ | | v₁₁ v₁₂ ↓ ↓ X₂₁ - h₂₁ -> X₂₂ | | v₂₁ v₂₂ ↓ ↓ X₃₁ - h₃₁ -> X₃₂ ``

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Cited by

19 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category