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

[Sergei Meshveliani]

I need to add the following.

1) In classical algebra,  Irreducible  is a synonym for  IsPrime
   -- in the Commutative case
   (and a non-commutative case is far too complex).

2) IsPrime  is defined only for  IntegralRing
   (for the reason I wrote earlier).

3) Integer  is an  IntegralRing,  so there is a notion of  IsPrime.
   Also there is an algorithm for  prime?  and factoring to primes. 

4) Nat  is not a Ring.
   But  Nat  is imbedded into  Integer,  and  IsPrimeNat n  is defined
   as  IsPrime (+ n)  in  Integer.
   And the correspondent algorithms are taken from  Integer. 

Regards,

------
Sergei


On Sat, 2015-03-07 at 18:55 +0400, Sergei Meshveliani wrote:
> 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
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>