OpenMath Content Dictionary: semigroup1

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

semigroup1.ocd

CD as XML Encoded OpenMath:

semigroup1.omcd

Defines:

carrier, is_commutative, is_subsemigroup, multiplication, semigroup, subsemigroup, expression, factor_of, magma

Date:

2004-06-01

Version:

3 (Revision 1)

Review Date:

2006-06-01

Status:

experimental

Basic functions for semigroup theory

Initiated by Arjeh M. Cohen 2003-05-17
Edited AMC 2004-0304

semigroup

Description:

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

Commented Mathematical property (CMP):

A semigroup is closed under its operation. A semigroup operation is associative.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="S"/>
      <OMA>
        <OMS cd="semigroup1" name="semigroup"/>
	<OMV name="set"/>
	<OMV name="binop"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <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>
        <OMS cd="relation1" name="eq"/>
	<OMA>
	  <OMV name="binop"/>
	  <OMV name="x"/>
	  <OMA>
	    <OMV name="binop"/>
	    <OMV name="y"/>
	    <OMV name="z"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMV name="binop"/>
	  <OMA>
	    <OMV name="binop"/>
	    <OMV name="x"/>
	    <OMV name="y"/>
	  </OMA>
	  <OMV name="z"/>
	</OMA>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="relation1">eq</csymbol>
   <ci>S</ci>
   <apply><csymbol cd="semigroup1">semigroup</csymbol><ci>set</ci><ci>binop</ci></apply>
  </apply>
  <apply><csymbol cd="logic1">and</csymbol>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol><ci>x</ci><ci>set</ci></apply>
     <apply><csymbol cd="set1">in</csymbol><ci>y</ci><ci>set</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><ci>binop</ci><ci>x</ci><ci>y</ci></apply>
     <ci>set</ci>
    </apply>
   </apply>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply>
     <ci>binop</ci>
     <ci>x</ci>
     <apply><ci>binop</ci><ci>y</ci><ci>z</ci></apply>
    </apply>
    <apply>
     <ci>binop</ci>
     <apply><ci>binop</ci><ci>x</ci><ci>y</ci></apply>
     <ci>z</ci>
    </apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

implies (eq ( S, semigroup ( set, binop) ) , and (implies (and (in ( x, set) , in ( y, set) ) , in ( binop ( x, y) , set) ) , eq ( binop ( x, binop ( y, z) ) , binop ( binop ( x, y) , z) ) ) )

Popcorn

$S = semigroup1.semigroup($set, $binop) ==> (set1.in($x, $set) and set1.in($y, $set) ==> set1.in($binop($x, $y), $set)) and $binop($x, $binop($y, $z)) = $binop($binop($x, $y), $z)

Rendered Presentation MathML

$$S=\mathrm{semigroup}(\mathrm{set},\mathrm{binop})\Rightarrow (x\in \mathrm{set}\wedge y\in \mathrm{set}\Rightarrow \mathrm{binop}(x,y)\in \mathrm{set})\wedge \mathrm{binop}(x,\mathrm{binop}(y,z))=\mathrm{binop}(\mathrm{binop}(x,y),z)$$

Example:

This example represents the semigroup of all functions f: R -> R with function composition as the operation.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="semigroup1" name="semigroup"/>
    <OMA><OMS cd="arith1" name="power"/>
      <OMS cd="setname1" name="R"/>
      <OMS cd="setname1" name="R"/>
    </OMA>
    <OMS cd="fns1" name="left_compose"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="semigroup1">semigroup</csymbol>
  <apply><csymbol cd="arith1">power</csymbol>
   <csymbol cd="setname1">R</csymbol>
   <csymbol cd="setname1">R</csymbol>
  </apply>
  <csymbol cd="fns1">left_compose</csymbol>
 </apply>
</math>

Prefix

semigroup (power (R, R) , left_compose)

Popcorn

semigroup1.semigroup(setname1.R ^ setname1.R, fns1.left_compose)

Rendered Presentation MathML

$$\mathrm{semigroup}({\mathbb{R}}^{\mathbb{R}},o)$$

Signatures:

sts

carrier

Description:

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

Example:

The carrier of semigroup(S,*) is S.

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="semigroup1">carrier</csymbol>
   <apply><csymbol cd="semigroup1">semigroup</csymbol><ci>S</ci><ci>times</ci></apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

eq (carrier (semigroup ( S, times) ) , S)

Popcorn

semigroup1.carrier(semigroup1.semigroup($S, $times)) = $S

Rendered Presentation MathML

$$\mathrm{carrier}\left(\mathrm{semigroup}(S,\mathrm{times})\right)=S$$

Signatures:

sts

multiplication

Description:

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

Example:

The multiplication of semigroup(S,*) is *.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="semigroup1" name="multiplication"/>
            <OMA><OMS cd="semigroup1" name="semigroup"/>
                 <OMV name="S"/>  <OMV name="times"/>
            </OMA>
       </OMA>
       <OMV name="times"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="semigroup1">multiplication</csymbol>
   <apply><csymbol cd="semigroup1">semigroup</csymbol><ci>S</ci><ci>times</ci></apply>
  </apply>
  <ci>times</ci>
 </apply>
</math>

Prefix

eq (multiplication (semigroup ( S, times) ) , times)

Popcorn

semigroup1.multiplication(semigroup1.semigroup($S, $times)) = $times

Rendered Presentation MathML

$$\mathrm{multiplication}\left(\mathrm{semigroup}(S,\mathrm{times})\right)=\mathrm{times}$$

Signatures:

sts

is_commutative

Description:

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

Commented Mathematical property (CMP):

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

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="semigroup1" name="is_commutative"/>
      <OMV name="S"/>
    </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="semigroup1" name="carrier"/>
	      <OMV name="S"/>
	    </OMA>
	  </OMA>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="b"/>
	    <OMA>
	      <OMS cd="semigroup1" name="carrier"/>
	      <OMV name="S"/>
	    </OMA>
	  </OMA>
	</OMA>
	<OMA><OMS cd="relation1" name="eq"/>
          <OMA>
            <OMA><OMS cd="semigroup1" name="multiplication"/>
              <OMV name="S"/>
            </OMA>
	    <OMV name="a"/>
	    <OMV name="b"/>
	  </OMA>
	  <OMA>
            <OMA><OMS cd="semigroup1" name="multiplication"/>
              <OMV name="S"/>
            </OMA>
	    <OMV name="b"/>
	    <OMV name="a"/>
	  </OMA>
	</OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="semigroup1">is_commutative</csymbol><ci>S</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="semigroup1">carrier</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>b</ci>
      <apply><csymbol cd="semigroup1">carrier</csymbol><ci>S</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply>
      <apply><csymbol cd="semigroup1">multiplication</csymbol><ci>S</ci></apply>
      <ci>a</ci>
      <ci>b</ci>
     </apply>
     <apply>
      <apply><csymbol cd="semigroup1">multiplication</csymbol><ci>S</ci></apply>
      <ci>b</ci>
      <ci>a</ci>
     </apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

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

Popcorn

semigroup1.is_commutative($S) ==> quant1.forall[$a, $b -> set1.in($a, semigroup1.carrier($S)) and set1.in($b, semigroup1.carrier($S)) ==> semigroup1.multiplication($S)($a, $b) = semigroup1.multiplication($S)($b, $a)]

Rendered Presentation MathML

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

Signatures:

sts

is_subsemigroup

Description:

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

Commented Mathematical property (CMP):

If is_subsemigroup(S,T) then T is a set of elements of S and T is closed under multiplication.

Signatures:

sts

magma

Description:

This symbol is a unary function. Its argument should be a semigroup S. When applied to S, it denotes the magma with the same element set and binary operation as S.

Example:

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="semigroup1">magma</csymbol>
   <apply><csymbol cd="semigroup1">semigroup</csymbol><ci>X</ci><ci>times</ci></apply>
  </apply>
  <apply><csymbol cd="magma1">magma</csymbol><ci>X</ci><ci>times</ci></apply>
 </apply>
</math>

Prefix

eq (magma (semigroup ( X, times) ) , magma ( X, times) )

Popcorn

semigroup1.magma(semigroup1.semigroup($X, $times)) = magma1.magma($X, $times)

Rendered Presentation MathML

$$\mathrm{magma}\left(\mathrm{semigroup}(X,\mathrm{times})\right)=\mathrm{magma}(X,\mathrm{times})$$

Signatures:

sts

subsemigroup

Description:

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

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="semigroup1" name="subsemigroup"/>
          <OMV name="S"/>  <OMV name="D"/>
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="semigroup1">subsemigroup</csymbol><ci>S</ci><ci>D</ci></apply></math>

Prefix

subsemigroup ( S, D)

Popcorn

semigroup1.subsemigroup($S, $D)

Rendered Presentation MathML

$$\mathrm{subsemigroup}(S,D)$$

Example:

This example represents the subsemigroup of the multiplicative semigroup of the nonzero reals generated by the constants Pi and E:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="semigroup1" name="semigroup"/>
     <OMA><OMS cd="semigroup1" name="semigroup"/>
          <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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="semigroup1">semigroup</csymbol>
  <apply><csymbol cd="semigroup1">semigroup</csymbol>
   <apply><csymbol cd="set1">suchthat</csymbol>
    <csymbol cd="setname1">R</csymbol>
    <bind><csymbol cd="fns1">lambda</csymbol>
     <bvar><ci>x</ci></bvar>
     <apply><csymbol cd="relation1">neq</csymbol><ci>x</ci><csymbol cd="alg1">zero</csymbol></apply>
    </bind>
   </apply>
   <csymbol cd="arith1">times</csymbol>
  </apply>
  <apply><csymbol cd="list1">list</csymbol>
   <csymbol cd="nums1">pi</csymbol>
   <csymbol cd="nums1">e</csymbol>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

semigroup1.semigroup(semigroup1.semigroup(set1.suchthat(setname1.R, fns1.lambda[$x -> $x != alg1.zero]), arith1.times), [nums1.pi , nums1.e])

Rendered Presentation MathML

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

Signatures:

sts

factor_of

Description:

This symbol is a ternary function. Its first argument should be a semigroup S and the second and third arguments should be elements of S. When applied to S, a, and b, it denotes the fact that a is a divisor of b in S. This means that there are u,v in carrier(S) such that uav=b.

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="semigroup1" name="factor_of"/>
          <OMV name="S"/>          <OMV name="a"/>          <OMV name="b"/>
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="semigroup1">factor_of</csymbol><ci>S</ci><ci>a</ci><ci>b</ci></apply>
</math>

Prefix

factor_of ( S, a, b)

Popcorn

semigroup1.factor_of($S, $a, $b)

Rendered Presentation MathML

$$\mathrm{factor\_of}(S,a,b)$$

Signatures:

sts

expression

Description:

This symbol is a function with two arguments. Its first argument should be a semigroup G. The second should be an arithmetic expression A, whose operators are times and power, and whose leaves are members of the carrier of G. The second argument of power should be positive. When applied to G and A, it denotes the element (of G) that is obtained from the leaves of A by applying the multiplication and the power map of G instead of the times and power of the CD arith1 appearing in A.

Example:

OpenMath XML (source)

  <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
         <OMA><OMS cd="group1" name="expression"/>
              <OMA><OMS cd="semigroup1" name="semigroup"/>
                   <OMS cd="setname1" name="Z"/>
                   <OMS cd="arith1" name="plus"/>
              </OMA>
              <OMA><OMS cd="arith1" name="times"/>
                   <OMI>2</OMI><OMI>3</OMI>
              </OMA>
         </OMA>
         <OMI>5</OMI>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="group1">expression</csymbol>
   <apply><csymbol cd="semigroup1">semigroup</csymbol>
    <csymbol cd="setname1">Z</csymbol>
    <csymbol cd="arith1">plus</csymbol>
   </apply>
   <apply><csymbol cd="arith1">times</csymbol><cn>2</cn><cn>3</cn></apply>
  </apply>
  <cn>5</cn>
 </apply>
</math>

Prefix

eq (expression (semigroup (Z, plus) , times (2, 3) ) , 5)

Popcorn

group1.expression(semigroup1.semigroup(setname1.Z, arith1.plus), 2 * 3) = 5

Rendered Presentation MathML

$$\mathrm{expression}(\mathrm{semigroup}(\mathbb{Z},+),2\times 3)=5$$

Signatures:

sts