OpenMath Content Dictionary: monoid1

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

monoid1.ocd

CD as XML Encoded OpenMath:

monoid1.omcd

Defines:

carrier, divisor_of, expression, identity, invertibles, is_commutative, is_invertible, is_submonoid, monoid, multiplication, semigroup, submonoid

Date:

2004-06-01

Version:

3 (Revision 2)

Review Date:

2006-06-01

Status:

experimental

---

Basic functions for monoid theory

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

---

monoid

Description:

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

Commented Mathematical property (CMP):

A monoid is closed under its operation. A monoid operation is associative. A monoid has an identity element.

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="M"/>
      <OMA>
        <OMS cd="monoid1" name="monoid"/>
        <OMV name="set"/>
        <OMV name="binop"/>
        <OMV name="elt"/>
      </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>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="elt"/>
          <OMV name="set"/>
        </OMA>
        <OMBIND>
          <OMS cd="quant1" name="forall"/>
          <OMBVAR>
            <OMV name="x"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="set1" name="in"/>
              <OMV name="x"/>
              <OMV name="set"/>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="and"/>
              <OMA>
                <OMS cd="relation1" name="eq"/>
                <OMA>
                  <OMV name="binop"/>
                  <OMV name="elt"/>
                  <OMV name="x"/>
                </OMA>
                <OMV name="x"/>
              </OMA>
              <OMA>
                <OMS cd="relation1" name="eq"/>
                <OMA>
                  <OMV name="binop"/>
                  <OMV name="x"/>
                  <OMV name="elt"/>
                </OMA>
                <OMV name="x"/>
              </OMA>
            </OMA>
          </OMA>
        </OMBIND>
      </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>M</ci>
   <apply><csymbol cd="monoid1">monoid</csymbol><ci>set</ci><ci>binop</ci><ci>elt</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><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol><ci>elt</ci><ci>set</ci></apply>
    <bind><csymbol cd="quant1">forall</csymbol>
     <bvar><ci>x</ci></bvar>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="set1">in</csymbol><ci>x</ci><ci>set</ci></apply>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply><csymbol cd="relation1">eq</csymbol>
        <apply><ci>binop</ci><ci>elt</ci><ci>x</ci></apply>
        <ci>x</ci>
       </apply>
       <apply><csymbol cd="relation1">eq</csymbol>
        <apply><ci>binop</ci><ci>x</ci><ci>elt</ci></apply>
        <ci>x</ci>
       </apply>
      </apply>
     </apply>
    </bind>
   </apply>
  </apply>
 </apply>
</math>

Prefix

implies (eq ( M, monoid ( set, binop, elt) ) , 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) ) , and (in ( elt, set) , forall [ x ] . (implies (in ( x, set) , and (eq ( binop ( elt, x) , x) , eq ( binop ( x, elt) , x) ) ) ) ) ) )

Popcorn

$M = monoid1.monoid($set, $binop, $elt) ==> (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) and set1.in($elt, $set) and quant1.forall[$x -> set1.in($x, $set) ==> $binop($elt, $x) = $x and $binop($x, $elt) = $x]

Rendered Presentation MathML

$$M=\mathrm{monoid}(\mathrm{set},\mathrm{binop},\mathrm{elt})\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)\wedge \mathrm{elt}\in \mathrm{set}\wedge \forall \hspace{0.17em}x.x\in \mathrm{set}\Rightarrow \mathrm{binop}(\mathrm{elt},x)=x\wedge \mathrm{binop}(x,\mathrm{elt})=x$$

Example:

This example represents the monoid which has as elements all positive and negative even numbers, the monoid operation is binary addition, inverses are the negative of the element and the identity is the zero element.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="monoid1" name="monoid"/>
       <OMA><OMS cd="set1" name="suchthat"/>
            <OMS cd="setname1" name="Z"/>
            <OMBIND><OMS cd="fns1" name="lambda"/>
                    <OMBVAR> <OMV name="x"/>  </OMBVAR>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMA><OMS cd="arith1" name="divide"/>
                              <OMV name="x"/>
                              <OMI> 2 </OMI>
                         </OMA>
                         <OMS cd="setname1" name="Z"/>
                    </OMA>
            </OMBIND>
       </OMA>
       <OMS cd="arith1" name="plus"/>
       <OMI>0</OMI>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="monoid1">monoid</csymbol>
  <apply><csymbol cd="set1">suchthat</csymbol>
   <csymbol cd="setname1">Z</csymbol>
   <bind><csymbol cd="fns1">lambda</csymbol>
    <bvar><ci>x</ci></bvar>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><csymbol cd="arith1">divide</csymbol><ci>x</ci><cn type="integer">2</cn></apply>
     <csymbol cd="setname1">Z</csymbol>
    </apply>
   </bind>
  </apply>
  <csymbol cd="arith1">plus</csymbol>
  <cn type="integer">0</cn>
 </apply>
</math>

Prefix

monoid (suchthat (Z, lambda [ x ] . (in (divide ( x, 2 ) , Z) ) ) , plus, 0)

Popcorn

monoid1.monoid(set1.suchthat(setname1.Z, fns1.lambda[$x -> set1.in($x / 2, setname1.Z)]), arith1.plus, 0)

Rendered Presentation MathML

$$\mathrm{monoid}(\left\{x\in \mathbb{Z}\right|\frac{x}{2}\in \mathbb{Z}\},+,0)$$

Signatures:

sts

---

[Next: carrier] [Last: expression] [Top]

---

carrier

Description:

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

Example:

The carrier of monoid(M,*,e) is M.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="monoid1" name="carrier"/>
            <OMA><OMS cd="monoid1" name="monoid"/>
                 <OMV name="M"/>  <OMV name="times"/> <OMV name="e"/>
            </OMA>
       </OMA>
       <OMV name="M"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="monoid1">carrier</csymbol>
   <apply><csymbol cd="monoid1">monoid</csymbol><ci>M</ci><ci>times</ci><ci>e</ci></apply>
  </apply>
  <ci>M</ci>
 </apply>
</math>

Prefix

eq (carrier (monoid ( M, times, e) ) , M)

Popcorn

monoid1.carrier(monoid1.monoid($M, $times, $e)) = $M

Rendered Presentation MathML

$$\mathrm{carrier}\left(\mathrm{monoid}(M,\mathrm{times},e)\right)=M$$

Signatures:

sts

---

[Next: multiplication] [Previous: monoid] [Top]

---

multiplication

Description:

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

Example:

The multiplication of monoid(M,*,e) is *.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="monoid1" name="multiplication"/>
            <OMA><OMS cd="monoid1" name="monoid"/>
                 <OMV name="M"/>  <OMV name="times"/> <OMV name="e"/>
            </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="monoid1">multiplication</csymbol>
   <apply><csymbol cd="monoid1">monoid</csymbol><ci>M</ci><ci>times</ci><ci>e</ci></apply>
  </apply>
  <ci>times</ci>
 </apply>
</math>

Prefix

eq (multiplication (monoid ( M, times, e) ) , times)

Popcorn

monoid1.multiplication(monoid1.monoid($M, $times, $e)) = $times

Rendered Presentation MathML

$$\mathrm{multiplication}\left(\mathrm{monoid}(M,\mathrm{times},e)\right)=\mathrm{times}$$

Example:

The product a_1 * ... * a_n of elements a_1, ..., a_n of M can be expressed as follows.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="fns2" name="apply_to_list"/>
         <OMA><OMA><OMS cd="monoid1" name="multiplication"/>
                   <OMV name="M"/>
              </OMA>         
              <OMA><OMS cd="list3" name="list_of_lengthn"/>
                   <OMV name="n"/>  <OMV name="a"/>
              </OMA>
         </OMA>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="fns2">apply_to_list</csymbol>
  <apply>
   <apply><csymbol cd="monoid1">multiplication</csymbol><ci>M</ci></apply>
   <apply><csymbol cd="list3">list_of_lengthn</csymbol><ci>n</ci><ci>a</ci></apply>
  </apply>
 </apply>
</math>

Prefix

apply_to_list (multiplication ( M) (list_of_lengthn ( n, a) ) )

Popcorn

fns2.apply_to_list(monoid1.multiplication($M)(list3.list_of_lengthn($n, $a)))

Rendered Presentation MathML

$$\mathrm{apply\_to\_list}\left(\left(\mathrm{multiplication}\left(M\right)\right)\left(\mathrm{list\_of\_lengthn}(n,a)\right)\right)$$

Signatures:

sts

---

[Next: identity] [Previous: carrier] [Top]

---

identity

Description:

This symbols represents a unary function, whose argument should be a monoid. It returns the identity element of the monoid.

Example:

The identity of monoid(M,*,e) is e.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="monoid1" name="identity"/>
            <OMA><OMS cd="monoid1" name="monoid"/>
                 <OMV name="M"/>  <OMV name="times"/> <OMV name="e"/>
            </OMA>
       </OMA>
       <OMV name="e"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="monoid1">identity</csymbol>
   <apply><csymbol cd="monoid1">monoid</csymbol><ci>M</ci><ci>times</ci><ci>e</ci></apply>
  </apply>
  <ci>e</ci>
 </apply>
</math>

Prefix

eq (identity (monoid ( M, times, e) ) , e)

Popcorn

monoid1.identity(monoid1.monoid($M, $times, $e)) = $e

Rendered Presentation MathML

$$\mathrm{identity}\left(\mathrm{monoid}(M,\mathrm{times},e)\right)=e$$

Signatures:

sts

---

[Next: is_commutative] [Previous: multiplication] [Top]

---

is_commutative

Description:

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

Commented Mathematical property (CMP):

If is_commutative(M) then for all a,b in carrier(M) 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="monoid1" name="is_commutative"/>
      <OMV name="M"/>
    </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="monoid1" name="carrier"/>
              <OMV name="M"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS cd="monoid1" name="carrier"/>
              <OMV name="M"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMS cd="monoid1" name="multiplication"/>
              <OMV name="M"/>
            </OMA>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMA>
          <OMA>
            <OMA>
              <OMS cd="monoid1" name="multiplication"/>
              <OMV name="M"/>
            </OMA>
            <OMV name="b"/>
            <OMV name="a"/>
          </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="monoid1">is_commutative</csymbol><ci>M</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="monoid1">carrier</csymbol><ci>M</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>b</ci>
      <apply><csymbol cd="monoid1">carrier</csymbol><ci>M</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="monoid1">multiplication</csymbol><ci>M</ci></apply>
     <ci>a</ci>
     <ci>b</ci>
    </apply>
    <apply>
     <apply><csymbol cd="monoid1">multiplication</csymbol><ci>M</ci></apply>
     <ci>b</ci>
     <ci>a</ci>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

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

Popcorn

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

Rendered Presentation MathML

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

Signatures:

sts

---

[Next: is_invertible] [Previous: identity] [Top]

---

is_invertible

Description:

This symbol represents a binary function, whose first argument is a monoid M and whose second argument is an element x of M. Its value is true iff the argument if x is invertible (that is, has a left and a right inverse) in M.

Commented Mathematical property (CMP):

x is invertible in M if and only if there is a in carrier(M) with a*x = x*a = 1.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="logic1" name="equivalent"/>
       <OMA><OMS cd="monoid1" name="is_invertible"/>
            <OMV name="M"/>            <OMV name="x"/>
       </OMA>
       <OMBIND><OMS cd="quant1" name="exists"/>
            <OMBVAR>   <OMV name="a"/>      </OMBVAR>
            <OMA><OMS cd="logic1" name="and"/>
                 <OMA><OMS cd="set1" name="in"/>
                      <OMV name="a"/>
                      <OMA><OMS cd="monoid1" name="carrier"/>
                           <OMV name="M"/>
                      </OMA>
                 </OMA>
                 <OMA><OMS cd="relation1" name="eq"/>
                      <OMA><OMA><OMS cd="monoid1" name="multiplication"/>
                                <OMV name="M"/>
                           </OMA>
                           <OMV name="x"/>
                           <OMV name="a"/>
                      </OMA>
                      <OMA><OMS cd="monoid1" name="identity"/>
                           <OMV name="M"/>
                      </OMA>
                 </OMA>
                 <OMA><OMS cd="relation1" name="eq"/>
                      <OMA><OMA><OMS cd="monoid1" name="multiplication"/>
                                <OMV name="M"/>
                           </OMA>
                           <OMV name="a"/>
                           <OMV name="x"/>
                      </OMA>
                      <OMA><OMS cd="monoid1" name="identity"/>
                           <OMV name="M"/>
                      </OMA>
                 </OMA>
            </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">equivalent</csymbol>
  <apply><csymbol cd="monoid1">is_invertible</csymbol><ci>M</ci><ci>x</ci></apply>
  <bind><csymbol cd="quant1">exists</csymbol>
   <bvar><ci>a</ci></bvar>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="monoid1">carrier</csymbol><ci>M</ci></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply>
      <apply><csymbol cd="monoid1">multiplication</csymbol><ci>M</ci></apply>
      <ci>x</ci>
      <ci>a</ci>
     </apply>
     <apply><csymbol cd="monoid1">identity</csymbol><ci>M</ci></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply>
      <apply><csymbol cd="monoid1">multiplication</csymbol><ci>M</ci></apply>
      <ci>a</ci>
      <ci>x</ci>
     </apply>
     <apply><csymbol cd="monoid1">identity</csymbol><ci>M</ci></apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

equivalent (is_invertible ( M, x) , exists [ a ] . (and (in ( a, carrier ( M) ) , eq (multiplication ( M) ( x, a) , identity ( M) ) , eq (multiplication ( M) ( a, x) , identity ( M) ) ) ) )

Popcorn

logic1.equivalent(monoid1.is_invertible($M, $x), quant1.exists[$a -> set1.in($a, monoid1.carrier($M)) and monoid1.multiplication($M)($x, $a) = monoid1.identity($M) and monoid1.multiplication($M)($a, $x) = monoid1.identity($M)])

Rendered Presentation MathML

$$\mathrm{is\_invertible}(M,x)\equiv \exists \hspace{0.17em}a.a\in \mathrm{carrier}\left(M\right)\wedge \left(\mathrm{multiplication}\left(M\right)\right)(x,a)=\mathrm{identity}\left(M\right)\wedge \left(\mathrm{multiplication}\left(M\right)\right)(a,x)=\mathrm{identity}\left(M\right)$$

Signatures:

sts

---

[Next: is_submonoid] [Previous: is_commutative] [Top]

---

is_submonoid

Description:

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

Commented Mathematical property (CMP):

If is_submonoid(M,N) then N is a nonempty set of elements of M and N is closed under multiplication and taking inverses.

Signatures:

sts

---

[Next: semigroup] [Previous: is_invertible] [Top]

---

semigroup

Description:

This symbol is a unary function, whose argument should be a monoid M. When applied to M its value is the semigroup underlying M.

Example:

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="monoid1">semigroup</csymbol><ci>M</ci></apply></math>

Prefix

semigroup ( M)

Popcorn

monoid1.semigroup($M)

Rendered Presentation MathML

$$\mathrm{semigroup}\left(M\right)$$

Signatures:

sts

---

[Next: submonoid] [Previous: is_submonoid] [Top]

---

submonoid

Description:

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

Example:

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="monoid1">submonoid</csymbol><ci>M</ci><ci>D</ci></apply></math>

Prefix

submonoid ( M, D)

Popcorn

monoid1.submonoid($M, $D)

Rendered Presentation MathML

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

Example:

This example represents the submonoid of the multiplicative monoid 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="monoid1" name="monoid"/>
     <OMA><OMS cd="monoid1" name="monoid"/>
          <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="monoid1">monoid</csymbol>
  <apply><csymbol cd="monoid1">monoid</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

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

Popcorn

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

Rendered Presentation MathML

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

Signatures:

sts

---

[Next: invertibles] [Previous: semigroup] [Top]

---

invertibles

Description:

This symbol is a unary function. Its argument should be a monoid M. When applied to M, it denotes the submonoid of M consisting of all invertible elements in M. This is a group.

Example:

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="monoid1">invertibles</csymbol><ci>M</ci></apply></math>

Prefix

invertibles ( M)

Popcorn

monoid1.invertibles($M)

Rendered Presentation MathML

$$\mathrm{invertibles}\left(M\right)$$

Signatures:

sts

---

[Next: divisor_of] [Previous: submonoid] [Top]

---

divisor_of

Description:

This symbol is a ternary function. Its first argument should be a monoid 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 divisor of b in M. This means that there are u,v in carrier(M) such that uav=b.

Example:

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="monoid1">divisor_of</csymbol><ci>M</ci><ci>a</ci><ci>b</ci></apply>
</math>

Prefix

divisor_of ( M, a, b)

Popcorn

monoid1.divisor_of($M, $a, $b)

Rendered Presentation MathML

$$\mathrm{divisor\_of}(M,a,b)$$

Signatures:

sts

---

[Next: expression] [Previous: invertibles] [Top]

---

expression

Description:

This symbol is a function with two arguments. Its first argument should be a monoid. 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 nonnegative. 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 from the CD arith1 appearing in A. The symbol alg1.one occurring in A will be interpreted as the identity of G.

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="monoid1" name="monoid"/>
                   <OMS cd="setname1" name="Z"/>
                   <OMS cd="arith1" name="plus"/>
                   <OMI>0</OMI>
              </OMA>
              <OMA><OMS cd="arith1" name="times"/>
                   <OMI>4</OMI><OMI>3</OMI>
              </OMA>
         </OMA>
         <OMI>7</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="monoid1">monoid</csymbol>
    <csymbol cd="setname1">Z</csymbol>
    <csymbol cd="arith1">plus</csymbol>
    <cn type="integer">0</cn>
   </apply>
   <apply><csymbol cd="arith1">times</csymbol>
    <cn type="integer">4</cn>
    <cn type="integer">3</cn>
   </apply>
  </apply>
  <cn type="integer">7</cn>
 </apply>
</math>

Prefix

eq (expression (monoid (Z, plus, 0) , times (4, 3) ) , 7)

Popcorn

group1.expression(monoid1.monoid(setname1.Z, arith1.plus, 0), 4 * 3) = 7

Rendered Presentation MathML

$$\mathrm{expression}(\mathrm{monoid}(\mathbb{Z},+,0),4\times 3)=7$$

Signatures:

sts

---

[First: monoid] [Previous: divisor_of] [Top]