constructive-algebra-0.3.0: A library of constructive algebra.



Prufer domains are non-Noetherian analogues of Dedekind domains. That is integral domains in which every finitely generated ideal is invertible. This implementation is mainly based on:



class IntegralDomain a => PruferDomain a whereSource

Given a and b it computes u, v and we such that:

  1. au = bv
  2. b(1-u) = aw


calcUVW :: a -> a -> (a, a, a)Source

propCalcUVW :: (PruferDomain a, Eq a) => a -> a -> BoolSource

Property specifying that: au = bv and b(1-u) = aw

propPruferDomain :: (PruferDomain a, Eq a) => a -> a -> a -> PropertySource

calcUVW_B :: (BezoutDomain a, Eq a) => a -> a -> (a, a, a)Source

Bezout domain -> Prufer domain

Proof that all Bezout domains are Prufer domains.

calcUVWT :: PruferDomain a => a -> a -> (a, a, a, a)Source

Alternative characterization of Prufer domains, given a and b compute u, v, w, t such that:

ua = vb && wa = tb && u+t = 1

propCalcUVWT :: (PruferDomain a, Eq a) => a -> a -> BoolSource

fromUVWTtoUVW :: (a, a, a, a) -> (a, a, a)Source

Go back to the original definition.

computePLM_PD :: (PruferDomain a, Eq a) => Ideal a -> Matrix aSource

Compute a principal localization matrix for an ideal in a Prufer domain.

invertIdeal :: (PruferDomain a, Eq a) => Ideal a -> Ideal aSource

Ideal inversion. Given I compute J such that IJ is principal. Uses the principal localization matrix for the ideal.

intersectionPDWitness :: (PruferDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])Source

Compute the intersection of I and J by:

(I \cap J)(I + J) = IJ => (I \cap J)(I + J)(I + J)' = IJ(I + J)'

solvePD :: (PruferDomain a, Eq a) => Vector a -> Matrix aSource

Coherence of Prufer domains.