English
Vertical pasting lemma for pullbacks: If the right-hand square is a pullback and the outer rectangle commutes, then the big left square is a pullback if and only if the left sub-square is a pullback.
Русский
Лемма вертикальной склейки для пуллбаков: если правый квадрат является пуллбаком и внешний прямоугольник коммутирует, то большой левый квадрат является пуллбаком тогда и только тогда, когда левый подпукольный квадрат является пуллбаком.
LaTeX
$$$ (s : IsPullback h_{21} \; v_{21} \; v_{22} \; h_{31}) \; (e : h_{11} \\gg v_{12} = v_{11} \\gg h_{21}) \\; \\Rightarrow \\\\ IsPullback(h_{11}, v_{11} \\gg v_{21}, v_{12} \\gg v_{22}, h_{31}) \\quad \\text{iff} \\quad IsPullback(h_{11}, v_{11}, v_{12}, h_{21}) $$$
Lean4
theorem paste_vert_iff {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₃₁)
(e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁) : IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ ↔ IsPullback h₁₁ v₁₁ v₁₂ h₂₁ :=
⟨fun h => h.of_bot e s, fun h => h.paste_vert s⟩
