hasCoproducts_of_colimit_cofans — Mathlib

English

If for every small index shape J and every diagram f: J → C there exists a cofan cf f which is a colimit, then C has all small coproducts.

Русский

Если для каждого малого индекса J и каждого диаграммного отображения f: J → C существует кофaн cf f, который является колимитом, то C имеет все малые копродукты.

LaTeX

$$$\text{HasCoproducts}(C)$$$

Lean4

theorem hasCoproducts_of_colimit_cofans (cf : ∀ {J : Type w} (f : J → C), Cofan f)
    (cf_isColimit : ∀ {J : Type w} (f : J → C), IsColimit (cf f)) : HasCoproducts.{w} C := fun _ : Type w =>
  {
    has_colimit := fun F =>
      HasColimit.mk
        ⟨(Cocones.precompose Discrete.natIsoFunctor.hom).obj (cf fun j => F.obj ⟨j⟩),
          (IsColimit.precomposeHomEquiv _ _).symm (cf_isColimit _)⟩ }

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