English
Let F: J^op → C^op be a diagram in the opposite category with a colimit. Then the inverse of the unop-isomorphism interacts with the projection π as (limitUnopIsoUnopColimit F).inv ≫ limit.π F.unop j = (colimit.ι F (op j)).unop for every j in J.
Русский
Пусть F: J^op → C^op — диаграмма в противоположной категории, у которой существует колимит. Тогда обратное отображение слева (обратное к унифицированному изоморфизму) совместимо с проекцией: (limitUnopIsoUnopColimit F).inv ≫ limit.π F.unop j = (colimit.ι F (op j)).unop для каждого j.
LaTeX
$$$$\\big(\\text{limitUnopIsoUnopColimit } F\\big)^{-1} \\; \\circ \\; \\big(\\text{limit.π } F.unop \\, j\\big) = (\\text{colimit.ι } F\\ (\\text{op } j)).^{unop}.$$$$
Lean4
@[reassoc (attr := simp)]
theorem limitUnopIsoUnopColimit_inv_comp_π (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasColimit F] (j : J) :
(limitUnopIsoUnopColimit F).inv ≫ limit.π F.unop j = (colimit.ι F (op j)).unop := by simp [limitUnopIsoUnopColimit]
