~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmno p q r s t u v w x y z { | } ~  4  !"#$%&'()*+,-./01234  !"#$%&'()*+,-./012343210/.-,+*)('&%$#"!  4  !"#$%&'()*+,-./01234Definition of rings. 5 Addition 6Multiplication 7Compute additive inverse 8The additive identity 9The multiplicative identity :ISpecification of rings. Test that the arguments satisfy the ring axioms. ; Subtraction < Summation =Product >Exponentiation ?KMultiply from left with an integer; n *> x means x + x + ... + x, n times. 456789:;<=>? 456789:;>?<= 45678956789:;<=>?@!Definition of commutative rings. AASpecification of commutative rings. Test that multiplication is 4 commutative and that it satisfies the ring axioms. 456789:;<=>?@A@A@A B2Ideals characterized by their list of generators. CDThe zero ideal. ETest if an ideal is principal. FG'Evaluate the ideal at a certain point. HAddition of ideals. IMultiplication of ideals. J2Test 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. KGCompute witnesses for two lists for the zero ideal. This is used when + computing the intersection of two ideals. BCDEFGHIJK BCDEFGHIJK BCCDEFGHIJKLStrongly 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. MNHTest that the witness is actually a witness that the element is in the  ideal. LMNLMNLMMNO Definition of integral domains. PHSpecification of integral domains. Test that there are no zero-divisors 8 and that it satisfies the axioms of commutative rings. 456789:;<=>?@AOPOPOPQEuclidean 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. RSTUVWX<The Euclidean algorithm for calculating the GCD of a and b. YFGeneralized Euclidean algorithm to compute GCD of a list of elements. ZLowest 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). ]*Generalized extended Euclidean algorithm. 3Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n) QRSTUVWXYZ[\] QRSTUVWXYZ[\] QRSRSTUVWXYZ[\]^ Matrices _` Row vectors abcdConstruct a mxn matrix. efghi#Compute the dimension of a matrix. jkTranspose a matrix. lMatrix addition. mMatrix multiplication. n!Construct a nxn identity matrix. ^_`abcdefghijklmn`abc^_dhgfenmlkji^__`aabcdefghijklmn oDefinition 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. pqrSolves a system of equations. sLTest that the solution of an MxN system is in fact a solution of the system t&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 u"Strongly discrete coherent rings. KIf the ring is strongly discrete and coherent then we can solve arbitrary  equations of the type AX=b. vw2Solves 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). opqrstuvwx opqrstuvwx oppqrstuvw yPrufer domain z{Property specifying that:  au = bv and b(1-u) = aw |}MAlternative characterization of Prufer domains, given a and b compute u, v,  w, t such that: ua = vb && wa = tb && u+t = 1 ~@Go back to the original definition (yes the name is stupid :P). ICompute a principal localization matrix for an ideal in a Prufer domain. >Ideal inversion. Given I compute J such that IJ is principal. 7 Uses the principal localization matrix for the ideal. (Compute the intersection of I and J by: -(I  J)(I + J) = IJ => (I  J)(I + J)(I + J)' = IJ(I + J)' yz{|}~ yz{|}~ yzz{|}~ Bezout 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 %Intersection of ideals with witness. JIf one of the ideals is the zero ideal then the intersection is the zero  ideal. Intersection without witness. Coherence of Bezout domains. Bezout domain -> Prfer domain )Strongly discreteness for Bezout domains 2Given x, compute as such that x = sum (a_i * x_i)  KA 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 MPrincipal localization matrices for ideals are computable in Bezout domains.   GCD domains 6Compute gcd(a,b) = (g,x,y) such that g = gcd(a,b) and  a = gx  b = gy  and a, b /= 0 HSpecification of GCD domains. They are integral domains in which every : pair of nonzero elements have a greatest common divisor.  Type synonym for integers. 456789456789Definition of fields. JSpecification of fields. Test that the multiplicative inverses behave as @ expected and that it satisfies the axioms of integral domains.  Division 456789:;<=>?@AOPField of fractions )Embed a value in the field of fractions. JExtract a value from the field of fractions. This is only possible if the  divisor is one. Reduce an element. "Q is the field of fractions of Z. Useful shorthand for Q[x]. GPolynomials over a commutative ring, indexed by a phantom type x that K denote the name of the variable that the polynomial is over. For example  UPoly Q X_ is Q[x] and UPoly Q T_ is Q[t]. The degree of the polynomial. The variable x in Q[x]. JTake a list and construct a polynomial by removing all zeroes in the end. ITake an element of the ring and the degree of the desired monomial, for  example: monomial 3 7 = 3x^7 *Compute the leading term of a polynomial. 'Formal derivative of polynomials in k[x]. Funny integration: ,Square free decomposition of a polynomial. <Distinct power factorization, aka square free decomposition  Pseudo-division of polynomials. 8Given s(x) and p(x) compute c, q(x) and r(x) such that: cs(x) = p(x)q(x)+r(x), deg r < deg p. The field of fraction of Q[x]. Field of rational functions. 7The phantom type n represents which modulo to work in.  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrs"tuvwxyz{|}~     ) constructive-algebra-0.1.5Algebra.TypeChar.CharAlgebra.Structures.Ring"Algebra.Structures.CommutativeRing Algebra.Ideal#Algebra.Structures.StronglyDiscrete!Algebra.Structures.IntegralDomain"Algebra.Structures.EuclideanDomainAlgebra.MatrixAlgebra.Structures.CoherentAlgebra.Structures.PruferDomainAlgebra.Structures.BezoutDomain Algebra.PLMAlgebra.Structures.GCDDomain Algebra.ZAlgebra.Structures.Field#Algebra.Structures.FieldOfFractions Algebra.Q Algebra.UPoly Algebra.FieldOfRationalFunctions Algebra.ZnZYXWVUTSRQPONMLKJIHGFEDCBAZ_Y_X_W_V_U_T_S_R_Q_P_O_N_M_L_K_J_I_H_G_F_E_D_C_B_A_Ring<+><*>negzeroonepropRing<->sumRing productRing<^>*>CommutativeRingpropCommutativeRingIdealId zeroIdeal isPrincipalfromIdevaladdIdmulId isSameIdealzeroIdealWitnessesStronglyDiscretememberpropStronglyDiscreteIntegralDomainpropIntegralDomainEuclideanDomaindquotientRemainderpropEuclideanDomainmoduloquotientdivides euclidAlg genEuclidAlglcmEgenLcmEextendedEuclidAlggenExtendedEuclidAlgMatrixVectorVecunVec lengthVecmatrixunMunMVecvectorToMatrixmatrixToVector dimensionisSquareMatrix transposeaddMmulMidentityCoherentsolve propCoherentsolveMxN propSolveMxNsolveWithIntersectionsolveGeneralEquationpropSolveGeneralEquation solveGeneralpropSolveGeneral PruferDomaincalcUVW propCalcUVWpropPruferDomaincalcUVWT propCalcUVWT fromUVWTtoUVW computePLM_PD invertIdeal BezoutDomain toPrincipalpropBezoutDomaindividesBintersectionBWitness intersectionBsolveBpropPLM computePLM_B GCDDomaingcd' propGCDDomainFieldinv propFieldFieldOfFractionstoFieldOfFractionsfromFieldOfFractionsreducetoQtoZQxUPolyUPdegxtoUPolymonomialltderivsqfrsqfrDecQXFieldOfRationalFunctionstoQXtoQxZn propAddAssocpropAddIdentity propAddInv propAddComm propMulAssoc propRightDist propLeftDistpropMulIdentity propMulCommpropZeroDivisorspropD propQuotRempropExtendedEuclidAlgpropGenExtEuclidAlgpropLeftIdentitypropRightIdentity isSolution intersectionPsolvePDpropToPrincipalpropIsSameIdeal handleZero$fPruferDomaina$fStronglyDiscreteapropGCDpropIntegralDomainZpropEuclideanDomainZpropBezoutDomainZpropStronglyDiscreteZ propCoherentZ propSolveMxNZpropSolveGeneralEquationZpropSolveGeneralZpropPLMZ propMulInv propReduce constUPoly integrateaddUPmulUP pseudoDividepropPD propFieldQXIsZeroPrime'PrimeSqrt'SqrtZ17Z3test1test2test3sqrtprime