hasColimit_multispan_comp — Mathlib

English

If the glue data diagram has a multicoequalizer and F preserves colimits, then the composed diagram F.map(D.diagram.multispan) has a multicoequalizer.

Русский

Если в диаграмме данных сцепления есть мультииквалентор и F сохраняет колимиты, то диаграмма D.diagram.multispan ⋙ F обладает мультииквализером.

LaTeX

$$$\\text{HasMulticoequalizer}(D.diagram.multispan \\circ F)$$$

Lean4

theorem hasColimit_multispan_comp : HasColimit (D.diagram.multispan ⋙ F) :=
  ⟨⟨⟨_, isColimitOfPreserves _ (colimit.isColimit _)⟩⟩⟩

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