#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 nthiery):
Dear Peter,
Replying to [comment:36 pbruin]:
> 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.
I agree that clarifying what additional structure, if any, a category
defines can be a fundamental guideline for the design. Now, from what
I have seen in practice, new category writers usually start with plain
structure categories, and they do intuitively the right thing (which
typically shows up in the documentation: a XXX is a YYY endowed with
an operation zzz).
Worst case, if XXX does not actually define new structure, the default
behavior remains safe. They just won't get some feature that they most
likely don't need anyway. Remember that the doc of
"is_full_subcategory" specifies:
{{{
A positive answer is guaranteed to be mathematically
correct. A negative answer may mean that Sage has not been
taught enough information to derive this information. See
:meth:`full_super_categories` for a discussion.
}}}
Things are also safe when implementing an existing axiom or
construction in a category where it was not yet there.
The above guideline becomes important when implementing new axioms,
new constructions, or deciding which it should be; but there we can
assume that the developer has gained enough experience.
> > > > 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).
> 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".
My point is that the two concepts of axioms and of categories adding
structure are rather orthogonal.
Axioms are relevant when a bunch of categories have something to say
about that axiom. An axiom by itself may or may not add structure.
And there are non structure categories that need not be axioms.
Whether a given category is a structure category or not is the matter
of a single method, and it's not worth the complexity of duplicating
the category class hierarchy just for this.
> (By the way, "over a base ring" is actually something that I am thinking
of as another example of "extra structure".)
Here, it's really the category `Modules` that adds the structure. The
class "Category_over_base_ring" is just a technical gadget to handle
the base ring parameter that the categories over base rings
takes. E.g. `Algebras.FiniteDimensional` is a category over a base
ring which does not add structure, whereas `Modules` does.
> > 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.
Yes, this need to be specified explicitly by the person *defining* a
new axiom. But if it's just about implementing an existing axiom for
some category where it was not yet there, then the answer is clear:
there is no new structure.
As we discussed with Travis, I believe something similar should hold
for functorial constructions categories, at least in the covariant
case, but I need to think more about it.
Cheers,
Nicolas
--
Ticket URL: <http://trac.sagemath.org/ticket/16340#comment:45>
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.
