hasColimit_of_coequalizer_and_coproduct

English

Isomorphisms arise between limits of equivalent diagrams.

Русский

Изоморфизмы возникают между пределами эквивалентных диаграмм.

LaTeX

$$Isomorphisms between limits$$

Lean4

/-- Given the existence of the appropriate (possibly finite) coproducts and coequalizers,
we know a colimit of `F` exists.
(This assumes the existence of all coequalizers, which is technically stronger than needed.)
-/
theorem hasColimit_of_coequalizer_and_coproduct (F : J ⥤ C) [HasColimit (Discrete.functor F.obj)]
    [HasColimit (Discrete.functor fun f : Σ p : J × J, p.1 ⟶ p.2 => F.obj f.1.1)] [HasCoequalizers C] : HasColimit F :=
  HasColimit.mk (colimitCoconeOfCoequalizerAndCoproduct F)

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