Copyright (c) 1995 Association of Mizar Users
environ
vocabulary UNIALG_1, FUNCT_1, FRAENKEL, ALG_1, FUNCT_2, BINOP_1, VECTSP_1,
VECTSP_2, AMI_1, MSUALG_1, ZF_REFLE, AUTALG_1, PRALG_1, CARD_3, NATTRA_1,
MSUALG_3, FUNCOP_1, MSUHOM_1, RELAT_1, PRE_TOPC, COHSP_1, GROUP_6,
WELLORD1, ENDALG;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, PRE_TOPC, RELAT_1, FUNCT_1,
CARD_3, STRUCT_0, MONOID_0, VECTSP_1, BINOP_1, PARTFUN1, FUNCT_2,
FRAENKEL, FINSEQ_1, UNIALG_1, MSUALG_1, ALG_1, MSUALG_3, MSUHOM_1,
AUTALG_1;
constructors TEX_2, BINOP_1, ALG_1, MSUALG_3, MSUHOM_1, AUTALG_1, MONOID_0,
MEMBERED;
clusters FRAENKEL, MONOID_0, RELSET_1, MSUALG_1, STRUCT_0, SUBSET_1, MEMBERED,
FUNCT_2, PARTFUN1, NUMBERS, ORDINAL2;
requirements SUBSET, BOOLE;
definitions AUTALG_1, FRAENKEL, TARSKI, VECTSP_1, XBOOLE_0;
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,
MONOID_0, RELSET_1, XBOOLE_0;
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 UA, UA;
existence
proof
set F = {x where x is Element of Funcs (the carrier of UA,
the carrier of UA): x is_homomorphism UA, UA};
A1: id the carrier of UA in F
proof
set I = id the carrier of UA;
A2: I in Funcs (the carrier of UA, the carrier of UA) by FUNCT_2:11;
I is_homomorphism UA, UA by ALG_1:6;
hence thesis by A2;
end;
reconsider F as set;
F is functional
proof
let q be set;
assume q in F;
then consider x be Element of Funcs (the carrier of UA, the carrier of UA
)
such that
A3: q = x & x is_homomorphism UA, UA;
thus thesis by A3;
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 consider x be Element of Funcs (the carrier of UA, the carrier of UA
)
such that
A4: a = x & x is_homomorphism UA, UA;
thus thesis by A4;
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 UA, UA
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 UA, UA;
hence h is_homomorphism UA, UA;
end;
assume A5: h is_homomorphism UA, UA;
h is Element of Funcs (the carrier of UA, the carrier of UA)
by FUNCT_2:11;
hence h in F by A5;
end;
uniqueness
proof
let F1,F2 be FUNCTION_DOMAIN of the carrier of UA,the carrier of UA;
A6:(for f be Element of F1 holds f is Function of UA, UA);
A7:(for f be Element of F2 holds f is Function of UA, UA);
assume that
A8:(for h be Function of UA, UA holds
h in F1 iff h is_homomorphism UA, UA) and
A9:(for h be Function of UA, UA holds
h in F2 iff h is_homomorphism UA, UA);
A10: F1 c= F2
proof
let q be set;
assume A11: q in F1;
then reconsider h1 = q as Function of UA, UA by A6;
h1 is_homomorphism UA, UA by A8,A11;
hence q in F2 by A9;
end;
F2 c= F1
proof
let q be set;
assume A12: q in F2;
then reconsider h1 = q as Function of UA, UA by A7;
h1 is_homomorphism UA, UA by A9,A12;
hence q in F1 by A8;
end;
hence F1 = F2 by A10,XBOOLE_0:def 10;
end;
end;
theorem
UAEnd UA c= Funcs (the carrier of UA, the carrier of UA)
proof
let q be set;
assume q in UAEnd UA;
then consider f be Element of UAEnd UA such that
A1: f = q;
thus thesis by A1,FUNCT_2:12;
end;
canceled;
theorem Th3:
id the carrier of UA in UAEnd UA
proof
id the carrier of UA is_homomorphism UA, UA by ALG_1:6;
hence thesis by Def1;
end;
theorem Th4:
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 UA, UA) & (f2 is_homomorphism UA, UA) by Def1;
then f1 * f2 is_homomorphism UA, UA by ALG_1:7;
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, Element of UAEnd UA]
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 Th4;
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 BinOpEx(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 mult of it = UAEndComp UA &
the unity of it = id the carrier of UA;
existence
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
take H = multLoopStr(#UAEnd UA, UAEndComp UA, i#);
thus the carrier of H = UAEnd UA;
thus the mult of H = UAEndComp UA;
thus the unity of H = id the carrier of UA;
end;
uniqueness;
end;
definition let UA;
cluster UAEndMonoid UA -> non empty;
coherence
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
multLoopStr(#UAEnd UA, UAEndComp UA, i#) is non empty;
hence thesis by Def3;
end;
end;
definition let UA;
cluster UAEndMonoid UA -> left_unital well-unital associative;
coherence
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
set H = multLoopStr (# UAEnd UA, UAEndComp UA, i#);
A1:H is left_unital
proof
A2: now
let f, g be Element of H,
A, B be Element of UAEnd UA;
assume f = A & g = B;
hence f * g = (UAEndComp UA).(A, B) by VECTSP_1:def 10
.= B * A by Def2;
end;
H is left_unital
proof
for x being Element of H holds (1_ H)*x = x
proof
let x be Element of H;
consider A be Element of UAEnd UA such that
A3: A = x;
(1_ H)*x = (the unity of H)*x by VECTSP_1:def 9
.= A*(id the carrier of UA) by A2,A3
.= x by A3,FUNCT_2:74;
hence thesis;
end;
hence thesis by VECTSP_1:def 19;
end;
hence thesis;
end;
A4:H is well-unital
proof
A5: now
let f, g be Element of H,
A, B be Element of UAEnd UA;
assume f = A & g = B;
hence f * g = (UAEndComp UA).(A, B) by VECTSP_1:def 10
.= B * A by Def2;
end;
consider e be Element of UAEnd UA such that
A6: e = i;
for a being Element of H holds
(the unity of H)*a = a & a*(the unity of H) = a
proof
let a be Element of H;
A7:(the unity of H)*a = a
proof
consider A be Element of UAEnd UA such that
A8: A = a;
(the unity of H)*a = A*e by A5,A6,A8
.= a by A6,A8,FUNCT_2:74;
hence thesis;
end;
a*(the unity of H) = a
proof
consider A be Element of UAEnd UA such that
A9: A = a;
a*(the unity of H) = e*A by A5,A6,A9
.= a by A6,A9,FUNCT_2:74;
hence thesis;
end;
hence thesis by A7;
end;
hence thesis by MONOID_0:18;
end;
H is associative
proof
A10: now
let f, g be Element of H,
A, B be Element of UAEnd UA;
assume f = A & g = B;
hence f * g = (UAEndComp UA).(A, B) by VECTSP_1:def 10
.= B * A by Def2;
end;
thus 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;
A11: f * g = B * A by A10;
A12: g * h = C * B by A10;
thus (f * g) * h = C * (B * A) by A10,A11
.= (C * B) * A by RELAT_1:55
.= f * (g * h) by A10,A12;
end;
thus thesis;
end;
hence thesis by A1,A4,Def3;
end;
end;
theorem Th5:
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
let x, y be Element of UAEndMonoid UA;
let f, g be Element of UAEnd UA;
assume A1: x = f & y = g;
reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
UAEndMonoid UA = multLoopStr (# UAEnd UA, UAEndComp UA,i #) by Def3;
hence x * y = (UAEndComp UA).(f, g) by A1,VECTSP_1:def 10
.= g * f by Def2;
end;
theorem Th6:
id the carrier of UA = 1_ UAEndMonoid UA
proof
reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
id the carrier of UA =
1_ multLoopStr(#UAEnd UA, UAEndComp UA, i#) by VECTSP_1:def 9;
hence thesis by Def3;
end;
reserve S for non void non empty ManySortedSign,
U1 for non-empty MSAlgebra over S;
definition let S, U1;
func MSAEnd U1 -> MSFunctionSet of the Sorts of U1, the Sorts of 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
set T = the Sorts of U1;
defpred P[set] 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 set holds x in X iff x in product MSFuncs (T, T) &
P[x] from Separation;
A2: id T in product MSFuncs (T, T) by AUTALG_1:22;
now
take F = id T;
thus id T = F;
thus F is_homomorphism U1, U1 by MSUALG_3:9;
end;
then reconsider X as non empty set by A1,A2;
X is MSFunctionSet of T, T
proof
thus T is_transformable_to T;
let q be set;
assume q in X;
then q in product MSFuncs (T, T) &
ex msf be ManySortedFunction of U1, U1 st
q = msf & msf is_homomorphism U1, U1 by A1;
hence q is ManySortedFunction of U1, U1;
end;
then reconsider X as MSFunctionSet of T, T;
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 h in product MSFuncs (T, T) &
ex msf be ManySortedFunction of U1, U1 st
h = msf & msf is_homomorphism U1, U1 by A1;
hence h is_homomorphism U1, U1;
end;
assume A3: h is_homomorphism U1, U1;
h in product MSFuncs(T, T) by AUTALG_1:22;
hence h in X by A1,A3;
end;
uniqueness
proof
set T = the Sorts of U1;
let F1, F2 be MSFunctionSet of T, T such that
A4: ( for f be Element of F1 holds f is ManySortedFunction of U1, U1 ) &
for h be ManySortedFunction of U1, U1 holds
h in F1 iff h is_homomorphism U1, U1 and
A5: ( for f be Element of F2 holds f is ManySortedFunction of U1, U1 ) &
for h be ManySortedFunction of U1, U1 holds
h in F2 iff h is_homomorphism U1, U1;
A6: F1 c= F2
proof
let q be set;
assume A7: q in F1;
then reconsider h1 = q as ManySortedFunction of U1, U1 by A4;
h1 is_homomorphism U1, U1 by A4,A7;
hence q in F2 by A5;
end;
F2 c= F1
proof
let q be set;
assume A8: q in F2;
then reconsider h1 = q as ManySortedFunction of U1, U1 by A5;
h1 is_homomorphism U1, U1 by A5,A8;
hence q in F1 by A4;
end;
hence F1 = F2 by A6,XBOOLE_0:def 10;
end;
end;
canceled 2;
theorem
MSAEnd U1 c= product MSFuncs (the Sorts of U1, the Sorts of U1)
proof
let q be set;
assume q in MSAEnd U1;
then consider f be Element of MSAEnd U1 such that
A1: f = q;
thus thesis by A1,AUTALG_1:22;
end;
theorem Th10:
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 Th11:
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 Th12:
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 UA, UA 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,Element of MSAEnd U1]
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 Th11;
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 BinOpEx(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 mult of it = MSAEndComp U1 &
the unity of it = id the Sorts of U1;
existence
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th10;
take H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
thus the carrier of H = MSAEnd U1;
thus the mult of H = MSAEndComp U1;
thus the unity of H = id the Sorts of U1;
end;
uniqueness;
end;
definition let S, U1;
cluster MSAEndMonoid U1 -> non empty;
coherence
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th10;
multLoopStr(#MSAEnd U1, MSAEndComp U1, i#) is non empty;
hence thesis by Def6;
end;
end;
definition let S,U1;
cluster MSAEndMonoid U1 -> left_unital well-unital associative;
coherence
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th10;
set H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
A1: H is left_unital
proof
A2: now
let f, g be Element of H,
A, B be Element of MSAEnd U1;
assume f = A & g = B;
hence f * g = (MSAEndComp U1).(A, B) by VECTSP_1:def 10
.= B ** A by Def5;
end;
H is left_unital
proof
for x being Element of H holds (1_ H)*x = x
proof
let x be Element of H;
consider A be Element of MSAEnd U1 such that
A3: A = x;
(1_ H)*x = (the unity of H)*x by VECTSP_1:def 9
.= A**(id the Sorts of U1) by A2,A3
.= x by A3,MSUALG_3:3;
hence thesis;
end;
hence thesis by VECTSP_1:def 19;
end;
hence thesis;
end;
A4: H is well-unital
proof
A5: now
let f, g be Element of H,
A, B be Element of MSAEnd U1;
assume f = A & g = B;
hence f * g = (MSAEndComp U1).(A, B) by VECTSP_1:def 10
.= B ** A by Def5;
end;
consider e be Element of MSAEnd U1 such that
A6: e = i;
for a being Element of H holds
(the unity of H)*a = a & a*(the unity of H) = a
proof
let a be Element of H;
A7:(the unity of H)*a = a
proof
consider A be Element of MSAEnd U1 such that
A8: A = a;
(the unity of H)*a = A**e by A5,A6,A8
.= a by A6,A8,MSUALG_3:3;
hence thesis;
end;
a*(the unity of H) = a
proof
consider A be Element of MSAEnd U1 such that
A9: A = a;
a*(the unity of H) = e**A by A5,A6,A9
.= a by A6,A9,MSUALG_3:4;
hence thesis;
end;
hence thesis by A7;
end;
hence thesis by MONOID_0:18;
end;
H is associative
proof
A10: now
let f, g be Element of H,
A, B be Element of MSAEnd U1;
assume f = A & g = B;
hence f * g = (MSAEndComp U1).(A, B) by VECTSP_1:def 10
.= B ** A by Def5;
end;
thus 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;
A11: f * g = B ** A by A10;
A12: g * h = C ** B by A10;
thus (f * g) * h = C ** (B ** A) by A10,A11
.= (C ** B) ** A by AUTALG_1:13
.= f * (g * h) by A10,A12;
end;
thus thesis;
end;
hence thesis by A1,A4,Def6;
end;
end;
theorem Th13:
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
let x, y be Element of MSAEndMonoid U1;
let f, g be Element of MSAEnd U1;
assume A1: x = f & y = g;
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th10;
MSAEndMonoid U1 = multLoopStr
(# MSAEnd U1, MSAEndComp U1, i #) by Def6;
hence x * y = (MSAEndComp U1).(f, g) by A1,VECTSP_1:def 10
.= g ** f by Def5;
end;
theorem Th14:
id the Sorts of U1 = 1_ MSAEndMonoid U1
proof
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th10;
id the Sorts of U1 = 1_ multLoopStr(#MSAEnd U1, MSAEndComp U1, i#)
by VECTSP_1:def 9;
hence thesis by Def6;
end;
canceled;
theorem Th16:
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;
Lm1:
for h be Function st (dom h = UAEnd UA &
for x be set 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 & for x be set st x in UAEnd UA holds h.x = {0} --> x;
thus rng h = MSAEnd (MSAlg UA)
proof
thus rng h c= MSAEnd (MSAlg UA)
proof
let x be set;
assume x in rng h;
then consider q be set such that
A2: q in dom h & x = h.q by FUNCT_1:def 5;
A3: x = {0} --> q by A1,A2;
{0} --> q is ManySortedFunction of MSAlg UA, MSAlg UA
by A1,A2,Th16;
then consider d be ManySortedFunction of MSAlg UA, MSAlg UA such that
A4: d = x by A3;
consider q' be Element of UAEnd UA such that
A5: q' = q by A1,A2;
q' is_homomorphism UA, UA by Def1;
then A6: MSAlg q' is_homomorphism MSAlg UA, MSAlg UA Over MSSign UA
by MSUHOM_1:16;
MSAlg q' = {0} --> q by A5,MSUHOM_1:def 3
.= x by A1,A2;
then d is_homomorphism MSAlg UA, MSAlg UA by A4,A6,MSUHOM_1:9;
hence thesis by A4,Def4;
end;
thus MSAEnd (MSAlg UA) c= rng h
proof
let x be set;
assume A7: x in MSAEnd (MSAlg UA);
then reconsider f = x as ManySortedFunction of MSAlg UA, MSAlg UA by Def4
;
A8: f is_homomorphism MSAlg UA, MSAlg UA by A7,Def4;
reconsider g = (*-->0)*(signature UA) as
Function of dom signature(UA), {0}* by MSUALG_1:7;
the carrier of MSSign UA = {0} &
the OperSymbols of MSSign UA = dom signature UA &
the Arity of MSSign UA = g &
the ResultSort of MSSign UA = dom signature UA -->0 by MSUALG_1:def 13;
then A9: f = {0} --> f.0 by AUTALG_1:12;
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 q' = q as Function of UA, UA by AUTALG_1:38;
MSAlg q' = f by A9,MSUHOM_1:def 3;
then MSAlg q' is_homomorphism MSAlg UA, (MSAlg UA Over MSSign UA)
by A8,MSUHOM_1:9;
then q' is_homomorphism UA, UA by MSUHOM_1:21;
hence
q in dom h by A1,Def1;
hence x = h.q by A1,A9;
end;
hence thesis by FUNCT_1:def 5;
end;
end;
end;
definition
let G,H be non empty HGrStr;
let IT be map of G,H;
attr IT is multiplicative means
:Def7: for x,y being Element of G holds
IT.(x*y) = (IT.x)*(IT.y);
end;
definition let G,H be non empty multLoopStr;
let IT be map of G,H;
attr IT is unity-preserving means
:Def8: IT.1_ G = 1_ H;
end;
definition
cluster left_unital (non empty multLoopStr);
existence
proof
consider m being BinOp of {0}, u be 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;
definition let G,H be left_unital (non empty multLoopStr);
cluster multiplicative unity-preserving map of G,H;
existence
proof
reconsider m = (the carrier of G) --> 1_ H
as Function of the carrier of G,the carrier of H by FUNCOP_1:57;
reconsider m as map of G,H;
take m;
thus m is multiplicative
proof
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:13
.= 1_ H * 1_ H by VECTSP_1:def 19
.= (m.x)* 1_ H by FUNCOP_1:13
.= (m.x)*(m.y) by FUNCOP_1:13;
hence thesis;
end;
hence thesis by Def7;
end;
thus m.1_ G = 1_ H by FUNCOP_1:13;
end;
end;
definition let G,H be left_unital (non empty multLoopStr);
mode Homomorphism of G,H is multiplicative unity-preserving map of G,H;
end;
definition let G,H be left_unital (non empty multLoopStr),h be map of G,H;
pred h is_monomorphism means :Def9:
h is one-to-one;
pred h is_epimorphism means :Def10:
rng h = the carrier of H;
end;
definition let G,H be left_unital (non empty multLoopStr),h be map of G,H;
pred h is_isomorphism means :Def11:
h is_epimorphism & h is_monomorphism;
end;
theorem Th17:
for G be left_unital (non empty multLoopStr) holds
id the carrier of G is Homomorphism of G,G
proof
let G be left_unital (non empty multLoopStr);
reconsider f = id the carrier of G as map of G,G;
A1: f is multiplicative map of G,G
proof
for a,b be Element of G holds f.(a * b) = f.a * f.b
proof
let a,b be Element of G;
f.(a * b) = a * b by FUNCT_1:35
.= f.a * b by FUNCT_1:35
.= f.a * f.b by FUNCT_1:35;
hence thesis;
end;
hence thesis by Def7;
end;
f is unity-preserving map of G,G
proof
f.1_ G = 1_ G by FUNCT_1:35;
hence thesis by Def8;
end;
hence thesis by A1;
end;
definition let G,H be left_unital (non empty multLoopStr);
pred G,H are_isomorphic means
:Def12: ex h be Homomorphism of G,H st h is_isomorphism;
reflexivity
proof
let G be left_unital (non empty multLoopStr);
reconsider i = id the carrier of G as Homomorphism of G,G by Th17;
rng i = the carrier of G
proof
thus rng i c= the carrier of G by RELSET_1:12;
thus the carrier of G c= rng i
proof
let y be set;
assume A1: y in the carrier of G;
ex x being set st x in dom i & y = i.x
proof
take y;
thus thesis by A1,FUNCT_1:34;
end;
hence thesis by FUNCT_1:def 5;
end;
end;
then i is_monomorphism & i is_epimorphism by Def9,Def10;
then i is_isomorphism by Def11;
hence thesis;
end;
end;
theorem Th18:
for h be Function st (dom h = UAEnd UA &
for x be set st x in UAEnd UA holds h.x = {0} --> x)
holds h is Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA)
proof
let h be Function such that
A1: dom h = UAEnd UA & for x be set st x in UAEnd UA holds h.x = {0} --> x;
set G = UAEndMonoid UA;
reconsider e = id the carrier of UA as Element of UAEnd UA by Th3;
set H = MSAEndMonoid (MSAlg UA);
reconsider i = id the Sorts of MSAlg UA
as Element of MSAEnd MSAlg UA by Th10;
A2: H = multLoopStr (# MSAEnd MSAlg UA, MSAEndComp MSAlg UA,i #) by Def6;
A3: the carrier of G = dom h by A1,Def3;
rng h c= the carrier of H by A1,A2,Lm1;
then h is Function of the carrier of G, the carrier of H
by A3,FUNCT_2:def 1,RELSET_1:11;
then reconsider h' = h as map of G,H;
A4: for a,b being Element of G holds
h'.(a * b) = h'.a * h'.b
proof
let a, b be Element of UAEndMonoid UA;
reconsider a' = a, b' = b as Element of UAEnd UA by Def3;
reconsider A = {0} --> a', B = {0} --> b' as
ManySortedFunction of MSAlg UA, MSAlg UA by Th16;
reconsider A' = A, B' = B
as Element of MSAEndMonoid MSAlg UA
by A2,Th12;
reconsider ha = h'.a, hb = h'.b
as Element of MSAEnd MSAlg UA by Def6;
A5: ha = A' & hb = B' by A1;
b' * a' is Element of UAEnd UA by Th4;
then A6: h'.(b' * a') = {0} --> (b' * a') by A1;
thus h'.(a * b) = h'.(b' * a') by Th5
.= MSAlg (b' * a') by A6,MSUHOM_1:def 3
.= (MSAlg b') ** (MSAlg a') by MSUHOM_1:26
.= B ** MSAlg a' by MSUHOM_1:def 3
.= B ** A by MSUHOM_1:def 3
.= h'.a * h'.b by A5,Th13;
end;
h'.1_ G = 1_ H
proof
A7: h'.(e) = {0} --> (e) by A1;
h'.1_ G = h'.e by Th6
.= MSAlg (e) by A7,MSUHOM_1:def 3
.= i by MSUHOM_1:25
.= 1_ H by Th14;
hence thesis;
end;
hence thesis by A4,Def7,Def8;
end;
theorem Th19:
for h be Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA) st
for x be set st x in UAEnd UA holds h.x = {0} --> x holds h is_isomorphism
proof
let h be Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA);
assume
A1: for x be set st x in UAEnd UA holds h.x = {0} --> x;
set G = UAEndMonoid UA;
set H = MSAEndMonoid MSAlg UA;
reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
A2: G = multLoopStr (# UAEnd UA, UAEndComp UA,i#) by Def3;
reconsider e = id the Sorts of MSAlg UA
as Element of MSAEnd MSAlg UA by Th10;
A3: H = multLoopStr (# MSAEnd MSAlg UA, MSAEndComp MSAlg UA,e#) by Def6;
thus h is_isomorphism
proof
thus h is_epimorphism
proof
dom h = UAEnd UA by A2,FUNCT_2:def 1;
hence
rng h = the carrier of MSAEndMonoid (MSAlg UA) by A1,A3,Lm1;
end;
thus h is_monomorphism
proof
thus h is one-to-one
proof
for a, b be Element of G st h.a = h.b holds a = b
proof
let a, b be Element of G;
assume A4: h.a = h.b;
A5: h.a = {0} --> a by A1,A2
.= [:{0}, {a}:] by FUNCOP_1:def 2;
h.b = {0} --> b by A1,A2
.= [:{0}, {b}:] by FUNCOP_1:def 2;
then {a} = {b} by A4,A5,ZFMISC_1:134;
hence thesis by ZFMISC_1:6;
end;
hence thesis by GROUP_6:1;
end;
end;
end;
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_isomorphism
proof
deffunc F(set) = {0} --> $1;
consider h be Function such that
A1: dom h = UAEnd UA
& for x be set st x in UAEnd UA holds h.x = F(x) from Lambda;
reconsider h as Homomorphism of G, H by A1,Th18;
h is_isomorphism by A1,Th19;
hence thesis;
end;
hence thesis by Def12;
end;