hasColimit_equivalence_comp — Mathlib

English

If an equivalence e : K ≌ J and HasColimit (e.functor ⋙ F) hold, then HasColimit F holds.

Русский

Если существует эквивалентность e : K ≌ J и HasColimit (e.functor ⋙ F), то HasColimit F также существует.

LaTeX

$$$ \\text{HasColimit} (e.functor \\;\\circ\\; F) \\Rightarrow \\text{HasColimit} F $$$

Lean4

instance hasColimit_equivalence_comp (e : K ≌ J) [HasColimit F] : HasColimit (e.functor ⋙ F) :=
  HasColimit.mk
    { cocone := Cocone.whisker e.functor (colimit.cocone F)
      isColimit := IsColimit.whiskerEquivalence (colimit.isColimit F) e }

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