post_post — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem post_post {E : Type u''} [Category.{v''} E]
    (H : D ⥤ E)
      -- H G (colimit F) ⟶ H (colimit (F ⋙ G)) ⟶ colimit ((F ⋙ G) ⋙ H) equals
          -- H G (colimit F) ⟶ colimit (F ⋙ (G ⋙ H))

    [h : HasColimit ((F ⋙ G) ⋙ H)] :
    haveI : HasColimit (F ⋙ G ⋙ H) := h
    colimit.post (F ⋙ G) H ≫ H.map (colimit.post F G) = colimit.post F (G ⋙ H) :=
  by
  ext j
  rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]
  haveI : HasColimit (F ⋙ G ⋙ H) := h
  exact (colimit.ι_post F (G ⋙ H) j).symm

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