limitOpIsoOpColimit — Mathlib

English

Definition: limit_op_iso_op_colimit is the isomorphism between limit F.op and op (colimit F).

Русский

Определение: limitOpIsoOpColimit — изоморфизм между пределом F.op и противоположностью колимита F.

LaTeX

$$$$ \\operatorname{limitOpIsoOpColimit}(F) : \\operatorname{limit}(F^{\\mathrm{op}}) \\cong \\mathrm{op}(\\operatorname{colim} F) $$$$

Lean4

/-- The limit of `F.op` is the opposite of `colimit F`. -/
def limitOpIsoOpColimit (F : J ⥤ C) [HasColimit F] : limit F.op ≅ op (colimit F) :=
  limit.isoLimitCone ⟨_, (colimit.isColimit _).op⟩

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