instHasStrongEpiMonoFactorisations

English

In the simplex category, every morphism factors as a strong epimorphism followed by a monomorphism.

Русский

В категории симплекссов каждый морфизм факторизуется через сильное эпиморфизм и моно.

LaTeX

$$$\\forall f:X\\to Y,\\ \\exists Z,\\ e:X\\to Z\\ \\text{(strong epi)},\\ m:Z\\to Y\\ \\text{(mono)},\\ f = m\\circ e.$$$

Lean4

instance : HasStrongEpiMonoFactorisations SimplexCategory :=
  Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence SimplexCategory.skeletalEquivalence.inverse

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