English
Let f,g be morphisms between Ind-object presentations P1 and P2 with A,B as appropriate functors. Then g equals the image of a canonical cocone under the colimit map: g = IsColimit.map (isColimit₁ f g P₁ P₂) (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ψ f g P₁ P₂) yoneda).
Русский
Пусть f,g : A ⟶ B; тогда g равен отображению из колимита, полученному из канонического кокониа через IsColimit.map: g = IsColimit.map (isColimit₁ f g P₁ P₂) (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ψ f g P₁ P₂) yoneda).
LaTeX
$$$g = \mathrm{IsColimit.map} (\mathrm{isColimit}_1 f g P_1 P_2)\; (\mathrm{Cocone.mk} B (\iota_2 f g P_1 P_2))\; (\mathrm{whiskerRight} (\psi f g P_1 P_2) \mathrm{yoneda})$$$
Lean4
theorem hg :
g = IsColimit.map (isColimit₁ f g P₁ P₂) (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ψ f g P₁ P₂) yoneda) :=
by
refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
rw [IsColimit.ι_map]
simpa using i.hom.2.w.symm
