isColimitMapEquiv — Mathlib

English

If d is a Multispan and c a multicofork, with F a functor, then IsColimit of F.mapCocone c is equivalent to IsColimit of c.map F.

Русский

Если d — мультиспан, c — мультикопор, и F — функтор, то IsColimit у F.mapCocone c эквивалентно IsColimit у c.map F.

LaTeX

$$$\text{IsColimit}(F.mapCocone(c)) \simeq \text{IsColimit}(c.map F)$$$

Lean4

/-- If `d : MultispanIndex J C`, `c : Multicofork d` and `F : C ⥤ D`,
the cocone `F.mapCocone c` is colimit iff the multicofork `c.map F` is. -/
def isColimitMapEquiv : IsColimit (F.mapCocone c) ≃ IsColimit (c.map F) :=
  (IsColimit.precomposeInvEquiv (d.multispanMapIso F).symm (F.mapCocone c)).symm.trans
    (IsColimit.equivIsoColimit (Multicofork.ext (Iso.refl _) (fun i ↦ by dsimp only [Multicofork.π]; simp)))

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