π_comp_colimitUnopIsoOpLimit_inv

English

Let F: J^op → C^op be a diagram with a limit. Then the unop of the j-th projection, followed by the inverse of the canonical isomorphism, coincides with the j.unop-th injection into the colimit of F.unop.

Русский

Пусть F: J^op → C^op — диаграмма, имеющая предел. Тогда неопр вызванный проекция j в ограничении, затем обращение канонического изоморфизма, совпадает с j.unop-й встраиванием в колимит F.unop.

LaTeX

$$$\\big(\\operatorname{limit.π}F(j)\\big)^{\\mathrm{unop}} \\; \\circledast\\; (\\operatorname{colimitUnopIsoOpLimit}F)^{-1} = \\operatorname{colimit.ι}F.unop(j.unop)$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_colimitUnopIsoOpLimit_inv (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasLimit F] (j : Jᵒᵖ) :
    (limit.π F j).unop ≫ (colimitUnopIsoOpLimit F).inv = colimit.ι F.unop j.unop := by simp [Iso.comp_inv_eq]

Похожие утверждения