Theorems · Theorem · category theory

CategoryTheory.IsPullback.paste_horiz

∀ {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₂₂} {h₂₂ : 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 (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
        (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)

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

Defined in

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

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category