English
If a square h is a CommSq and i: P ≅ pushout f g is an isomorphism satisfying w1,w2, then IsPushout f g inl inr.
Русский
Если CommSq согласован и есть изоморфизм P ≅ pushout f g удовлетворяющий условиям w1, w2, тогда IsPushout f g inl inr.
LaTeX
$$$IsPushout f g inl inr$$$
Lean4
theorem of_iso (h : IsPushout f g inl inr) {Z' X' Y' P' : C} {f' : Z' ⟶ X'} {g' : Z' ⟶ Y'} {inl' : X' ⟶ P'}
{inr' : Y' ⟶ P'} (e₁ : Z ≅ Z') (e₂ : X ≅ X') (e₃ : Y ≅ Y') (e₄ : P ≅ P') (commf : f ≫ e₂.hom = e₁.hom ≫ f')
(commg : g ≫ e₃.hom = e₁.hom ≫ g') (comminl : inl ≫ e₄.hom = e₂.hom ≫ inl')
(comminr : inr ≫ e₄.hom = e₃.hom ≫ inr') : IsPushout f' g' inl' inr'
where
w := by rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl, ← reassoc_of% commg, ← comminr, h.w_assoc]
isColimit' :=
⟨(IsColimit.precomposeHomEquiv (spanExt e₁ e₂ e₃ commf.symm commg.symm) _).1
(IsColimit.ofIsoColimit h.isColimit (PushoutCocone.ext e₄ comminl comminr))⟩
