English
For any cocone t of F, there exists a unique linear map from the colimit of F to t.pt that makes the obvious triangles commute; this is the induced map colimitDesc F t.
Русский
Для любой коконы F существует единственный линейный отображение от колимита F к точке t, которое делает треугольники часовки коммьютирующими; это отображение colimitDesc F t.
LaTeX
$$$\exists!\varphi: \operatorname{colim} F \to t.\mathrm{pt} \quad\text{such that}\quad \forall j,\ (\text{colimitCocone }F).ι._{\mathrm.app j} \;\varphi = t.\iota_j$$$
Lean4
/-- Given a cocone `t` of `F`, the induced monoid linear map from the colimit to the cocone point.
We already know that this is a morphism between additive groups. The only thing left to see is that
it is a linear map, i.e. preserves scalar multiplication.
-/
def colimitDesc (t : Cocone F) : colimit F ⟶ t.pt :=
let h := (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ _ _))
let f : colimit F →+ t.pt := (h.desc ((forget₂ _ _).mapCocone t)).hom
have hf {j : J} (x : F.obj j) : f (M.mk _ ⟨j, x⟩) = t.ι.app j x :=
congr_fun ((forget _).congr_map (h.fac ((forget₂ _ _).mapCocone t) j)) x
ofHom
{ f with
map_smul' := fun r x => by
obtain ⟨j, x, rfl⟩ := M.mk_surjective F x
simp [hf] }
