sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.43k stars 479 forks source link

Infrastructure for modelling full subcategories #16340

Closed nthiery closed 10 years ago

nthiery commented 10 years ago

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

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:

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

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 commented 10 years ago
comment:1

Suggestions anyone before I start implementing this?

Cheers,

darijgr commented 10 years ago
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 commented 10 years ago
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 commented 10 years ago

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

nthiery commented 10 years ago

Commit: 2f2d09b

nthiery commented 10 years ago
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:

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
79f4766Merge branch 'public/categories/over-a-base-ring-category-15801' of trac.sagemath.org:sage into public/categories/over-a-base-ring-category-15801
281f539Added back in import statement as per comment.
96c631fMerge branch 'develop' into categories/axioms-10963
b1a2aedTrac 10963: two typo fixes to let the pdf documentation compile
c16f18bMerge branch 'public/ticket/10963-doc-distributive' of trac.sagemath.org:sage into categories/axioms-10963
dcb11d8Merge branch 'categories/axioms-10963' into categories/over_a_base_category-15801
15658bdTrac 15801: fixed merge with #12630
2f2d09b16340: infrastructure for modelling full subcategories
nthiery commented 10 years ago
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 commented 10 years ago
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 commented 10 years ago
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.

simon-king-jena commented 10 years ago
comment:10

Replying to @nthiery:

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.

Or, even more informative: Return a pair (op, method), such that

nthiery commented 10 years ago
comment:11

Replying to @simon-king-jena:

Or, even more informative: Return a pair (op, method), such that

  • op is the operator (either as in operator.contains, operator.mul, operator.and, or a parent/element method such as an_element), and
  • method is an abstract parent/element method that has to be implemented for op (i.e., __contains__, _mul_, or _an_element)

Possibly so indeed. Although this would be duplicating a bit the job of required_methods. I am not sure we want to put a specific emphasis on the methods related to an operation that adds structure (e.g. '+') or that does not (e.g. '-').

Speaking of which: see #16363.

nthiery commented 10 years ago
comment:12

Any other suggestions for the terminology? At this point, I am leaning toward additional_structure. But there remains to name "structure categories", and the method returning all the super "structure categories".

nthiery commented 10 years ago
comment:13

One thing I don't know how to handle. Assume we want the morphisms of euclidean rings to preserve euclidean division (I'd say that this is equivalent to preserving the degree). Then, EuclideanDomains() is not a full subcategory of Rings(). Yet Fields(), which is a subcategory of EuclideanDomains(), is a full subcategory of Rings(). This is because the additional structure defined by EuclideanDomains() (the degree) is trivial in this case.

We can't model this in the current implementation. An approach might be to have Fields() explicitly remove EuclideanDomains() from its structure categories. But then we have to be more careful in the full subcategory test. Maybe we can test, for B a subcategory of A that B.super_structure_categories() is a subset of A.super_structure_categories(); given that we hash and check for equality by id, that should be fast enough if deemed correct.

A similar situation appears for graded connected hopf algebras where there is a single choice for the antipode (and, IIRC, it's preserved for free by bialgebra morphisms). So this is a full subcategory of the category of bialgebras.

Cheers, Nicolas

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Changed commit from 2f2d09b to c06e2ef

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

c06e2ef16340: added full_super_categories method, a test, and some doc
rwst commented 10 years ago
comment:15
Error building the documentation.
Traceback (most recent call last):
  File "/home/ralf/sage/src/doc/common/builder.py", line 1477, in <module>
    getattr(get_builder(name), type)()
  File "/home/ralf/sage/src/doc/common/builder.py", line 276, in _wrapper
    getattr(get_builder(document), 'inventory')(*args, **kwds)
  File "/home/ralf/sage/src/doc/common/builder.py", line 487, in _wrapper
    x.get(99999)
  File "/home/ralf/sage/local/lib/python/multiprocessing/pool.py", line 554, in get
    raise self._value
OSError: [categorie] /home/ralf/sage/local/lib/python2.7/site-packages/sage/categories/category_with_axiom.py:docstring of sage.categories.category_with_axiom.CategoryWithAxiom.is_structure_category:7: WARNING: Literal block expected; none found.

make: *** [doc-html] Error 1
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Changed commit from c06e2ef to 2b0164b

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

2b0164b16340: trivial ReST fix
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

b6342d1Merge branch 'develop' into categories/full-subcategories-16340
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Changed commit from 2b0164b to b6342d1

nthiery commented 10 years ago

Work Issues: find good names

fchapoton commented 10 years ago
comment:19

There are some failing doctests, see patchbot report.

tscrim commented 10 years ago

Changed commit from b6342d1 to edb29e6

tscrim commented 10 years ago
comment:20

I've fixed the trivial doctest failures in category.py. I get the same warning messages about the stack size using develop and I don't see any additional memory usage without this branch (so I'd say we can ignore those). I don't get any of the other failures.


New commits:

93273a7Merge branch 'u/nthiery/categories/full-subcategories-16340' of trac.sagemath.org:sage into public/categories/full_subcategories-16340
edb29e6Fixed trivial doctest failures.
tscrim commented 10 years ago

Changed branch from u/nthiery/categories/full-subcategories-16340 to public/categories/full_subcategories-16340

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

eaa56bc16340: super_structure_categories -> all_structure_super_categories
afc9724Merge branch 'develop' into categories/full-subcategories-16340
99a8eb1Merge branch 'public/categories/full_subcategories-16340' of trac.sagemath.org:sage into categories/full-subcategories-16340
8bc456cMerge branch 'master=6.3' into categories/full-subcategories-16340
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Changed commit from edb29e6 to 8bc456c

anneschilling commented 10 years ago
comment:23

Simon, could you review this ticket since we need it for other applications? Thanks!

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

737a8f016340: improved warnings about the current limitation of the model
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Changed commit from 8bc456c to 737a8f0

nthiery commented 10 years ago

Description changed:

--- 
+++ 
@@ -102,12 +102,23 @@
      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

-- How to handle the case where the extra structure is forced by the

nthiery commented 10 years ago
comment:26

I put here for the record a summary of a private discussion by e-mail.

Darij:

I don't see any better names than "full" and "structure" subcategory. In my opinion, these are clear and don't conflict with common usage. While I am still not very keen on the name "subcategory" itself, we can keep the "full" and "structure" adjectives even if we change it.

Travis:

This is the big thing that we needed. I can do the rest of the review at this point I think. However thanks for looking things over and giving us your notes.

Darij:

Nicolas: I believe that this limitation could be raised, though at this point I don't quite know what's the best approach. I also don't see a critical need (it's already a good progress). So, as long as it's properly documented (I just reworked that piece of the documentation; now it's up to you guys to judge), I think that's fine for now.
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Changed commit from 737a8f0 to 282ac4e

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

282ac4e16340: fixed typos reported by Darij
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Changed commit from 282ac4e to d4c7a88

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 10 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

e5f210cMerge branch 'public/categories/full_subcategories-16340' of trac.sagemath.org:sage into public/categories/full_subcategories-16340
d4c7a88Specified more categories as not being structure categories.
tscrim commented 10 years ago

Reviewer: Darij Grinberg, Travis Scrimshaw

tscrim commented 10 years ago

Changed work issues from find good names to none

tscrim commented 10 years ago
comment:29

I made some other categories into non-structure categories. This made me wonder if we actually want the default category be a structure category. Yet I don't think we have enough data currently to answer this right now. I'm going to double-check to make sure I didn't miss any others and I'd appreciate if someone else could do the same. Otherwise I think we're okay to positive review it.

Darij, I've added you as a reviewer since you did look over the code and give suggestions.

pjbruin commented 10 years ago
comment:30

Is it clear that the "structure category" terminology is the way to go? Personally I still don't like it very much (again, it pretends to be about categories but instead is about relations to their supercategories). I would prefer the proposals made by Nicolas in comment:9 and Simon in comment:10 to have an additional_structure() method that returns something meaningful about the additional structure, not just True or False.

tscrim commented 10 years ago
comment:31

Replying to @pjbruin:

Is it clear that the "structure category" terminology is the way to go? Personally I still don't like it very much (again, it pretends to be about categories but instead is about relations to their supercategories).

It's more of there has been no better alternative proposed. If we move away from the terminology "structure category", then I feel like we loose the ability to name methods like all_structure_super_categories. However I do understand your objection.

I would prefer the proposals made by Nicolas in comment:9 and Simon in comment:10 to have an additional_structure() method that returns something meaningful about the additional structure, not just True or False.

Currently the default is that new subcategories are structure categories (so they are not full subcategories). If we were to go with returning pairs (op, method), then the question becomes do we want the default to be False or do we allow True to remain the default and have it be when we can't adequately define the structure?

Actually, that made me have a thought. How about instead of is_structure_category we have has_additional_structure, and then we could extend this to additional_structure (on a followup ticket).

tscrim commented 10 years ago

Description changed:

--- 
+++ 
@@ -45,7 +45,7 @@
     {Magmas(), AdditiveMagmas()}

(just take the union of the structure super categories of the super -categories of self, and add self if relevant). +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 @@ -104,8 +104,7 @@

 ## 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
+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`
pjbruin commented 10 years ago
comment:32

Hi Travis,

Replying to @pjbruin:

Is it clear that the "structure category" terminology is the way to go? Personally I still don't like it very much (again, it pretends to be about categories but instead is about relations to their supercategories).

It's more of there has been no better alternative proposed. If we move away from the terminology "structure category", then I feel like we loose the ability to name methods like all_structure_super_categories. However I do understand your objection.

After looking at the code, I actually have the feeling that this all_structure_super_categories() method is a somewhat unnatural solution to the question of determining whether one category is a full subcategory of another. At first sight it looks like a category should be able to simply declare if is it a full subcategory of its supercategories (for each supercategory individually, if necessary). Then is_full_subcategory(), given two categories, could check if there is a sequence of full subcategory inclusions between the two categories.

I would prefer the proposals made by Nicolas in comment:9 and Simon in comment:10 to have an additional_structure() method that returns something meaningful about the additional structure, not just True or False.

Currently the default is that new subcategories are structure categories (so they are not full subcategories). If we were to go with returning pairs (op, method), then the question becomes do we want the default to be False or do we allow True to remain the default and have it be when we can't adequately define the structure?

Hmm, it doesn't sound very desirable to define a category where you can't define what its extra structure is...

Actually, that made me have a thought. How about instead of is_structure_category we have has_additional_structure, and then we could extend this to additional_structure (on a followup ticket).

This sounds good. We could go even further and formalise the notion of category with extra structure, so we would have

  1. CategoryWithAxiom: like the existing class, but more restrictive. Specifies an additional axiom to be satisfied by the objects, and defines the full subcategory objects satisfying this axiom. For example, commutativity for groups.
  2. CategoryWithStructure: proposed new class. Specifies an additional structure on objects that must be preserved by morphisms, and defines a usually non-full subcategory. In certain cases something that is now called an axiom would become an extra structure. For example (thinking about the discussion on #16843) the Unital property for rings (as a subcategory of Rngs) would become a structure instead of an axiom, because morphisms are restricted by the requirement that they preserve the unit element.
nthiery commented 10 years ago
comment:33

Replying to @tscrim:

I made some other categories into non-structure categories.

Thanks. I double checked on this, and mostly agree up to one point: I think Coxeter Groups should be a structure category, the extra structure being the chosen set of simple generators.

This made me wonder if we actually want the default category be a structure category.

I believe this would be dangerous. Being accidently a structure category means that your homsets will miss some code that could be available. So just a missing feature. Whereas being accidently a non structure category can let your homset inherit from code that is not applicable which can lead to wrong code.

Besides, all the categories your changed should actually become CategoryWithAxioms at some point, which will have precisely the desired effect.

So now one could wonder whether having a CategoryWithAxiom be a non structure category is not a dangerous default. I believe it's ok, because for a category with axiom A.B, one only has to be careful about being a full subcategory or not if A is the category defining the axiom B. There are not soo many of them.

I'm going to double-check to make sure I didn't miss any others and I'd appreciate if someone else could do the same.

Thanks!

Cheers, Nicolas

nthiery commented 10 years ago
comment:34

Replying to @pjbruin:

At first sight it looks like a category should be able to simply declare if is it a full subcategory of its supercategories (for each supercategory individually, if necessary). Then is_full_subcategory(), given two categories, could check if there is a sequence of full subcategory inclusions between the two categories.

That was the original plan, but this means having to encode much more information. And it's quite more costly to compute.

I would prefer the proposals made by Nicolas in comment:9 and Simon in comment:10 to have an additional_structure() method that returns something meaningful about the additional structure, not just True or False.

Currently the default is that new subcategories are structure categories (so they are not full subcategories). If we were to go with returning pairs (op, method), then the question becomes do we want the default to be False or do we allow True to remain the default and have it be when we can't adequately define the structure?

Hmm, it doesn't sound very desirable to define a category where you can't define what its extra structure is...

But this is imposing the category writer to do implement one more thing, when implementing a category is already a barrier. Being a full subcategory only adds extra features to homsets. In most cases, when implementing a category for the first time, one does not need this feature. So being able to just not have to worry about it is a definite plus.

Actually, that made me have a thought. How about instead of is_structure_category we have has_additional_structure, and then we could extend this to additional_structure (on a followup ticket).

Possibly so. What would be the names for all the related methods (like all_structure_categories)?

This sounds good. We could go even further and formalise the notion of category with extra structure, so we would have

  1. CategoryWithAxiom: like the existing class, but more restrictive. Specifies an additional axiom to be satisfied by the objects, and defines the full subcategory objects satisfying this axiom. For example, commutativity for groups.
  2. CategoryWithStructure: proposed new class. Specifies an additional structure on objects that must be preserved by morphisms, and defines a usually non-full subcategory. In certain cases something that is now called an axiom would become an extra structure. For example (thinking about the discussion on #16843) the Unital property for rings (as a subcategory of Rngs) would become a structure instead of an axiom, because morphisms are restricted by the requirement that they preserve the unit element.

We want Unital to have all the other features of axioms like:

    sage: Rngs() & Semigroups().Unital()
    Category of Rings

So this would require a more complicated hierarchy of classes, especially since one would also need to take care of the over_base_ring variations. I am not sure this is worth it for just a single method.

By the way: Semigroups().Unital() is indeed a structure category. But not Rngs().Unital(): all the structure is defined in the super categories Rngs() and Semigroups().Unital().

Also: there is room for improvement in functorial constructions: in some cases, we could automatically deduce that the category is a structure category. I believe this is easier to implement by mean of methods than by inheriting from one class or the other (and past has proven that I can live with class surgery when needed).

Cheers, Nicolas

tscrim commented 10 years ago
comment:35

Replying to @nthiery:

Thanks. I double checked on this, and mostly agree up to one point: I think Coxeter Groups should be a structure category, the extra structure being the chosen set of simple generators.

I don't think so. If we wanted the generators to be part of the structure (definition), that should be the category of Coxeter syetems as it is much more rigid than just the groups.

This made me wonder if we actually want the default category be a structure category.

I believe this would be dangerous. Being accidentally a structure category means that your homsets will miss some code that could be available. So just a missing feature. Whereas being accidentally a non structure category can let your homset inherit from code that is not applicable which can lead to wrong code.

I agree with this, although my thought is more about how many categories will we have are structure categories. As I stated, we need more data and I agree that having this default is the safe route.

Besides, all the categories your changed should actually become CategoryWithAxioms at some point, which will have precisely the desired effect.

Probably.

So now one could wonder whether having a CategoryWithAxiom be a non structure category is not a dangerous default. I believe it's ok, because for a category with axiom A.B, one only has to be careful about being a full subcategory or not if A is the category defining the axiom B. There are not soo many of them.

Most axioms that come to my mind adds extra structure, but we can see what happens as we add more axioms.

I'm going to double-check to make sure I didn't miss any others and I'd appreciate if someone else could do the same.

Thanks!

Thanks for double-checking my double-check.

Replying to @nthiery:

Possibly so. What would be the names for all the related methods (like all_structure_categories)?

With this, we could keep the same names (although I believe the method your referring to is all_structure_super_categories).

Are we all in agreement that we should change is_structure_category to has_additional_structure and the current framework is a good enough to merge in (since it could be extended at a later date to carry additional info)?

pjbruin commented 10 years ago
comment:36

Hi Nicolas,

Replying to @pjbruin:

At first sight it looks like a category should be able to simply declare if is it a full subcategory of its supercategories (for each supercategory individually, if necessary). Then is_full_subcategory(), given two categories, could check if there is a sequence of full subcategory inclusions between the two categories.

That was the original plan, but this means having to encode much more information. And it's quite more costly to compute.

I don't see why this should necessarily be the case; we would just encode for each direct supercategory (of which there are usually just one or two) whether it is a full supercategory. This makes computing all full supercategories not any slower (and probably faster) than computing all supercategories, or presumably all "structure supercategories" for that matter.

I would prefer the proposals made by Nicolas in comment:9 and Simon in comment:10 to have an additional_structure() method that returns something meaningful about the additional structure, not just True or False.

Currently the default is that new subcategories are structure categories (so they are not full subcategories). If we were to go with returning pairs (op, method), then the question becomes do we want the default to be False or do we allow True to remain the default and have it be when we can't adequately define the structure?

Hmm, it doesn't sound very desirable to define a category where you can't define what its extra structure is...

But this is imposing the category writer to do implement one more thing, when implementing a category is already a barrier. Being a full subcategory only adds extra features to homsets. In most cases, when implementing a category for the first time, one does not need this feature. So being able to just not have to worry about it is a definite plus.

It seems to me that the first thing one has to do when defining a category (and maybe the only essential thing!) should be to decide how to encode its mathematical meaning. The distinction between adding a new axiom to the objects (thereby creating a full subcategory) and adding a new type of structure (thereby creating a relationship that I was thinking of as "category refinement" in earlier discussions) is really fundamental in my opinion.

Actually, that made me have a thought. How about instead of is_structure_category we have has_additional_structure, and then we could extend this to additional_structure (on a followup ticket).

Possibly so. What would be the names for all the related methods (like all_structure_categories)?

This sounds good. We could go even further and formalise the notion of category with extra structure, so we would have

  1. CategoryWithAxiom: like the existing class, but more restrictive. Specifies an additional axiom to be satisfied by the objects, and defines the full subcategory objects satisfying this axiom. For example, commutativity for groups.
  2. CategoryWithStructure: proposed new class. Specifies an additional structure on objects that must be preserved by morphisms, and defines a usually non-full subcategory. In certain cases something that is now called an axiom would become an extra structure. For example (thinking about the discussion on #16843) the Unital property for rings (as a subcategory of Rngs) would become a structure instead of an axiom, because morphisms are restricted by the requirement that they preserve the unit element.

We want Unital to have all the other features of axioms like:

    sage: Rngs() & Semigroups().Unital()
    Category of Rings

Of course, this type of construction should stay the same.

So this would require a more complicated hierarchy of classes, especially since one would also need to take care of the over_base_ring variations. I am not sure this is worth it for just a single method.

On the contrary, I think it there is an essential distinction between just adding an axiom to the objects (hence creating a full subcategory) and adding "extra structure". (By the way, "over a base ring" is actually something that I am thinking of as another example of "extra structure".)

By the way: Semigroups().Unital() is indeed a structure category. But not Rngs().Unital(): all the structure is defined in the super categories Rngs() and Semigroups().Unital().

This actually strengthens my conviction that "structure category" is not a well-defined notion. Instead, I have the impression that the structure should be regarded as being attached to what is currently called the "axiom" rather than to the category.

In this example, it depends on how you define Rings(): either as Rngs() & Semigroups().Unital(), in which case it is just a join of categories without new structure, _or_ as Rngs().Unital(), in which it does have extra structure (at least at first sight; you have to know that the category code magically rearranges the construction to turn Rngs().Unital() into a join of larger categories). In fact, Semigroups().Unital() (= Monoids()) is not a structure category either; it is the join of Magmas().Unital() and Semigroups().

Also: there is room for improvement in functorial constructions: in some cases, we could automatically deduce that the category is a structure category.

I am wondering how you could possibly detect such a thing. In the case of the Unital() structure (correct me if this is somehow an exception), how do you know that this does not just mean the existence of a unit element in the objects, but also the requirement that morphisms preserve this element? This seems to me precisely the type of information that has to be specified by the person implementing the Unital() structure.

nthiery commented 10 years ago
comment:37

Replying to @tscrim:

I don't think so. If we wanted the generators to be part of the structure (definition), that should be the category of Coxeter syetems as it is much more rigid than just the groups.

Both concepts are useful, but it's far from clear for me that we want to maintain both categories Coxeter groups / coxeter systems. Given that:

I agree with this, although my thought is more about how many categories will we have are structure categories. As I stated, we need more data and I agree that having this default is the safe route.

I agree that we need more data. My bet is that most categories will be either structure categories or categories with axioms.

Most axioms that come to my mind adds extra structure, but we can see what happens as we add more axioms.

Do they? So far, only one of the existing axioms (Unital and its additive variant) add extra structure. And the one I am thinking for the future don't add extra structure (about monoids: L,R,J-Trivial, ...).

With this, we could keep the same names (although I believe the method your referring to is all_structure_super_categories).

If we switch to has_additional_structure, it feels like we are not using structure as an adjective for qualifying a category anymore, but rather as a noun. So all_structure_super_categories does not really make sense. On the other hand, we could possibly name this method "structure":

sage: Rings().structure()
[Category of unital magmas, Category of additive unital additive magmas]

We could actually get rid of "has_additional_structure" altogether, and instead have C.additional_structure() return C by default, with the possibility to override it to return None, or, in the future, something more meaningful than C.

Cheers, Nicolas

nthiery commented 10 years ago
comment:38

Replying to @pjbruin:

This actually strengthens my conviction that "structure category" is not a well-defined notion.

It's perfectly defined: C is a structure category if whenever A and B are in C and phi is a morphism between A and B for any strict super category of C, then phi is a C morphism. And it coincides with the intuition we have of it: does C define some additional structure (typically an operation) that has to be preserved by C-morphisms.

Instead, I have the impression that the structure should be regarded as being attached to what is currently called the "axiom" rather than to the category.

In this example, it depends on how you define Rings(): either as Rngs() & Semigroups().Unital(), in which case it is just a join of categories without new structure, _or_ as Rngs().Unital(), in which it does have extra structure (at least at first sight; you have to know that the category code magically rearranges the construction to turn Rngs().Unital() into a join of larger categories). In fact, Semigroups().Unital() (= Monoids()) is not a structure category either; it is the join of Magmas().Unital() and Semigroups().

I don't see why Rngs().Unital() should suggest it's a structure category. A.Unital() is never a structure category unless A is the category defining Unital. That is A=Magmas().

I don't see why this should necessarily be the case; we would just encode for each direct supercategory (of which there are usually just one or two) whether it is a full supercategory.

Well, I tried, and the code stunk with duplication, urging me to do it differently :-) Feel free to try for yourself. In particular, it becomes painful for categories with axioms or functorial construction categories where the super categories are computed automatically for you.

This makes computing all full supercategories not any slower (and probably faster) than computing all supercategories,

Yup.

or presumably all "structure supercategories" for that matter.

Possibly so. There are few structure supercategories so that's rather cheap too.

I'll answer the rest tomorrow.

Cheers, Nicolas

tscrim commented 10 years ago
comment:39

Replying to @nthiery:

Both concepts are useful, but it's far from clear for me that we want to maintain both categories Coxeter groups / coxeter systems. Given that:

  • Our Coxeter groups all come endowed with a distinguished set of generators.

    • It's easier to change a structure category to a non structure category than the converse (since it's adding features).

    • With the current setting, we already have both concepts: e.g. when constructing a morphism between two coxeter groups, you can choose to construct it as a group morphism or as a Coxeter group morphism.

After looking over the category, I agree with you that it is modeling a Coxeter system. However I think we should expand the documentation at the beginning of the category to emphasize this (and I'd almost say we should rename the category to reflect this).

Do they? So far, only one of the existing axioms (Unital and its additive variant) add extra structure. And the one I am thinking for the future don't add extra structure (about monoids: L,R,J-Trivial, ...).

I was thinking associative and inverse add structure (to the morphism), but they don't, they just guarantee properties about the elements (and the axioms are preserved under the morphisms). I was also thinking of things like "grading", "topogolical", and "metric" but they aren't axioms (they are/would be functorial constructions). So perhaps axiom categories could not be structure categories by default...more data is probably needed.

Actually that brings up another question, should (regressive) functorial constructions be structure categories by default? Or again do you think more data needed?

If we switch to has_additional_structure, it feels like we are not using structure as an adjective for qualifying a category anymore, but rather as a noun. So all_structure_super_categories does not really make sense. On the other hand, we could possibly name this method "structure":

sage: Rings().structure() [Category of unital magmas, Category of additive unital additive magmas]

We could actually get rid of "has_additional_structure" altogether, and instead have C.additional_structure() return C by default, with the possibility to override it to return None, or, in the future, something more meaningful than C.

However with doing things this way, how is it different than explicitly specifying the full subcategories (well, in reverse)?