#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):
Replying to [comment:427 nthiery]:
> Replying to [comment:425 SimonKing]:
> > I have attached [attachment:consistency.py],
... and updated it now, because of some previous typos.
> > which provides routines to check whether Nicolas' local choice of
default constructions for categories with axiom is globally consistent.
>
> Fun :-)
Agreed, but I didn't tell how to use it. So, here it goes: Start sage and
attach the file. Then:
{{{
sage: Bad, I,S,Rel = TestCategoryModel()
Import all category classes
Create boolean polynomial ring with 168 generators
Collect all available axiomatic constructions
=> Found 277 constructions for 256 category classes
8 cases of alternative axiomatic constructions
Testing that default constructions are compatible
Bad: <class 'sage.categories.category_with_axiom.Unital.Blue'> = <class
'sage.categories.category_with_axiom.Blahs.Unital'>.Blue
expected default Blahs*Unital
got Blahs*Blue*Unital
Basis is given by Blahs*Unital
but Blahs*Blue*Unital is no standard monomial
}}}
What I find very strange: Apparently the number of alternative axiomatic
constructions is not well-defined! Namely yesterday I got different
figures.
To be investigated...
Anyway, we find:
{{{
sage: Bad
[(sage.categories.category_with_axiom.Unital.Blue,
Blahs*Blue*Unital,
Blahs*Unital)]
}}}
which means that `Blahs.Unital.Blue` should coincide with `Blahs.Unital`,
which makes perfect sense since
{{{
sage: Blahs().Blue() is Blahs().Unital()
True
}}}
and thus `Blahs().Unital().Blue()` should be the same as
`Blahs().Blue().Blue()`, thus the same as `Blahs().Blue()`, which is
`Blahs().Unital()`. However, we find
{{{
sage: Blahs().Unital().Blue() is Blahs().Blue()
False
}}}
This is a bug, which my test function correctly detects!
Moreover, we have
{{{
sage: len(I)
121
}}}
which means that 121 category classes do not give a reasonable answer when
asked to return an instance.
Finally,
{{{
sage: for rel in Rel.groebner_basis():
....: print rel
....:
Blahs*DistributiveMagmasAndAdditiveMagmas*Flying*Facade*Finite*Commutative*Associative*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
+
Blahs*DistributiveMagmasAndAdditiveMagmas*Flying*Finite*Commutative*Associative*Inverse*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
Blahs*DistributiveMagmasAndAdditiveMagmas*Flying*Finite*Infinite*Commutative*Associative*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
+
Blahs*DistributiveMagmasAndAdditiveMagmas*Flying*Finite*Commutative*Associative*Inverse*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
Blahs*Flying*Unital + Blahs*Flying
Blahs*Blue + Blahs*Unital
TestObjects*Blue + TestObjects*Unital
TestObjectsOverBaseRing*Blue + TestObjectsOverBaseRing*Unital
DistributiveMagmasAndAdditiveMagmas*Facade*Finite*Commutative*Associative*Unital*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
+
DistributiveMagmasAndAdditiveMagmas*Finite*Commutative*Associative*Inverse*Unital*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
DistributiveMagmasAndAdditiveMagmas*Finite*Infinite*Commutative*Associative*Unital*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
+
DistributiveMagmasAndAdditiveMagmas*Finite*Commutative*Associative*Inverse*Unital*Division*NoZeroDivisors*AdditiveCommutative*AdditiveAssociative*AdditiveInverse*AdditiveUnital
}}}
As we can see, most of the relations come from Nicolas' examples, but not
from real mathematical theorems.
One thing really irritates me, though. Yesterday, I also saw relations
{{{
Modules*VectorSpaces==VectorSpaces
}}}
which makes sense: The join of the module category over a base ring and
the vector space category over the same base ring should be the vector
space category, simply since in this case the module category coincides
with the vector space category.
So, why am I not seeing the same relations today??
> > 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.
OK, but then we'd like to have 121 more implementations of
`an_instance()`...
> You are taking some term order here, probably based on some order of
> the axioms, right?
Yes. That's another point that I should change. `BooleanPolynomialRing`
apparently uses a lexicographic ordering by default. What I wanted was a
degrevlex ordering: A construction involving fewer axioms should be
preferred over a construction involving many axioms.
Anyway. The generators of the ring correspond to
1. All category classes that are not category-with-axiom, sorted (I don't
know how Python sorts them).
2. All axioms, in the same order as given in
`sage.categories.category_with_axiom.all_axioms`.
Is the sorting of category classes perhaps depending on the memory
addresses of the classes? This would explain why I get different results
on different runs.
> > 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.
Well, the reason for the complaint is that the axioms `Blue` and `Unital`
do not commute. But applying axioms ''has'' to commute. Hence, the feature
is not "desirable but non-implemented", but it is "mathematically
illegal".
> 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)?
Consistency is a global property. Hence, I think there is no way around to
consider ''all'' category classes at once when testing consistency. It is
clear that this must not happen during startup. Hence, as it is, the
consistency test is a test that may be a tool for a developer wanting to
add a new category.
However, turning things "upside down" is what I want. But I mean a
different thing.
Currently, my functions import all categories, extract from it the local
information that define the category-with-axiom lattice, and then uses
commutative algebra to assert that the local information gives a globally
consistent picture.
Turning this upside down would mean:
- First of all, create a Boolean polynomial ring, whose generators
correspond to the list of basic categories and axioms available in Sage
(this list may grow). Fix a reasonable monomial ordering, best would be a
degree ordering.
- Create an ideal in this ring, whose generators are given by mathematical
results such as Wedderburn's. Compute the Gröbner basis. This Gröbner
basis could be computed once, stored, and then loaded at Sage startup
time. Hence, Sage startup would not suffer from an expensive Gröbner basis
computation, it only is loading a fixed result.
- When creating a category class, the Gröbner basis helps to provide this
class with the available axiomatic constructions (this is what you do with
lazy imports and with `SubcategoryMethods`), and also determines a default
construction for this class (this is the `_base_category_class_and_axiom`
attribute). Commutative algebra ensures consistency of this local
information. This would be implemented by a meta-class for `Category`.
This would be my approach to add more rigour to your category-with-axiom
model, and replace handmade choices of default constructions by something
that scales better.
> 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?
No.
> 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
Which I totally don't like!
Namely, as a consequence, you need to treat `DivisionRings.Finite`
different from `Fields.Finite`: The latter is a (lazily imported) class
stored as a class attribute, the former is a cached method obtained from
Set() and will ''only'' work on instances, not on classes. This asymmetry
is unfortunate, and I think using a metaclass that works with standard
monomials corresponding to default axiomatic constructions is a nice way
to make the implementation symmetric.
You see, if a developer wants to implement a new mathematical theorem on
equality of two axiomatic constructions, then your model is a bit awkward:
(S)he needs to pick one of the constructions to become a cached method on
instances, while the other stays a class attribute. But which of them?
Doing the wrong choice would mean subtle inconsistencies resulting in
difficult to find bugs.
It seems obvious to me that we want that all axiomatic constructions can
be implemented in the same way, and that there is no danger of wrong
choices, because all choices will be made automatic by a method that is
proven to yield well-defined results (namely: Computing normal forms using
Gröbner bases).
In other words: There is a tree structure in the set of standard
monomials. We shouldn't force the developer to put the same tree structure
''manually'' into the class definitions.
> I also believe we don't event need to impose a term order, but that I
> have to think about.
I think we at least want a degree order, so that applying three axioms
will always be preferred over applying four axioms to get the same result.
> 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.
Well, in the case of `Blahs.Blue.Unital`, you did wrong. I don't know if
it was on purpose that you did wrong, but your example shows something
that should never happen, namely axioms that do not commute.
--
Ticket URL: <http://trac.sagemath.org/ticket/10963#comment:429>
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.
