úÎaŜ[}\      !"#$%&'()*+,-./0123456789:;<=>?@ABCD E F G H I J K L M N O P Q R S TUVWXYZ[Definition of rings.  Addition Multiplication Compute additive inverse The additive identity The multiplicative identity \]^_`abcISpecification of rings. Test that the arguments satisfy the ring axioms.  Subtraction  Summation Product Exponentiation      !Definition of commutative rings. d ASpecification of commutative rings. Test that multiplication is 4 commutative and that it satisfies the ring axioms.     2Ideals characterized by their list of generators. The zero ideal. Test if an ideal is principal. 'Evaluate the ideal at a certain point. Addition of ideals. Multiplication of ideals. 2Test if an operations compute the correct ideal. DThe operation should give a witness that the comuted ideal contains the same elements. If [ x_1, ..., x_n ] `op` [ y_1, ..., y_m ] = [ z_1, ..., z_l ] "Then the witness should give that $z_k = a_k1 * x_1 + ... + a_kn * x_n $ = b_k1 * y_1 + ... + b_km * y_m AThis is used to check that the intersection computed is correct. GCompute witnesses for two lists for the zero ideal. This is used when + computing the intersection of two ideals.   Strongly discrete rings EA ring is called strongly discrete if ideal membership is decidable. K Nothing correspond to that x is not in the ideal and Just is the witness. ; Examples include all Bezout domains and polynomial rings. HTest that the witness is actually a witness that the element is in the  ideal.  Definition of integral domains. eHSpecification of integral domains. Test that there are no zero-divisors 8 and that it satisfies the axioms of commutative rings.  Euclidean domains BGiven a and b compute (q,r) such that a = bq + r and r = 0 || d r < d b. $ Where d is the Euclidean function. fg !"#<The Euclidean algorithm for calculating the GCD of a and b. $FGeneralized Euclidean algorithm to compute GCD of a list of elements. %Lowest common multiple, (a*b)/ gcd(a,b). &IGeneralized lowest common multiple to compute lcm of a list of elements. '#The extended Euclidean algorithm. (Computes x and y in ax + by = gcd(a,b). h(*Generalized extended Euclidean algorithm. 3Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n) i  !"#$%&'(  !"#$%&'(  !"#$%&'() Matrices *+ Row vectors ,-./Construct a mxn matrix. 01234#Compute the dimension of a matrix. 56Transpose a matrix. 7Matrix addition. 8Matrix multiplication. 9!Construct a nxn identity matrix. jk)*+,-./0123456789+,-.)*/3210987654)**+,,-./0123456789 :Definition of coherent rings. JWe say that R is coherent iff for any M, we can find L such that ML=0 and MX=0 <-> exists Y. X=LY Kthat is, iff we can generate the solutions of any linear homogeous system  of equations. GThe main point here is that ML=0, it is not clear how to represent the I equivalence in Haskell. This would probably be possible in type theory. ;l<=Solves a system of equations. >LTest that the solution of an MxN system is in fact a solution of the system ?&Intersection computable -> Coherence. MProof 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 ] 4then 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. KIf the ring is strongly discrete and coherent then we can solve arbitrary  equations of the type AX=b. AB2Solves general linear systems of the kind AX = B. LA is given as a matrix and B is given as a row vector (it should be column  vector). :;<=>?@ABC :;<=>?@ABC :;;<=>?@AB DBezout domains ICompute a principal ideal from another ideal. Also give witness that the . principal ideal is equal to the first ideal.  toPrincipal <a_1,...,a_n> = (< a>,u_i,v_i)  where sum (u_i * a_i) = a a_i = v_i * a EmnFG%Intersection of ideals with witness. JIf one of the ideals is the zero ideal then the intersection is the zero  ideal. oHIntersection without witness. ICoherence of Bezout domains. p)Strongly discreteness for Bezout domains 2Given x, compute as such that x = sum (a_i * x_i) DEFGHIDEFHGIDEEFGHI JKA principal localization matrix for an ideal (x1,...,xn) is a matrix such that: ) The sum of the diagonal should equal 1. 4 For all i, j, l in {1..n}: a_lj * x_i = a_li * x_j KMPrincipal localization matrices for ideals are computable in Bezout domains. JKJKJK L GCD domains M6Compute gcd(a,b) = (g,x,y) such that g = gcd(a,b) and  a = gx  b = gy  and a, b /= 0 qNHSpecification of GCD domains. They are integral domains in which every : pair of nonzero elements have a greatest common divisor. LMNLMNLMMN OType synonym for integers. rstuvwxyzOOO PDefinition of fields. Q{RJSpecification of fields. Test that the multiplicative inverses behave as @ expected and that it satisfies the axioms of integral domains. S Division  PQRSPQRSPQQRSTField of fractions UV)Embed a value in the field of fractions. WJExtract a value from the field of fractions. This is only possible if the  divisor is one. XReduce an element. |TUVWXTUVWXTUUVWXY"Q is the field of fractions of Z. Z[YZ[YZ[YZ[} !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRS T U V W X Y Z [ \ ] ^ _ ` a b cdefghijklmnopqrstuvwxyz{| } ~  €  ‚ ƒ „ … † ‡ ˆ ‰ Š ‹Œconstructive-algebra-0.1.2Algebra.Structures.Ring"Algebra.Structures.CommutativeRing Algebra.Ideal#Algebra.Structures.StronglyDiscrete!Algebra.Structures.IntegralDomain"Algebra.Structures.EuclideanDomainAlgebra.MatrixAlgebra.Structures.CoherentAlgebra.Structures.BezoutDomain Algebra.PLMAlgebra.Structures.GCDDomain Algebra.ZAlgebra.Structures.Field#Algebra.Structures.FieldOfFractions Algebra.QRing<+><*>negzeroonepropRing<->sumRing productRing<^>CommutativeRingpropCommutativeRingIdealId zeroIdeal isPrincipalfromIdevaladdIdmulId isSameIdealzeroIdealWitnessesStronglyDiscretememberpropStronglyDiscreteIntegralDomainpropIntegralDomainEuclideanDomaindquotientRemainderpropEuclideanDomainmoduloquotientdivides euclidAlg genEuclidAlglcmEgenLcmEextendedEuclidAlggenExtendedEuclidAlgMatrixMVectorVecunVec lengthVecmatrixunMunMVecvectorToMatrixmatrixToVector dimensionisSquareMatrix transposeaddMmulMidentityCoherentsolve propCoherentsolveMxN propSolveMxNsolveWithIntersectionsolveGeneralEquationpropSolveGeneralEquation solveGeneralpropSolveGeneral BezoutDomain toPrincipalpropBezoutDomainintersectionBWitness intersectionBsolveBpropPLM computePLM_B GCDDomaingcd' propGCDDomainZFieldinv propFieldFieldOfFractionsFtoFieldOfFractionsfromFieldOfFractionsreduceQtoQtoZ propAddAssocpropAddIdentity propAddInv propAddComm propMulAssoc propRightDist propLeftDistpropMulIdentity propMulCommpropZeroDivisorspropD propQuotRempropExtendedEuclidAlgpropGenExtEuclidAlgpropLeftIdentitypropRightIdentity isSolutionpropToPrincipalpropIsSameIdeal handleZero$fStronglyDiscreteapropGCDpropIntegralDomainZpropEuclideanDomainZpropBezoutDomainZpropStronglyDiscreteZ propCoherentZ propSolveMxNZpropSolveGeneralEquationZpropSolveGeneralZpropPLMZ propMulInv propReduce