[Agda] Re: Data.Nat.Primality.Prime and irreducibility

[N. Raghavendra]

At 2015-03-07T18:55:53+04:00, Sergei Meshveliani wrote:

>> A lot of the basic stuff about divisibility, irreducibility, primality,
>> coprimality, gcd, lcm, etc., can be done for cancellative commutative
>> monoids, as in, e.g., Jacobson's Basic Algebra, vol. 1, section 2.14
>> (Factorial monoids and rings).  I think it'd be nice to have that
>> generality in stdlib.
>> 
>> []
>
> 1) Consider the ring  R = Integer/(6)   (Integer modulo 6).
> It has CommutativeMonoid for _*_,  and CommutativeSemiring  too.
> According to the above suggestions, we have 
>
>   [2] ≈ [2] * [4]   in R.   
>
> So [2] occurs reducible in R, is has "reduced" to the two non-unit
> factors:  [2] and [4].
>
> This definition looks counter-intuitive.

Dunno if that's counter-intuitive.  Anyway, I only said that the basic
theory of divisibility, gcd, etc., goes through for any cancellative
commutative monoid.  The multiplicative monoid of the ring Z/6Z isn't
cancellative.

> 1) to define  IntegralRing  as a CommutativeRing  
>    in which it holds 
>                       x * y ≈ 0  → x ≈ 0 ⊎ y ≈ 0
>    ("no zero divisors")
>    and to consider irreducibility only for an  IntegralRing,

I agree that it's better to avoid an arbitrary monoid even while
defining irreducible elements, etc.  However, one can and should define
them for cancellative commutative monoids.  There's a complete theory
there.  Moreover, there are common examples of cancellative commutative
monoids which have gcds, unique factorisation, etc., but aren't of the
form A\{0}, where A is an integral domain.  E.g, the multiplicative
monoid of non-zero ideals in a Dedekind domain.

> 2) to add the condition   ¬0 : ¬ n ≈ #0  to the definition if
> irreducibility.

You don't need to add that condition in an integral domain.  It follows
from the other one because 0=0*0, and neither of the factors 0 and 0 on
the right hand side is a unit, because an integral domain is non-zero by
definition.

> See textbooks on Algebra:  Wan Der Waerden, and such.

And such as ... Jacobson's book that I'd cited :-)  Or, Mines, Richman,
and Ruitenberg, A course in constructive algebra, Chapter IV.; section 1
there is titled "Divisibility in cancellation monoids".

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/