instHasFunctorialFactorizationLlpRlp

English

If I has the small object argument, then the left class I.rlp.llp admits a functorial factorization with respect to I.rlp.

Русский

Если у свойства морфизмов I есть малый объектный аргумент, то класс слева I.rlp.llp имеет факторизацию, которая функционально однозначна через I.rlp.

LaTeX

$$$ HasFunctorialFactorization(I.rlp.llp, I.rlp) $$$

Lean4

instance : HasFunctorialFactorization I.rlp.llp I.rlp :=
  hasFunctorialFactorization I I.smallObjectκ

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