English
Vertical paste of two pullbacks yields a larger pullback: combining h11,h21 and v11,v21 yields a pullback for h11 and h21.
Русский
Вертикальная конкатенация двух вытягиваемых квадратов даёт новый вытягиваемый квадрат.
LaTeX
$$$IsPullback(h_{11}, v_{11} \circ v_{21}, v_{12} \circ v_{22}, h_{31})$$$
Lean4
/-- 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₃₂
```
-/
theorem paste_vert {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₃₂} (s : IsPullback h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁) : IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ :=
of_isLimit (pasteHorizIsPullback rfl t.isLimit s.isLimit)
