preservesLimit_of_preserves_limit_cone

English

If h is an IsLimit cone t and hF is IsLimit (F.mapCone t), then F preserves the limit for K; i.e., preserves is witnessed by h and hF.

Русский

Если h является предел-конусом t и hF является предел-конусом F.mapCone t, тогда F сохраняет предел для K.

LaTeX

$$$$\text{IsLimit}(t) \wedge \text{IsLimit}(F\mapsto t) \Rightarrow \mathrm{PreservesLimit}(K,F).$$$$

Lean4

/-- If F preserves one limit cone for the diagram K,
  then it preserves any limit cone for K. -/
theorem preservesLimit_of_preserves_limit_cone {F : C ⥤ D} {t : Cone K} (h : IsLimit t) (hF : IsLimit (F.mapCone t)) :
    PreservesLimit K F where preserves h' := ⟨IsLimit.ofIsoLimit hF (Functor.mapIso _ (IsLimit.uniqueUpToIso h h'))⟩

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