English
Let F: J^op → C be a diagram in a category C that has a colimit. Then for every j in J^op, the isomorphism limitRightOpIsoOpColimit F relates the colimit of F.op to the limit of F.rightOp in such a way that the op of the colimit injections corresponds to the right-op projection; explicitly, (limitRightOpIsoOpColimit F).hom ≫ (colimit.ι F j).op = limit.π F.rightOp j.unop.
Русский
Пусть F: J^op → C — диаграмма в категории C, для которой существует колимит. Тогда для каждого j ∈ J^op выполняется связь, устанавливаемая изоморфизмом limitRightOpIsoOpColimit F между ко-лимитом F.op и пределом F.rightOp: композиция гомоморфизма изоморфности с_OP-подобной инъекцией коллекта равна π-проекции предела; то есть (limitRightOpIsoOpColimit F).hom ≫ (colimit.ι F j).op = limit.π F.rightOp j.unop.
LaTeX
$$$$\\left(\\text{limitRightOpIsoOpColimit } F\\right).hom \\; \\circ \\; (\\text{colimit.ι } F\\, j)^{op} = \\text{limit.π } F.\\text{rightOp } j^{\\text{unop}}.$$$$
Lean4
@[reassoc (attr := simp)]
theorem limitRightOpIsoOpColimit_hom_comp_ι (F : Jᵒᵖ ⥤ C) [HasColimit F] (j : Jᵒᵖ) :
(limitRightOpIsoOpColimit F).hom ≫ (colimit.ι F j).op = limit.π F.rightOp j.unop := by simp [← Iso.eq_inv_comp]
