English
Given a binary cofan c : BinaryCofan X Y with IsColimit, and an initial object I, the induced maps to I witness a pushout: IsPushout (to I) (to I) c.inr c.inl.
Русский
Пусть c — бинарный кофан X, Y с тем, что он изолирует IsColimit, и I является начальным объектом; полученные отображения образуют пуш-аут: IsPushout (to I) (to I) c.inr c.inl.
LaTeX
$$$ \\operatorname{IsPushout}(\\text{to}_I, \\text{to}_I, c.inr, c.inl) $$$
Lean4
theorem of_isColimit_binaryCofan_of_isInitial {X Y : C} {c : BinaryCofan X Y} (hc : IsColimit c) {I : C}
(hI : IsInitial I) : IsPushout (hI.to _) (hI.to _) c.inr c.inl
where
w := hI.hom_ext _ _
isColimit' :=
⟨PushoutCocone.IsColimit.mk _ (fun s ↦ hc.desc (BinaryCofan.mk s.inr s.inl))
(fun s ↦ hc.fac (BinaryCofan.mk s.inr s.inl) ⟨.right⟩) (fun s ↦ hc.fac (BinaryCofan.mk s.inr s.inl) ⟨.left⟩)
(fun s m h₁ h₂ ↦ by
apply BinaryCofan.IsColimit.hom_ext hc
· rw [h₂, hc.fac (BinaryCofan.mk s.inr s.inl) ⟨.left⟩]
rfl
· rw [h₁, hc.fac (BinaryCofan.mk s.inr s.inl) ⟨.right⟩]
rfl)⟩
