colimitCoconeOfCoequalizerAndCoproduct

English

Given appropriate data on parallel pairs, there exists a limit for F.

Русский

Даны подходящие данные для параллельной пары, существует предел для F.

LaTeX

$$Limit from parallel pair$$

Lean4

/-- Given the existence of the appropriate (possibly finite) coproducts and coequalizers,
we can construct a colimit cocone for `F`.
(This assumes the existence of all coequalizers, which is technically stronger than needed.)
-/
noncomputable def colimitCoconeOfCoequalizerAndCoproduct (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] : ColimitCocone F
    where
  cocone := _
  isColimit :=
    buildIsColimit (Sigma.desc fun f => F.map f.2 ≫ colimit.ι (Discrete.functor F.obj) ⟨f.1.2⟩)
      (Sigma.desc fun f => colimit.ι (Discrete.functor F.obj) ⟨f.1.1⟩) (by simp) (by simp) (colimit.isColimit _)
      (colimit.isColimit _) (colimit.isColimit _)

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