English
If `coconeOfCoconeUncurry Q c` is a colimit cocone, then `c` is a colimit cocone.
Русский
Если кокон coconeOfCoconeUncurry Q c является колимитным коконом, то и сам c является колимитным коконом.
LaTeX
$$$\text{IsColimit}(\text{coconeOfCoconeUncurry } Q c) \Rightarrow \text{IsColimit}(c).$$$
Lean4
/-- If `coconeOfCoconeUncurry Q c` is a colimit cocone then `c` is in fact a colimit
cocone. -/
def ofCoconeUncurry {D : DiagramOfCocones F} (Q : ∀ j, IsColimit (D.obj j)) {c : Cocone (uncurry.obj F)}
(P : IsColimit (coconeOfCoconeUncurry Q c)) : IsColimit c :=
-- These constructions are used in various fields of the proof so we abstract them here.
letI E (j : J) : (Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j) := NatIso.ofComponents (fun _ ↦ Iso.refl _)
letI S (s : Cocone (uncurry.obj F)) : Cocone D.coconePoints :=
{ pt := s.pt
ι :=
{ app j := (Q j).desc <| (Cocones.precompose (E j).inv).obj <| s.whisker (Prod.sectR j K)
naturality {j j'} f := (Q j).hom_ext <| fun k ↦ by simpa [E] using s.ι.naturality ((Prod.sectL J k).map f) } }
{ desc s := P.desc (S s)
fac s
p := by
have h1 := (Q p.1).fac ((Cocones.precompose (E p.1).inv).obj <| s.whisker (Prod.sectR p.1 K)) p.2
simp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj, Cocones.precompose_obj_pt, Cocone.whisker_pt,
Functor.const_obj_obj, Cocones.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app,
NatIso.ofComponents_inv_app, Iso.refl_inv, whiskerLeft_app, Category.id_comp, E] at h1
have h2 := (P.fac (S s) p.1)
dsimp only [DiagramOfCocones.coconePoints_obj, Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj, NatTrans.id_app,
Functor.const_obj_obj, DiagramOfCocones.coconePoints_map, Functor.const_obj_map, id_eq,
Cocones.precompose_obj_pt, Cocone.whisker_pt, Cocones.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app,
NatIso.ofComponents_inv_app, Iso.refl_inv, whiskerLeft_app, Prod.sectL_obj, Prod.sectL_map, eq_mp_eq_cast,
eq_mpr_eq_cast, coconeOfCoconeUncurry_pt, coconeOfCoconeUncurry_ι_app, S, E] at h2 ⊢
simp [← h1, ← h2]
uniq s f hf := P.uniq (s := S s) _ <| fun j ↦ (Q j).hom_ext <| fun k ↦ by simpa [S, E] using hf (j, k) }
