English
A variant of the top-pushout where the top morphism is induced by a universal property of the top square.
Русский
Вариант вершины пушаута, когда верхняя стрелка получается по универсальному свойству верхнего квадрата.
LaTeX
$$$\operatorname{IsPushout}(h_{21}, v_{21}, v_{22}, h_{31})$ with a desc construction$$
Lean4
/-- Variant of `IsPushout.of_top` where `v₂₂` is induced from a morphism `v₁₃ : X₁₂ ⟶ X₃₂`, and
the universal property of the top 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₁₃ h₃₁)
(t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : IsPushout h₂₁ v₂₁ (t.desc v₁₃ (v₂₁ ≫ h₃₁) (by rw [s.w, Category.assoc])) h₃₁ :=
of_top ((t.inl_desc _ _ _).symm ▸ s) (t.inr_desc _ _ _) t
