instPreservesColimitπ₂ — Mathlib

English

For F : J ⥤ ShortComplex C with π₁, π₂, π₃ having colimits, F preserves the colimit π₂.

Русский

Для F: J ⥤ ShortComplex C, если существуют колимиты для π₁, π₂, π₃, F сохраняет колимит π₂.

LaTeX

$$$ \text{PreservesColimit } F \pi_2 $$$

Lean4

noncomputable instance : PreservesColimit F π₂ :=
  preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F) (isColimitπ₂MapCoconeColimitCocone F)

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