Improve the terminology for the hierarchy relation between categories

[nthiery]

On #10963, it was noted that the use of "subcategory" for the hierarchy relation between categories is abusive (implicit use of forgetfull functors) and can be confusing. The purpose of this ticket is to discuss a possible improvement to the terminology. While we are at it, we may want to improve the suboptimal "join" and "meet" terminology.

[SimonKing]

Here is a little summary:

Our current use of subcategory and/or supercategory is a bit sloppy: We say that Groups() is a subcategory of Sets(), but in fact it is not, in the mathematical meaning of the notion "subcategory". All what we have is a forgetful functor from Groups() to Sets(). It was suggested to call this a "refinement", not a "subcategory".

In addition to that, we should have a framework for distinguishing between subcategories and full subcategories.

Applications

Let C be a category, let R be a category with a forgetful functor to C, let F be a full subcategory of C, and let S be a subcategory of C.

If an object O belongs to R, then we want that it inherits parent methods from C. So, "refinement" (or forgetful functors) is what we need for the hierarchy of parent and element methods---but rather not for subcategory methods! It was suggested to deal with the existence of a forgetful functor similarly to what we do with has_coerce_map_from() for parents.

I guess S and F should inherit subcategory methods of C, but R should not.

There sadly is this method _refine_category_(). As Nils points out in comment 634 of #10963, it should be renamed, since it makes no sense to "refine" an object of Sets() to an object of Groups(): Groups() is a "refinement" of (i.e. has a forgetful functor to) Sets(), but is not a subcategory of Sets(). He also claims that _refine_category_() mutates objects (by changing their type) that should better be immutable. But I argued that the dependence of hash/comparison on the type is a bug that _refine_category_() is not to blame for.

But I see a different problem: _refine_category_() should only be used for full subcategories (this currently is the case, we only use it to pass from Rings() to Fields()). Suppose O1, O2 have been initialised in C, and it was found that there is a coercion map phi from O1 to O2. This coercion map is cached, and by the coercion axioms it is a morphism, in C. Now suppose that O1 and O2 were refined to S, but S is not a full subcategory, and hence phi may not be a morphism in S. By consequence, phi can not be a coercion map after "refining" O1 and O2, and it might actually be the case that there is no coercion map at all---but it is still present in the coercion cache!

Therefore, as soon as we have a framework for "categories with forgetful functors" versus "subcategories" versus "full subcategories", we should rename _refine_category_() into, say, _interprete_in_full_subcategory_(), and add an assertion that prevents us from pushing an object of C into a non-full subcategory of C.

[nthiery]

Replying to SimonKing:

Here is a little summary:

Thanks Simon!

Let C be a category, let R be a category with a forgetful functor to C, let F be a full subcategory of C, and let S be a subcategory of C.

If an object O belongs to R, then we want that it inherits parent methods from C. So, "refinement" (or forgetful functors) is what we need for the hierarchy of parent and element methods

as well as morphism methods. But not homset methods!

---but rather not for subcategory methods!

For our current usage of "SubcategoryMethods?", refinement is actually what we want. So it's more like we should rename "SubcategoryMethods?" to something inline with whatever terminology we choose. Something like "RefinementCategoryMethods?"?

Maybe there is also a use case for "SubcategoryMethods?" in the context of subcategories, but that's a feature for later.

Cheers,

Nicolas