instHasColimitCompOfPreservesColimit

English

If HasColimit K and PreservesColimit K F, then HasColimit K ⋙ F; i.e., colimits are preserved through composition.

Русский

Если у K есть колимит и PreservesColimit K F, то HasColimit K ⋙ F; то есть колимиты сохраняются через композицию.

LaTeX

$$$$\text{HasColimit}(K) \land \mathrm{PreservesColimit}(K,F) \Rightarrow \mathrm{HasColimit}(K\cdot F).$$$$

Lean4

instance [HasColimit K] {F : C ⥤ D} [PreservesColimit K F] : HasColimit (K ⋙ F) where
  exists_colimit := ⟨_, isColimitOfPreserves F (colimit.isColimit K)⟩

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