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

Algebra.Structures.PruferDomain

Description

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:

http://hlombardi.free.fr/liens/salouThesis.pdf

Synopsis

# Documentation

class IntegralDomain a => PruferDomain a whereSource

Prufer domain

Methods

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

Instances

 PruferDomain Z PruferDomain EllipticCurve PruferDomain ZSqrt5 (Field k, Eq k) => PruferDomain (UPoly k x)

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 -> Prfer 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  J)(I + J) = IJ => (I  J)(I + J)(I + J)' = IJ(I + J)'

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

Coherence of Prufer domains.