instHasFunctorialSurjectiveInjectiveFactorization

English

In a concrete category with suitable epi/mono factorisations and forgetful functor preserving monos and epis, every morphism admits a functorial factorization into a surjective part followed by an injective part.

Русский

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

LaTeX

$$$\\text{HasFunctorialSurjectiveInjectiveFactorization}(C)$$$

Lean4

instance (priority := 100) : HasFunctorialSurjectiveInjectiveFactorization C where
  nonempty_functorialFactorizationData := ⟨functorialSurjectiveInjectiveFactorizationData C⟩

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