#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 nthiery):
Hi Simon!
Short answer for now. I have a longer answer from yesterday which did
not go through before I went to bed.
Replying to [comment:436 SimonKing]:
> As indicated above, it seems natural to me that we prefer a "short"
> construction (start with a basic category and apply few axioms) over a
"long"
> construction (involving a long chain of axioms. This means we would
prefer a
> degree order. However, it ''really'' matters what happens after
comparing
> degrees.
>
> In all examples, I am using a degneglex order.
>
> - Start with the basic categories ''reversedly'' sorted by their name,
> followed by the axioms in the ''reversed'' order given by
> `sage.categories.categories_with_axioms.all_axioms`. Then, there is
only one
> complaint, namely: `Blahs.Unital.Blue` should coincide with
> `Blahs.Unital`.
>
> - Start with the basic categories ''directly'' sorted by their name,
followed
> by the xioms in the ''reversed'' order given by
> `sage.categories.categories_with_axioms.all_axioms`. Then, we
additionally
> find: `TestObjects.FiniteDimensional.Unital` should better be provided
by
> `Bars.Unital.FiniteDimensional`. Similarly for other educational
examples in
> `sage.categories.category_with_axiom`.
>
> - Start with the basic categories ''reversedly'' sorted by their name,
> followed by the axioms in the ''direct'' order given by
> `sage.categories.categories_with_axioms.all_axioms`. Then the problems
are
> similar to the previous case, in the educational examples in
> `sage.categories.category_with_axiom`. Such as:
`TestObjects.FiniteDimensional.Unital` should
> better be provided by `TestObjects.Blue.FiniteDimensional`.
>
> - Start with the basic categories ''directly'' sorted by their name,
followed
> by the axioms in the ''direct'' order given by
> `sage.categories.categories_with_axioms.all_axioms`. Again, problems
with
> the educational examples in `sage.categories.category_with_axiom`.
Such as:
> `TestObjectsOverBaseRing.Unital` should rather be provided as
`TestObjectsOverBaseRing.Blue`.
>
> This result is temporary, as I still seem to miss a couple of category
> classes. However, what does it tell us?
>
> On the plus side, all "real" examples work consistently.
>
> On the negative side, a consistent choice of local spanning tree data
does
> depend on choosing a monomial order. This order is nowhere explicit, but
with
> some orders the choices made in educational examples fail. Who can
guarantee
> that the same will never happen in future real world examples, unless we
make
> the implicit order explicit?
Let me state it in bold: the current algorithm has been designed so
that *there is no local-global problem*. The global consistency
conditions that you are trying to impose on the code are *not*
required by the current specifications. You need a tree, but the tree
need not be that of standard monomials for whatever term order. One
can for example very well choose to implement an axiom category as
Cs.A.B in a category Cs, and in Ds.B.A in a subcategory.
When I claimed the code was correct, I really meant that the
infrastructure algorithm was correct. That is, not only the current
category code works properly, but every new category/axiom code
written that respects the specifications given in the axiom
documentation should work properly.
You are of course very well entitled to not believe me and I am glad
that you are checking my claims. Which is why I'll try today to
formalize a proof of the infrastructure. One of the point is that the
algorithm computes a normal form, but that normal form is given by the
lattice structure itself, without a need for a term order. The
computations occur in a concrete lattice, not in the free lattice
modulo relations.
In the mean time, a hint is the fact that the algorithm gives correct
results even on examples where there are local choices that do not
satisfy your global consistency conditions (I am of course excluding
the example which breaks voluntarily the current specifications).
Cheers,
Nicolas
--
Ticket URL: <http://trac.sagemath.org/ticket/10963#comment:437>
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.
