English
If a bot square s and top square t are pullbacks, then the bottom square is a pullback.
Русский
Если верхний и нижний квадрат являются вытягиваемыми, то нижний левый квадрат тоже вытягивает.
LaTeX
$$$IsPullback(h_{11}, v_{11}, v_{12}, h_{21})\to IsPullback(h_{11}, v_{11}, v_{12}, h_{21})$$$
Lean4
/-- Given a pullback square assembled from a commuting square on the left and
a pullback square on the right, the left square is a 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₂₃
```
-/
theorem of_right {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₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂))
(p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁) (t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) : IsPullback h₁₁ v₁₁ v₁₂ h₂₁ :=
(of_bot s.flip p.symm t.flip).flip
