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 where
- propCoherent :: (Coherent a, Eq a) => Vector a -> Bool
- isSolution :: (CommutativeRing a, Eq a) => Matrix a -> Matrix a -> Bool
- solveMxN :: (Coherent a, Eq a) => Matrix a -> Matrix a
- propSolveMxN :: (Coherent a, Eq a) => Matrix a -> Bool
- solveWithIntersection :: (IntegralDomain a, Eq a) => Vector a -> (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Matrix a
- solveGeneralEquation :: (Coherent a, StronglyDiscrete a) => Vector a -> a -> Maybe (Matrix a)
- propSolveGeneralEquation :: (Coherent a, StronglyDiscrete a, Eq a) => Vector a -> a -> Bool
- solveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Maybe (Matrix a, Matrix a)
- propSolveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Property
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.
Test that the second matrix is a solution to the first.
Test that the solution of an MxN system is in fact a solution of the system
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
Strongly discrete coherent rings.
If the ring is strongly discrete and coherent then we can solve arbitrary equations of the type AX=b.
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).