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

[Sergei Meshveliani]

On Sat, 2015-03-07 at 10:27 +0530, N. Raghavendra wrote:
> At 2015-03-07T12:21:33+08:00, Dr. ERDI Gergo wrote:
> 
> > Would it make sense to add Irreducible to the standard library? Here's
> > the generalization I have in mind:
> 
> I too feel it'd be good to have the general notion of irreducible
> element in stdlib.
> 
> > open import Algebra
> > open import Relation.Nullary
> > open import Data.Sum
> > open import Level using (Level; _⊔_)
> > import Algebra.FunctionProperties
> >
> > module _ {c ℓ : Level} (R : Algebra.CommutativeSemiring c ℓ) where
> 
> All you need is a monoid structure to define irreducible element.  Most
> books I've seen assume that the monoid is cancellative and commutative.
> That's needed in the proofs of some statements, but isn't necessary for
> the definition to make sense.
> 
> > data Irreducible (n : Carrier) : Set (ℓ ⊔ c) where
> >   irreducible : (not0 : ¬ is0 n) → (not1 : ¬ is1 n) →
> >                 (prf : ∀ x y → ≈ x * y → is1 x ⊎ is1 y) →
> >                 Irreducible n
> 
> module _ {c ℓ : Level} (R : Algebra.CommutativeMonoid c ℓ) where
> 
> ...
> 
> data Irreducible (n : Carrier) : Set (ℓ ⊔ c) where
>   irreducible : (notUnit : ¬ isUnit n) →
>                 (prf : ∀ x y → n ≈ x * y → isUnit x ⊎ isUnit y) →
>                 Irreducible n
> 
> where isUnit n means that n . m ~ e for some m, where e is the identity
> element of the monoid.
> 
> 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.

This is why it is desirable

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,

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

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

Regards,

------
Sergei