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_1 $$$

Lean4

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

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