isLimitCoyonedaEquiv — Mathlib

English

A cone is limit iff its Yoneda-mapped version is limit for every X in Cᵒᵖ.

Русский

Конус есть предел тогда и только тогда, когда его отображение через Yoneda является пределом для каждого X в Cᵒᵖ.

LaTeX

$$$\\forall c:\\mathrm{Cone} F,\\; \\mathrm{IsLimit}(c) \\iff \\forall X:\\, C^{op},\\; \\mathrm{IsLimit}((\\mathrm{coyoneda.obj} X).mapCone c)$$$

Lean4

/-- A cone is limit iff it is so after the application of `coyoneda.obj X` for all `X : Cᵒᵖ`. -/
noncomputable def isLimitCoyonedaEquiv {F : J ⥤ C} (c : Cone F) :
    IsLimit c ≃ ∀ (X : Cᵒᵖ), IsLimit ((coyoneda.obj X).mapCone c)
    where
  toFun h _ := isLimitOfPreserves _ h
  invFun h := coyonedaJointlyReflectsLimits _ _ h
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := by ext; apply Subsingleton.elim

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