English
Let F: J^op → C^op be a diagram with a colimit. Then the hom component of the unop iso composed with the colimit injections recovers the standard π-map: (limitUnopIsoUnopColimit F).hom ≫ (colimit.ι F j).unop = limit.π F.unop j.unop for every j in J^op.
Русский
Пусть F: J^op → C^op — диаграмма с колимитом. Тогда гом-компонента унифицированного изоморфизма с.unop, композиция с инъекциями колимита даёт π-морфизм: (limitUnopIsoUnopColimit F).hom ≫ (colimit.ι F j).unop = limit.π F.unop j.unop для каждого j ∈ J^op.
LaTeX
$$$$\\left(\\text{limitUnopIsoUnopColimit } F\\right).hom \\\\circ \\\\left(\\text{colimit.ι } F\\ j \\\\right)^{unop} = \\text{limit.π } F.unop \\, j^{unop}.$$$$
Lean4
@[reassoc (attr := simp)]
theorem limitUnopIsoUnopColimit_hom_comp_ι (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasColimit F] (j : Jᵒᵖ) :
(limitUnopIsoUnopColimit F).hom ≫ (colimit.ι F j).unop = limit.π F.unop j.unop := by simp [← Iso.eq_inv_comp]
