module Algebra.Structures.PruferDomain
( PruferDomain(..)
, propCalcUVW, propPruferDomain
, calcUVW_B, calcUVWT, propCalcUVWT, fromUVWTtoUVW
, computePLM_PD
, invertIdeal
, intersectionPD, intersectionPDWitness, solvePD
) where
import Test.QuickCheck
import Data.List (nub, (\\))
import Algebra.Structures.IntegralDomain
import Algebra.Structures.BezoutDomain
import Algebra.Structures.Coherent
import Algebra.Ideal
import Algebra.Matrix
class IntegralDomain a => PruferDomain a where
calcUVW :: a -> a -> (a,a,a)
propCalcUVW :: (PruferDomain a, Eq a) => a -> a -> Bool
propCalcUVW a b = a <*> u == b <*> v && b <*> (one <-> u) == a <*> w
where (u,v,w) = calcUVW a b
propPruferDomain :: (PruferDomain a, Eq a) => a -> a -> a -> Property
propPruferDomain a b c | propCalcUVW a b = propIntegralDomain a b c
| otherwise = whenFail (print "propCalcUVW") False
calcUVWT :: PruferDomain a => a -> a -> (a,a,a,a)
calcUVWT a b = (x,y,z,one <-> x)
where (x,y,z) = calcUVW a b
propCalcUVWT :: (PruferDomain a, Eq a) => a -> a -> Bool
propCalcUVWT a b = u <*> a == v <*> b && w <*> a == t <*> b && u <+> t == one
where (u,v,w,t) = calcUVWT a b
fromUVWTtoUVW :: (a,a,a,a) -> (a,a,a)
fromUVWTtoUVW (u,v,w,t) = (u,v,w)
calcUVW_B :: (BezoutDomain a, Eq a) => a -> a -> (a,a,a)
calcUVW_B a b | a == zero = (one,zero,zero)
| b == zero = (zero,zero,zero)
| otherwise = fromUVWTtoUVW (u,v,w,t)
where
(g,[_,_],[a1,b1]) = toPrincipal (Id [a,b])
(_,[c,d],_) = toPrincipal (Id [a1,b1])
u = d <*> b1
t = c <*> a1
v = d <*> a1
w = c <*> b1
computePLM_PD :: (PruferDomain a, Eq a) => Ideal a -> Matrix a
computePLM_PD (Id [_]) = matrix [[one]]
computePLM_PD (Id [a,b]) = let (u,v,w,t) = calcUVWT b a
in M [ Vec [u,v], Vec [w,t]]
computePLM_PD (Id xs) = matrix a
where
x_is = init xs
b = unMVec $ computePLM_PD (Id x_is)
m = length b 1
s_is = [ (b !! i) !! i | i <- [0..m]]
x_n = last xs
uvwt_i = [ calcUVWT x_n x_i | x_i <- x_is ]
u_is = [ u_i | (u_i,_,_,_) <- uvwt_i ]
v_is = [ v_i | (_,v_i,_,_) <- uvwt_i ]
w_js = [ w_i | (_,_,w_i,_) <- uvwt_i ]
t_is = [ t_i | (_,_,_,t_i) <- uvwt_i ]
a_ij = [ [ if i == j
then (s_is !! i) <*> (u_is !! i)
else (u_is !! i) <*> (b !! i !! j)
| j <- [0..m] ]
| i <- [0..m] ]
a_nn = sumRing $ zipWith (<*>) s_is t_is
a_ni = [ sumRing [ (b !! j !! i) <*> (w_js !! j)
| j <- [0..m] ]
| i <- [0..m] ]
a_in = [ (s_is !! i) <*> (v_is !! i)
| i <- [0..m] ]
a = [ x ++ [y] | (x,y) <- zip a_ij a_in ] ++ [a_ni ++ [a_nn]]
invertIdeal :: (PruferDomain a, Eq a) => Ideal a -> Ideal a
invertIdeal xs =
let a = unMVec $ computePLM_PD xs
a_njs = [ head (a !! j) | j <- [0..length a 1]]
in Id a_njs
intersectionPDWitness :: (PruferDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a,[[a]],[[a]])
intersectionPDWitness (Id is) (Id js) = (int,wis,wjs)
where
lj = length js
li = length is
ij = Id (is ++ js)
plm = computePLM_PD ij
as = take li $ unMVec $ transpose plm
as' = drop li $ unMVec $ transpose plm
int = Id $ concat [ map (j <*>) a | j <- js , a <- as ]
wis = concat [ [ addZ i li a | a <- as ] | as <- as', i <- [0..li1] ]
wjs = [ addZ i lj a | i <- [0..lj1], a <- concat as ]
addZ n l x = replicate n zero ++ x : replicate (ln1) zero
intersectionPD :: (PruferDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a
intersectionPD i j = fst3 (intersectionPDWitness i j)
where fst3 (x,_,_) = x
solvePD :: (PruferDomain a, Eq a) => Vector a -> Matrix a
solvePD x = solveWithIntersection x intersectionPDWitness