OpenMath Content Dictionary: group2

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

group2.ocd

CD as XML Encoded OpenMath:

group2.omcd

Defines:

conjugation, is_automorphism, is_endomorphism, is_homomorphism, is_isomorphism, isomorphic, left_multiplication, right_inverse_multiplication, right_multiplication

Date:

2004-06-01

Version:

1 (Revision 3)

Review Date:

2006-06-01

Status:

experimental

A CD of functions like homomorphisms for groups

Written by Arjeh M. Cohen 2004-02-20.
Edited AMC 2004-03-02

is_homomorphism

Description:

This symbol is a boolean function with three arguments. The first two arguments are groups M, N, the third is a map f from the element set of M to the element set of N. When applied to M, N, and f, it denotes that f is a group homomorphism from M to N.

Commented Mathematical property (CMP):

If is_homomorphism(M,N,f) then, for each pair of elements x, y of M, we have f(x * y) = f(x) * f(y).

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="group2" name="is_homomorphism"/>
            <OMV name="M"/> <OMV name="N"/>  <OMV name="f"/>
       </OMA>
       <OMBIND><OMS cd="quant1" name="forall"/>
            <OMBVAR><OMV name="x"/><OMV name="y"/>  </OMBVAR>
            <OMA><OMS cd="logic1" name="implies"/>
                 <OMA><OMS cd="logic1" name="and"/>
                      <OMA><OMS cd="set1" name="in"/>
                           <OMV name="x"/>
                           <OMA><OMS cd="group1" name="carrier"/>
                                <OMV name="M"/>
                           </OMA>
                      </OMA>
	              <OMA><OMS cd="set1" name="in"/>
                           <OMV name="y"/>
                           <OMA><OMS cd="group1" name="carrier"/>
                                <OMV name="G"/>
                           </OMA>
                      </OMA>
                 </OMA>
                 <OMA><OMS cd="relation1" name="eq"/>
                      <OMA><OMV name="f"/>
                           <OMA><OMS cd="arith1" name="times"/>
	                        <OMV name="x"/> <OMV name="y"/>
                           </OMA>
                      </OMA>
                      <OMA><OMS cd="arith1" name="times"/>
                           <OMA><OMV name="f"/>
                                <OMV name="y"/>
                           </OMA>
                           <OMA><OMV name="f"/>
                                <OMV name="x"/>
                           </OMA>
                      </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="group2">is_homomorphism</csymbol><ci>M</ci><ci>N</ci><ci>f</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>x</ci></bvar>
   <bvar><ci>y</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>x</ci>
      <apply><csymbol cd="group1">carrier</csymbol><ci>M</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>y</ci>
      <apply><csymbol cd="group1">carrier</csymbol><ci>G</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply>
      <ci>f</ci>
      <apply><csymbol cd="arith1">times</csymbol><ci>x</ci><ci>y</ci></apply>
     </apply>
     <apply><csymbol cd="arith1">times</csymbol>
      <apply><ci>f</ci><ci>y</ci></apply>
      <apply><ci>f</ci><ci>x</ci></apply>
     </apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (is_homomorphism ( M, N, f) , forall [ x y ] . (implies (and (in ( x, carrier ( M) ) , in ( y, carrier ( G) ) ) , eq ( f (times ( x, y) ) , times ( f ( y) , f ( x) ) ) ) ) )

Popcorn

group2.is_homomorphism($M, $N, $f) ==> quant1.forall[$x, $y -> set1.in($x, group1.carrier($M)) and set1.in($y, group1.carrier($G)) ==> $f($x * $y) = $f($y) * $f($x)]

Rendered Presentation MathML

$$\mathrm{is\_homomorphism}(M,N,f)\Rightarrow \forall \hspace{0.17em}x,y.x\in \mathrm{carrier}\left(M\right)\wedge y\in \mathrm{carrier}\left(G\right)\Rightarrow f\left(xy\right)=f\left(y\right)f\left(x\right)$$

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="group2" name="is_homomorphism"/>
          <OMV name="M"/>  <OMV name="N"/> <OMV name="f"/>
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="group2">is_homomorphism</csymbol><ci>M</ci><ci>N</ci><ci>f</ci></apply>
</math>

Prefix

is_homomorphism ( M, N, f)

Popcorn

group2.is_homomorphism($M, $N, $f)

Rendered Presentation MathML

$$\mathrm{is\_homomorphism}(M,N,f)$$

Signatures:

sts

is_isomorphism

Description:

This symbol is a boolean function with three arguments. The first and arguments are groups M, N, the third is a map f from the element set of M to the element set of N. When applied to M, N, and f, it denotes that f is a group isomorphism from M to N. This means that f is a homomorphism from M to N, that f is bijective, and that its inverse is a homomorphism from N to M.

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="group2" name="is_isomorphism"/>
          <OMV name="M"/>  <OMV name="N"/> <OMV name="f"/>
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="group2">is_isomorphism</csymbol><ci>M</ci><ci>N</ci><ci>f</ci></apply>
</math>

Prefix

is_isomorphism ( M, N, f)

Popcorn

group2.is_isomorphism($M, $N, $f)

Rendered Presentation MathML

$$\mathrm{is\_isomorphism}(M,N,f)$$

Signatures:

sts

isomorphic

Description:

This symbol is a Boolean function with n arguments, n at least 2, which are groups. When applied to M_1, ..., M_n, it denotes the fact that there is an isomorphism from each M_i to each M_j.

Example:

OpenMath XML (source)

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

Strict Content MathML

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

Prefix

isomorphic ( M, N)

Popcorn

group2.isomorphic($M, $N)

Rendered Presentation MathML

$$\mathrm{isomorphic}(M,N)$$

Signatures:

sts

is_endomorphism

Description:

This symbol is a boolean function with two arguments. The first argument is a group M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes that f is a group endomorphism from M to M.

Commented Mathematical property (CMP):

If is_endomorphism(M,f) then is_homomorphism(M,M,f)

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="group2" name="is_endomorphism"/>
            <OMV name="M"/>  <OMV name="f"/>
       </OMA>
       <OMA><OMS cd="group2" name="is_homomorphism"/>
            <OMV name="M"/> <OMV name="M"/>  <OMV name="f"/>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="group2">is_endomorphism</csymbol><ci>M</ci><ci>f</ci></apply>
  <apply><csymbol cd="group2">is_homomorphism</csymbol><ci>M</ci><ci>M</ci><ci>f</ci></apply>
 </apply>
</math>

Prefix

implies (is_endomorphism ( M, f) , is_homomorphism ( M, M, f) )

Popcorn

group2.is_endomorphism($M, $f) ==> group2.is_homomorphism($M, $M, $f)

Rendered Presentation MathML

$$\mathrm{is\_endomorphism}(M,f)\Rightarrow \mathrm{is\_homomorphism}(M,M,f)$$

Example:

OpenMath XML (source)

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

Strict Content MathML

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

Prefix

is_endomorphism ( M, f)

Popcorn

group2.is_endomorphism($M, $f)

Rendered Presentation MathML

$$\mathrm{is\_endomorphism}(M,f)$$

Signatures:

sts

is_automorphism

Description:

This symbol is a boolean function with two arguments. The first is a group M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes a group automorphism f of M.

Commented Mathematical property (CMP):

If is_automorphism(M,f) then is_isomorphism(M,M,f)

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="group2" name="is_automorphism"/>
            <OMV name="M"/>  <OMV name="f"/>
       </OMA>
       <OMA><OMS cd="group2" name="is_isomorphism"/>
            <OMV name="M"/> <OMV name="M"/>  <OMV name="f"/>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="group2">is_automorphism</csymbol><ci>M</ci><ci>f</ci></apply>
  <apply><csymbol cd="group2">is_isomorphism</csymbol><ci>M</ci><ci>M</ci><ci>f</ci></apply>
 </apply>
</math>

Prefix

implies (is_automorphism ( M, f) , is_isomorphism ( M, M, f) )

Popcorn

group2.is_automorphism($M, $f) ==> group2.is_isomorphism($M, $M, $f)

Rendered Presentation MathML

$$\mathrm{is\_automorphism}(M,f)\Rightarrow \mathrm{is\_isomorphism}(M,M,f)$$

Example:

OpenMath XML (source)

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

Strict Content MathML

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

Prefix

is_automorphism ( M, f)

Popcorn

group2.is_automorphism($M, $f)

Rendered Presentation MathML

$$\mathrm{is\_automorphism}(M,f)$$

Signatures:

sts

left_multiplication

Description:

This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes left multiplication on M by x.

Commented Mathematical property (CMP):

left_multiplication(M,x) (y) = x * y.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
       <OMBIND><OMS cd="quant1" name="forall"/>
            <OMBVAR><OMV name="M"/><OMV name="x"/><OMV name="y"/>  </OMBVAR>
            <OMA><OMS cd="relation1" name="eq"/>
                 <OMA><OMA><OMS cd="group2" name="left_multiplication"/>
                           <OMV name="M"/> <OMV name="x"/>
                      </OMA>
                      <OMV name="y"/>
                 </OMA>
                 <OMA><OMS cd="group1" name="multiplication"/>
                      <OMV name="M"/>
                      <OMV name="x"/><OMV name="y"/>
                 </OMA>
             </OMA>
        </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>M</ci></bvar>
  <bvar><ci>x</ci></bvar>
  <bvar><ci>y</ci></bvar>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply>
    <apply><csymbol cd="group2">left_multiplication</csymbol><ci>M</ci><ci>x</ci></apply>
    <ci>y</ci>
   </apply>
   <apply><csymbol cd="group1">multiplication</csymbol><ci>M</ci><ci>x</ci><ci>y</ci></apply>
  </apply>
 </bind>
</math>

Prefix

forall [ M x y ] . (eq (left_multiplication ( M, x) ( y) , multiplication ( M, x, y) ) )

Popcorn

quant1.forall[$M, $x, $y -> group2.left_multiplication($M, $x)($y) = group1.multiplication($M, $x, $y)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}M,x,y.\left(\mathrm{left\_multiplication}(M,x)\right)\left(y\right)=\mathrm{multiplication}(M,x,y)$$

Signatures:

sts

right_multiplication

Description:

This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes right multiplication on M by x.

Commented Mathematical property (CMP):

right_multiplication(M,x) (y) = y * x.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
       <OMBIND><OMS cd="quant1" name="forall"/>
            <OMBVAR><OMV name="M"/><OMV name="x"/><OMV name="y"/>  </OMBVAR>
            <OMA><OMS cd="relation1" name="eq"/>
                 <OMA><OMA><OMS cd="group2" name="right_multiplication"/>
                           <OMV name="M"/> <OMV name="x"/>
                      </OMA>
                      <OMV name="y"/>
                 </OMA>
                 <OMA><OMS cd="group1" name="multiplication"/>
                      <OMV name="M"/>
                      <OMV name="y"/><OMV name="x"/>
                 </OMA>
             </OMA>
        </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>M</ci></bvar>
  <bvar><ci>x</ci></bvar>
  <bvar><ci>y</ci></bvar>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply>
    <apply><csymbol cd="group2">right_multiplication</csymbol><ci>M</ci><ci>x</ci></apply>
    <ci>y</ci>
   </apply>
   <apply><csymbol cd="group1">multiplication</csymbol><ci>M</ci><ci>y</ci><ci>x</ci></apply>
  </apply>
 </bind>
</math>

Prefix

forall [ M x y ] . (eq (right_multiplication ( M, x) ( y) , multiplication ( M, y, x) ) )

Popcorn

quant1.forall[$M, $x, $y -> group2.right_multiplication($M, $x)($y) = group1.multiplication($M, $y, $x)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}M,x,y.\left(\mathrm{right\_multiplication}(M,x)\right)\left(y\right)=\mathrm{multiplication}(M,y,x)$$

Signatures:

sts

right_inverse_multiplication

Description:

This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes right multiplication on M by the inverse of x.

Commented Mathematical property (CMP):

right_inverse_multiplication(M,x) (y) = y * x^(-1).

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
       <OMBIND><OMS cd="quant1" name="forall"/>
            <OMBVAR><OMV name="M"/><OMV name="x"/><OMV name="y"/>  </OMBVAR>
            <OMA><OMS cd="relation1" name="eq"/>
                 <OMA><OMA><OMS cd="group2" name="right_inverse_multiplication"/>
                           <OMV name="M"/> <OMV name="x"/>
                      </OMA>
                      <OMV name="y"/>
                 </OMA>
                 <OMA><OMS cd="group1" name="multiplication"/>
                      <OMV name="M"/>
                      <OMV name="y"/>
                      <OMA><OMS cd="arith1" name="power"/>
                           <OMV name="x"/><OMI>-1</OMI>
                      </OMA>
                 </OMA>
             </OMA>
        </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>M</ci></bvar>
  <bvar><ci>x</ci></bvar>
  <bvar><ci>y</ci></bvar>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply>
    <apply><csymbol cd="group2">right_inverse_multiplication</csymbol><ci>M</ci><ci>x</ci></apply>
    <ci>y</ci>
   </apply>
   <apply><csymbol cd="group1">multiplication</csymbol>
    <ci>M</ci>
    <ci>y</ci>
    <apply><csymbol cd="arith1">power</csymbol><ci>x</ci><cn>-1</cn></apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

forall [ M x y ] . (eq (right_inverse_multiplication ( M, x) ( y) , multiplication ( M, y, power ( x, -1) ) ) )

Popcorn

quant1.forall[$M, $x, $y -> group2.right_inverse_multiplication($M, $x)($y) = group1.multiplication($M, $y, $x ^ -1)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}M,x,y.\left(\mathrm{right\_inverse\_multiplication}(M,x)\right)\left(y\right)=\mathrm{multiplication}(M,y,x^{-1})$$

Signatures:

sts

conjugation

Description:

This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes conjugation on M by x.

Commented Mathematical property (CMP):

conjugation(M,x) (y) = x * y * x^ {-1}.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
       <OMBIND><OMS cd="quant1" name="forall"/>
            <OMBVAR><OMV name="M"/><OMV name="x"/><OMV name="y"/>  </OMBVAR>
            <OMA><OMS cd="relation1" name="eq"/>
                 <OMA><OMA><OMS cd="group2" name="conjugation"/>
                           <OMV name="M"/> <OMV name="x"/>
                      </OMA>
                      <OMV name="y"/>
                 </OMA>
                 <OMA><OMS cd="group1" name="expression"/>
                      <OMV name="M"/>
                      <OMA><OMS cd="arith1" name="times"/>
                           <OMV name="x"/>
                           <OMV name="y"/>
                           <OMA><OMS cd="arith1" name="power"/>
                                <OMV name="x"/>
                                <OMI> -1</OMI>
                           </OMA>
                      </OMA>
                 </OMA>
            </OMA>
       </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>M</ci></bvar>
  <bvar><ci>x</ci></bvar>
  <bvar><ci>y</ci></bvar>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply>
    <apply><csymbol cd="group2">conjugation</csymbol><ci>M</ci><ci>x</ci></apply>
    <ci>y</ci>
   </apply>
   <apply><csymbol cd="group1">expression</csymbol>
    <ci>M</ci>
    <apply><csymbol cd="arith1">times</csymbol>
     <ci>x</ci>
     <ci>y</ci>
     <apply><csymbol cd="arith1">power</csymbol><ci>x</ci><cn>-1</cn></apply>
    </apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

forall [ M x y ] . (eq (conjugation ( M, x) ( y) , expression ( M, times ( x, y, power ( x, -1) ) ) ) )

Popcorn

quant1.forall[$M, $x, $y -> group2.conjugation($M, $x)($y) = group1.expression($M, $x * $y * $x ^ -1)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}M,x,y.\left(\mathrm{conjugation}(M,x)\right)\left(y\right)=\mathrm{expression}(M,xy{x}^{-1})$$

Signatures:

sts