Infrastructure for modelling full subcategories

[nthiery]

It has been desired for a while to be able to test, when B is a subcategory of A, whether it is a full subcategory or not; equivalently this is whether any A-morphism is a B-morphism (up to forgetfull functor; note that the converse always holds).

The main application is for #10668, which will let B.homset_class inherit from A.homset_class in this case and only in this case.

References

• http://trac.sagemath.org/wiki/CategoriesRoadMap
• The discussion around #10668 comment:16
• The terminology is subject to Improve the terminology for the hierarchy relation between categories #16183

Implementation proposal

For each category C, we encode the following data: is C is a full
subcategory of the join of its super categories? Informally, the
question is whether C introduces more structure or operations. For
the sake of the discussion, I am going to call C a structure
category in this case, but a better name is to be found.

Here are some of the main structure categories in Sage, and the
structure or main operation they introduce:

• AdditiveMagmas: +
• AdditiveMagmas.AdditiveUnital: 0
• Magmas: *
• Magmas.Unital: 1
• Module: . (product by scalars)
• Coalgebra: coproduct
• Hopf algebra: antipode
• Enumerated sets: a distinguished enumeration of the elements
• Coxeter groups: distinguished coxeter generators
• Euclidean ring: the euclidean division
• Crystals: crystal operators

Possible implementation: provide a method C.is_structure_category()
(name to be found). The default implementation would return True for
a plain category and False for a CategoryWithAxiom. This would cover
most cases, and require to implement foo methods only in a few
categories (e.g. the Unital axiom categories).

Once we have this data encoded, we can implement recursively a
(cached) method such as:

    sage: Rings().structure_super_categories()
    {Magmas(), AdditiveMagmas()}

(just take the union of the structure super categories of the super
categories of ``self``, and add ``self`` if relevant).

It is now trivial to check whether a subcategory B of A is actually a
full subcategory: they just need to have the same structure super
categories! Hence is_full_subcategory can be written as:

    def is_full_subcategory(self, other):
        return self.is_subcategory(other) and
           len(self.structure_super_categories()) == len(other.structure_super_categories())

Advantages of this proposal

This requires very little data to be encoded, and should be quite
cheap to compute.

This is generally useful; in particular, for a user, the structure
super categories together with the axioms would give an interesting
overview of a category:

    sage: Rings().structure_super_categories()
    {Magmas(), AdditiveMagmas()}
    sage: Rings().axioms()
    frozenset({'AdditiveAssociative', 'AdditiveCommutative', 'AdditiveInverse', 'AdditiveUnital', 'Associative', 'Distributive', 'Unital'})

In fact, we could hope/want to always have:

    C is Category.join(C.structure_super_categories()).with_axioms(C.axioms())

which could be used e.g. for pickling by construction while exposing
very little implementation details.

Bonus

Each structure category could name the main additional operations, so
that we could have something like:

    sage: Magmas().new_operation()
    "+"
    sage: Rings().operations()
    {"+", "0", "*", "1"}

or maybe:

    sage: Rings().operations()
    {Category of additive magmas: "+",
     Category of additive unital additive magmas: "0",
     Category of magmas: "*",
     Category of unital magmas: "1"}

Limitation

The current model forces the following assumption: C \subset B \subset A is a chain of categories and C is a full subcategory of A, then
C is a full subcategory of B and B is a full subcategory of A.
In particular, we can't model situations where, within the context of
C, any A morphism is in fact a B morphism because the B
structure is rigid.

Example: C=Groups, B=Monoids, A=Semigroups.

This is documented in details in the methods .is_fullsubcategory and
.full_super_categories.

Questions

• Find good names for all the methods above

• Ideas on how to later lift the limitation?

CC: @sagetrac-sage-combinat @hivert @simon-king-jena @darijgr @nbruin @pjbruin @vbraun

Component: categories

Keywords: full subcategories, homset

Author: Nicolas M. Thiéry

Branch: eb621c7

Reviewer: Darij Grinberg, Travis Scrimshaw, Simon King

Issue created by migration from https://trac.sagemath.org/ticket/16340

[nthiery]

comment:1

Suggestions anyone before I start implementing this?

Cheers,

[darijgr]

comment:2

Ideally, for every piece of algebraic structure there should be both a full and a fully structure-aware subcategory. So there should be a UnitalAlgebrasWithUnitalMorphisms and a UnitalAlgebrasWithArbitraryMorphisms, etc.; more importantly, there should be categories for graded modules with graded morphisms and with arbitrary morphisms (I don't remember out of the hat which is the one we have) and categories for modules-with-basis with basis-preserving morphisms and with arbitrary morphisms etc.. This might not belong into this ticket, but please make sure that your model takes this into account and does not handle fullness as a hardcoded property of the relevant axiom / functorial construct.

Other than this I like the proposal!

[tscrim]

comment:3

Is it possible to have a proper subcategory (within Sage) which has the same number, but actually different set, of operators (i.e. is len a sufficient check or do we need to compare sorted lists)? I'm pretty sure this is mathematically wrong, but can someone confirm.

[nthiery]

Branch: u/nthiery/categories/full-subcategories-16340

[nthiery]

Commit: 2f2d09b

[nthiery]

comment:5

Replying to @darijgr:

Ideally, for every piece of algebraic structure there should be both a full and a fully structure-aware subcategory. So there should be a UnitalAlgebrasWithUnitalMorphisms and a UnitalAlgebrasWithArbitraryMorphisms, etc.; more importantly, there should be categories for graded modules with graded morphisms and with arbitrary morphisms (I don't remember out of the hat which is the one we have) and categories for modules-with-basis with basis-preserving morphisms and with arbitrary morphisms etc.

Agreed.

This might not belong into this ticket, but please make sure that your model takes this into account and does not handle fullness as a hardcoded property of the relevant axiom / functorial construct.

I guess that's alright: when we will want both, we will just need to
have two distinct categories/axioms/functorial construction for the
two situations. I am missing a good idiom / naming convention though.

In the mean time, the current implementation makes a default choice on
a case by case basis, according to the foreseen main use case for the
category (see the doc).

Other than this I like the proposal!

Cool. I just pushed a first attempt. It's probably reasonably
complete. The main things that need discussion are:

• Terminology and method names

• Are there categories which need special handling that I missed?

• The default choices I have made.

Cheers,
Nicolas

---

Last 10 new commits:

54c3d67	#15801: Initialize the base ring for module homsets
aa01591	#15801: doctests for CategoryObjects.base_ring + docfix in Modules.SubcategoryMethods.base_ring
79f4766	Merge branch 'public/categories/over-a-base-ring-category-15801' of trac.sagemath.org:sage into public/categories/over-a-base-ring-category-15801
281f539	Added back in import statement as per comment.
96c631f	Merge branch 'develop' into categories/axioms-10963
b1a2aed	Trac 10963: two typo fixes to let the pdf documentation compile
c16f18b	Merge branch 'public/ticket/10963-doc-distributive' of trac.sagemath.org:sage into categories/axioms-10963
dcb11d8	Merge branch 'categories/axioms-10963' into categories/over_a_base_category-15801
15658bd	Trac 15801: fixed merge with #12630
2f2d09b	16340: infrastructure for modelling full subcategories

[nthiery]

comment:6

Replying to @tscrim:

Is it possible to have a proper subcategory (within Sage) which has the same number, but actually different set, of operators (i.e. is len a sufficient check or do we need to compare sorted lists)? I'm pretty sure this is mathematically wrong, but can someone confirm.

In the current implementation, we are comparing the set of all super categories that define some structure. This set can only become larger for inclusion when going down the category hierarchy. So technically we are fine.

And this implementation seems to correctly models the mathematics, right?

[pjbruin]

comment:8

I haven't had time to look at this in detail, but at first sight it looks like a good approach to me.

For me the main point to think about is the terminology "structure category". It would be nice if the name made it slightly clearer that this property is not so much about the category itself as about its relation to its supercategories. (Some random alternative names for is_structure_category(): adds_structure()? is_augmented_category()? is_enriched_category()?)

[nthiery]

comment:9

Replying to @pjbruin:

For me the main point to think about is the terminology "structure category".
It would be nice if the name made it slightly clearer that this property is not so much about the category itself as about its relation to its supercategories.

Definitely!

(Some random alternative names for is_structure_category(): adds_structure()? is_augmented_category()? is_enriched_category()?)

Also, instead of an "is_..." method, we could name the method something like additional_structure and have it return something possibly meaningfull, like "*" for magmas or "+" for additive magmas, and None if there is none. It would still evaluate appropriately to True/False in boolean context.