preservesLimitsOfShape_of_evaluation

English

If for every k in K, the evaluation preserves limits of shape J, then the whole functor F preserves limits of shape J.

Русский

Если для каждого k в K оценивание сохраняет пределы формы J, то всякий F сохраняет пределы формы J.

LaTeX

$$$\forall k,\ PreservesLimitsOfShape(J, (\mathrm{ev}_k)) \Rightarrow PreservesLimitsOfShape(J, F)$$$

Lean4

/-- `F : D ⥤ K ⥤ C` preserves limits of shape `J` if it does for each `k : K`. -/
theorem preservesLimitsOfShape_of_evaluation (F : D ⥤ K ⥤ C) (J : Type*) [Category J]
    (_ : ∀ k : K, PreservesLimitsOfShape J (F ⋙ (evaluation K C).obj k)) : PreservesLimitsOfShape J F :=
  ⟨fun {G} => preservesLimit_of_evaluation F G fun _ => PreservesLimitsOfShape.preservesLimit⟩

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