isColimitMapCoconeEmptyCoconeEquiv

English

If the terminal comparison map is an isomorphism, then G preserves terminal objects.

Русский

Если терминальное сравнение изоморфно, то G сохраняет терминальные объекты.

LaTeX

$$$(\\text{terminalComparison } G) \\text{ is an isomorphism } \\Rightarrow \\operatorname{PreservesLimit}(\\mathrm{empty}, G).$$$

Lean4

/-- The map of an empty cocone is a colimit iff the mapped object is initial.
-/
def isColimitMapCoconeEmptyCoconeEquiv : IsColimit (G.mapCocone (asEmptyCocone.{v₁} X)) ≃ IsInitial (G.obj X) :=
  isColimitEmptyCoconeEquiv D _ _ (eqToIso rfl)

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