equivIsoColimit — Mathlib

English

Given an equivalence of cocone categories e: Cocone K ≌ Cocone J, the collection of IsColimit structures on a cocone is equivalent when transported along the equivalence to the other cocone.

Русский

Дано эквивалентность категорий коконов e: Cocone K ≌ Cocone J; передачи структур IsColimit через эквивалент дают эквивалентность IsColimit на коконе.

LaTeX

$$$ \text{equivIsoColimit} : IsColimit r \cong IsColimit t $$$

Lean4

/-- Isomorphism of cocones preserves whether or not they are colimiting cocones. -/
def equivIsoColimit {r t : Cocone F} (i : r ≅ t) : IsColimit r ≃ IsColimit t
    where
  toFun h := h.ofIsoColimit i
  invFun h := h.ofIsoColimit i.symm
  left_inv := by cat_disch
  right_inv := by cat_disch

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