limitOpIsoOpColimit_inv_comp_π — Mathlib

English

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

Русский

Обратная к предел-операция изоморфизма, умноженная на инъекцию противоположности колимита, дает противоположность инъекции.

LaTeX

$$$$ (\\operatorname{limitOpIsoOpColimit}(F))^{-1} \\circ \\operatorname{limit.\\pi} F^{op} = \\operatorname{colimit.\\iota} F $$$$

Lean4

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

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