Lean4
/-- Given
X₁ - f₁ -> X₂ - f₂ -> X₃
| | |
i₁ i₂ i₃
∨ ∨ ∨
Y₁ - g₁ -> Y₂ - g₂ -> Y₃
Then the right square is a pushout if the left square and the big square are.
-/
def rightSquareIsPushout (H : IsColimit t₁) (H' : IsColimit (t₁.pasteHoriz t₂ hi₂)) : IsColimit t₂ :=
by
apply PushoutCocone.isColimitAux'
intro s
obtain ⟨l, hl, hl'⟩ :=
PushoutCocone.IsColimit.desc' H' (g₁ ≫ s.inl) s.inr
(by rw [reassoc_of% t₁.condition, ← hi₂, s.condition, Category.assoc])
refine
⟨l, ?_, hl', ?_⟩
-- To check that `l` is compatible with the projections, we use the universal property of `t₁`
· simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hl hl'
apply PushoutCocone.IsColimit.hom_ext H hl
rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']
-- Uniqueness of the lift follows from the universal property of the big square
· intro m hm₁ hm₂
apply PushoutCocone.IsColimit.hom_ext H'
· simpa [← hm₁] using hl.symm
· simpa [← hm₂] using hl'.symm
