isColimitCocone — Mathlib

English

If c is a limit cone and G maps cones to colimits, then the constructed cone is a colimit cone.

Русский

Если c — предел-конус и G переводит конусы в пределы, то полученный конус является пределом.

LaTeX

$$$\\text{isColimitCone }(c)\\; (G)$$$

Lean4

/-- If `c` is a limit cone, `G.mapCocone c.op` is a colimit cone and the projection maps in `c`
are epimorphic, then `cocone G c.pt` is a colimit cone.
-/
noncomputable def isColimitCocone (hc : IsLimit c) [∀ i, Epi (c.π.app i)] (hc' : IsColimit <| G.mapCocone c.op) :
    IsColimit (cocone G c.pt) :=
  haveI := functorOp_final c hc
  (Functor.final_comp (opOpEquivalence ℕ).functor (functorOp c)).isColimitWhiskerEquiv _ _ hc'

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