instEssSurjArrowHomotopyCategoryIntUpMapArrowQh

English

The map-arrow functor in the localization is essentially surjective; i.e., every arrow in the target category is represented up to isomorphism by a map arrow from the source.

Русский

Функтор перехода стрелок локализации является эссенциально сюръективным; то есть любая стрелка в целевой категории представима нами до изоморфизма стрелкой источника.

LaTeX

$$$\mathrm{essSurj}_{\text{arrow}}(\text{mapArrow})$$$

Lean4

instance : (Qh (C := C)).mapArrow.EssSurj :=
  Localization.essSurj_mapArrow _ (HomotopyCategory.subcategoryAcyclic C).trW

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