Lean4
/-- If a cocone with values in `ShortComplex C` is such that it becomes colimit
when we apply the three projections `ShortComplex C ⥤ C`, then it is colimit. -/
def isColimitOfIsColimitπ (c : Cocone F) (h₁ : IsColimit (π₁.mapCocone c)) (h₂ : IsColimit (π₂.mapCocone c))
(h₃ : IsColimit (π₃.mapCocone c)) : IsColimit c
where
desc
s :=
{ τ₁ := h₁.desc (π₁.mapCocone s)
τ₂ := h₂.desc (π₂.mapCocone s)
τ₃ := h₃.desc (π₃.mapCocone s)
comm₁₂ :=
h₁.hom_ext
(fun j => by
have eq₁ := h₁.fac (π₁.mapCocone s)
have eq₂ := h₂.fac (π₂.mapCocone s)
have eq₁₂ := fun j => (c.ι.app j).comm₁₂
have eq₁₂' := fun j => (s.ι.app j).comm₁₂
dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂])
comm₂₃ :=
h₂.hom_ext
(fun j => by
have eq₂ := h₂.fac (π₂.mapCocone s)
have eq₃ := h₃.fac (π₃.mapCocone s)
have eq₂₃ := fun j => (c.ι.app j).comm₂₃
have eq₂₃' := fun j => (s.ι.app j).comm₂₃
dsimp at eq₂ eq₃ eq₂₃ eq₂₃' ⊢
rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]) }
fac s
j := by
ext
· apply IsColimit.fac h₁
· apply IsColimit.fac h₂
· apply IsColimit.fac h₃
uniq s m
hm := by
ext
· exact h₁.uniq (π₁.mapCocone s) _ (fun j => π₁.congr_map (hm j))
· exact h₂.uniq (π₂.mapCocone s) _ (fun j => π₂.congr_map (hm j))
· exact h₃.uniq (π₃.mapCocone s) _ (fun j => π₃.congr_map (hm j))
