[Agda] (Semi)RingWithOne

[Sergei Meshveliani]

Dear all,

This is a certain minor point about algebra in Standard library.
I am writing a certain application that relies on Standard library
algebra, from Semigroup up to CommutativeRing.
And I observe the following.

(I) A classical book by Lang (1968) defines that a Ring has an unity
element by multiplication.

(II) A classical book by Van Der Waerden (1971) defines that a Ring does
not necessary has unity. If it has, people call it "Ring with unity".
I expected that in Standard library it would be called RinWithOne.
But I do not find such there.

(III) Standard library defines that Semiring has unity (1#),
and Ring inherits Semiring, so that Ring always has an unity element
by multiplication. And this agrees with (I).
(and naturally, the name RingWithOne is skipped).

(IV) But Standard library also introduces SemiringWithoutOne.
-------

(V) Even integer numbers occur a Ring according to (II),
but not according to (I).


Summing all this, I think that this will be more natural for Standard
library
* to define Ring as in (II),
* to define Semiring with skipping 1# (instead of SemiringWihoutOne),
* to define SemiringWithOne as including 1#,
* to define RingWithOne as inheriting SemiringWithOne.

-- ?

Regards,

------
Sergei

[Matthew Daggitt]

Hi Sergei,
Without wishing to get into a citation war, I think there is no clear
consensus that (semi)rings are traditionally defined without a
multiplicative identity. Indeed in every course or textbook I've seen,
they've come with a one defined. Of course that may be a cultural thing.
However given that it's not necessarily clear which way is most common, I
think the standard library will err on the side of sticking with the
current definition. To do otherwise would raise a lot of backwards
compatibility issues with other people's code.

I'm also a bit confused by your statement that the integer numbers does not
have a one. Surely the multiplicative identity of the integers is just "1"?

If there is anything else we can do in the existing framework of the
standard library to help you use the current definitions, do let us know
and we'll consider it for addition.
Best,
Matthew

Post by Sergei Meshveliani
Dear all,
This is a certain minor point about algebra in Standard library.
I am writing a certain application that relies on Standard library
algebra, from Semigroup up to CommutativeRing.
And I observe the following.
(I) A classical book by Lang (1968) defines that a Ring has an unity
element by multiplication.
(II) A classical book by Van Der Waerden (1971) defines that a Ring does
not necessary has unity. If it has, people call it "Ring with unity".
I expected that in Standard library it would be called RinWithOne.
But I do not find such there.
(III) Standard library defines that Semiring has unity (1#),
and Ring inherits Semiring, so that Ring always has an unity element
by multiplication. And this agrees with (I).
(and naturally, the name RingWithOne is skipped).
(IV) But Standard library also introduces SemiringWithoutOne.
-------
(V) Even integer numbers occur a Ring according to (II),
but not according to (I).
Summing all this, I think that this will be more natural for Standard
library
* to define Ring as in (II),
* to define Semiring with skipping 1# (instead of SemiringWihoutOne),
* to define SemiringWithOne as including 1#,
* to define RingWithOne as inheriting SemiringWithOne.
-- ?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Matthew Daggitt
Hi Sergei,
Without wishing to get into a citation war, I think there is no clear
consensus that (semi)rings are traditionally defined without a
multiplicative identity. Indeed in every course or textbook I've seen,
they've come with a one defined. Of course that may be a cultural
thing. However given that it's not necessarily clear which way is most
common, I think the standard library will err on the side of sticking
with the current definition. To do otherwise would raise a lot of
backwards compatibility issues with other people's code.

All right.

Post by Matthew Daggitt
I'm also a bit confused by your statement that the integer numbers
does not have a one. Surely the multiplicative identity of the
integers is just "1"?

Post by Sergei Meshveliani
(V) Even integer numbers occur a Ring according to (II),
but not according to (I).

I have run into a play on words.
The word `even' also has mathematical meanings.
By "Even integer numbers" I meant the set Z2 of even integers:
Z2 = {2 * n | n <- Integer}.

The operations 0, +, -_, * restricted on Z2 satisfy the ring axioms --
except the unity one for multiplication
(if I am not missing something).

------
Sergei

Post by Matthew Daggitt
If there is anything else we can do in the existing framework of the
standard library to help you use the current definitions, do let us
know and we'll consider it for addition.
Best,
Matthew
Dear all,
This is a certain minor point about algebra in Standard library.
I am writing a certain application that relies on Standard library
algebra, from Semigroup up to CommutativeRing.
And I observe the following.
(I) A classical book by Lang (1968) defines that a Ring has an unity
element by multiplication.
(II) A classical book by Van Der Waerden (1971) defines that a Ring does
not necessary has unity. If it has, people call it "Ring with unity".
I expected that in Standard library it would be called
RinWithOne.
But I do not find such there.
(III) Standard library defines that Semiring has unity (1#),
and Ring inherits Semiring, so that Ring always has an unity element
by multiplication. And this agrees with (I).
(and naturally, the name RingWithOne is skipped).
(IV) But Standard library also introduces SemiringWithoutOne.
-------
(V) Even integer numbers occur a Ring according to (II),
but not according to (I).
Summing all this, I think that this will be more natural for Standard
library
* to define Ring as in (II),
* to define Semiring with skipping 1# (instead of
SemiringWihoutOne),
* to define SemiringWithOne as including 1#,
* to define RingWithOne as inheriting SemiringWithOne.
-- ?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda