English
Horizontal pasting lemma for pullbacks: If the bottom-right square is a pullback and the horizontal composite commutes, then the larger right-hand square is a pullback iff the top-left square is a pullback.
Русский
Лемма горизонтальной склейки для пуллбаков: если нижнег-правый квадрат является пуллбаком и горизонтальная композиция коммутирует, то больший правый квадрат является пуллбаком тогда и только тогда, когда верхний левый квадрат также является пуллбаком.
LaTeX
$$$ (s : IsPullback h_{12} \; v_{12} \; v_{13} \; h_{22}) \; (e : h_{11} \\gg v_{12} = v_{11} \\gg h_{21}) \\; \\Rightarrow \\\\ IsPullback(h_{11} \\gg h_{12}, v_{11}, v_{13}, h_{22} \\gg h_{22}) \\quad \\text{iff} \\quad IsPullback(h_{11}, v_{11}, v_{12}, h_{21}) $$$
Lean4
theorem paste_horiz_iff {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₂₃} (s : IsPullback h₁₂ v₁₂ v₁₃ h₂₂)
(e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁) : IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ IsPullback h₁₁ v₁₁ v₁₂ h₂₁ :=
⟨fun h => h.of_right e s, fun h => h.paste_horiz s⟩
