Lean4
/-- Provided that `L` preserves the appropriate colimit, then the cocone in `coconeOfPreserves` is
a colimit. -/
noncomputable def coconeOfPreservesIsColimit [PreservesColimit (F ⋙ fst L R) L] {c₁ : Cocone (F ⋙ fst L R)}
(t₁ : IsColimit c₁) {c₂ : Cocone (F ⋙ snd L R)} (t₂ : IsColimit c₂) : IsColimit (coconeOfPreserves F t₁ c₂)
where
desc
s :=
{ left := t₁.desc ((fst L R).mapCocone s)
right := t₂.desc ((snd L R).mapCocone s)
w :=
(isColimitOfPreserves L t₁).hom_ext fun j =>
by
rw [coconeOfPreserves_pt_hom, (isColimitOfPreserves L t₁).fac_assoc, colimitAuxiliaryCocone_ι_app, assoc, ←
R.map_comp, t₂.fac, L.mapCocone_ι_app, ← L.map_comp_assoc, t₁.fac]
exact (s.ι.app j).w }
uniq s m
w := by
apply CommaMorphism.ext
· exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w])
· exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w])
