Remove attributes unitsKnown, leftUnitary, rightUnitary, canonicalsClosed, central, noetherian, NullSquare, JacobiIdentity.

10 files changed, 8 insertions, 88 deletions

diff --git a/src/algebra/attreg.spad.pamphlet b/src/algebra/attreg.spad.pamphlet
index b8853786..68028a29 100644
--- a/src/algebra/attreg.spad.pamphlet
+++ b/src/algebra/attreg.spad.pamphlet
@@ -18,15 +18,6 @@ AttributeRegistry(): Category == with
   commutative("*")
     ++ \spad{commutative("*")} is true if it has an operation
     ++ \spad{"*": (D,D) -> D} which is commutative.
-  unitsKnown
-    ++ \spad{unitsKnown} is true if a monoid (a multiplicative semigroup 
-    ++ with a 1) has \spad{unitsKnown} means that
-    ++ the operation \spadfun{recip} can only return "failed" 
-    ++ if its argument is not a unit.
-  leftUnitary
-    ++ \spad{leftUnitary} is true if \spad{1 * x = x} for all x.
-  rightUnitary
-    ++ \spad{rightUnitary} is true if \spad{x * 1 = x} for all x.
   noZeroDivisors
     ++ \spad{noZeroDivisors} is true if \spad{x * y \~~= 0} implies 
     ++ both x and y are non-zero.
@@ -35,37 +26,17 @@ AttributeRegistry(): Category == with
     ++ representative for each class of associate elements, that is
     ++ \spad{associates?(a,b)} returns true if and only if 
     ++ \spad{unitCanonical(a) = unitCanonical(b)}.
-  canonicalsClosed
-    ++ \spad{canonicalsClosed} is true if 
-    ++ \spad{unitCanonical(a)*unitCanonical(b) = unitCanonical(a*b)}.
-  arbitraryPrecision
-    ++ \spad{arbitraryPrecision} means the user can set the 
-    ++ precision for subsequent calculations.
   partiallyOrderedSet
     ++ \spad{partiallyOrderedSet} is true if
     ++ a set with \spadop{<} which is transitive, 
     ++ but \spad{not(a < b or a = b)}
     ++ does not necessarily imply \spad{b<a}.
-  central
-    ++ \spad{central} is true if, given an algebra over a ring R,
-    ++ the image of R is the center
-    ++ of the algebra, i.e. the set of members of the algebra which commute
-    ++ with all others is precisely the image of R in the algebra.
-  noetherian
-    ++ \spad{noetherian} is true if all of its ideals are finitely generated.
   additiveValuation
     ++ \spad{additiveValuation} implies
     ++ \spad{euclideanSize(a*b)=euclideanSize(a)+euclideanSize(b)}.
   multiplicativeValuation
     ++ \spad{multiplicativeValuation} implies
     ++ \spad{euclideanSize(a*b)=euclideanSize(a)*euclideanSize(b)}.
-  NullSquare
-    ++ \axiom{NullSquare} means that \axiom{[x,x] = 0} holds.
-    ++ See \axiomType{LieAlgebra}.
-  JacobiIdentity
-    ++ \axiom{JacobiIdentity} means that 
-    ++ \axiom{[x,[y,z]]+[y,[z,x]]+[z,[x,y]] = 0} holds.
-    ++ See \axiomType{LieAlgebra}.
   canonical
     ++ \spad{canonical} is true if and only if distinct elements have 
     ++ distinct data structures. For example, a domain of mathematical objects 
diff --git a/src/algebra/catdef.spad.pamphlet b/src/algebra/catdef.spad.pamphlet
index 9e6a8102..1e9370df 100644
--- a/src/algebra/catdef.spad.pamphlet
+++ b/src/algebra/catdef.spad.pamphlet
@@ -489,9 +489,7 @@ OrderedStructure(T: Type,f: (T,T) -> Boolean): Public == Private where
 ++ Axiom:
 ++   \spad{ r*(x*s) = (r*x)*s }
 BiModule(R:Ring,S:Ring):Category ==
-  Join(LeftModule(R),RightModule(S)) with
-     leftUnitary ++ \spad{1 * x = x}
-     rightUnitary ++ \spad{x * 1 = x}
+  Join(LeftModule(R),RightModule(S)) 
 
 @
 \section{category CABMON CancellationAbelianMonoid}
@@ -1033,7 +1031,6 @@ Field(): Category == Join(EuclideanDomain,UniqueFactorizationDomain,
         ++ x/y divides the element x by the element y.
         ++ Error: if y is 0.
       canonicalUnitNormal  ++ either 0 or 1.
-      canonicalsClosed     ++ since \spad{0*0=0}, \spad{1*1=1}
     add
       --declarations
       x,y: %
@@ -1224,8 +1221,6 @@ Group(): Category == Monoid with
       inv: % -> %             ++ inv(x) returns the inverse of x.
       /: (%,%) -> %           ++ x/y is the same as x times the inverse of y.
       **: (%,Integer) -> %    ++ x**n returns x raised to the integer power n.
-      unitsKnown                ++ unitsKnown asserts that recip only returns
-                                ++ "failed" for non-units.
       conjugate: (%,%) -> %
         ++ conjugate(p,q) computes \spad{inv(q) * p * q}; this is 'right action
         ++ by conjugation'.
@@ -1261,7 +1256,6 @@ Group(): Category == Monoid with
 ++
 ++ Conditional attributes:
 ++   canonicalUnitNormal\tab{20}the canonical field is the same for all associates
-++   canonicalsClosed\tab{20}the product of two canonicals is itself canonical
 
 IntegralDomain(): Category ==
   Join(CommutativeRing, Algebra(%), EntireRing) with
@@ -1411,8 +1405,6 @@ Module(R:CommutativeRing): Category == Join(BiModule(R,R), LinearSet R)
 ++    \spad{leftIdentity("*":(%,%)->%,1)}\tab{30}\spad{1*x=x}
 ++    \spad{rightIdentity("*":(%,%)->%,1)}\tab{30}\spad{x*1=x}
 ++
-++ Conditional attributes:
-++    unitsKnown\tab{15}\spadfun{recip} only returns "failed" on non-units
 Monoid(): Category == SemiGroup with
     --operations
       1:              %                   ++ 1 is the multiplicative identity.
@@ -1422,7 +1414,7 @@ Monoid(): Category == SemiGroup with
                                           ++ of x n times, i.e. exponentiation.
       recip: % -> Union(%,"failed")
           ++ recip(x) tries to compute the multiplicative inverse for x
-          ++ or "failed" if it cannot find the inverse (see unitsKnown).
+          ++ or "failed" if it cannot find the inverse.
     add
       import RepeatedSquaring(%)
       one? x == x = 1
@@ -2012,10 +2004,6 @@ Ring(): Category == Join(Rng,SemiRing,LeftModule(%),CoercibleFrom Integer) with
         ++ \spad{n*x=0} for all x in the ring, or zero if no such n
         ++ exists.
         --We can not make this a constant, since some domains are mutable
-      unitsKnown
-        ++ recip truly yields
-        ++ reciprocal or "failed" if not a unit.
-        ++ Note: \spad{recip(0) = "failed"}.
    add
       n:Integer
       coerce(n) == n * 1$%
diff --git a/src/algebra/integer.spad.pamphlet b/src/algebra/integer.spad.pamphlet
index ba924720..df709373 100644
--- a/src/algebra/integer.spad.pamphlet
+++ b/src/algebra/integer.spad.pamphlet
@@ -73,10 +73,6 @@ IntegerSolveLinearPolynomialEquation(): C ==T
 Integer: IntegerNumberSystem with
     canonical
       ++ mathematical equality is data structure equality.
-    canonicalsClosed
-      ++ two positives multiply to give positive.
-    noetherian
-      ++ ascending chain condition on ideals.
  == add
       ZP ==> SparseUnivariatePolynomial %
       ZZP ==> SparseUnivariatePolynomial Integer
@@ -298,10 +294,6 @@ PositiveInteger: Join(OrderedAbelianSemiGroup,Monoid) with
 RomanNumeral(): Join(IntegerNumberSystem,ConvertibleFrom Symbol) with
     canonical
       ++ mathematical equality is data structure equality.
-    canonicalsClosed
-      ++ two positives multiply to give positive.
-    noetherian
-      ++ ascending chain condition on ideals.
     roman  : Symbol  -> %
       ++ roman(n) creates a roman numeral for symbol n.
     roman  : Integer -> %
diff --git a/src/algebra/lie.spad.pamphlet b/src/algebra/lie.spad.pamphlet
index d039c5ef..a8d2c857 100644
--- a/src/algebra/lie.spad.pamphlet
+++ b/src/algebra/lie.spad.pamphlet
@@ -201,8 +201,6 @@ LieSquareMatrix(n,R): Exports == Implementation where
 --    symdecomp : % -> Record(sym:%,antisym:%)
 --    if R has commutative("*") then
 --      minorsVect: -> Vector(Union(R,"uncomputed")) --range: 1..2**n-1
---    if R has commutative("*") then central
---    if R has commutative("*") and R has unitsKnown then unitsKnown
 
 @
 \section{License}
diff --git a/src/algebra/matrix.spad.pamphlet b/src/algebra/matrix.spad.pamphlet
index 6aded198..159f0217 100644
--- a/src/algebra/matrix.spad.pamphlet
+++ b/src/algebra/matrix.spad.pamphlet
@@ -310,13 +310,6 @@ SquareMatrix(ndim,R): Exports == Implementation where
 --  if R has commutative("*") then
 --    minorsVect: -> Vector(Union(R,"uncomputed")) --range: 1..2**n-1
 --      ++ \spad{minorsVect(m)} returns a vector of the minors of the matrix m
-    if R has commutative("*") then central
-      ++ the elements of the Ring R, viewed as diagonal matrices, commute
-      ++ with all matrices and, indeed, are the only matrices which commute
-      ++ with all matrices.
-    if R has commutative("*") and R has unitsKnown then unitsKnown
-      ++ the invertible matrices are simply the matrices whose determinants
-      ++ are units in the Ring R.
     if R has ConvertibleTo InputForm then ConvertibleTo InputForm
  
   Implementation ==> Matrix R add
diff --git a/src/algebra/naalgc.spad.pamphlet b/src/algebra/naalgc.spad.pamphlet
index f5b56a47..3f85f7ef 100644
--- a/src/algebra/naalgc.spad.pamphlet
+++ b/src/algebra/naalgc.spad.pamphlet
@@ -78,8 +78,6 @@ Monad(): Category == SetCategory with
 ++ Axioms
 ++    leftIdentity("*":(%,%)->%,1)   \tab{30} 1*x=x
 ++    rightIdentity("*":(%,%)->%,1)  \tab{30} x*1=x
-++ Common Additional Axioms
-++    unitsKnown---if "recip" says "failed", that PROVES input wasn't a unit
 MonadWithUnit(): Category == Monad with
     --constants
       1: constant ->  %
@@ -102,15 +100,15 @@ MonadWithUnit(): Category == Monad with
         ++ recip(a) returns an element, which is both a left and a right
         ++ inverse of \spad{a},
         ++ or \spad{"failed"} if such an element doesn't exist or cannot
-        ++ be determined (see unitsKnown).
+        ++ be determined.
       leftRecip: % -> Union(%,"failed")
         ++ leftRecip(a) returns an element, which is a left inverse of \spad{a},
         ++ or \spad{"failed"} if such an element doesn't exist or cannot
-        ++ be determined (see unitsKnown).
+        ++ be determined.
       rightRecip: % -> Union(%,"failed")
         ++ rightRecip(a) returns an element, which is a right inverse of
         ++ \spad{a}, or \spad{"failed"} if such an element doesn't exist
-        ++ or cannot be determined (see unitsKnown).
+        ++ or cannot be determined.
     add
       import RepeatedSquaring(%)
       one? x == x = 1
@@ -404,16 +402,16 @@ FiniteRankNonAssociativeAlgebra(R:CommutativeRing):
         ++ recip(a) returns an element, which is both a left and a right
         ++ inverse of \spad{a},
         ++ or \spad{"failed"} if there is no unit element, if such an
-        ++ element doesn't exist or cannot be determined (see unitsKnown).
+        ++ element doesn't exist or cannot be determined.
       leftRecip: % -> Union(%,"failed")
         ++ leftRecip(a) returns an element, which is a left inverse of \spad{a},
         ++ or \spad{"failed"} if there is no unit element, if such an
-        ++ element doesn't exist or cannot be determined (see unitsKnown).
+        ++ element doesn't exist or cannot be determined.
       rightRecip: % -> Union(%,"failed")
         ++ rightRecip(a) returns an element, which is a right inverse of
         ++ \spad{a},
         ++ or \spad{"failed"} if there is no unit element, if such an
-        ++ element doesn't exist or cannot be determined (see unitsKnown).
+        ++ element doesn't exist or cannot be determined.
       associatorDependence:() -> List Vector R
         ++ associatorDependence() looks for the associator identities, i.e.
         ++ finds a basis of the solutions of the linear combinations of the
@@ -450,13 +448,6 @@ FiniteRankNonAssociativeAlgebra(R:CommutativeRing):
       -- about characteristic
       -- if R has CharacteristicZero then CharacteristicZero
       -- if R has CharacteristicNonZero then CharacteristicNonZero
-      unitsKnown
-        ++ unitsKnown means that \spadfun{recip} truly yields reciprocal
-        ++ or \spad{"failed"} if not a unit,
-        ++ similarly for \spadfun{leftRecip} and
-        ++ \spadfun{rightRecip}. The reason is that we use left, respectively
-        ++ right, minimal polynomials to decide this question.
-
   add
     --n := rank()
     --b := someBasis()
diff --git a/src/algebra/si.spad.pamphlet b/src/algebra/si.spad.pamphlet
index 795a75ed..561fc89e 100644
--- a/src/algebra/si.spad.pamphlet
+++ b/src/algebra/si.spad.pamphlet
@@ -182,12 +182,6 @@ IntegerNumberSystem(): Category ==
 SingleInteger(): Join(IntegerNumberSystem,OrderedFinite,BooleanLogic) with
    canonical
       ++ \spad{canonical} means that mathematical equality is implied by data structure equality.
-   canonicalsClosed
-      ++ \spad{canonicalClosed} means two positives multiply to give positive.
-   noetherian
-      ++ \spad{noetherian} all ideals are finitely generated (in fact principal).
-
-   -- bit operations
    xor: (%, %) -> %
       ++ xor(n,m)  returns the bit-by-bit logical {\em xor} of
       ++ the single integers n and m.
diff --git a/src/algebra/vector.spad.pamphlet b/src/algebra/vector.spad.pamphlet
index ea83ba12..7d143b7a 100644
--- a/src/algebra/vector.spad.pamphlet
+++ b/src/algebra/vector.spad.pamphlet
@@ -238,7 +238,6 @@ DirectProductCategory(dim:NonNegativeInteger, R:Type): Category ==
          if R has Monoid then LinearSet R
          if R has Finite then Finite
          if R has CommutativeRing then Module R
-         if R has unitsKnown then unitsKnown
          if R has OrderedSet then OrderedSet
          if R has OrderedAbelianMonoidSup then OrderedAbelianMonoidSup
          if R has Field then VectorSpace R
diff --git a/src/algebra/xlpoly.spad.pamphlet b/src/algebra/xlpoly.spad.pamphlet
index f607199d..6090799a 100644
--- a/src/algebra/xlpoly.spad.pamphlet
+++ b/src/algebra/xlpoly.spad.pamphlet
@@ -353,11 +353,6 @@ import Field
 ++ \axiomType{LiePolynomial} and 
 ++ \axiomType{XPBWPolynomial}. \newline Author : Michel Petitot (petitot@lifl.fr).
 LieAlgebra(R: CommutativeRing): Category ==  Module(R) with
-  --attributes
-    NullSquare 
-          ++ \axiom{NullSquare} means that \axiom{[x,x] = 0} holds.
-    JacobiIdentity 
-          ++ \axiom{JacobiIdentity} means that \axiom{[x,[y,z]]+[y,[z,x]]+[z,[x,y]] = 0} holds.
   --exports
     construct:  ($,$) -> $
           ++ \axiom{construct(x,y)} returns the Lie bracket of \axiom{x} and \axiom{y}.
diff --git a/src/algebra/xpoly.spad.pamphlet b/src/algebra/xpoly.spad.pamphlet
index b2021bf8..dbaf46dc 100644
--- a/src/algebra/xpoly.spad.pamphlet
+++ b/src/algebra/xpoly.spad.pamphlet
@@ -536,7 +536,6 @@ XPolynomialRing(R:Ring,E:OrderedMonoid): T == C where
 
     --assertions
       if R has noZeroDivisors then noZeroDivisors
-      if R has unitsKnown then unitsKnown
       if R has canonicalUnitNormal then canonicalUnitNormal
           ++ canonicalUnitNormal guarantees that the function
           ++ unitCanonical returns the same representative for all