colimitQuotientCoproduct — Mathlib

English

If a functor preserves coequalizers and coproducts, it preserves colimits.

Русский

Если функтор сохраняет ко-эквалайзеры и coproducts, он сохраняет колимиты.

LaTeX

$$PreservesColimitsOfShape J G$$

Lean4

/-- A colimit can be realised as a quotient of a coproduct. -/
noncomputable def colimitQuotientCoproduct [HasColimitsOfSize.{w, w} C] (F : J ⥤ C) :
    ∐ (fun j => F.obj j) ⟶ colimit F :=
  have := hasFiniteColimits_of_hasColimitsOfSize C
  coequalizer.π _ _ ≫ (colimit.isoColimitCocone (colimitCoconeOfCoequalizerAndCoproduct F)).inv

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