Commit 2025-04-23 10:36 0d617900

refactor(CategoryTheory): redefine full subcategories using ObjectProperty (#22574) The type ObjectProperty was recently introduced #22286 for predicates on the objects of a category. We redefine FullSubcategory as ObjectProperty.FullSubcategory. This refactor PR mostly does only minimal changes to take into account that some definitions were renamed. The only significant exception is for the definition of the category of finitely generated modules in Algebra.Category.FGModuleCat.Basic, which should become the better practice for defining full subcategories, especially when we want to infer certain type classes: define a property of objects (here ModuleCat.isFG) and define the category as an abbreviation (here abbrev FGModuleCat := (ModuleCat.isFG R).FullSubcategory). Following this approach, significantly many of the typeclasses on the category FGModuleCat R can be inferred automatically.