Commit 2025-12-01 18:53 4777673f

feat(CategoryTheory): localization of locally presentable categories (#30554) Let W : MorphismProperty C be a w-small property of morphisms in a locally κ-presentable category C (with κ : Cardinal.{w} a regular cardinal), such that the domains and codomains of morphisms satisfying W are κ-presentable. Then, the fullsubcategory W.rightOrthogonal is also locally κ-presentable (it is also stable under κ-filtered colimits, and the inclusion functor has a left adjoint).