preservesFiniteLimits_of_evaluation

English

Let F: C ⥤ D ⥤ E. If for every d ∈ D, F ∘ evaluation_d preserves finite limits, then F itself preserves finite limits.

Русский

Пусть F: C ⥤ D ⥤ E. Если для каждого объекта d ∈ D отображение F ∘ evaluation_d сохраняет конечные пределы, тогда F сохраняет конечные пределы.

LaTeX

$$$\\operatorname{preservesFiniteLimits}\\left(F : C \\to D \\to E\\right) \\Rightarrow \\forall d, \\operatorname{preservesFiniteLimits}\\left(F \\circ (\\mathrm{evaluation}\\; D\\; E)_{\\!d}\\right)$$$

Lean4

/-- `F : C ⥤ D ⥤ E` preserves finite limits if it does for each `d : D`. -/
theorem preservesFiniteLimits_of_evaluation {D : Type*} [Category D] {E : Type*} [Category E] (F : C ⥤ D ⥤ E)
    (h : ∀ d : D, PreservesFiniteLimits (F ⋙ (evaluation D E).obj d)) : PreservesFiniteLimits F :=
  ⟨fun J _ _ => preservesLimitsOfShape_of_evaluation F J fun k => (h k).preservesFiniteLimits _⟩

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