#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):
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.
Idea:
First, we load all available subclasses of `Category`. Those that are not
`CategoryWithAxiom` are "basic" (or atomic?) categories, and correspond to
some generators of a boolean polynomial ring R. The remaining generators
of this ring correspond to the available axioms (there is an exhaustive
list).
Then, for each category class, it is tested what other category class can
be obtained by applying an axiom. Difficulty: Only the default
construction can be given by a class attribute. All other constructions
have to be given on the level of instances. Hence, if C is a category
class and A is an axiom, then C.A might not be available. 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.
Problem: There are a couple of categories that do not provide instances!
Hence, I couldn't test them. So, for now, we restrict on those cases where
we find a way to apply axiom A to category class C, either by an attribute
of the class C, or by using an instance of C.
As we all know, different constructions may yield the same result. This
happens 20ish times. Now, each alternative construction yields a relation
in the lattice that is modelled by the above mentioned boolean polynomial
ring R. Hence, the next step is to create the relation ideal `Rel` of `R`.
And now we are ready to test consistency of the choice of default
constructions: For each category C with axiom, we have the famous
`_base_category_class_and_axiom` attribute. Say, C is obtained from
category class B by applying axiom A.
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`.
As it turns out, this is largely the case.
Problematic cases:
- There are 121 category classes that do no support `an_instance()`. So,
we can't really vouch for complete consistency. Note, in particular, that
`Modules.an_instance()` returns the category of rational vector space,
hence, ''not'' and instance of the class `Modules`.
- In two cases, applying an axiom to a category class does ''not'' return
a category class:
{{{
age: type(sage.categories.category_with_axiom.SmallTestObjects.Connected)
<type 'int'>
sage:
type(sage.categories.category_with_axiom.SmallTestObjects.Commutative)
<type 'classobj'>
}}}
In only two cases, my routine seems to find non-consistent choices.
1. According to the routine, `Modules.WithBasis` should be
`VectorSpaces.WithBasis`. That's clearly an artefact of the above
mentioned problem that `Modules.an_instance()` does not return a category
of modules.
2. In one nonsensical example, my routine finds this inconsistency:
{{{
sage: from sage.categories.category_with_axiom import Blahs
sage: Blahs.Unital.Blue._base_category_class_and_axiom
(sage.categories.category_with_axiom.Blahs.Unital, 'Blue')
sage: Blahs().Blue()
Category of unital blahs
sage: Blahs().Blue() is Blahs().Blue().Unital() is Blahs().Unital()
True
}}}
Axioms are supposed to commute. However, we get
{{{
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.
'''__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()`.
- With the exception of the `Blahs().Unital()` example, Nicolas did a fine
job to build the local data in a globally consistent way.
- 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.
--
Ticket URL: <http://trac.sagemath.org/ticket/10963#comment:425>
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.
