:: On the Monoid of Endomorphisms of Universal Algebra \& Many
:: Sorted Algebra
:: by Jaros{\l}aw Gryko
::
:: Received October 17, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies UNIALG_1, FUNCT_2, STRUCT_0, FUNCT_1, MSUALG_3, SUBSET_1,
RELAT_1, XBOOLE_0, TARSKI, BINOP_1, ALGSTR_0, MESFUNC1, VECTSP_1,
GROUP_1, MSUALG_1, AUTALG_1, PBOOLE, MEMBER_1, CARD_1, FUNCOP_1,
MSUHOM_1, MSSUBFAM, GROUP_6, WELLORD1, ZFMISC_1, ENDALG;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE,
CARD_3, BINOP_1, PARTFUN1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS,
STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, FINSEQ_1, PZFMISC1, UNIALG_1,
MSUALG_1, ALG_1, MSUALG_3, MSUHOM_1, AUTALG_1, GROUP_6;
constructors BINOP_1, CARD_3, PZFMISC1, VECTSP_1, GROUP_6, ALG_1, MSUALG_3,
MSUHOM_1, AUTALG_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, PBOOLE, STRUCT_0, VECTSP_1,
MSUALG_1, ALGSTR_0, RELSET_1;
requirements SUBSET, BOOLE;
definitions FUNCT_1, TARSKI, VECTSP_1, GROUP_1, FUNCT_2;
equalities FUNCOP_1, STRUCT_0, ALGSTR_0;
expansions TARSKI, GROUP_1, FUNCT_2;
theorems AUTALG_1, ALG_1, BINOP_1, FUNCOP_1, FUNCT_1, FUNCT_2, GROUP_6,
MSUALG_1, MSUALG_3, MSUHOM_1, TARSKI, ZFMISC_1, RELAT_1, VECTSP_1,
RELSET_1, XBOOLE_0, GROUP_1, PBOOLE;
schemes BINOP_1, FUNCT_1, XBOOLE_0;
begin
reserve UA for Universal_Algebra;
definition
let UA;
func UAEnd UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
means
:Def1:
for h be Function of UA, UA holds h in it iff h is_homomorphism;
existence
proof
set F = {x where x is Element of Funcs (the carrier of UA, the carrier of
UA): x is_homomorphism};
A1: id the carrier of UA in F
proof
set I = id the carrier of UA;
I in Funcs (the carrier of UA, the carrier of UA) & I
is_homomorphism by ALG_1:5,FUNCT_2:8;
hence thesis;
end;
F is functional
proof
let q be object;
assume q in F;
then
ex x be Element of Funcs(the carrier of UA, the carrier of UA ) st q
= x & x is_homomorphism;
hence thesis;
end;
then reconsider F as functional non empty set by A1;
F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
proof
let a be Element of F;
a in F;
then
ex x be Element of Funcs(the carrier of UA, the carrier of UA ) st a
= x & x is_homomorphism;
hence thesis;
end;
then reconsider
F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA;
take F;
let h be Function of UA, UA;
thus h in F implies h is_homomorphism
proof
assume h in F;
then ex f be Element of Funcs (the carrier of UA, the carrier of UA) st
f = h & f is_homomorphism;
hence thesis;
end;
A2: h is Element of Funcs (the carrier of UA, the carrier of UA) by FUNCT_2:8;
assume h is_homomorphism;
hence thesis by A2;
end;
uniqueness
proof
let F1,F2 be FUNCTION_DOMAIN of the carrier of UA,the carrier of UA;
assume that
A3: for h be Function of UA, UA holds h in F1 iff h is_homomorphism and
A4: for h be Function of UA, UA holds h in F2 iff h is_homomorphism;
A5: for f be Element of F2 holds f is Function of UA, UA;
A6: F2 c= F1
proof
let q be object;
assume
A7: q in F2;
then reconsider h1 = q as Function of UA, UA by A5;
h1 is_homomorphism by A4,A7;
hence thesis by A3;
end;
A8: for f be Element of F1 holds f is Function of UA, UA;
F1 c= F2
proof
let q be object;
assume
A9: q in F1;
then reconsider h1 = q as Function of UA, UA by A8;
h1 is_homomorphism by A3,A9;
hence thesis by A4;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
end;
theorem
UAEnd UA c= Funcs (the carrier of UA, the carrier of UA)
proof
let q be object;
assume q in UAEnd UA;
then q is Element of UAEnd UA;
hence thesis by FUNCT_2:9;
end;
theorem Th2:
id the carrier of UA in UAEnd UA
proof
id the carrier of UA is_homomorphism by ALG_1:5;
hence thesis by Def1;
end;
theorem Th3:
for f1, f2 be Element of UAEnd UA holds f1 * f2 in UAEnd UA
proof
let f1, f2 be Element of UAEnd UA;
f1 is_homomorphism & f2 is_homomorphism by Def1;
then f1 * f2 is_homomorphism by ALG_1:6;
hence thesis by Def1;
end;
definition
let UA;
func UAEndComp UA -> BinOp of UAEnd UA means
:Def2:
for x, y be Element of UAEnd UA holds it.(x, y) = y * x;
existence
proof
defpred P[Element of UAEnd UA, Element of UAEnd UA, set] means $3 = $2 *
$1;
A1: for x, y be Element of UAEnd UA ex m be Element of UAEnd UA st P[x,y,m ]
proof
let x, y be Element of UAEnd UA;
reconsider xx = x, yy = y as Function of UA, UA;
reconsider m = yy * xx as Element of UAEnd UA by Th3;
take m;
thus thesis;
end;
ex B being BinOp of UAEnd UA st for x, y be Element of UAEnd UA holds
P[x,y,B.(x, y)] from BINOP_1:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let b1, b2 be BinOp of UAEnd UA such that
A2: for x, y be Element of UAEnd UA holds b1.(x, y) = y * x and
A3: for x, y be Element of UAEnd UA holds b2.(x, y) = y * x;
for x, y be Element of UAEnd UA holds b1.(x, y) = b2.(x, y)
proof
let x, y be Element of UAEnd UA;
thus b1.(x, y) = y * x by A2
.= b2.(x, y) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let UA;
func UAEndMonoid UA -> strict multLoopStr means
:Def3:
the carrier of it = UAEnd UA &
the multF of it = UAEndComp UA & 1.it = id the carrier of UA;
existence
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
take multLoopStr(#UAEnd UA, UAEndComp UA, i#);
thus thesis;
end;
uniqueness;
end;
registration
let UA;
cluster UAEndMonoid UA -> non empty;
coherence
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
set M = multLoopStr(#UAEnd UA, UAEndComp UA, i#);
1.M = i;
hence thesis by Def3;
end;
end;
Lm1: now
let UA;
let x, e be Element of UAEndMonoid UA;
reconsider i = e, y = x as Element of UAEnd UA by Def3;
assume
A1: e = id the carrier of UA;
thus x*e = (UAEndComp UA).(y,i) by Def3
.= i*y by Def2
.= x by A1,FUNCT_2:17;
thus e*x = (UAEndComp UA).(i,y) by Def3
.= y*i by Def2
.= x by A1,FUNCT_2:17;
end;
registration
let UA;
cluster UAEndMonoid UA -> well-unital associative;
coherence
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
set H = multLoopStr (# UAEnd UA, UAEndComp UA, i#);
thus UAEndMonoid UA is well-unital
proof
let x be Element of UAEndMonoid UA;
1.UAEndMonoid UA = i by Def3;
hence thesis by Lm1;
end;
for f, g, h be Element of H holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of H;
reconsider A = f, B = g, C = h as Element of UAEnd UA;
A1: g * h = C * B by Def2;
f * g = B * A by Def2;
hence (f * g) * h = C * (B * A) by Def2
.= (C * B) * A by RELAT_1:36
.= f * (g * h) by A1,Def2;
end;
then 1.H = i & H is associative;
hence thesis by Def3;
end;
end;
theorem Th4:
for x, y be Element of UAEndMonoid UA for f, g be Element of
UAEnd UA st x = f & y = g holds x * y = g * f
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
let x, y be Element of UAEndMonoid UA;
let f, g be Element of UAEnd UA;
set H = multLoopStr (# UAEnd UA, UAEndComp UA,i #);
1.H = i;
then
A1: UAEndMonoid UA = H by Def3;
assume x = f & y = g;
hence thesis by A1,Def2;
end;
theorem
id the carrier of UA = 1_UAEndMonoid UA by Def3;
reserve S for non void non empty ManySortedSign,
U1 for non-empty MSAlgebra over S;
definition
let S, U1;
set T = the Sorts of U1;
func MSAEnd U1 -> MSFunctionSet of U1,U1 means
:Def4:
(for f be Element of it holds f is ManySortedFunction of U1, U1) & for h
be ManySortedFunction of U1, U1 holds h in it iff h is_homomorphism U1, U1;
existence
proof
defpred P[object]
means ex msf be ManySortedFunction of U1, U1 st $1 = msf &
msf is_homomorphism U1, U1;
consider X be set such that
A1: for x be object holds x in X iff x in MSFuncs(T,T) & P[x]
from XBOOLE_0:sch 1;
id T in MSFuncs(T,T) & ex F being ManySortedFunction of U1,
U1 st id T = F & F is_homomorphism U1, U1 by AUTALG_1:20,MSUALG_3:9;
then reconsider X as non empty set by A1;
X c= MSFuncs(T,T)
by A1;
then reconsider X as MSFunctionSet of U1,U1;
take X;
thus for f be Element of X holds f is ManySortedFunction of U1, U1;
let h be ManySortedFunction of U1, U1;
hereby
assume h in X;
then ex msf be ManySortedFunction of U1, U1 st h = msf & msf
is_homomorphism U1, U1 by A1;
hence h is_homomorphism U1, U1;
end;
h in MSFuncs(T,T) by AUTALG_1:20;
hence thesis by A1;
end;
uniqueness
proof
let F1, F2 be MSFunctionSet of U1,U1 such that
A2: for f be Element of F1 holds f is ManySortedFunction of U1, U1 and
A3: for h be ManySortedFunction of U1, U1 holds h in F1 iff h
is_homomorphism U1, U1 and
A4: for f be Element of F2 holds f is ManySortedFunction of U1, U1 and
A5: for h be ManySortedFunction of U1, U1 holds h in F2 iff h
is_homomorphism U1, U1;
A6: F2 c= F1
proof
let q be object;
assume
A7: q in F2;
then reconsider h1 = q as ManySortedFunction of U1, U1 by A4;
h1 is_homomorphism U1, U1 by A5,A7;
hence thesis by A3;
end;
F1 c= F2
proof
let q be object;
assume
A8: q in F1;
then reconsider h1 = q as ManySortedFunction of U1, U1 by A2;
h1 is_homomorphism U1, U1 by A3,A8;
hence thesis by A5;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
end;
theorem
MSAEnd U1 c= MSFuncs(the Sorts of U1, the Sorts of U1);
theorem Th7:
id the Sorts of U1 in MSAEnd U1
proof
id the Sorts of U1 is_homomorphism U1, U1 by MSUALG_3:9;
hence thesis by Def4;
end;
theorem Th8:
for f1, f2 be Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
proof
let f1, f2 be Element of MSAEnd U1;
f1 is_homomorphism U1, U1 & f2 is_homomorphism U1, U1 by Def4;
then f1 ** f2 is_homomorphism U1, U1 by MSUALG_3:10;
hence thesis by Def4;
end;
theorem Th9:
for F be ManySortedFunction of MSAlg UA, MSAlg UA for f be
Element of UAEnd UA st F = 0 .--> f holds F in MSAEnd MSAlg UA
proof
let F be ManySortedFunction of MSAlg UA, MSAlg UA;
let f be Element of UAEnd UA;
assume F = 0 .--> f;
then
A1: F = MSAlg f by MSUHOM_1:def 3;
f is_homomorphism by Def1;
then MSAlg f is_homomorphism MSAlg UA, MSAlg UA Over MSSign UA by MSUHOM_1:16
;
then F is_homomorphism MSAlg UA, MSAlg UA by A1,MSUHOM_1:9;
hence thesis by Def4;
end;
definition
let S, U1;
func MSAEndComp U1 -> BinOp of MSAEnd U1 means
:Def5:
for x, y be Element of MSAEnd U1 holds it.(x, y) = y ** x;
existence
proof
defpred P[Element of MSAEnd U1,Element of MSAEnd U1,set] means $3 = $2 **
$1;
A1: for x, y be Element of MSAEnd U1 ex m be Element of MSAEnd U1 st P[x,y ,m]
proof
let x, y be Element of MSAEnd U1;
reconsider xx = x, yy = y as ManySortedFunction of U1, U1;
reconsider m = yy ** xx as Element of MSAEnd U1 by Th8;
take m;
thus thesis;
end;
ex B being BinOp of MSAEnd U1 st for x, y be Element of MSAEnd U1
holds P[x,y,B.(x, y)] from BINOP_1:sch 3 (A1);
hence thesis;
end;
uniqueness
proof
let b1, b2 be BinOp of MSAEnd U1 such that
A2: for x, y be Element of MSAEnd U1 holds b1.(x, y) = y ** x and
A3: for x, y be Element of MSAEnd U1 holds b2.(x, y) = y ** x;
for x, y be Element of MSAEnd U1 holds b1.(x, y) = b2.(x, y)
proof
let x, y be Element of MSAEnd U1;
thus b1.(x, y) = y ** x by A2
.= b2.(x, y) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let S, U1;
func MSAEndMonoid U1 -> strict multLoopStr means
:Def6:
the carrier of it =
MSAEnd U1 & the multF of it = MSAEndComp U1 & 1.it = id the Sorts of U1;
existence
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
take H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
thus the carrier of H = MSAEnd U1;
thus the multF of H = MSAEndComp U1;
thus thesis;
end;
uniqueness;
end;
registration
let S, U1;
cluster MSAEndMonoid U1 -> non empty;
coherence
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
set H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
1.H = i;
hence thesis by Def6;
end;
end;
Lm2: now
let S,U1;
set F = MSAEndMonoid U1;
let x, e be Element of F;
reconsider i = e, y = x as Element of MSAEnd U1 by Def6;
assume
A1: e = id the Sorts of U1;
thus x*e = (MSAEndComp U1).(y,i) by Def6
.= i**y by Def5
.= x by A1,MSUALG_3:4;
thus e*x = (MSAEndComp U1).(i,y) by Def6
.= y**i by Def5
.= x by A1,MSUALG_3:3;
end;
registration
let S,U1;
cluster MSAEndMonoid U1 -> well-unital associative;
coherence
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
set H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
thus MSAEndMonoid U1 is well-unital
proof
let x be Element of MSAEndMonoid U1;
1.MSAEndMonoid U1 = i by Def6;
hence thesis by Lm2;
end;
for f, g, h be Element of H holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of H;
reconsider A = f, B = g, C = h as Element of MSAEnd U1;
A1: g * h = C ** B by Def5;
f * g = B ** A by Def5;
hence (f * g) * h = C ** (B ** A) by Def5
.= (C ** B) ** A by PBOOLE:140
.= f * (g * h) by A1,Def5;
end;
then 1.H = i & H is associative;
hence thesis by Def6;
end;
end;
theorem Th10:
for x, y be Element of MSAEndMonoid U1 for f, g be Element of
MSAEnd U1 st x = f & y = g holds x * y = g ** f
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
let x, y be Element of MSAEndMonoid U1;
let f, g be Element of MSAEnd U1;
set H = multLoopStr(# MSAEnd U1, MSAEndComp U1, i #);
1.H = i;
then
A1: MSAEndMonoid U1 = H by Def6;
assume x = f & y = g;
hence thesis by A1,Def5;
end;
theorem
id the Sorts of U1 = 1_MSAEndMonoid U1 by Def6;
theorem Th12:
for f be Element of UAEnd UA holds 0 .--> f is
ManySortedFunction of MSAlg UA, MSAlg UA
proof
let f be Element of UAEnd UA;
MSAlg f is ManySortedFunction of MSAlg UA, MSAlg UA by MSUHOM_1:9;
hence thesis by MSUHOM_1:def 3;
end;
Lm3: for h be Function st (dom h = UAEnd UA &
for x be object st x in UAEnd UA
holds h.x = 0 .--> x) holds rng h = MSAEnd (MSAlg UA)
proof
let h be Function such that
A1: dom h = UAEnd UA and
A2: for x be object st x in UAEnd UA holds h.x = 0 .--> x;
A3: MSAEnd (MSAlg UA) c= rng h
proof
let x be object;
assume
A4: x in MSAEnd (MSAlg UA);
then reconsider f = x as ManySortedFunction of MSAlg UA, MSAlg UA by Def4;
the carrier of MSSign UA = {0} by MSUALG_1:def 8;
then
A5: f = 0 .--> f.0 by AUTALG_1:11;
A6: f is_homomorphism MSAlg UA, MSAlg UA by A4,Def4;
ex q be set st q in dom h & x = h.q
proof
take q = f.0;
f is ManySortedFunction of MSAlg UA, (MSAlg UA Over MSSign UA) by
MSUHOM_1:9;
then reconsider q9 = q as Function of UA, UA by AUTALG_1:31;
MSAlg q9 = f by A5,MSUHOM_1:def 3;
then
MSAlg q9 is_homomorphism MSAlg UA, (MSAlg UA Over MSSign UA) by A6,
MSUHOM_1:9;
then q9 is_homomorphism by MSUHOM_1:21;
hence q in dom h by A1,Def1;
hence thesis by A1,A2,A5;
end;
hence thesis by FUNCT_1:def 3;
end;
rng h c= MSAEnd (MSAlg UA)
proof
let x be object;
assume x in rng h;
then consider q be object such that
A7: q in dom h and
A8: x = h.q by FUNCT_1:def 3;
consider q9 be Element of UAEnd UA such that
A9: q9 = q by A1,A7;
x = 0 .--> q & 0 .--> q is ManySortedFunction of MSAlg UA, MSAlg UA by A1
,A2,A7,A8,Th12;
then consider d be ManySortedFunction of MSAlg UA, MSAlg UA such that
A10: d = x;
q9 is_homomorphism by Def1;
then
A11: MSAlg q9 is_homomorphism MSAlg UA, MSAlg UA Over MSSign UA by MSUHOM_1:16;
MSAlg q9 = 0 .--> q by A9,MSUHOM_1:def 3
.= x by A1,A2,A7,A8;
then d is_homomorphism MSAlg UA, MSAlg UA by A10,A11,MSUHOM_1:9;
hence thesis by A10,Def4;
end;
hence rng h = MSAEnd (MSAlg UA) by A3,XBOOLE_0:def 10;
end;
registration
cluster left_unital for non empty multLoopStr;
existence
proof
set m = the BinOp of {0},u = the Element of {0};
take multLoopStr(#{0},m,u#);
let x be Element of multLoopStr(#{0},m,u#);
thus (1.multLoopStr(#{0},m,u#))*x = 0 by TARSKI:def 1
.= x by TARSKI:def 1;
end;
end;
registration
let G,H be well-unital non empty multLoopStr;
cluster multiplicative unity-preserving for Function of G,H;
existence
proof
reconsider m = (the carrier of G) --> 1.H as Function of the carrier of G,
the carrier of H;
reconsider m as Function of G,H;
take m;
for x,y being Element of G holds m.(x*y) = (m.x)*(m.y)
proof
let x,y be Element of G;
m.(x*y) = 1.H by FUNCOP_1:7
.= 1.H * 1.H
.= (m.x)* 1.H by FUNCOP_1:7
.= (m.x)*(m.y) by FUNCOP_1:7;
hence thesis;
end;
hence m is multiplicative by GROUP_6:def 6;
thus m.1_G = 1_H by FUNCOP_1:7;
end;
end;
definition
let G,H be well-unital non empty multLoopStr;
mode Homomorphism of G,H is multiplicative unity-preserving Function of G,H;
end;
theorem Th13:
for G be well-unital non empty multLoopStr holds id the
carrier of G is Homomorphism of G,G
proof
let G be well-unital non empty multLoopStr;
reconsider f = id the carrier of G as Function of G,G;
A1: for a,b be Element of G holds f.(a * b) = f.a * f.b;
f.1_G = 1_G;
hence thesis by A1,GROUP_1:def 13,GROUP_6:def 6;
end;
definition
let G,H be well-unital non empty multLoopStr;
pred G,H are_isomorphic means
ex h be Homomorphism of G,H st h is bijective;
reflexivity
proof
let G be well-unital non empty multLoopStr;
reconsider i = id the carrier of G as Homomorphism of G,G by Th13;
A1: the carrier of G c= rng i
proof
let y be object;
assume
A2: y in the carrier of G;
ex x being set st x in dom i & y = i.x
proof
take y;
thus thesis by A2,FUNCT_1:17;
end;
hence thesis by FUNCT_1:def 3;
end;
rng i c= the carrier of G by RELAT_1:def 19;
then rng i = the carrier of G by A1,XBOOLE_0:def 10;
then i is onto;
hence thesis;
end;
end;
theorem Th14:
for h be Function st (dom h = UAEnd UA & for x be object st x in
UAEnd UA holds h.x = 0 .--> x) holds h is Homomorphism of UAEndMonoid UA,
MSAEndMonoid (MSAlg UA)
proof
reconsider i = id the Sorts of MSAlg UA as Element of MSAEnd MSAlg UA by Th7;
set G = UAEndMonoid UA;
set H = MSAEndMonoid (MSAlg UA), M = multLoopStr (# MSAEnd MSAlg UA,
MSAEndComp MSAlg UA,i #);
reconsider e = id the carrier of UA as Element of UAEnd UA by Th2;
let h be Function such that
A1: dom h = UAEnd UA and
A2: for x be object st x in UAEnd UA holds h.x = 0 .--> x;
A3: the carrier of G = dom h by A1,Def3;
1.M = i;
then
A4: H = M by Def6;
then rng h c= the carrier of H by A1,A2,Lm3;
then reconsider h9 = h as Function of G,H by A3,FUNCT_2:def 1,RELSET_1:4;
A5: h9.(e) = 0 .--> (e) by A2;
A6: for a,b being Element of G holds h9.(a * b) = h9.a * h9.b
proof
let a, b be Element of UAEndMonoid UA;
reconsider a9 = a, b9 = b as Element of UAEnd UA by Def3;
reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of MSAlg UA,
MSAlg UA by Th12;
reconsider ha = h9.a, hb = h9.b as Element of MSAEnd MSAlg UA by Def6;
A7: h9.(b9 * a9) = 0 .--> (b9 * a9) by A2,Th3;
reconsider A9 = A, B9 = B as Element of MSAEndMonoid MSAlg UA by A4,Th9;
A8: ha = A9 & hb = B9 by A2;
thus h9.(a * b) = h9.(b9 * a9) by Th4
.= MSAlg (b9 * a9) by A7,MSUHOM_1:def 3
.= (MSAlg b9) ** (MSAlg a9) by MSUHOM_1:26
.= B ** MSAlg a9 by MSUHOM_1:def 3
.= B ** A by MSUHOM_1:def 3
.= h9.a * h9.b by A8,Th10;
end;
h9.1.G = h9.e by Def3
.= MSAlg (e) by A5,MSUHOM_1:def 3
.= i by MSUHOM_1:25
.= 1_H by Def6;
then h9.1_G = 1_H;
hence thesis by A6,GROUP_1:def 13,GROUP_6:def 6;
end;
theorem Th15:
for h be Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA)
st for x be object st x in UAEnd UA
holds h.x = 0 .--> x holds h is bijective
proof
reconsider e = id the Sorts of MSAlg UA as Element of MSAEnd MSAlg UA by Th7;
set N = multLoopStr (# MSAEnd MSAlg UA, MSAEndComp MSAlg UA,e#);
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
let h be Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA);
set G = UAEndMonoid UA;
set H = MSAEndMonoid MSAlg UA, M = multLoopStr (# UAEnd UA, UAEndComp UA,i#);
1.M = i;
then
A1: G = M by Def3;
assume
A2: for x be object st x in UAEnd UA holds h.x = 0 .--> x;
for a, b be Element of G st h.a = h.b holds a = b
proof
let a, b be Element of G;
assume
A3: h.a = h.b;
A4: h.b = 0 .--> b by A2,A1
.= [:{0}, {b}:];
h.a = 0 .--> a by A2,A1
.= [:{0}, {a}:];
then {a} = {b} by A3,A4,ZFMISC_1:110;
hence thesis by ZFMISC_1:3;
end;
then
A5: h is one-to-one by GROUP_6:1;
1.N = e;
then
A6: H = N by Def6;
dom h = UAEnd UA by A1,FUNCT_2:def 1;
then rng h = the carrier of MSAEndMonoid (MSAlg UA) by A2,A6,Lm3;
then h is onto;
hence h is bijective by A5;
end;
theorem
UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic
proof
set G = UAEndMonoid UA;
set H = MSAEndMonoid (MSAlg UA);
ex h be Homomorphism of G,H st h is bijective
proof
deffunc F(object) = 0 .--> $1;
consider h be Function such that
A1: dom h = UAEnd UA & for x be object st x in UAEnd UA holds h.x = F(x)
from FUNCT_1:sch 3;
reconsider h as Homomorphism of G, H by A1,Th14;
h is bijective by A1,Th15;
hence thesis;
end;
hence thesis;
end;