preservesColimitsOfShape_of_evaluation

English

Let F: D ⥤ K ⥤ C and J be a shape. If for every k ∈ K, PreservesColimitsOfShape J (F ⋙ ev_k), then PreservesColimitsOfShape J F.

Русский

Пусть F: D ⥤ K ⥤ C и J — форма. Если для каждого k ∈ K выполняется PreservesColimitsOfShape J (F ⋙ ev_k), тогда PreservesColimitsOfShape J F.

LaTeX

$$$\\forall k,\\ \\operatorname{PreservesColimitsOfShape}\\; J\\big( F \\;\\circ\\; ((\\mathrm{evaluation}\\; K\\; C).obj\\; k) \\big) \\Rightarrow \\operatorname{PreservesColimitsOfShape}\\; J\\; F.$$$

Lean4

/-- `F : D ⥤ K ⥤ C` preserves all colimits of shape `J` if it does for each `k : K`. -/
theorem preservesColimitsOfShape_of_evaluation (F : D ⥤ K ⥤ C) (J : Type*) [Category J]
    (_ : ∀ k : K, PreservesColimitsOfShape J (F ⋙ (evaluation K C).obj k)) : PreservesColimitsOfShape J F :=
  ⟨fun {G} => preservesColimit_of_evaluation F G fun _ => PreservesColimitsOfShape.preservesColimit⟩

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