English
Let t be a colimit cocone for F. The natural bijection h.homEquiv between morphisms t.pt ⟶ W and natural transformations F ⇒ const_W is natural in W. In particular, for any g: W ⟶ W', h.homEquiv.symm (f ≫ (const J).map g) = h.homEquiv.symm f ≫ g.
Русский
Пусть t — колимитный кокон для F. Натуральное биекции между морфизмами t.pt ⟶ W и натуральными преобразованиями F ⇒ const_W сохраняют построение при смене целевого объекта W; в частности, для любого g: W ⟶ W' имеет место равенство h.homEquiv.symm (f ≫ (const J).map g) = h.homEquiv.symm f ≫ g.
LaTeX
$$$ h.homEquiv^{-1}\bigl(f \circ (\mathrm{const}_J).\mathrm{map} g\bigr) = h.homEquiv^{-1} f \circ g. $$$
Lean4
theorem homEquiv_symm_naturality (h : IsColimit t) {W W' : C} (f : F ⟶ (const J).obj W) (g : W ⟶ W') :
h.homEquiv.symm (f ≫ (Functor.const _).map g) = h.homEquiv.symm f ≫ g :=
h.homEquiv.injective (by aesop)
