#10963: More functorial constructions
-------------------------------------+-------------------------------------
Reporter: nthiery | Owner: stumpc5
Type: enhancement | Status: needs_review
Priority: major | Milestone: sage-6.1
Component: categories | Resolution:
Keywords: days54 | Merged in:
Authors: Nicolas M. Thiéry | Reviewers: Simon King, Frédéric
Report Upstream: N/A | Chapoton
Branch: | Work issues:
public/ticket/10963 | Commit:
Dependencies: #11224, #8327, | eb7b486c6fecac296052f980788e15e2ad1b59e4
#10193, #12895, #14516, #14722, | Stopgaps:
#13589, #14471, #15069, #15094, |
#11688, #13394, #15150, #15506 |
-------------------------------------+-------------------------------------
Comment (by SimonKing):
Here is the announced example. Since Nicolas did not post here, I do. But
it is his example.
Recall: I wanted to start with the category `As()`, with available axioms
"B",...,"F". In the first place, there should be no relations between the
axioms. Moreover, I somehow want that `As().B().C()` is implemented using
a dedicated class (such as `FiniteFields()` uses a dedicated class) and no
join category is needed at this point.
This can be done by a basic category `Bases` that defines the axioms:
{{{
#!python
from sage.categories.category_singleton import Category_singleton
from sage.categories.category_with_axiom import axiom, CategoryWithAxiom
import sage.categories.category_with_axiom
sage.categories.category_with_axiom.all_axioms += ("B","C","D","E","F")
# This is just here so that As is not the category that defines the
axioms.
class Bases(Category_singleton):
def super_categories(self):
return [Objects()]
class SubcategoryMethods:
B = axiom("B")
C = axiom("C")
D = axiom("D")
E = axiom("E")
F = axiom("F")
class B(CategoryWithAxiom):
pass
class C(CategoryWithAxiom):
pass
class D(CategoryWithAxiom):
pass
class E(CategoryWithAxiom):
pass
class F(CategoryWithAxiom):
pass
}}}
and then, `As` becomes
{{{
#!python
class As(Category_singleton):
def super_categories(self):
return [Bases()]
class B(CategoryWithAxiom):
class C(CategoryWithAxiom):
pass
class E(CategoryWithAxiom):
class F(CategoryWithAxiom):
pass
class D(CategoryWithAxiom):
pass
}}}
Simple enough! And nicely, the commutativity and idempotency of applying
axioms is taken care of by the system:
{{{
sage: As().C().B() is As().B().C().B()
True
sage: type(As().B().C())
<class '__main__.B.C_with_category'>
}}}
Of course, in the above implementation, one has a join category, if `D`
and another axiom are involved:
{{{
sage: type(As().B().D())
<class 'sage.categories.category.JoinCategory_with_category'>
}}}
And now, I assume that some theorem says that
`As().B().C()==As().E().F()`. How to modify the above code? And in
particular: Will the system automatically take care of the implications of
the theorem? Again, I want a dedicated class for `As().B().C()`.
Here is one way to modify the code (calling the result `As2` rather than
`As`):
{{{
#!python
class As2(Category_singleton):
def super_categories(self):
return [Bases()]
class B(CategoryWithAxiom):
class C(CategoryWithAxiom):
def extra_super_categories(self):
return [Bases().E(), Bases().F()]
class E(CategoryWithAxiom):
def F_extra_super_categories(self):
return [Bases().B(), Bases().C()]
}}}
What does this code tell? Well, it tells that
- `As().B().C()` uses a dedicated class, and that it additionally
satisfies axioms E and F, by providing extra super categories.
- `As().E().F()` has the additional axioms B and C. Note the asymmetry in
the definition: It tells that `As().E().F()` will use the class `As.B.C`,
and the output of `F_extra_super_categories` tells how to find this class.
What I don't like is that we have a method `F_extra_super_categories`,
whose name is then mangled.
In the first moment I thought that the asymmetry is not nice. However, on
second thought, we ''must'' have asymmetry! After all, we want that
`As.B.C` is used for `As().E().F()` and not the other way around.
I believe that the above solution is simple enough, and it does address my
concern: The following works out of the box.
{{{
sage: As2().B().C() # it is recognised that axioms B, C, E and F
hold
Category of b c e f as2
sage: type(As2().E().F()) # the dedicated class is used
<class '__main__.B.C_with_category'>
sage: As2().B().F().D().E().C() is As2().B().C().D()
True
}}}
The last line means that the system finds non-trivial consequences of the
theorem together with idempotency and commutativity.
I don't think that the changes needed for implementing the theorem are
totally obvious: One has to learn rules and naming conventions. However,
if one has learnt these rules (which of course must be well documented)
then implementing the theorem in the code seems to be fairly straight
forward.
--
Ticket URL: <http://trac.sagemath.org/ticket/10963#comment:453>
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/groups/opt_out.
