limitRightOpIsoOpColimit_inv_comp_π

English

Inverse of the limit-right-op–colimit iso composed with the projection equals the opposite of the colimit injection.

Русский

Обратная к предел-правыйOp-колимитного изоморфизма, скомпозированная с проекцией, равна противоположности инъекции колимита.

LaTeX

$$$$ (\\text{limitRightOpIsoOpColimit}(F)).inv \\circ \\text{limit.\\pi} F^{rightOp} j = (\\text{colimit.\\ι} F (op\\, j)).op $$$$

Lean4

@[reassoc (attr := simp)]
theorem limitRightOpIsoOpColimit_inv_comp_π (F : Jᵒᵖ ⥤ C) [HasColimit F] (j : J) :
    (limitRightOpIsoOpColimit F).inv ≫ limit.π F.rightOp j = (colimit.ι F (op j)).op := by
  simp [limitRightOpIsoOpColimit]

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