[Agda] (Semi)RingWithOne

[Sergei Meshveliani]

On Tue, 2018-02-27 at 22:51 +0000, Matthew Daggitt wrote:
> 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.


> 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"?

I wrote 
>>  (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
  


> 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
> 
> On Tue, Feb 27, 2018 at 9:11 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         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
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>