#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):
Replying to [comment:425 SimonKing]:
> I have attached [attachment:consistency.py], which provides routines to
check whether Nicolas' local choice of default constructions for
categories with axiom is globally consistent.
Fun :-)
> In this case, I try `C.an_instance().A().__class__.__base__` to get the
class that is used to implement the result of applying axiom A to
instances of category C.
I believe that's the right approach for this need.
> B corresponds to a standard monomial b_monomial, that describes a
construction of B. Axiom A corresponds to a generator of the ring R. The
condition for consistency is simple: `b_monomial*R(A)` has to be a
standard monomial with respect to `Rel`.
You are taking some term order here, probably based on some order of
the axioms, right?
> 2. In one nonsensical example, my routine finds this inconsistency ...
> {{{
> sage: Blahs().Blue().Unital() is Blahs().Unital().Blue()
> False
> sage: Blahs().Blue().Unital() is Blahs().Unital().Blue()
> False
> }}}
> It is thus no surprise that my routine complains here. I won't check
now whether this example is ''supposed'' to demonstrate an illegal
construction.
Yup. This class demonstrates a possibly desirable but non-implemented
feature. See Blahs.Blue_extra_super_categories.
>
> '''__Conclusion__'''
>
> - I think the basic principle of the consistency check is sound.
However, it is incomplete, since a lot of categories do not support
`an_instance()`.
Question: what about turning the problem upside down, and write a
C._test_??? method that checks that everything is consistent within
the context of the super categories of ``C`` (and possibly all axiom
categories you can derive from those, though I guess it's not necessary)?
Since every category class is supposed to be TestSuit'ed, we should
cover all categories this way. Do you think we would get a global
enough view?
An inconvenient is that this would be redundant: we would be checking
over and over the consistency of the semigroup categories while
checking lower categories. This is, or not, a problem depending on the
cost of the check.
> - With the exception of the `Blahs().Unital()` example, Nicolas did a
fine job to build the local data in a globally consistent way.
And I believe that I have no merit in that. I haven't proven it
formally yet, but I am pretty much convinced that as long as the two
following specifications (which I have now described in detail in the
documentation) are satisfied:
- Tree structure on the classes
- If Ds() is a subcategory of Cs() and Ds().A() = Cs().A() then that
axiom should be implemented in Ds.A. And the mathematical theorem
stating the above equality should be implemented in Cs.
then the algorithmic works.
I also believe we don't event need to impose a term order, but that I
have to think about.
> - If we would go the opposite way, we could turn the consistency check
into a method to ''create'' the default constructions of categories in an
automated way (so that Nicolas does not need to choose them manually).
Therefore, in the long run, we could have a database of category classes,
using identifiers that are monomials with respect to some ideal Rel in a
boolean polynomial ring R. Adding a new base category or adding a new
axiom means to add more generators to R. Adding a theorem "these two
constructions yield the same category" add a new generator to the ideal
Rel. Global consistency is guaranteed by letting the default constructions
correspond to standard monomials with respect to Rel. Note that this would
also allow to deal with non-default constructions on the level of category
classes and polynomial ideals, hence, without the problem that
`an_instance()` often does not work.
I always like consistency check. And that one has the bonus of being
fun for commutative algebraist like us :-)
On the other hand, I believe that there is at this point no need to
have a tool for deciding where to put the axiom category. So far I
have always been putting the axiom category where mathematics told me
to put it.
The point is that we are at this point only implementing well known
facts. And the goal of the infrastructure is only to make it easy to
provide only minimal information about those facts and have it derive
the immediate consequences.
One day might come where we will want to use the category
infrastructure to prove *new* facts. But then that would be going to a
completely different level, and we should first discuss seriously with
the scientific communities that work on computer algebra and proofs.
--
Ticket URL: <http://trac.sagemath.org/ticket/10963#comment:427>
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.
