precomposeHomEquiv — Mathlib

English

If i is an isomorphism between cocones r and t and P is a colimit cocone on r, then (equivIsoColimit i) P equals P.ofIsoColimit i.

Русский

Если i — изоморфизм коконов r и t и P — колимитный кокон на r, тогда (equivIsoColimit i) P = P.ofIsoColimit i.

LaTeX

$$$ (equivIsoColimit i) P = P.ofIsoColimit i $$$

Lean4

/-- A cocone precomposed with a natural isomorphism is a colimit cocone
if and only if the original cocone is.
-/
def precomposeHomEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cocone G) :
    IsColimit ((Cocones.precompose α.hom).obj c) ≃ IsColimit c :=
  ofCoconeEquiv (Cocones.precomposeEquivalence α)

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