English
If s is a pushout of h11 by v11 and v12 with h21, and t is a pushout of h11 by v11 and v12, then the bottom square is pushout.
Русский
Если верхний квадрат является пушаутом, то нижний квадрат также является пушаутом при задании соответствующих композиционных условий.
LaTeX
$$$\operatorname{IsPushout}(h_{21}, v_{21}, v_{22}, h_{31})$$$
Lean4
/-- Given a pushout square assembled from a pushout square on the top and
a commuting square on the bottom, the bottom square is a pushout 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 of_top {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 : IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁)
(p : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : IsPushout h₂₁ v₂₁ v₂₂ h₃₁ :=
of_isColimit <| rightSquareIsPushout (PushoutCocone.mk _ _ p) (cocone_inr _) t.isColimit s.isColimit
