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



Representation of coherent rings. Traditionally a ring is coherent if every finitely generated ideal is finitely presented. This means that it is possible to solve homogenous linear equations in them.



class IntegralDomain a => Coherent a whereSource

Definition of coherent rings.

We say that R is coherent iff for any M, we can find L such that ML=0 and

MX=0 <-> exists Y. X=LY

that is, iff we can generate the solutions of any linear homogeous system of equations.

The main point here is that ML=0, it is not clear how to represent the equivalence in Haskell. This would probably be possible in type theory.


solve :: Vector a -> Matrix aSource

isSolution :: (CommutativeRing a, Eq a) => Matrix a -> Matrix a -> BoolSource

Test that the second matrix is a solution to the first.

solveMxN :: (Coherent a, Eq a) => Matrix a -> Matrix aSource

Solves a system of equations.

propSolveMxN :: (Coherent a, Eq a) => Matrix a -> BoolSource

Test that the solution of an MxN system is in fact a solution of the system

solveWithIntersection :: (IntegralDomain a, Eq a) => Vector a -> (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Matrix aSource

Intersection computable -> Coherence.

Proof that if there is an algorithm to compute a f.g. set of generators for the intersection of two f.g. ideals then the ring is coherent.

Takes the vector to solve, [x1,...,xn], and a function (int) that computes the intersection of two ideals.

If [ x_1, ..., x_n ] `int` [ y_1, ..., y_m ] = [ z_1, ..., z_l ]

then int should give witnesses us and vs such that:

z_k = n_k1 * x_1 + ... + u_kn * x_n = u_k1 * y_1 + ... + n_km * y_m

solveGeneralEquation :: (Coherent a, StronglyDiscrete a) => Vector a -> a -> Maybe (Matrix a)Source

Strongly discrete coherent rings.

If the ring is strongly discrete and coherent then we can solve arbitrary equations of the type AX=b.

solveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Maybe (Matrix a, Matrix a)Source

Solves general linear systems of the kind AX = B.

A is given as a matrix and B is given as a row vector (it should be column vector).