#16340: Infrastructure for modelling full subcategories
-------------------------------------+-------------------------------------
Reporter: nthiery | Owner:
Type: enhancement | Status: needs_review
Priority: major | Milestone: sage-6.4
Component: categories | Resolution:
Keywords: full | Merged in:
subcategories, homset | Reviewers: Darij Grinberg,
Authors: Nicolas M. Thiéry | Travis Scrimshaw
Report Upstream: N/A | Work issues:
Branch: | Commit:
public/categories/full_subcategories-16340|
d4c7a88563a397291b6cd5ddadb8f574cc1eedb5
Dependencies: | Stopgaps:
-------------------------------------+-------------------------------------
Comment (by pbruin):
Hi Nicolas,
> Replying to [comment:32 pbruin]:
> > 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.
--
Ticket URL: <http://trac.sagemath.org/ticket/16340#comment:36>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sage-trac.
For more options, visit https://groups.google.com/d/optout.
