OpenMath Content Dictionary: magma1

Canonical URL:

http://www.openmath.org/cd/magma1.ocd

CD File:

magma1.ocd

CD as XML Encoded OpenMath:

magma1.omcd

Defines:

carrier, is_associative, is_commutative, is_identity, is_submagma, left_divides, left_expression, magma, multiplication, right_divides, right_expression, submagma

Date:

2004-06-01

Version:

1 (Revision 2)

Review Date:

2006-06-01

Status:

experimental

Basic functions for magma theory

Initiated by Arjeh M. Cohen 2003-10-03
Edited by AMC 2004-0302

magma

Description:

This symbol is a constructor for magmas. It takes two arguments in the following order: a set to specify the elements in the magma and a binary operation to specify the magma operation. The binary operation should act on elements of the set and return an element of the set.

Commented Mathematical property (CMP):

A magma is closed under its operation.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="logic1" name="implies"/>
       <OMA><OMS cd="relation1" name="eq"/>
            <OMV name="G"/>
            <OMA><OMS cd="magma1" name="magma"/>
                 <OMV name="set"/>
                 <OMV name="binop"/>
            </OMA>
       </OMA>
       <OMA><OMS cd="logic1" name="implies"/>
	    <OMA><OMS cd="logic1" name="and"/>
                 <OMA><OMS cd="set1" name="in"/>
                      <OMV name="x"/><OMV name="set"/>
                 </OMA>
                 <OMA><OMS cd="set1" name="in"/>
                      <OMV name="y"/><OMV name="set"/>
                 </OMA>
            </OMA>
            <OMA><OMS cd="set1" name="in"/>
                 <OMA><OMV name="binop"/>
                      <OMV name="x"/><OMV name="y"/>
                 </OMA>
                 <OMV name="set"/>
            </OMA>
      </OMA>
 </OMA>
</OMOBJ>

implies (eq ( G, magma ( set, binop) ) , implies (and (in ( x, set) , in ( y, set) ) , in ( binop ( x, y) , set) ) )

$$G=\mathrm{magma}(\mathrm{set},\mathrm{binop})\Rightarrow x\in \mathrm{set}\wedge y\in \mathrm{set}\Rightarrow \mathrm{binop}(x,y)\in \mathrm{set}$$

Example:

This example represents the magma which has as elements all integers, and the magma operation is addition of the square of the first argument to the second.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="magma1" name="magma"/>
       <OMS cd="setname1" name="Z"/>
       <OMBIND><OMS cd="fns1" name="lambda"/>
            <OMBVAR><OMV name="x"/><OMV name="y"/></OMBVAR>
            <OMA><OMS cd="arith1" name="plus"/>
                 <OMA><OMS cd="arith1" name="power"/>
                      <OMV name="x"/> <OMI>2</OMI>
                 </OMA>
                 <OMV name="y"/>
            </OMA>
       </OMBIND>
  </OMA>
</OMOBJ>

magma (Z, lambda [ x y] . (plus (power ( x, 2) , y) ) )

$$\mathrm{magma}(\mathbb{Z},\lambda \hspace{0.17em}x,y.x^2+y)$$

Signatures:

sts

carrier

Description:

This symbol represents a unary function, whose argument should be a magma G (for instance constructed by magma). When applied to G, its value should be the set of elements of a magma.

Example:

The carrier of magma(G,*) is G.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="magma1" name="carrier"/>
            <OMA><OMS cd="magma1" name="magma"/>
                 <OMV name="G"/>  <OMV name="times"/>
            </OMA>
       </OMA>
       <OMV name="G"/>
  </OMA>
</OMOBJ>

eq (carrier (magma ( G, times) ) , G)

$$\mathrm{carrier}\left(\mathrm{magma}(G,\mathrm{times})\right)=G$$

Signatures:

sts

multiplication

Description:

This symbol represents a unary function, whose argument should be a magma G. It returns the multiplication map on G. We allow for the map to be n-ary.

Example:

The multiplication of magma(G,*) is *.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="magma1" name="multiplication"/>
            <OMA><OMS cd="group1" name="group"/>
                 <OMV name="G"/>
                 <OMV name="times"/>
            </OMA>
       </OMA>
       <OMV name="times"/>
  </OMA>
</OMOBJ>

eq (multiplication (group ( G, times) ) , times)

$$\mathrm{multiplication}\left(\mathrm{group}(G,\mathrm{times})\right)=\mathrm{times}$$

Signatures:

sts

is_commutative

Description:

The unary boolean function whose value is true iff the argument is a commutative magma.

Commented Mathematical property (CMP):

If is_commutative(G) then for all a,b in carrier(G) a*b = b*a

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="magma1" name="is_commutative"/>
      <OMV name="G"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="a"/>
	<OMV name="b"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
	<OMA>
	  <OMS cd="logic1" name="and"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="a"/>
	    <OMA>
	      <OMS cd="magma1" name="carrier"/>
	      <OMV name="G"/>
	    </OMA>
	  </OMA>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="b"/>
	    <OMA>
	      <OMS cd="magma1" name="carrier"/>
	      <OMV name="G"/>
	    </OMA>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
            <OMA>
              <OMS cd="magma1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
	    <OMV name="a"/>
	    <OMV name="b"/>
	  </OMA>
	  <OMA>
            <OMA>
              <OMS cd="magma1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
	    <OMV name="b"/>
	    <OMV name="a"/>
	  </OMA>
	</OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

implies (is_commutative ( G) , forall [ a b ] . (implies (and (in ( a, carrier ( G) ) , in ( b, carrier ( G) ) ) , eq (multiplication ( G) ( a, b) , multiplication ( G) ( b, a) ) ) ) )

$$\mathrm{is\_commutative}\left(G\right)\Rightarrow \forall \hspace{0.17em}a,b.a\in \mathrm{carrier}\left(G\right)\wedge b\in \mathrm{carrier}\left(G\right)\Rightarrow \left(\mathrm{multiplication}\left(G\right)\right)(a,b)=\left(\mathrm{multiplication}\left(G\right)\right)(b,a)$$

Signatures:

sts

is_associative

Description:

The unary boolean function whose value is true iff the argument is an associative magma.

Commented Mathematical property (CMP):

If is_associative(G) then for all a,b in carrier(G) (a*b) * c = a*(b*c)

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="logic1" name="implies"/>
       <OMA><OMS cd="magma1" name="is_associative"/>
            <OMV name="G"/>
       </OMA>
       <OMBIND><OMS cd="quant1" name="forall"/>
            <OMBVAR>  <OMV name="a"/> <OMV name="b"/><OMV name="c"/>
            </OMBVAR>
            <OMA><OMS cd="logic1" name="implies"/>
                 <OMA><OMS cd="logic1" name="and"/>
                      <OMA><OMS cd="set1" name="in"/>
                           <OMV name="a"/>
                           <OMA><OMS cd="magma1" name="carrier"/>
                                <OMV name="G"/>
                           </OMA>
                      </OMA>
                      <OMA><OMS cd="set1" name="in"/>
                           <OMV name="b"/>
                           <OMA><OMS cd="magma1" name="carrier"/>
                                <OMV name="G"/>
                           </OMA>
                      </OMA>
                      <OMA><OMS cd="set1" name="in"/>
                           <OMV name="c"/>
                           <OMA><OMS cd="magma1" name="carrier"/>
                                <OMV name="G"/>
                           </OMA>
                      </OMA>
                 </OMA>
                 <OMA><OMS cd="relation1" name="eq"/>
                      <OMA><OMA><OMS cd="magma1" name="multiplication"/>
                                <OMV name="G"/>
                           </OMA>
                           <OMA><OMA><OMS cd="magma1" name="multiplication"/>
                                     <OMV name="G"/>
                                </OMA>
                                <OMV name="a"/>
                                <OMV name="b"/>
                           </OMA>
                           <OMV name="c"/>
                      </OMA>
                      <OMA><OMA><OMS cd="magma1" name="multiplication"/>
                                <OMV name="G"/>
                           </OMA>
                           <OMV name="a"/>
                           <OMA><OMA><OMS cd="magma1" name="multiplication"/>
                                     <OMV name="G"/>
                                </OMA>
                                <OMV name="b"/>
                                <OMV name="c"/>
                           </OMA>
                      </OMA>
                 </OMA>
            </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

implies (is_associative ( G) , forall [ a b c ] . (implies (and (in ( a, carrier ( G) ) , in ( b, carrier ( G) ) , in ( c, carrier ( G) ) ) , eq (multiplication ( G) (multiplication ( G) ( a, b) , c) , multiplication ( G) ( a, multiplication ( G) ( b, c) ) ) ) ) )

$$\mathrm{is\_associative}\left(G\right)\Rightarrow \forall \hspace{0.17em}a,b,c.a\in \mathrm{carrier}\left(G\right)\wedge b\in \mathrm{carrier}\left(G\right)\wedge c\in \mathrm{carrier}\left(G\right)\Rightarrow \left(\mathrm{multiplication}\left(G\right)\right)(\left(\mathrm{multiplication}\left(G\right)\right)(a,b),c)=\left(\mathrm{multiplication}\left(G\right)\right)(a,\left(\mathrm{multiplication}\left(G\right)\right)(b,c))$$

Signatures:

sts

is_submagma

Description:

The binary boolean function whose value is true iff the second argument is a submagma of the first.

Commented Mathematical property (CMP):

If is_submagma(G,H) then H is a set of elements of G and H is closed under multiplication.

Signatures:

sts

is_identity

Description:

This symbols represents a binary boolean function, whose arguments should be a magma and an element of the element set of the magma. When applied to the arguments M and x, it returns true if the element x is an identity of the magma M, that is, x*y = y* x = y for all elements y of M.

Signatures:

sts

submagma

Description:

This symbol is a constructor symbol with two arguments. The first argument is a magma M, the second a list or set, D, of elements of M. When applied to M and D, it denotes the submagma of M generated by D.

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="magma1" name="submagma"/>
          <OMV name="M"/>  <OMV name="D"/>
     </OMA>
    </OMOBJ>

submagma ( M, D)

$$\mathrm{submagma}(M,D)$$

Example:

This example represents the submagma of the multiplicative magma of the nonzero reals generated by the constants Pi and E:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="magma1" name="magma"/>
     <OMA><OMS cd="magma1" name="magma"/>
          <OMA><OMS cd="set1" name="suchthat"/>
               <OMS cd="setname1" name="R"/>
               <OMBIND><OMS cd="fns1" name="lambda"/>
                       <OMBVAR> <OMV name="x"/>
                       </OMBVAR>
                       <OMA><OMS cd="relation1" name="neq"/>
                            <OMV name="x"/>
                            <OMS cd="alg1" name="zero"/>
                       </OMA>
               </OMBIND>
          </OMA>
          <OMS cd="arith1" name="times"/>
     </OMA>
     <OMA>
       <OMS cd="list1" name="list"/>
         <OMS cd="nums1" name="pi"/>
         <OMS cd="nums1" name="e"/>
     </OMA>
</OMA>
</OMOBJ>

magma (magma (suchthat (R, lambda [ x ] . (neq ( x, zero) ) ) , times) , list (pi, e) )

$$\mathrm{magma}(\mathrm{magma}(\left\{x\in \mathbb{R}\right|x\ne 0\},\times ),(\pi ,e))$$

Signatures:

sts

left_divides

Description:

This symbol is a ternary function. Its first argument should be a magma M and the second and third arguments should be elements of M. When applied to M, a, and b, it denotes the fact that a is a left_divisor of b in M. This means that there is v in M such that av=b.

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="magma1" name="left_divides"/>
         <OMV name="M"/><OMV name="a"/><OMV name="b"/>
    </OMA>
</OMOBJ>

left_divides ( M, a, b)

$$\mathrm{left\_divides}(M,a,b)$$

Signatures:

sts

right_divides

Description:

This symbol is a ternary function. Its first argument should be a magma M and the second and third arguments should be elements of M. When applied to M, a, and b, it denotes the fact that a is a right_divisor of b in M. This means that there is v in M such that va = b.

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="magma1" name="right_divides"/>
          <OMV name="M"/>          <OMV name="a"/>          <OMV name="b"/>
     </OMA>
    </OMOBJ>

right_divides ( M, a, b)

$$\mathrm{right\_divides}(M,a,b)$$

Signatures:

sts

left_expression

Description:

This symbol is a binary function. Its first argument should be a magma M, the second argument a list L of elements of M. When applied to M and L, it denotes the left product (L[1] * ( ... (L[n-1] * L[n]) ... )) of all elements in the list L.

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
         <OMA><OMS cd="magma1" name="left_expression"/>
              <OMA><OMS cd="magma1" name="magma"/>
                   <OMS cd="setname1" name="Z"/>
                   <OMS cd="arith1" name="times"/>
              </OMA>
              <OMA><OMS cd="list1" name="list"/>
                   <OMI>3</OMI><OMI>2</OMI>
              </OMA>
         </OMA>
         <OMI>6</OMI>
    </OMA>
  </OMOBJ>

eq (left_expression (magma (Z, times) , list (3, 2) ) , 6)

$$\mathrm{left\_expression}(\mathrm{magma}(\mathbb{Z},\times ),(3,2))=6$$

Signatures:

sts

right_expression

Description:

This symbol is a binary function. Its first argument should be a magma M, the second argument a list L of elements of M When applied to M and L, it denotes the right product (( ... (L[1] * L[2]) * ... ) * L[n]) of all elements in the list L.

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
         <OMA><OMS cd="magma1" name="right_expression"/>
              <OMA><OMS cd="magma1" name="magma"/>
                   <OMS cd="setname1" name="Z"/>
                   <OMS cd="arith1" name="times"/>
              </OMA>
              <OMA><OMS cd="list1" name="list"/>
                   <OMI>3</OMI><OMI>2</OMI>
              </OMA>
         </OMA>
         <OMI>6</OMI>
    </OMA>
  </OMOBJ>

eq (right_expression (magma (Z, times) , list (3, 2) ) , 6)

$$\mathrm{right\_expression}(\mathrm{magma}(\mathbb{Z},\times ),(3,2))=6$$

Signatures:

sts