Copyright (c) 1994 Association of Mizar Users
environ
vocabulary UNIALG_1, FUNCT_1, GROUP_6, ALG_1, RELAT_1, FRAENKEL, FUNCT_2,
BINOP_1, REALSET1, VECTSP_1, GROUP_1, PBOOLE, NATTRA_1, BOOLE, FUNCOP_1,
PRALG_1, MSUALG_3, ZF_REFLE, AMI_1, MSUALG_1, CARD_3, MSUHOM_1, CQC_SIM1,
WELLORD1, AUTALG_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, STRUCT_0, FINSEQ_1, BINOP_1, FRAENKEL, PBOOLE, VECTSP_1,
GROUP_1, GROUP_6, CARD_3, UNIALG_1, UNIALG_2, ALG_1, PRALG_1, MSUALG_1,
MSUALG_3, MSUHOM_1;
constructors BINOP_1, FRAENKEL, GROUP_6, ALG_1, MSUALG_3, MSUHOM_1, MEMBERED,
XBOOLE_0;
clusters FRAENKEL, FUNCT_1, GROUP_1, MSUALG_1, PBOOLE, PRALG_1, RELSET_1,
STRUCT_0, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0,
NUMBERS, ORDINAL2;
requirements BOOLE, SUBSET;
definitions ALG_1, FRAENKEL, VECTSP_1, GROUP_1, GROUP_6, MSUALG_3, TARSKI,
XBOOLE_0;
theorems ALG_1, BINOP_1, CARD_3, FUNCOP_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_6,
MSUALG_1, MSUALG_3, MSUHOM_1, PBOOLE, TARSKI, ZFMISC_1, RELAT_1,
VECTSP_1, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes BINOP_1, FUNCT_1, MSUALG_1, XBOOLE_0;
begin
:: On the Group of Automorphisms of Universal Algebra
reserve UA for Universal_Algebra,
f, g for Function of UA, UA;
theorem Th1:
id the carrier of UA is_isomorphism UA, UA
proof
set I = id the carrier of UA;
thus I is_monomorphism UA, UA
proof
thus I is_homomorphism UA, UA by ALG_1:6;
thus I is one-to-one;
end;
thus I is_epimorphism UA, UA
proof
thus I is_homomorphism UA, UA by ALG_1:6;
thus rng I = the carrier of UA by RELAT_1:71;
end;
end;
definition let UA;
func UAAut UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
means
:Def1: (for f be Element of it holds f is Function of UA, UA) &
for h be Function of UA, UA holds h in it iff h is_isomorphism UA, UA;
existence
proof
set F = {x where x is Element of Funcs (the carrier of UA,
the carrier of UA): x is_isomorphism 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_isomorphism UA, UA by Th1;
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_isomorphism 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_isomorphism UA, UA;
thus thesis by A4;
end;
then reconsider F as FUNCTION_DOMAIN of the carrier of UA, the carrier of
UA;
take F;
thus for f be Element of F holds f is Function of UA, UA;
let h be Function of UA, UA;
thus h in F implies h is_isomorphism 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_isomorphism UA, UA;
hence h is_isomorphism UA, UA;
end;
assume A5: h is_isomorphism 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
such that
A6: ( for f be Element of F1 holds f is Function of UA, UA ) &
for h be Function of UA, UA holds h in F1 iff h is_isomorphism UA, UA and
A7: ( for f be Element of F2 holds f is Function of UA, UA ) &
for h be Function of UA, UA holds h in F2 iff h is_isomorphism UA, UA;
A8: F1 c= F2
proof
let q be set;
assume A9: q in F1;
then reconsider h1 = q as Function of UA, UA by A6;
h1 is_isomorphism UA, UA by A6,A9;
hence q in F2 by A7;
end;
F2 c= F1
proof
let q be set;
assume A10: q in F2;
then reconsider h1 = q as Function of UA, UA by A7;
h1 is_isomorphism UA, UA by A7,A10;
hence q in F1 by A6;
end;
hence F1 = F2 by A8,XBOOLE_0:def 10;
end;
end;
theorem
UAAut UA c= Funcs (the carrier of UA, the carrier of UA)
proof
let q be set;
assume q in UAAut UA;
then consider f be Element of UAAut UA such that
A1: f = q;
thus thesis by A1,FUNCT_2:12;
end;
canceled;
theorem Th4:
id the carrier of UA in UAAut UA
proof
id the carrier of UA is_isomorphism UA, UA by Th1;
hence thesis by Def1;
end;
theorem
for f, g st f is Element of UAAut UA & g = f" holds g is_isomorphism UA, UA
proof
let f, g;
assume A1: f is Element of UAAut UA & g = f";
then f is_isomorphism UA, UA by Def1;
hence thesis by A1,ALG_1:11;
end;
Lm1:
for f st f is_isomorphism UA, UA holds f" is Function of UA, UA
proof
let f;
assume A1: f is_isomorphism UA, UA;
then A2: (f is one-to-one) by ALG_1:8;
(f is_epimorphism UA, UA) by A1,ALG_1:def 4;
then rng f = the carrier of UA by ALG_1:def 3;
hence thesis by A2,FUNCT_2:31;
end;
theorem Th6:
for f be Element of UAAut UA holds f" in UAAut UA
proof
let f be Element of UAAut UA;
A1: f is_isomorphism UA, UA by Def1;
then f" is Function of UA, UA by Lm1;
then consider ff be Function of UA, UA such that
A2: ff = f";
ff is_isomorphism UA, UA by A1,A2,ALG_1:11;
hence thesis by A2,Def1;
end;
theorem Th7:
for f1, f2 be Element of UAAut UA holds f1 * f2 in UAAut UA
proof
let f1, f2 be Element of UAAut UA;
(f1 is_isomorphism UA, UA) & (f2 is_isomorphism UA, UA) by Def1;
then f1 * f2 is_isomorphism UA, UA by ALG_1:12;
hence thesis by Def1;
end;
definition
let UA;
func UAAutComp UA -> BinOp of UAAut UA means
:Def2: for x, y be Element of UAAut UA holds it.(x, y) = y * x;
existence
proof
defpred _P[Element of UAAut UA,Element of UAAut UA,Element of UAAut UA]
means $3 = $2 * $1;
A1: for x, y be Element of UAAut UA ex m be Element of UAAut UA st _P[x,y,m]
proof let x, y be Element of UAAut UA;
reconsider xx = x, yy = y as Function of UA, UA;
reconsider m = yy * xx as Element of UAAut UA by Th7;
take m;
thus thesis;
end;
thus ex IT being BinOp of UAAut UA st
for x, y be Element of UAAut UA holds _P[x,y,IT.(x, y)] from BinOpEx(A1);
end;
uniqueness
proof
let b1, b2 be BinOp of UAAut UA such that
A2: for x, y be Element of UAAut UA holds b1.(x, y) = y * x and
A3: for x, y be Element of UAAut UA holds b2.(x, y) = y * x;
for x, y be Element of UAAut UA holds b1.(x, y) = b2.(x, y)
proof
let x, y be Element of UAAut 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 UAAutGroup UA -> Group equals
:Def3: HGrStr (# UAAut UA, UAAutComp UA #);
coherence
proof
set H = HGrStr (# UAAut UA, UAAutComp UA #);
H is associative Group-like
proof
A1: now
let f, g be Element of H,
A, B be Element of UAAut UA;
assume f = A & g = B;
hence f * g = (UAAutComp 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 UAAut UA;
A2: f * g = B * A by A1;
A3: g * h = C * B by A1;
thus (f * g) * h = C * (B * A) by A1,A2
.= (C * B) * A by RELAT_1:55
.= f * (g * h) by A1,A3;
end;
thus
ex e be Element of H st
for h be Element of H holds
h * e = h & e * h = h &
ex g be Element of H st h * g = e & g * h = e
proof
reconsider e = id the carrier of UA as Element of H
by Th4;
take e;
let h be Element of H;
consider A be Element of UAAut UA such that
A4: A = h;
h * e = (id the carrier of UA) * A by A1,A4
.= A by FUNCT_2:74;
hence h * e = h by A4;
e * h = A * (id the carrier of UA) by A1,A4
.= A by FUNCT_2:74;
hence e * h = h by A4;
reconsider g = A" as Element of H by Th6;
take g;
A5: A is_isomorphism UA, UA by Def1;
then A6: (A is one-to-one) by ALG_1:8;
(A is_epimorphism UA, UA) by A5,ALG_1:def 4;
then A7: rng A = the carrier of UA by ALG_1:def 3;
thus h * g = A" * A by A1,A4
.= e by A6,A7,FUNCT_2:35;
thus g * h = A * A" by A1,A4
.= e by A6,A7,FUNCT_2:35;
end;
end;
hence thesis;
end;
end;
definition let UA;
cluster UAAutGroup UA -> strict;
coherence
proof
UAAutGroup UA = HGrStr (# UAAut UA, UAAutComp UA #) by Def3;
hence thesis;
end;
end;
Lm2:
for f be Element of UAAut UA holds dom f = rng f &
dom f = the carrier of UA
proof
let f be Element of UAAut UA;
f is_isomorphism UA, UA by Def1;
then (dom f = the carrier of UA) & (rng f = the carrier of UA) by ALG_1:9;
hence thesis;
end;
theorem Th8:
for x, y be Element of UAAutGroup UA
for f, g be Element of UAAut UA st x = f & y = g holds x * y = g * f
proof
let x, y be Element of UAAutGroup UA;
let f, g be Element of UAAut UA;
assume A1: x = f & y = g;
UAAutGroup UA = HGrStr (# UAAut UA, UAAutComp UA #) by Def3;
hence x * y = (UAAutComp UA).(f, g) by A1,VECTSP_1:def 10
.= g * f by Def2;
end;
theorem Th9:
id the carrier of UA = 1.UAAutGroup UA
proof
A1: UAAutGroup UA = HGrStr (# UAAut UA, UAAutComp UA #) by Def3;
then reconsider g = id the carrier of UA
as Element of UAAutGroup UA by Th4;
consider g1 be Function of the carrier of UA, the carrier of UA such that
A2: g1 = g;
consider f be Element of UAAutGroup UA;
f is Element of UAAut UA by A1;
then consider f1 be Function of the carrier of UA, the carrier of UA such
that
A3: f1 = f;
g * f = f1 * g1 by A1,A2,A3,Th8
.= f by A2,A3,FUNCT_2:74;
hence thesis by GROUP_1:15;
end;
theorem
for f be Element of UAAut UA
for g be Element of UAAutGroup UA st f = g holds f" = g"
proof
let f be Element of UAAut UA;
let g be Element of UAAutGroup UA;
assume A1: f = g;
UAAutGroup UA = HGrStr (# UAAut UA, UAAutComp UA #) by Def3;
then consider g1 be Element of UAAut UA such that
A2: g1 = g";
A3: rng f = dom f by Lm2
.= the carrier of UA by Lm2;
f is_isomorphism UA, UA by Def1;
then f is_monomorphism UA, UA by ALG_1:def 4;
then A4: f is one-to-one by ALG_1:def 2;
g1 * f = g * g" by A1,A2,Th8;
then g1 * f = 1.UAAutGroup UA by GROUP_1:def 5;
then g1 * f = id the carrier of UA by Th9;
hence thesis by A2,A3,A4,FUNCT_2:36;
end;
begin
:: Some properties of Many Sorted Functions
reserve I for set,
A, B, C for ManySortedSet of I;
definition let I, A, B;
pred A is_transformable_to B means
:Def4: for i be set st i in I holds B.i = {} implies A.i = {};
reflexivity;
end;
theorem
A is_transformable_to B & B is_transformable_to C
implies A is_transformable_to C
proof
assume A1: A is_transformable_to B & B is_transformable_to C;
thus thesis
proof
let i be set;
assume i in I;
then (B.i = {} implies A.i = {}) & (C.i = {} implies B.i = {}) by A1,Def4
;
hence C.i = {} implies A.i = {};
end;
end;
theorem Th12:
for x be set, A be ManySortedSet of {x} holds A = {x} --> A.x
proof
let x be set;
let A be ManySortedSet of {x};
A1: dom A = {x} by PBOOLE:def 3;
then rng A = {A.x} by FUNCT_1:14;
hence thesis by A1,FUNCOP_1:15;
end;
theorem Th13:
for F, G, H be Function-yielding Function
holds (H ** G) ** F = H ** (G ** F)
proof
let F, G, H be Function-yielding Function;
set f = (H ** G) ** F,
g = H ** (G ** F);
now
A1: dom f = (dom (H ** G)) /\ dom F by MSUALG_3:def 4
.= (dom H) /\ (dom G) /\ (dom F) by MSUALG_3:def 4;
then A2: dom f = (dom H) /\ ((dom G) /\ dom F) by XBOOLE_1:16;
hence
A3: dom f
= (dom H) /\ (dom (G ** F)) by MSUALG_3:def 4
.= dom g by MSUALG_3:def 4;
let x be set; assume
A4: x in dom f;
then x in (dom H) /\ (dom G) by A1,XBOOLE_0:def 3;
then A5: x in dom (H ** G) by MSUALG_3:def 4;
x in (dom G) /\ (dom F) by A2,A4,XBOOLE_0:def 3;
then A6: x in dom (G ** F) by MSUALG_3:def 4;
thus f.x
= ((H**G).x) * (F.x) by A4,MSUALG_3:def 4
.= (H.x)*(G.x)*(F.x) by A5,MSUALG_3:def 4
.= (H.x)*((G.x)*(F.x)) by RELAT_1:55
.= (H.x)*((G**F).x) by A6,MSUALG_3:def 4
.= g.x by A3,A4,MSUALG_3:def 4;
end;
hence thesis by FUNCT_1:9;
end;
theorem Th14:
for A, B be non-empty ManySortedSet of I
for F be ManySortedFunction of A, B st F is "1-1" "onto"
holds F"" is "1-1" "onto"
proof
let A, B be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B;
assume A1: F is "1-1" "onto";
now
let i be set;
assume A2: i in I;
then reconsider g = F.i as Function of A.i, B.i by MSUALG_1:def 2;
g is one-to-one by A1,A2,MSUALG_3:1;
then g" is one-to-one by FUNCT_1:62;
hence (F"".i) is one-to-one by A1,A2,MSUALG_3:def 5;
end;
hence F"" is "1-1" by MSUALG_3:1;
thus F"" is "onto"
proof
let i be set;
assume A3: i in I;
then A4: A.i <> {} & B.i <> {} by PBOOLE:def 16;
reconsider g = F.i as Function of A.i, B.i by A3,MSUALG_1:def 2;
A5: g is one-to-one by A1,A3,MSUALG_3:1;
A.i = dom g by A4,FUNCT_2:def 1
.= rng (g") by A5,FUNCT_1:55;
hence rng (F"".i) = A.i by A1,A3,MSUALG_3:def 5;
end;
end;
theorem
for A, B be non-empty ManySortedSet of I
for F be ManySortedFunction of A, B st F is "1-1" "onto"
holds (F"")"" = F
proof
let A, B be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B;
assume A1: F is "1-1" "onto";
now
let i be set;
assume A2: i in I;
then reconsider f' = (F"").i as Function of B.i, A.i by MSUALG_1:def 2;
reconsider f = F.i as Function of A.i, B.i by A2,MSUALG_1:def 2;
F"" is "1-1" "onto" by A1,Th14;
then A3: (F"")"".i = f'" by A2,MSUALG_3:def 5;
f is one-to-one by A1,A2,MSUALG_3:1;
then (f")" = f by FUNCT_1:65;
hence (F"")"".i = F.i by A1,A2,A3,MSUALG_3:def 5;
end;
hence thesis by PBOOLE:3;
end;
theorem Th16:
for F, G being Function-yielding Function st F is "1-1" & G is "1-1"
holds G ** F is "1-1"
proof
let F, G be Function-yielding Function such that
A1: F is "1-1" & G is "1-1";
let i be set,
f be Function such that
A2: i in dom (G**F) and
A3: (G**F).i = f;
dom (G**F) = (dom G) /\ (dom F) by MSUALG_3:def 4;
then i in dom G & i in dom F by A2,XBOOLE_0:def 3;
then G.i is one-to-one & F.i is one-to-one by A1,MSUALG_3:def 2;
then (G.i)*(F.i) is one-to-one by FUNCT_1:46;
hence f is one-to-one by A2,A3,MSUALG_3:def 4;
end;
theorem Th17:
for B, C be non-empty ManySortedSet of I
for F be ManySortedFunction of A, B
for G be ManySortedFunction of B, C st
F is "onto" & G is "onto"
holds G ** F is "onto"
proof
let B, C be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B;
let G be ManySortedFunction of B, C;
assume that A1: F is "onto" and
A2: G is "onto";
now
let i be set;
assume A3: i in I;
then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
reconsider g = G.i as Function of B.i, C.i by A3,MSUALG_1:def 2;
A4: B.i <> {} by A3,PBOOLE:def 16;
A5: C.i <> {} by A3,PBOOLE:def 16;
rng f = B.i & rng g = C.i by A1,A2,A3,MSUALG_3:def 3;
then rng (g * f) = C.i by A4,A5,FUNCT_2:20;
hence rng ((G ** F).i) = C.i by A3,MSUALG_3:2;
end;
hence thesis by MSUALG_3:def 3;
end;
theorem
for A, B, C be non-empty ManySortedSet of I
for F be ManySortedFunction of A, B
for G be ManySortedFunction of B, C st
F is "1-1" "onto" & G is "1-1" "onto"
holds (G ** F)"" = (F"") ** (G"")
proof
let A, B, C be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B;
let G be ManySortedFunction of B, C;
assume that A1: F is "1-1" "onto" and
A2: G is "1-1" "onto";
now
let i be set;
assume A3: i in I;
then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
reconsider g = G.i as Function of B.i, C.i by A3,MSUALG_1:def 2;
A4: (F"").i = f" by A1,A3,MSUALG_3:def 5;
A5: (G"").i = g" by A2,A3,MSUALG_3:def 5;
A6: (G ** F) is "1-1" "onto" by A1,A2,Th16,Th17;
A7: f is one-to-one by A1,A3,MSUALG_3:1;
A8: g is one-to-one by A2,A3,MSUALG_3:1;
(G ** F).i = g * f by A3,MSUALG_3:2;
then A9: ((G ** F)"").i = (g * f)" by A3,A6,MSUALG_3:def 5;
rng f = B.i by A1,A3,MSUALG_3:def 3;
then reconsider ff = (F"").i as Function of B.i, A.i
by A4,A7,FUNCT_2:31;
rng g = C.i by A2,A3,MSUALG_3:def 3;
then reconsider gg = (G"").i as Function of C.i, B.i
by A5,A8,FUNCT_2:31;
((F"") ** (G"")).i = ff * gg by A3,MSUALG_3:2
.= ff * (g") by A2,A3,MSUALG_3:def 5
.= f" * g" by A1,A3,MSUALG_3:def 5;
hence ((G ** F)"").i = ((F"") ** (G"")).i by A7,A8,A9,FUNCT_1:66;
end;
hence thesis by PBOOLE:3;
end;
theorem Th19:
for A, B be non-empty ManySortedSet of I
for F be ManySortedFunction of A, B
for G be ManySortedFunction of B, A st
F is "1-1" & F is "onto" & G ** F = id A
holds G = F""
proof
let A, B be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B;
let G be ManySortedFunction of B, A;
assume A1: F is "1-1" & F is "onto" & G ** F = id A;
now
let i be set;
assume A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
reconsider g = G.i as Function of B.i, A.i by A2,MSUALG_1:def 2;
A3: (F"").i = f" by A1,A2,MSUALG_3:def 5;
now
thus A.i <> {} by A2,PBOOLE:def 16;
thus B.i <> {} by A2,PBOOLE:def 16;
thus rng f = B.i by A1,A2,MSUALG_3:def 3;
(G ** F).i = id (A.i) by A1,A2,MSUALG_3:def 1;
hence g*f = id (A.i) by A2,MSUALG_3:2;
thus f is one-to-one by A1,A2,MSUALG_3:1;
end;
hence G.i = (F"").i by A3,FUNCT_2:36;
end;
hence thesis by PBOOLE:3;
end;
begin
:: On the Group of Automorphisms of Many Sorted Algebra
reserve S for non void non empty ManySortedSign,
U1, U2 for non-empty MSAlgebra over S;
definition let I, A, B;
deffunc _F(set) = Funcs(A.$1, B.$1);
func MSFuncs (A, B) -> ManySortedSet of I means
:Def5: for i be set st i in I holds it.i = Funcs(A.i, B.i);
existence proof
thus ex M being ManySortedSet of I st
for i be set st i in I holds M.i = _F(i) from MSSLambda;
end;
uniqueness
proof
let F1, F2 be ManySortedSet of I such that
A1: for i be set st i in I holds F1.i = Funcs(A.i, B.i) and
A2: for i be set st i in I holds F2.i = Funcs(A.i, B.i);
now
let i be set;
assume A3: i in I;
hence F1.i = Funcs(A.i, B.i) by A1
.= F2.i by A2,A3;
end;
hence thesis by PBOOLE:3;
end;
end;
canceled;
theorem Th21:
for A, B be ManySortedSet of I st A is_transformable_to B
for x be set st x in product MSFuncs(A, B)
holds x is ManySortedFunction of A, B
proof
let A, B be ManySortedSet of I;
assume A1: A is_transformable_to B;
let x be set;
assume A2: x in product MSFuncs(A, B);
set f = MSFuncs(A, B);
consider g be Function such that
A3: x = g & dom g = dom f &
for i be set st i in dom f holds g.i in f.i by A2,CARD_3:def 5;
A4: dom f = I & dom g = I by A3,PBOOLE:def 3;
A5: for i be set st i in I holds g.i in Funcs(A.i, B.i)
proof
let i be set;
assume A6: i in I;
then MSFuncs(A, B).i = Funcs(A.i, B.i) by Def5;
hence thesis by A3,A4,A6;
end;
A7: for i be set st i in I holds ex F be Function st F = g.i & dom F = A.i &
rng F c= B.i
proof
let i be set;
assume i in I;
then g.i in Funcs(A.i, B.i) by A5;
hence thesis by FUNCT_2:def 2;
end;
A8: for i be set st i in I holds g.i is Function of A.i, B.i
proof
let i be set;
assume A9: i in I;
then consider F be Function such that
A10: F = g.i & dom F = A.i & rng F c= B.i by A7;
B.i = {} implies A.i = {} by A1,A9,Def4;
hence thesis by A10,FUNCT_2:def 1,RELSET_1:11;
end;
g is ManySortedSet of I by A4,PBOOLE:def 3;
hence thesis by A3,A8,MSUALG_1:def 2;
end;
theorem Th22:
for A, B be ManySortedSet of I st A is_transformable_to B
for g be ManySortedFunction of A, B holds g in product MSFuncs(A, B)
proof
let A, B be ManySortedSet of I;
assume A1: A is_transformable_to B;
let g be ManySortedFunction of A, B;
set f = MSFuncs(A, B);
A2: dom g = I & dom f = I by PBOOLE:def 3;
now
let x be set;
assume A3: x in dom f;
then reconsider i = x as Element of I by PBOOLE:def 3;
A4: g.i is Function of A.i, B.i by A2,A3,MSUALG_1:def 2;
B.i = {} implies A.i = {} by A1,A2,A3,Def4;
then g.i in Funcs(A.i, B.i) by A4,FUNCT_2:11;
hence g.x in f.x by A2,A3,Def5;
end;
hence thesis by A2,CARD_3:18;
end;
theorem Th23:
for A, B be ManySortedSet of I st A is_transformable_to B
holds MSFuncs(A, B) is non-empty
proof
let A, B be ManySortedSet of I;
assume A1: A is_transformable_to B;
A2: for i be set st i in I holds Funcs(A.i, B.i) <> {}
proof
let i be set;
assume i in I;
then B.i = {} implies A.i = {} by A1,Def4;
hence thesis by FUNCT_2:11;
end;
for i be set st i in I holds MSFuncs(A, B).i <> {}
proof
let i be set;
assume A3: i in I;
then MSFuncs(A, B).i = Funcs(A.i, B.i) by Def5;
hence thesis by A2,A3;
end;
then for i be set st i in I holds MSFuncs(A, B).i is non empty;
hence thesis by PBOOLE:def 16;
end;
definition let I, A, B;
assume A1: A is_transformable_to B;
mode MSFunctionSet of A, B -> non empty set means
:Def6: for x be set st x in it holds x is ManySortedFunction of A, B;
existence
proof
MSFuncs(A, B) is non-empty by A1,Th23;
then not ({} in rng MSFuncs(A, B)) by MSUALG_1:1;
then reconsider X = product MSFuncs(A, B) as non empty set by CARD_3:37;
take X;
let x be set;
assume x in X;
hence thesis by A1,Th21;
end;
end;
definition let I, A;
cluster MSFuncs(A, A) -> non-empty;
coherence
proof
for i be set st i in I holds MSFuncs(A, A).i is non empty
proof
let i be set;
assume A1: i in I;
then (id A).i is Function of A.i, A.i by MSUALG_1:def 2;
then (id A).i in Funcs(A.i, A.i) by FUNCT_2:12;
hence thesis by A1,Def5;
end;
hence MSFuncs(A, A) is non-empty by PBOOLE:def 16;
end;
end;
definition let S, U1, U2;
mode MSFunctionSet of U1, U2 is MSFunctionSet of the Sorts of U1,
the Sorts of U2;
end;
definition let I be set;
let D be ManySortedSet of I;
cluster non empty MSFunctionSet of D, D;
existence
proof
not ({} in rng MSFuncs(D, D)) by MSUALG_1:1;
then reconsider X = product MSFuncs(D, D) as non empty set by CARD_3:37;
X is MSFunctionSet of D, D
proof
thus D is_transformable_to D;
let x be set;
assume x in X;
hence thesis by Th21;
end;
then reconsider X as MSFunctionSet of D, D;
take X;
thus thesis;
end;
end;
definition let I be set;
let D be ManySortedSet of I;
let A be non empty MSFunctionSet of D, D;
redefine mode Element of A -> ManySortedFunction of D, D;
coherence by Def6;
end;
theorem
id A is "onto"
proof
let i be set;
assume i in I;
then (id A).i = id (A.i) by MSUALG_3:def 1;
hence rng ((id A).i) = A.i by RELAT_1:71;
end;
theorem
id A is "1-1"
proof
now
let i be set;
assume i in I;
then (id A).i = id (A.i) by MSUALG_3:def 1;
hence (id A).i is one-to-one;
end;
hence thesis by MSUALG_3:1;
end;
canceled;
theorem
id the Sorts of U1 in product MSFuncs (the Sorts of U1, the Sorts of U1)
by Th22;
definition let S, U1;
func MSAAut U1 -> MSFunctionSet of the Sorts of U1, the Sorts of U1 means
:Def7: (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_isomorphism 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_isomorphism 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 Th22;
now
take F = id T;
thus id T = F;
thus F is_isomorphism U1, U1 by MSUALG_3:16;
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_isomorphism 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_isomorphism U1, U1 by A1;
hence h is_isomorphism U1, U1;
end;
assume A3: h is_isomorphism U1, U1;
h in product MSFuncs(T, T) by Th22;
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_isomorphism 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_isomorphism 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_isomorphism 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_isomorphism U1, U1 by A5,A8;
hence q in F1 by A4;
end;
hence F1 = F2 by A6,XBOOLE_0:def 10;
end;
end;
canceled;
theorem
for f be Element of MSAAut U1 holds
f in product MSFuncs (the Sorts of U1, the Sorts of U1) by Th22;
theorem
MSAAut U1 c= product MSFuncs (the Sorts of U1, the Sorts of U1)
proof
let q be set;
assume q in MSAAut U1;
then consider f be Element of MSAAut U1 such that
A1: f = q;
thus thesis by A1,Th22;
end;
Lm3:
for f be Element of MSAAut U1 holds f is "1-1" & f is "onto"
proof
let f be Element of MSAAut U1;
f is_isomorphism U1, U1 by Def7;
hence thesis by MSUALG_3:13;
end;
theorem Th31:
id the Sorts of U1 in MSAAut U1
proof
id the Sorts of U1 is_isomorphism U1, U1 by MSUALG_3:16;
hence thesis by Def7;
end;
theorem Th32:
for f be Element of MSAAut U1 holds f"" in MSAAut U1
proof
let f be Element of MSAAut U1;
f is_isomorphism U1, U1 by Def7;
then f"" is_isomorphism U1, U1 by MSUALG_3:14;
hence thesis by Def7;
end;
theorem Th33:
for f1, f2 be Element of MSAAut U1 holds f1 ** f2 in MSAAut U1
proof
let f1, f2 be Element of MSAAut U1;
(f1 is_isomorphism U1, U1) & (f2 is_isomorphism U1, U1) by Def7;
then f1 ** f2 is_isomorphism U1, U1 by MSUALG_3:15;
hence thesis by Def7;
end;
theorem Th34:
for F be ManySortedFunction of MSAlg UA, MSAlg UA
for f be Element of UAAut UA st F = {0} --> f
holds F in MSAAut MSAlg UA
proof
let F be ManySortedFunction of MSAlg UA, MSAlg UA;
let f be Element of UAAut UA;
assume F = {0} --> f;
then A1: F = MSAlg f by MSUHOM_1:def 3;
f is_isomorphism UA, UA by Def1;
then MSAlg f is_isomorphism MSAlg UA, MSAlg UA Over MSSign UA
by MSUHOM_1:20;
then F is_isomorphism MSAlg UA, MSAlg UA by A1,MSUHOM_1:9;
hence thesis by Def7;
end;
definition let S, U1;
func MSAAutComp U1 -> BinOp of MSAAut U1 means
:Def8: for x, y be Element of MSAAut U1 holds it.(x, y) = y ** x;
existence
proof
defpred _P[Element of MSAAut U1,Element of MSAAut U1,Element of MSAAut U1]
means $3 = $2 ** $1;
A1: for x, y be Element of MSAAut U1 ex m be Element of MSAAut U1 st _P[x,y,m]
proof
let x, y be Element of MSAAut U1;
reconsider xx = x, yy = y as ManySortedFunction of U1, U1;
reconsider m = yy ** xx as Element of MSAAut U1 by Th33;
take m;
thus thesis;
end;
thus ex IT being BinOp of MSAAut U1 st
for x, y be Element of MSAAut U1 holds _P[x,y,IT.(x, y)] from BinOpEx(A1);
end;
uniqueness
proof
let b1, b2 be BinOp of MSAAut U1 such that
A2: for x, y be Element of MSAAut U1 holds b1.(x, y) = y ** x and
A3: for x, y be Element of MSAAut U1 holds b2.(x, y) = y ** x;
for x, y be Element of MSAAut U1 holds b1.(x, y) = b2.(x, y)
proof
let x, y be Element of MSAAut 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 MSAAutGroup U1 -> Group equals
:Def9: HGrStr (# MSAAut U1, MSAAutComp U1 #);
coherence
proof
set H = HGrStr (# MSAAut U1, MSAAutComp U1 #);
set SO = the Sorts of U1;
H is associative Group-like
proof
A1: now
let f, g be Element of H,
A, B be Element of MSAAut U1;
assume f = A & g = B;
hence f * g = (MSAAutComp U1).(A, B) by VECTSP_1:def 10
.= B ** A by Def8;
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 MSAAut U1;
A2: f * g = B ** A by A1;
A3: g * h = C ** B by A1;
thus (f * g) * h = C ** (B ** A) by A1,A2
.= (C ** B) ** A by Th13
.= f * (g * h) by A1,A3;
end;
thus
ex e be Element of H st
for h be Element of H holds
h * e = h & e * h = h &
ex g be Element of H st h * g = e & g * h = e
proof
reconsider e = id SO as Element of H by Th31;
take e;
let h be Element of H;
consider A be Element of MSAAut U1 such that
A4: A = h;
A5: A is "onto" & A is "1-1" by Lm3;
h * e = (id SO) ** A by A1,A4
.= A by MSUALG_3:4;
hence h * e = h by A4;
e * h = A ** (id SO) by A1,A4
.= A by MSUALG_3:3;
hence e * h = h by A4;
reconsider g = A"" as Element of H by Th32;
take g;
thus h * g = (A"") ** A by A1,A4
.= e by A5,MSUALG_3:5;
thus g * h = A ** (A"") by A1,A4
.= e by A5,MSUALG_3:5;
end;
end;
hence thesis;
end;
end;
definition let S, U1;
cluster MSAAutGroup U1 -> strict;
coherence
proof
MSAAutGroup U1 = HGrStr (# MSAAut U1, MSAAutComp U1 #) by Def9;
hence thesis;
end;
end;
theorem Th35:
for x, y be Element of MSAAutGroup U1
for f, g be Element of MSAAut U1 st x = f & y = g holds x * y = g ** f
proof
let x, y be Element of MSAAutGroup U1;
let f, g be Element of MSAAut U1;
assume A1: x = f & y = g;
MSAAutGroup U1 = HGrStr (# MSAAut U1, MSAAutComp U1 #) by Def9;
hence x * y = (MSAAutComp U1).(f, g) by A1,VECTSP_1:def 10
.= g ** f by Def8;
end;
theorem Th36:
id the Sorts of U1 = 1.MSAAutGroup U1
proof
set T = the Sorts of U1;
A1: MSAAutGroup U1 = HGrStr (# MSAAut U1, MSAAutComp U1 #) by Def9;
then reconsider g = id T as Element of MSAAutGroup U1 by
Th31;
consider g1 be ManySortedFunction of T, T such that
A2: g1 = g;
consider f be Element of MSAAutGroup U1;
f is Element of MSAAut U1 by A1;
then consider f1 be ManySortedFunction of T, T such that
A3: f1 = f;
g * f = f1 ** g1 by A1,A2,A3,Th35
.= f by A2,A3,MSUALG_3:3;
hence thesis by GROUP_1:15;
end;
theorem
for f be Element of MSAAut U1
for g be Element of MSAAutGroup U1 st f = g holds f"" = g"
proof
let f be Element of MSAAut U1;
let g be Element of MSAAutGroup U1;
assume A1: f = g;
MSAAutGroup U1 = HGrStr (# MSAAut U1, MSAAutComp U1 #) by Def9;
then consider g1 be Element of MSAAut U1 such that
A2: g1 = g";
A3: f is "1-1" & f is "onto" by Lm3;
g1 ** f = g * g" by A1,A2,Th35;
then g1 ** f = 1.MSAAutGroup U1 by GROUP_1:def 5;
then g1 ** f = id the Sorts of U1 by Th36;
hence thesis by A2,A3,Th19;
end;
begin
:: On the Relationship of Automorphisms of 1-Sorted and Many Sorted Algebras
theorem Th38:
for UA1, UA2 be Universal_Algebra st UA1, UA2 are_similar
for F be ManySortedFunction of MSAlg UA1, (MSAlg UA2 Over MSSign UA1)
holds F.0 is Function of UA1, UA2
proof
let UA1, UA2 be Universal_Algebra;
assume A1: UA1, UA2 are_similar;
let F be ManySortedFunction of MSAlg UA1, (MSAlg UA2 Over MSSign UA1);
A2: MSSign UA1 = MSSign UA2 by A1,MSUHOM_1:10;
reconsider f = (*-->0)*(signature UA1) as
Function of dom signature(UA1), {0}* by MSUALG_1:7;
A3: the carrier of MSSign UA1 = {0} &
the OperSymbols of MSSign UA1 = dom signature UA1 &
the Arity of MSSign UA1 = f &
the ResultSort of MSSign UA1 = dom signature UA1-->0 by MSUALG_1:def 13;
A4: 0 in {0} by TARSKI:def 1;
A5: (MSSorts UA1).0 = ({0} --> the carrier of UA1).0 by MSUALG_1:def 14
.= the carrier of UA1 by A4,FUNCOP_1:13;
A6: MSAlg UA1 = MSAlgebra (#MSSorts UA1, MSCharact UA1#) by MSUALG_1:def 16;
A7: (MSSorts UA2).0 = ({0} --> the carrier of UA2).0 by MSUALG_1:def 14
.= the carrier of UA2 by A4,FUNCOP_1:13;
A8: MSAlg UA2 = MSAlgebra (#MSSorts UA2, MSCharact UA2#) by MSUALG_1:def 16;
MSAlg UA2 Over MSSign UA1 = MSAlg UA2 by A2,MSUHOM_1:9;
hence thesis by A3,A4,A5,A6,A7,A8,MSUALG_1:def 2;
end;
theorem Th39:
for f be Element of UAAut UA
holds {0} --> f is ManySortedFunction of MSAlg UA, MSAlg UA
proof
let f be Element of UAAut UA;
MSAlg f is ManySortedFunction of MSAlg UA, MSAlg UA by MSUHOM_1:9;
hence thesis by MSUHOM_1:def 3;
end;
Lm4:
for h be Function st (dom h = UAAut UA &
for x be set st x in UAAut UA holds h.x = {0} --> x)
holds rng h = MSAAut (MSAlg UA)
proof
let h be Function such that
A1: dom h = UAAut UA & for x be set st x in UAAut UA holds h.x = {0} --> x;
thus rng h = MSAAut (MSAlg UA)
proof
thus rng h c= MSAAut (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,Th39;
then consider d be ManySortedFunction of MSAlg UA, MSAlg UA such that
A4: d = x by A3;
consider q' be Element of UAAut UA such that
A5: q' = q by A1,A2;
q' is_isomorphism UA, UA by Def1;
then A6: MSAlg q' is_isomorphism MSAlg UA, MSAlg UA Over MSSign UA
by MSUHOM_1:20;
MSAlg q' = {0} --> q by A5,MSUHOM_1:def 3
.= x by A1,A2;
then d is_isomorphism MSAlg UA, MSAlg UA by A4,A6,MSUHOM_1:9;
hence thesis by A4,Def7;
end;
thus MSAAut (MSAlg UA) c= rng h
proof
let x be set;
assume A7: x in MSAAut (MSAlg UA);
then reconsider f = x as ManySortedFunction of MSAlg UA, MSAlg UA by Def7
;
A8: f is_isomorphism MSAlg UA, MSAlg UA by A7,Def7;
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 Th12;
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 Th38;
MSAlg q' = f by A9,MSUHOM_1:def 3;
then MSAlg q' is_isomorphism MSAlg UA, (MSAlg UA Over MSSign UA)
by A8,MSUHOM_1:9;
then q' is_isomorphism UA, UA by MSUHOM_1:24;
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;
theorem Th40:
for h be Function st (dom h = UAAut UA &
for x be set st x in UAAut UA holds h.x = {0} --> x)
holds h is Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA)
proof
let h be Function such that
A1: dom h = UAAut UA & for x be set st x in UAAut UA holds h.x = {0} --> x;
set G = UAAutGroup UA;
set H = MSAAutGroup (MSAlg UA);
A2: G = HGrStr (# UAAut UA, UAAutComp UA #) by Def3;
A3: H = HGrStr (# MSAAut MSAlg UA, MSAAutComp MSAlg UA #) by Def9;
then rng h c= the carrier of H by A1,Lm4;
then reconsider h' = h as Function of the carrier of G, the carrier of H
by A1,A2,FUNCT_2:def 1,RELSET_1:11;
h' is Homomorphism of G, H
proof
let a, b be Element of UAAutGroup UA;
thus h'.(a * b) = (h'.a) * (h'.b)
proof
reconsider a' = a, b' = b as Element of UAAut UA by A2;
reconsider A = {0} --> a', B = {0} --> b' as
ManySortedFunction of MSAlg UA, MSAlg UA by Th39;
reconsider A' = A, B' = B
as Element of MSAAutGroup MSAlg UA
by A3,Th34;
reconsider ha = h'.a, hb = h'.b as Element of MSAAut MSAlg UA by A3;
A4: ha = A' & hb = B' by A1;
b' * a' is Element of UAAut UA by Th7;
then A5: h'.(b' * a') = {0} --> (b' * a') by A1;
thus h'.(a * b) = h'.(b' * a') by Th8
.= MSAlg (b' * a') by A5,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 A4,Th35;
end;
end;
hence thesis;
end;
theorem Th41:
for h be Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA) st
for x be set st x in UAAut UA holds h.x = {0} --> x
holds h is_isomorphism
proof
let h be Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA);
assume
A1: for x be set st x in UAAut UA holds h.x = {0} --> x;
set G = UAAutGroup UA;
A2: G = HGrStr (# UAAut UA, UAAutComp UA #) by Def3;
A3: MSAAutGroup MSAlg UA = HGrStr (# MSAAut MSAlg UA, MSAAutComp MSAlg UA #)
by Def9;
thus h is_isomorphism
proof
thus h is_epimorphism
proof
dom h = UAAut UA by A2,FUNCT_2:def 1;
hence rng h = the carrier of MSAAutGroup (MSAlg UA) by A1,A3,Lm4;
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
UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
proof
deffunc _F(set) = {0} --> $1;
consider h be Function such that
A1: dom h = UAAut UA
& for x be set st x in UAAut UA holds h.x = _F(x) from Lambda;
reconsider h as Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA)
by A1,Th40;
take h;
thus thesis by A1,Th41;
end;