Changes to products.

[Waldek Hebisch]

I would like to reorganize products. I have created a new
category called AbelianProductCategory with source below:

)abbrev category APRODC AbelianProductCategory
AbelianProductCategory(A : Type) : Category == with
if A has AbelianMonoid then AbelianMonoid
if A has CancellationAbelianMonoid then CancellationAbelianMonoid
if A has AbelianGroup then AbelianGroup

I have changed IndexedDirectProductCategory so that is exports
AbelianProductCategory. After that I merged
IndexedDirectProductOrderedAbelianMonoid,
IndexedDirectProductOrderedAbelianMonoidSup and
IndexedDirectProductAbelianGroup into
IndexedDirectProductObject. You can see my current
wersion of IndexedDirectProductCategory and
IndexedDirectProductObject at:

http://www.math.uni.wroc.pl/~hebisch/fricas/IDPC.spad

http://www.math.uni.wroc.pl/~hebisch/fricas/IDPO.spad

I would like to weaken restrictions in AbelianMonoidRing and
possibly also MonoidRing so that argument can be a semiring
(currently I have a problem with Spad compiler when I try
to do this).

The idea is to have less restrictions in toplevel categories
and propagate structure when present. In particular I want
better support for semirings (actually, I started this to
have polynomials with coefficients in a semiring).

Looking at other categories I see that logically DirectProductCategory
is quite similar to IndexedDirectProductCategory. One difference
is that DirectProductCategory is indexed by integers from 1 to n.
Another is that DirectProductCategory propagates more properties.
In particular, DirectProductCategory category propagates coordinatwise
multiplication. Since IndexedDirectProductCategory is used
to define polynomial (which have its own multiplication) we
do not want coordinatwise multiplication on IndexedDirectProductCategory.
However, it would be nice to factor out similarities and
make things more regular.

--
Waldek Hebisch
heb...@math.uni.wroc.pl