Commit 2025-01-20 16:09 4e3f39f8
View on Github →feat(CategoryTheory/Localization): HasLocalization holds iff the localized category is locally small (#20670)
In this file, given W : MorphismProperty C and a universe w, we show that there exists a term in HasLocaliaation.{w} W if and only if there exists (or for all) localization functors L : C ⥤ D for W, the category D is locally w-small.