isColimitWhiskerEquiv — Mathlib

English

IsColimit(extendCocone.obj t) ≃ IsColimit t when F is final.

Русский

IsColimit(extendCocone.obj t) эквивалентно IsColimit t при финальности F.

LaTeX

$$$$ \text{IsColimit}(\operatorname{extendCocone.obj} t) \cong \text{IsColimit}(t). $$$$

Lean4

/-- When `F : C ⥤ D` is final, and `t : Cocone G` for some `G : D ⥤ E`,
`t.whisker F` is a colimit cocone exactly when `t` is.
-/
def isColimitWhiskerEquiv (t : Cocone G) : IsColimit (t.whisker F) ≃ IsColimit t :=
  IsColimit.ofCoconeEquiv (coconesEquiv F G).symm

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