π_comp_colimitRightOpIsoUnopLimit_inv

English

For F: J^op ⥤ C, HasLimit F, and j in J^op, the opposite of the limit map composed with the inverse of colimitRightOpIsoUnopLimit equals the opposite of the colimit map at j.unop.

Русский

Для F: J^op ⥤ C, имеющего предел, и j ∈ J^op, обобщение противоположности limit-map композиция с Inv(colimitRightOpIsoUnopLimit) даёт противоположное colimit.ι по j.unop.

LaTeX

$$$$ \\big(\\text{limit.π } F\\big)^{op} \\; \\circ \\big( \\text{colimitRightOpIsoUnopLimit } F \\big)^{-1} = \\text{colimit.ι } F.rightOp (op j)^{op}. $$$$

Lean4

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

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