Commit 2026-09-25 12:29 4e284f90
View on Github →feat(CategoryTheory): pure morphisms are filtered colimits of split monomorphisms (#44044) This holds in a locally presentable category (or an accessible category with pushouts).
feat(CategoryTheory): pure morphisms are filtered colimits of split monomorphisms (#44044) This holds in a locally presentable category (or an accessible category with pushouts).