hasLimit_of_hasLimit_forget₂ — Mathlib

English

TopModuleCat R has limits of shape J whenever ModuleCat R has them.

Русский

TopModuleCat R имеет пределы формы J, когда у ModuleCat R они существуют.

LaTeX

$$$\\text{HasLimitsOfShape } J (TopModuleCat\\,R) \\Longleftarrow \\text{HasLimitsOfShape } J (ModuleCat\\,R).$$$

Lean4

instance hasLimit_of_hasLimit_forget₂ {J : Type*} [Category J] {F : J ⥤ TopModuleCat.{v} R}
    [HasLimit (F ⋙ forget₂ _ (ModuleCat.{v} R))] : HasLimit F :=
  ⟨_, isLimit (limit.isLimit _)⟩

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