English
Let F be a functor F: J^op → C^op that has a limit. Then there exists a canonical isomorphism between the colimit of F.unop and the limit of F, and this isomorphism is compatible with the canonical shape maps: for every j ∈ J, the j-th colimit map composed with the isomorphism equals the unop of the j-th limit projection.
Русский
Пусть F: J^op → C^op имеет предел. Тогда существует каноническое изоморфизм колимита F.unop и предела F, и этот изоморфизм совместим с каноническими отображениями: для каждого j ∈ J композиция j-й инъекции колимита F.unop с изоморфизмом равна неопряжённому ограничению j-го предела.
LaTeX
$$$\\operatorname{colim}_{J}(F^{\\mathrm{unop}}) \\cong \\operatorname{lim}_{J}F \\quad \\land\\quad \\forall j:\\, J,\\quad \\operatorname{colimit.ι}F^{\\mathrm{unop}}(j) \\;\\;\\circledast\\;\\; (\\operatorname{colimitUnopIsoOpLimit}F)^{\\mathrm{hom}} = (\\operatorname{limit.π}F(\\operatorname{op} j)).\\mathrm{unop}$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_comp_colimitUnopIsoOpLimit_hom (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasLimit F] (j : J) :
colimit.ι F.unop j ≫ (colimitUnopIsoOpLimit F).hom = (limit.π F (op j)).unop := by simp [colimitUnopIsoOpLimit]
