Coverage for local/lib/python2.7/site-packages/sage/categories/category_with_axiom.py : 54%

""" 

Axioms 

This documentation covers how to implement axioms and proceeds with an 

overview of the implementation of the axiom infrastructure. It assumes 

that the reader is familiar with the :ref:`category primer 

<sage.categories.primer>`, and in particular its :ref:`section about 

axioms <category-primer-axioms>`. 

Implementing axioms 

=================== 

Simple case involving a single predefined axiom 

----------------------------------------------- 

Suppose that one wants to provide code (and documentation, tests, ...) 

for the objects of some existing category ``Cs()`` that satisfy some 

predefined axiom ``A``. 

The first step is to open the hood and check whether there already 

exists a class implementing the category ``Cs().A()``. For example, 

taking ``Cs=Semigroups`` and the ``Finite`` axiom, there already 

exists a class for the category of finite semigroups:: 

sage: Semigroups().Finite() 

Category of finite semigroups 

sage: type(Semigroups().Finite()) 

<class 'sage.categories.finite_semigroups.FiniteSemigroups_with_category'> 

In this case, we say that the category of semigroups *implements* the 

axiom ``Finite``, and code about finite semigroups should go in the 

class :class:`FiniteSemigroups` (or, as usual, in its nested classes 

``ParentMethods``, ``ElementMethods``, and so on). 

On the other hand, there is no class for the category of infinite 

semigroups:: 

sage: Semigroups().Infinite() 

Category of infinite semigroups 

sage: type(Semigroups().Infinite()) 

<class 'sage.categories.category.JoinCategory_with_category'> 

This category is indeed just constructed as the intersection of the 

categories of semigroups and of infinite sets respectively:: 

sage: Semigroups().Infinite().super_categories() 

[Category of semigroups, Category of infinite sets] 

In this case, one needs to create a new class to implement the axiom 

``Infinite`` for this category. This boils down to adding a nested 

class ``Semigroups.Infinite`` inheriting from :class:`CategoryWithAxiom`. 

In the following example, we implement a category ``Cs``, with a 

subcategory for the objects satisfying the ``Finite`` axiom defined in 

the super category ``Sets`` (we will see later on how to *define* new 

axioms):: 

sage: from sage.categories.category_with_axiom import CategoryWithAxiom 

sage: class Cs(Category): 

....: def super_categories(self): 

....: return [Sets()] 

....: class Finite(CategoryWithAxiom): 

....: class ParentMethods: 

....: def foo(self): 

....: print("I am a method on finite C's") 

:: 

sage: Cs().Finite() 

Category of finite cs 

sage: Cs().Finite().super_categories() 

[Category of finite sets, Category of cs] 

sage: Cs().Finite().all_super_categories() 

[Category of finite cs, Category of finite sets, 

Category of cs, Category of sets, ...] 

sage: Cs().Finite().axioms() 

frozenset({'Finite'}) 

Now a parent declared in the category ``Cs().Finite()`` inherits from 

all the methods of finite sets and of finite `C`'s, as desired:: 

sage: P = Parent(category=Cs().Finite()) 

sage: P.is_finite() # Provided by Sets.Finite.ParentMethods 

True 

sage: P.foo() # Provided by Cs.Finite.ParentMethods 

I am a method on finite C's 

.. _category-with-axiom-design: 

.. NOTE:: 

- This follows the same idiom as for 

:ref:`sage.categories.covariant_functorial_construction`. 

- From an object oriented point of view, any subcategory ``Cs()`` 

of :class:`Sets` inherits a ``Finite`` method. Usually ``Cs`` 

could complement this method by overriding it with a method 

``Cs.Finite`` which would make a super call to ``Sets.Finite`` 

and then do extra stuff. 

In the above example, ``Cs`` also wants to complement 

``Sets.Finite``, though not by doing more stuff, but by 

providing it with an additional mixin class containing the code 

for finite ``Cs``. To keep the analogy, this mixin class is to 

be put in ``Cs.Finite``. 

- By defining the axiom ``Finite``, :class:`Sets` fixes the 

semantic of ``Cs.Finite()`` for all its subcategories ``Cs``: 

namely "the category of ``Cs`` which are finite as sets". Hence, 

for example, ``Modules.Free.Finite`` cannot be used to model the 

category of free modules of finite rank, even though their 

traditional name "finite free modules" might suggest it. 

- It may come as a surprise that we can actually use the same name 

``Finite`` for the mixin class and for the method defining the 

axiom; indeed, by default a class does not have a binding 

behavior and would completely override the method. See the 

section :ref:`axioms-defining-a-new-axiom` for details and the 

rationale behind it. 

An alternative would have been to give another name to the mixin 

class, like ``FiniteCategory``. However this would have resulted 

in more namespace pollution, whereas using ``Finite`` is already 

clear, explicit, and easier to remember. 

- Under the hood, the category ``Cs().Finite()`` is aware that it 

has been constructed from the category ``Cs()`` by adding the 

axiom ``Finite``:: 

sage: Cs().Finite().base_category() 

Category of cs 

sage: Cs().Finite()._axiom 

'Finite' 

Over time, the nested class ``Cs.Finite`` may become large and too 

cumbersome to keep as a nested subclass of ``Cs``. Or the category with 

axiom may have a name of its own in the literature, like *semigroups* 

rather than *associative magmas*, or *fields* rather than *commutative 

division rings*. In this case, the category with axiom can be put 

elsewhere, typically in a separate file, with just a link from 

``Cs``:: 

sage: class Cs(Category): 

....: def super_categories(self): 

....: return [Sets()] 

sage: class FiniteCs(CategoryWithAxiom): 

....: class ParentMethods: 

....: def foo(self): 

....: print("I am a method on finite C's") 

sage: Cs.Finite = FiniteCs 

sage: Cs().Finite() 

Category of finite cs 

For a real example, see the code of the class :class:`FiniteGroups` and the 

link to it in :class:`Groups`. Note that the link is implemented using 

:class:`~sage.misc.lazy_import.LazyImport`; this is highly recommended: it 

makes sure that :class:`FiniteGroups` is imported after :class:`Groups` it 

depends upon, and makes it explicit that the class :class:`Groups` can be 

imported and is fully functional without importing :class:`FiniteGroups`. 

.. NOTE:: 

Some categories with axioms are created upon Sage's startup. In such a 

case, one needs to pass the ``at_startup=True`` option to 

:class:`~sage.misc.lazy_import.LazyImport`, in order to quiet the warning 

about that lazy import being resolved upon startup. See for example 

``Sets.Finite``. 

This is undoubtedly a code smell. Nevertheless, it is preferable 

to stick to lazy imports, first to resolve the import order 

properly, and more importantly as a reminder that the category 

would be best not constructed upon Sage's startup. This is to spur 

developers to reduce the number of parents (and therefore 

categories) that are constructed upon startup. Each 

``at_startup=True`` that will be removed will be a measure of 

progress in this direction. 

.. NOTE:: 

In principle, due to a limitation of 

:class:`~sage.misc.lazy_import.LazyImport` with nested classes (see 

:trac:`15648`), one should pass the option ``as_name`` to 

:class:`~sage.misc.lazy_import.LazyImport`:: 

Finite = LazyImport('sage.categories.finite_groups', 'FiniteGroups', as_name='Finite') 

in order to prevent ``Groups.Finite`` to keep on reimporting 

``FiniteGroups``. 

Given that passing this option introduces some redundancy and is 

error prone, the axiom infrastructure includes a little workaround 

which makes the ``as_name`` unnecessary in this case. 

Making the category with axiom directly callable 

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 

If desired, a category with axiom can be constructed directly through 

its class rather than through its base category:: 

sage: Semigroups() 

Category of semigroups 

sage: Semigroups() is Magmas().Associative() 

True 

sage: FiniteGroups() 

Category of finite groups 

sage: FiniteGroups() is Groups().Finite() 

True 

For this notation to work, the class :class:`Semigroups` needs to be 

aware of the base category class (here, :class:`Magmas`) and of the 

axiom (here, ``Associative``):: 

sage: Semigroups._base_category_class_and_axiom 

(<class 'sage.categories.magmas.Magmas'>, 'Associative') 

sage: Fields._base_category_class_and_axiom 

(<class 'sage.categories.division_rings.DivisionRings'>, 'Commutative') 

sage: FiniteGroups._base_category_class_and_axiom 

(<class 'sage.categories.groups.Groups'>, 'Finite') 

sage: FiniteDimensionalAlgebrasWithBasis._base_category_class_and_axiom 

(<class 'sage.categories.algebras_with_basis.AlgebrasWithBasis'>, 'FiniteDimensional') 

In our example, the attribute ``_base_category_class_and_axiom`` was 

set upon calling ``Cs().Finite()``, which makes the notation seemingly 

work:: 

sage: FiniteCs() 

Category of finite cs 

sage: FiniteCs._base_category_class_and_axiom 

(<class '__main__.Cs'>, 'Finite') 

sage: FiniteCs._base_category_class_and_axiom_origin 

'set by __classget__' 

But calling ``FiniteCs()`` right after defining the class would have 

failed (try it!). In general, one needs to set the attribute explicitly:: 

sage: class FiniteCs(CategoryWithAxiom): 

....: _base_category_class_and_axiom = (Cs, 'Finite') 

....: class ParentMethods: 

....: def foo(self): 

....: print("I am a method on finite C's") 

Having to set explicitly this link back from ``FiniteCs`` to ``Cs`` 

introduces redundancy in the code. It would therefore be desirable to 

have the infrastructure set the link automatically instead (a 

difficulty is to achieve this while supporting lazy imported 

categories with axiom). 

As a first step, the link is set automatically upon accessing the 

class from the base category class:: 

sage: Algebras.WithBasis._base_category_class_and_axiom 

(<class 'sage.categories.algebras.Algebras'>, 'WithBasis') 

sage: Algebras.WithBasis._base_category_class_and_axiom_origin 

'set by __classget__' 

Hence, for whatever this notation is worth, one can currently do:: 

sage: Algebras.WithBasis(QQ) 

Category of algebras with basis over Rational Field 

We don't recommend using syntax like ``Algebras.WithBasis(QQ)``, as it 

may eventually be deprecated. 

As a second step, Sage tries some obvious heuristics to deduce the link 

from the name of the category with axiom (see 

:func:`base_category_class_and_axiom` for the details). This typically 

covers the following examples:: 

sage: FiniteCoxeterGroups() 

Category of finite coxeter groups 

sage: FiniteCoxeterGroups() is CoxeterGroups().Finite() 

True 

sage: FiniteCoxeterGroups._base_category_class_and_axiom_origin 

'deduced by base_category_class_and_axiom' 

sage: FiniteDimensionalAlgebrasWithBasis(QQ) 

Category of finite dimensional algebras with basis over Rational Field 

sage: FiniteDimensionalAlgebrasWithBasis(QQ) is Algebras(QQ).FiniteDimensional().WithBasis() 

True 

If the heuristic succeeds, the result is guaranteed to be correct. If 

it fails, typically because the category has a name of its own like 

:class:`Fields`, the attribute ``_base_category_class_and_axiom`` 

should be set explicitly. For more examples, see the code of the 

classes :class:`Semigroups` or :class:`Fields`. 

.. NOTE:: 

When printing out a category with axiom, the heuristic determines 

whether a category has a name of its own by checking out how 

``_base_category_class_and_axiom`` was set:: 

sage: Fields._base_category_class_and_axiom_origin 

'hardcoded' 

See :meth:`CategoryWithAxiom._without_axioms`, 

:meth:`CategoryWithAxiom._repr_object_names_static`. 

In our running example ``FiniteCs``, Sage failed to deduce 

automatically the base category class and axiom because the class 

``Cs`` is not in the standard location ``sage.categories.cs``. 

.. TOPIC:: Design discussion 

The above deduction, based on names, is undoubtedly inelegant. But 

it's safe (either the result is guaranteed to be correct, or an 

error is raised), it saves on some redundant information, and it 

is only used for the simple shorthands like ``FiniteGroups()`` for 

``Groups().Finite()``. Finally, most if not all of these 

shorthands are likely to eventually disappear (see :trac:`15741` 

and the :ref:`related discussion in the primer 

<category-primer-axioms-single-entry-point>`). 

.. _axioms-defining-a-new-axiom: 

Defining a new axiom 

-------------------- 

We describe now how to define a new axiom. The first step is to figure 

out the largest category where the axiom makes sense. For example 

``Sets`` for ``Finite``, ``Magmas`` for ``Associative``, or 

``Modules`` for ``FiniteDimensional``. Here we define the axiom 

``Green`` for the category ``Cs`` and its subcategories:: 

sage: from sage.categories.category_with_axiom import CategoryWithAxiom 

sage: class Cs(Category): 

....: def super_categories(self): 

....: return [Sets()] 

....: class SubcategoryMethods: 

....: def Green(self): 

....: '<documentation of the axiom Green>' 

....: return self._with_axiom("Green") 

....: class Green(CategoryWithAxiom): 

....: class ParentMethods: 

....: def foo(self): 

....: print("I am a method on green C's") 

With the current implementation, the name of the axiom must also be 

added to a global container:: 

sage: all_axioms = sage.categories.category_with_axiom.all_axioms 

sage: all_axioms += ("Green",) 

We can now use the axiom as usual:: 

sage: Cs().Green() 

Category of green cs 

sage: P = Parent(category=Cs().Green()) 

sage: P.foo() 

I am a method on green C's 

Compared with our first example, the only newcomer is the method 

``.Green()`` that can be used by any subcategory ``Ds()`` of ``Cs()`` 

to add the axiom ``Green``. Note that the expression ``Ds().Green`` 

always evaluates to this method, regardless of whether ``Ds`` has a 

nested class ``Ds.Green`` or not (an implementation detail):: 

sage: Cs().Green 

<bound method Cs_with_category.Green of Category of cs> 

Thanks to this feature (implemented in :meth:`CategoryWithAxiom.__classget__`), 

the user is systematically referred to the documentation of this 

method when doing introspection on ``Ds().Green``:: 

sage: C = Cs() 

sage: C.Green? # not tested 

sage: Cs().Green.__doc__ 

'<documentation of the axiom Green>' 

It is therefore the natural spot for the documentation of the axiom. 

.. NOTE:: 

The presence of the nested class ``Green`` in ``Cs`` is currently 

mandatory even if it is empty. 

.. TODO:: 

Specify whether or not one should systematically use 

@cached_method in the definition of the axiom. And make sure all 

the definition of axioms in Sage are consistent in this respect! 

.. TODO:: 

We could possibly define an @axiom decorator? This could hide two 

little implementation details: whether or not to make the method a 

cached method, and the call to _with_axiom(...) under the hood. It 

could do possibly do some more magic. The gain is not obvious though. 

.. NOTE:: 

``all_axioms`` is only used marginally, for sanity checks and when 

trying to derive automatically the base category class. The order 

of the axioms in this tuple also controls the order in which they 

appear when printing out categories with axioms (see 

:meth:`CategoryWithAxiom._repr_object_names_static`). 

During a Sage session, new axioms should only be added at the *end* 

of ``all_axioms``, as above, so as to not break the cache of 

:func:`axioms_rank`. Otherwise, they can be inserted statically 

anywhere in the tuple. For axioms defined within the Sage library, 

the name is best inserted by editing directly the definition of 

``all_axioms`` in :mod:`sage.categories.category_with_axiom`. 

.. TOPIC:: Design note 

Let us state again that, unlike what the existence of 

``all_axioms`` might suggest, the definition of an axiom is local 

to a category and its subcategories. In particular, two 

independent categories ``Cs()`` and ``Ds()`` can very well define 

axioms with the same name and different semantics. As long as the 

two hierarchies of subcategories don't intersect, this is not a 

problem. And if they do intersect naturally (that is if one is 

likely to create a parent belonging to both categories), this 

probably means that the categories ``Cs`` and ``Ds`` are about 

related enough areas of mathematics that one should clear the 

ambiguity by having either the same semantic or different names. 

This caveat is no different from that of name clashes in hierarchy 

of classes involving multiple inheritance. 

.. TODO:: 

Explore ways to get rid of this global ``all_axioms`` tuple, 

and/or have automatic registration there, and/or having a 

register_axiom(...) method. 

Special case: defining an axiom depending on several categories 

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 

In some cases, the largest category where the axiom makes sense is the 

intersection of two categories. This is typically the case for axioms 

specifying compatibility conditions between two otherwise unrelated 

operations, like ``Distributive`` which specifies a compatibility 

between `*` and `+`. Ideally, we would want the ``Distributive`` axiom 

to be defined by:: 

sage: Magmas() & AdditiveMagmas() 

Join of Category of magmas and Category of additive magmas 

The current infrastructure does not support this perfectly: indeed, 

defining an axiom for a category `C` requires `C` to have a class of 

its own; hence a :class:`~.category.JoinCategory` as above won't do; 

we need to implement a new class like 

:class:`~.magmas_and_additive_magmas.MagmasAndAdditiveMagmas`; 

furthermore, we cannot yet model the fact that ``MagmasAndAdditiveMagmas()`` 

*is* the intersection of ``Magmas()`` and ``AdditiveMagmas()`` rather than a 

mere subcategory:: 

sage: from sage.categories.magmas_and_additive_magmas import MagmasAndAdditiveMagmas 

sage: Magmas() & AdditiveMagmas() is MagmasAndAdditiveMagmas() 

False 

sage: Magmas() & AdditiveMagmas() # todo: not implemented 

Category of magmas and additive magmas 

Still, there is a workaround to get the natural notations:: 

sage: (Magmas() & AdditiveMagmas()).Distributive() 

Category of distributive magmas and additive magmas 

sage: (Monoids() & CommutativeAdditiveGroups()).Distributive() 

Category of rings 

The trick is to define ``Distributive`` as usual in 

:class:`~.magmas_and_additive_magmas.MagmasAndAdditiveMagmas`, and to 

add a method :meth:`Magmas.SubcategoryMethods.Distributive` which 

checks that ``self`` is a subcategory of both ``Magmas()`` and 

``AdditiveMagmas()``, complains if not, and otherwise takes the 

intersection of ``self`` with ``MagmasAndAdditiveMagmas()`` before 

calling ``Distributive``. 

The downsides of this workaround are: 

- Creation of an otherwise empty class 

:class:`~.magmas_and_additive_magmas.MagmasAndAdditiveMagmas`. 

- Pollution of the namespace of ``Magmas()`` (and subcategories like 

``Groups()``) with a method that is irrelevant (but safely complains 

if called). 

- ``C._with_axiom('Distributive')`` is not strictly equivalent to 

``C.Distributive()``, which can be unpleasantly surprising:: 

sage: (Monoids() & CommutativeAdditiveGroups()).Distributive() 

Category of rings 

sage: (Monoids() & CommutativeAdditiveGroups())._with_axiom('Distributive') 

Join of Category of monoids and Category of commutative additive groups 

.. TODO:: 

Other categories that would be better implemented via an axiom 

depending on a join category include: 

- :class:`Algebras`: defining an associative unital algebra as a 

ring and a module satisfying the suitable compatibility axiom 

between inner multiplication and multiplication by scalars 

(bilinearity). Of course this should be implemented at the level 

of :class:`~.magmatic_algebras.MagmaticAlgebras`, if not higher. 

- :class:`Bialgebras`: defining an bialgebra as an algebra and 

coalgebra where the coproduct is a morphism for the product. 

- :class:`Bimodules`: defining a bimodule as a left and right 

module where the two actions commute. 

.. TODO:: 

- Design and implement an idiom for the definition of an axiom by a join 

category. 

- Or support more advanced joins, through some hook or registration 

process to specify that a given category *is* the intersection of two 

(or more) categories. 

- Or at least improve the above workaround to avoid the last issue; this 

possibly could be achieved using a class ``Magmas.Distributive`` with a 

bit of ``__classcall__`` magic. 

Handling multiple axioms, arborescence structure of the code 

------------------------------------------------------------ 

Prelude 

^^^^^^^ 

Let us consider the category of magmas, together with two of its 

axioms, namely ``Associative`` and ``Unital``. An associative magma is 

a *semigroup* and a unital semigroup is a *monoid*. We have also seen 

that axioms commute:: 

sage: Magmas().Unital() 

Category of unital magmas 

sage: Magmas().Associative() 

Category of semigroups 

sage: Magmas().Associative().Unital() 

Category of monoids 

sage: Magmas().Unital().Associative() 

Category of monoids 

At the level of the classes implementing these categories, the 

following comes as a general naturalization of the previous section:: 

sage: Magmas.Unital 

<class 'sage.categories.magmas.Magmas.Unital'> 

sage: Magmas.Associative 

<class 'sage.categories.semigroups.Semigroups'> 

sage: Magmas.Associative.Unital 

<class 'sage.categories.monoids.Monoids'> 

However, the following may look suspicious at first:: 

sage: Magmas.Unital.Associative 

Traceback (most recent call last): 

... 

AttributeError: type object 'Magmas.Unital' has no attribute 'Associative' 

The purpose of this section is to explain the design of the code 

layout and the rationale for this mismatch. 

Abstract model 

^^^^^^^^^^^^^^ 

As we have seen in the :ref:`Primer <category-primer-axioms-explosion>`, 

the objects of a category ``Cs()`` can usually satisfy, or not, many 

different axioms. Out of all combinations of axioms, only a small 

number are relevant in practice, in the sense that we actually want to 

provide features for the objects satisfying these axioms. 

Therefore, in the context of the category class ``Cs``, we want to 

provide the system with a collection `(D_S)_{S\in \mathcal S}` where 

each `S` is a subset of the axioms and the corresponding `D_S` is a 

class for the subcategory of the objects of ``Cs()`` satisfying the 

axioms in `S`. For example, if ``Cs()`` is the category of magmas, the 

pairs `(S, D_S)` would include:: 

{Associative} : Semigroups 

{Associative, Unital} : Monoids 

{Associative, Unital, Inverse}: Groups 

{Associative, Commutative} : Commutative Semigroups 

{Unital, Inverse} : Loops 

Then, given a subset `T` of axioms, we want the system to be able to 

select automatically the relevant classes 

`(D_S)_{S\in \mathcal S, S\subset T}`, 

and build from them a category for the objects of ``Cs`` satisfying 

the axioms in `T`, together with its hierarchy of super categories. If 

`T` is in the indexing set `\mathcal S`, then the class of the 

resulting category is directly `D_T`:: 

sage: C = Magmas().Unital().Inverse().Associative(); C 

Category of groups 

sage: type(C) 

<class 'sage.categories.groups.Groups_with_category'> 

Otherwise, we get a join category:: 

sage: C = Magmas().Infinite().Unital().Associative(); C 

Category of infinite monoids 

sage: type(C) 

<class 'sage.categories.category.JoinCategory_with_category'> 

sage: C.super_categories() 

[Category of monoids, Category of infinite sets] 

Concrete model as an arborescence of nested classes 

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 

We further want the construction to be efficient and amenable to 

laziness. This led us to the following design decision: the collection 

`(D_S)_{S\in \mathcal S}` of classes should be structured as an 

arborescence (or equivalently a *rooted forest*). The root is ``Cs``, 

corresponding to `S=\emptyset`. Any other class `D_S` should be the 

child of a single class `D_{S'}` where `S'` is obtained from `S` by 

removing a single axiom `A`. Of course, `D_{S'}` and `A` are 

respectively the base category class and axiom of the category with 

axiom `D_S` that we have met in the first section. 

At this point, we urge the reader to explore the code of 

:class:`Magmas` and 

:class:`~.distributive_magmas_and_additive_magmas.DistributiveMagmasAndAdditiveMagmas` 

and see how the arborescence structure on the categories with axioms 

is reflected by the nesting of category classes. 

Discussion of the design 

^^^^^^^^^^^^^^^^^^^^^^^^ 

Performance 

~~~~~~~~~~~ 

Thanks to the arborescence structure on subsets of axioms, 

constructing the hierarchy of categories and computing intersections 

can be made efficient with, roughly speaking, a linear/quadratic 

complexity in the size of the involved category hierarchy multiplied 

by the number of axioms (see Section :ref:`axioms-algorithmic`). This 

is to be put in perspective with the manipulation of arbitrary 

collections of subsets (aka boolean functions) which can easily raise 

NP-hard problems. 

Furthermore, thanks to its locality, the algorithms can be made 

suitably lazy: in particular, only the involved category classes need 

to be imported. 

Flexibility 

~~~~~~~~~~~ 

This design also brings in quite some flexibility, with the 

possibility to support features such as defining new axioms depending 

on other axioms and deduction rules. See below. 

Asymmetry 

~~~~~~~~~ 

As we have seen at the beginning of this section, this design 

introduces an asymmetry. It's not so bad in practice, since in most 

practical cases, we want to work incrementally. It's for example more 

natural to describe :class:`FiniteFields` as :class:`Fields` with the 

axiom ``Finite`` rather than :class:`Magmas` and 

:class:`AdditiveMagmas` with all (or at least sufficiently many) of 

the following axioms:: 

sage: sorted(Fields().axioms()) 

['AdditiveAssociative', 'AdditiveCommutative', 'AdditiveInverse', 

'AdditiveUnital', 'Associative', 'Commutative', 'Distributive', 

'Division', 'NoZeroDivisors', 'Unital'] 

The main limitation is that the infrastructure currently imposes to be 

incremental by steps of a single axiom. 

In practice, among the roughly 60 categories with axioms that are 

currently implemented in Sage, most admitted a (rather) natural choice 

of a base category and single axiom to add. For example, one usually 

thinks more naturally of a monoid as a semigroup which is unital 

rather than as a unital magma which is associative. Modeling this 

asymmetry in the code actually brings a bonus: it is used for printing 

out categories in a (heuristically) mathematician-friendly way:: 

sage: Magmas().Commutative().Associative() 

Category of commutative semigroups 

Only in a few cases is a choice made that feels mathematically 

arbitrary. This is essentially in the chain of nested classes 

:class:`.distributive_magmas_and_additive_magmas.DistributiveMagmasAndAdditiveMagmas.AdditiveAssociative.AdditiveCommutative.AdditiveUnital.Associative`. 

Placeholder classes 

~~~~~~~~~~~~~~~~~~~ 

Given that we can only add a single axiom at a time when implementing 

a :class:`CategoryWithAxiom`, we need to create a few category classes 

that are just placeholders. For the worst example, see the chain of 

nested classes 

:class:`.distributive_magmas_and_additive_magmas.DistributiveMagmasAndAdditiveMagmas.AdditiveAssociative.AdditiveCommutative.AdditiveUnital.Associative`. 

This is suboptimal, but fits within the scope of the axiom 

infrastructure which is to reduce a potentially exponential number of 

placeholder category classes to just a couple. 

Note also that, in the above example, it's likely that some of the 

intermediate classes will grow to non placeholder ones, as people will 

explore more weaker variants of rings. 

Mismatch between the arborescence of nested classes and the hierarchy of categories 

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 

The fact that the hierarchy relation between categories is not 

reflected directly as a relation between the classes may sound 

suspicious at first! However, as mentioned in the primer, this is 

actually a big selling point of the axioms infrastructure: by 

calculating automatically the hierarchy relation between categories 

with axioms one avoids the nightmare of maintaining it by hand. 

Instead, only a rather minimal number of links needs to be maintainted 

in the code (one per category with axiom). 

Besides, with the flexibility introduced by runtime deduction rules 

(see below), the hierarchy of categories may depend on the parameters 

of the categories and not just their class. So it's fine to make it 

clear from the onset that the two relations do not match. 

Evolutivity 

~~~~~~~~~~~ 

At this point, the arborescence structure has to be hardcoded by hand 

with the annoyances we have seen. This does not preclude, in a future 

iteration, to design and implement some idiom for categories with 

axioms that adds several axioms at once to a base category; maybe some 

variation around:: 

class DistributiveMagmasAndAdditiveMagmas: 

... 

@category_with_axiom( 

AdditiveAssociative, 

AdditiveCommutative, 

AdditiveUnital, 

AdditiveInverse, 

Associative) 

def _(): return LazyImport('sage.categories.rngs', 'Rngs', at_startup=True) 

or:: 

register_axiom_category(DistributiveMagmasAndAdditiveMagmas, 

{AdditiveAssociative, 

AdditiveCommutative, 

AdditiveUnital, 

AdditiveInverse, 

Associative}, 

'sage.categories.rngs', 'Rngs', at_startup=True) 

The infrastructure would then be in charge of building the appropriate 

arborescence under the hood. Or rely on some database (see discussion 

on :trac:`10963`, in particular at the end of comment 332). 

Axioms defined upon other axioms 

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 

Sometimes an axiom can only be defined when some other axiom 

holds. For example, the axiom ``NoZeroDivisors`` only makes sense if 

there is a zero, that is if the axiom ``AdditiveUnital`` holds. Hence, 

for the category 

:class:`~.magmas_and_additive_magmas.MagmasAndAdditiveMagmas`, we 

consider in the abstract model only those subsets of axioms where the 

presence of ``NoZeroDivisors`` implies that of ``AdditiveUnital``. We 

also want the axiom to be only available if meaningful:: 

sage: Rings().NoZeroDivisors() 

Category of domains 

sage: Rings().Commutative().NoZeroDivisors() 

Category of integral domains 

sage: Semirings().NoZeroDivisors() 

Traceback (most recent call last): 

... 

AttributeError: 'Semirings_with_category' object has no attribute 'NoZeroDivisors' 

Concretely, this is to be implemented by defining the new axiom in the 

(``SubcategoryMethods`` nested class of the) appropriate category with 

axiom. For example the axiom ``NoZeroDivisors`` would be naturally 

defined in 

:class:`.magmas_and_additive_magmas.MagmasAndAdditiveMagmas.Distributive.AdditiveUnital`. 

.. NOTE:: 

The axiom ``NoZeroDivisors`` is currently defined in 

:class:`Rings`, by simple lack of need for the feature; it should 

be lifted up as soon as relevant, that is when some code will be 

available for parents with no zero divisors that are not 

necessarily rings. 

.. _axioms-deduction-rules: 

Deduction rules 

^^^^^^^^^^^^^^^ 

A similar situation is when an axiom ``A`` of a category ``Cs`` 

implies some other axiom ``B``, with the same consequence as above on 

the subsets of axioms appearing in the abstract model. For example, a 

division ring necessarily has no zero divisors:: 

sage: 'NoZeroDivisors' in Rings().Division().axioms() 

True 

sage: 'NoZeroDivisors' in Rings().axioms() 

False 

This deduction rule is implemented by the method 

:meth:`Rings.Division.extra_super_categories`:: 

sage: Rings().Division().extra_super_categories() 

(Category of domains,) 

In general, this is to be implemented by a method 

``Cs.A.extra_super_categories`` returning a tuple ``(Cs().B(),)``, or 

preferably ``(Ds().B(),)`` where ``Ds`` is the category defining the 

axiom ``B``. 

This follows the same idiom as for deduction rules about functorial 

constructions (see :meth:`.covariant_functorial_construction.CovariantConstructionCategory.extra_super_categories`). 

For example, the fact that a Cartesian product of associative magmas 

(i.e. of semigroups) is an associative magma is implemented in 

:meth:`Semigroups.CartesianProducts.extra_super_categories`:: 

sage: Magmas().Associative() 

Category of semigroups 

sage: Magmas().Associative().CartesianProducts().extra_super_categories() 

[Category of semigroups] 

Similarly, the fact that the algebra of a commutative magma is 

commutative is implemented in 

:meth:`Magmas.Commutative.Algebras.extra_super_categories`:: 

sage: Magmas().Commutative().Algebras(QQ).extra_super_categories() 

[Category of commutative magmas] 

.. WARNING:: 

In some situations this idiom is inapplicable as it would require 

to implement two classes for the same category. This is the 

purpose of the next section. 

Special case 

~~~~~~~~~~~~ 

In the previous examples, the deduction rule only had an influence on 

the super categories of the category with axiom being constructed. For 

example, when constructing ``Rings().Division()``, the rule 

:meth:`Rings.Division.extra_super_categories` simply adds 

``Rings().NoZeroDivisors()`` as a super category thereof. 

In some situations this idiom is inapplicable because a class for the 

category with axiom under construction already exists elsewhere. Take 

for example Wedderburn's theorem: any finite division ring is 

commutative, i.e. is a finite field. In other words, 

``DivisionRings().Finite()`` *coincides* with ``Fields().Finite()``:: 

sage: DivisionRings().Finite() 

Category of finite enumerated fields 

sage: DivisionRings().Finite() is Fields().Finite() 

True 

Therefore we cannot create a class ``DivisionRings.Finite`` to hold 

the desired ``extra_super_categories`` method, because there is 

already a class for this category with axiom, namely