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
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
is_homomorphism
(
M
,
N
,
f
)
⇒
∀
x
,
y
.
x
∈
carrier
(
M
)
∧
y
∈
carrier
(
G
)
⇒
f
(
x
y
)
=
f
(
y
)
f
(
x
)
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
Popcorn
group2.is_homomorphism($M, $N, $f)
Rendered Presentation MathML
is_homomorphism
(
M
,
N
,
f
)
Signatures:
sts
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
Popcorn
group2.is_isomorphism($M, $N, $f)
Rendered Presentation MathML
is_isomorphism
(
M
,
N
,
f
)
Signatures:
sts
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
Popcorn
group2.isomorphic($M, $N)
Rendered Presentation MathML
Signatures:
sts
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
Popcorn
group2.is_endomorphism($M, $f) ==> group2.is_homomorphism($M, $M, $f)
Rendered Presentation MathML
is_endomorphism
(
M
,
f
)
⇒
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
Popcorn
group2.is_endomorphism($M, $f)
Rendered Presentation MathML
is_endomorphism
(
M
,
f
)
Signatures:
sts
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
Popcorn
group2.is_automorphism($M, $f) ==> group2.is_isomorphism($M, $M, $f)
Rendered Presentation MathML
is_automorphism
(
M
,
f
)
⇒
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
Popcorn
group2.is_automorphism($M, $f)
Rendered Presentation MathML
is_automorphism
(
M
,
f
)
Signatures:
sts
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
Popcorn
quant1.forall[$M, $x, $y -> group2.left_multiplication($M, $x)($y) = group1.multiplication($M, $x, $y)]
Rendered Presentation MathML
∀
M
,
x
,
y
.
(
left_multiplication
(
M
,
x
)
)
(
y
)
=
multiplication
(
M
,
x
,
y
)
Signatures:
sts
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
Popcorn
quant1.forall[$M, $x, $y -> group2.right_multiplication($M, $x)($y) = group1.multiplication($M, $y, $x)]
Rendered Presentation MathML
∀
M
,
x
,
y
.
(
right_multiplication
(
M
,
x
)
)
(
y
)
=
multiplication
(
M
,
y
,
x
)
Signatures:
sts
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 type="integer">-1</cn></apply>
</apply>
</apply>
</bind>
</math>
Prefix
Popcorn
quant1.forall[$M, $x, $y -> group2.right_inverse_multiplication($M, $x)($y) = group1.multiplication($M, $y, $x ^ -1)]
Rendered Presentation MathML
∀
M
,
x
,
y
.
(
right_inverse_multiplication
(
M
,
x
)
)
(
y
)
=
multiplication
(
M
,
y
,
x
-1
)
Signatures:
sts
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 type="integer">-1</cn></apply>
</apply>
</apply>
</apply>
</bind>
</math>
Prefix
Popcorn
quant1.forall[$M, $x, $y -> group2.conjugation($M, $x)($y) = group1.expression($M, $x * $y * $x ^ -1)]
Rendered Presentation MathML
∀
M
,
x
,
y
.
(
conjugation
(
M
,
x
)
)
(
y
)
=
expression
(
M
,
x
y
x
-1
)
Signatures:
sts