:: On the Group of Automorphisms of Universal Algebra & Many
:: Sorted Algebra
:: by Artur Korni{\l}owicz
::
:: Received December 13, 1994
:: Copyright (c) 1994-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_1, RELAT_1, STRUCT_0, MSUALG_3, FUNCT_2,
SUBSET_1, XBOOLE_0, TARSKI, BINOP_1, GROUP_1, ALGSTR_0, PBOOLE, PZFMISC1,
FUNCOP_1, MEMBER_1, MSUALG_1, CARD_3, CARD_1, MSUHOM_1, CQC_SIM1,
GROUP_6, ZFMISC_1, WELLORD1, AUTALG_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE,
PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCOP_1, STRUCT_0, ALGSTR_0,
FINSEQ_1, BINOP_1, GROUP_1, GROUP_6, CARD_3, PZFMISC1, UNIALG_1,
UNIALG_2, ALG_1, MSUALG_1, MSUALG_3, MSUHOM_1;
constructors BINOP_1, CARD_3, PZFMISC1, GROUP_6, ALG_1, MSUALG_3, MSUHOM_1,
RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, PBOOLE,
STRUCT_0, MSUALG_1, SUBSET_1;
requirements BOOLE, SUBSET;
definitions FUNCT_1, ALG_1, GROUP_6, MSUALG_3, TARSKI, XBOOLE_0, PZFMISC1,
FUNCT_2;
equalities FUNCOP_1, ALGSTR_0;
expansions ALG_1, MSUALG_3, TARSKI, XBOOLE_0, PZFMISC1, FUNCT_2;
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,
RELSET_1, XBOOLE_0, PARTFUN1;
schemes BINOP_1, FUNCT_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
proof
set I = id the carrier of UA;
I is_homomorphism by ALG_1:5;
hence I is_monomorphism;
I is_homomorphism & rng I = the carrier of UA by ALG_1:5,RELAT_1:45;
hence I is_epimorphism;
end;
definition
let UA;
func UAAut 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_isomorphism;
existence
proof
set F = {x where x is Element of Funcs (the carrier of UA, the carrier of
UA): x is_isomorphism};
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_isomorphism
by Th1,FUNCT_2:8;
hence thesis;
end;
reconsider F as set;
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_isomorphism;
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_isomorphism;
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_isomorphism
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;
hence thesis;
end;
A2: h is Element of Funcs (the carrier of UA, the carrier of UA) by FUNCT_2:8;
assume h is_isomorphism;
hence thesis by A2;
end;
uniqueness
proof
let F1, F2 be FUNCTION_DOMAIN of the carrier of UA, the carrier of UA such
that
A3: for h be Function of UA, UA holds h in F1 iff h is_isomorphism and
A4: for h be Function of UA, UA holds h in F2 iff h is_isomorphism;
A5: F2 c= F1
proof
let q be object;
assume
A6: q in F2;
then reconsider h1 = q as Function of UA, UA by FUNCT_2:def 12;
h1 is_isomorphism by A4,A6;
hence thesis by A3;
end;
F1 c= F2
proof
let q be object;
assume
A7: q in F1;
then reconsider h1 = q as Function of UA, UA by FUNCT_2:def 12;
h1 is_isomorphism by A3,A7;
hence thesis by A4;
end;
hence thesis by A5;
end;
end;
theorem
UAAut UA c= Funcs (the carrier of UA, the carrier of UA)
proof
let q be object;
assume q in UAAut UA;
then ex f be Element of UAAut UA st f = q;
hence thesis by FUNCT_2:9;
end;
theorem Th3:
id the carrier of UA in UAAut UA
proof
id the carrier of UA is_isomorphism by Th1;
hence thesis by Def1;
end;
theorem
for f, g st f is Element of UAAut UA & g = f" holds g is_isomorphism
proof
let f, g;
assume that
A1: f is Element of UAAut UA and
A2: g = f";
f is_isomorphism by A1,Def1;
hence thesis by A2,ALG_1:10;
end;
Lm1: for f st f is_isomorphism holds f" is Function of UA, UA
proof
let f;
assume
A1: f is_isomorphism;
then f is_epimorphism;
then
A2: rng f = the carrier of UA;
f is one-to-one by A1,ALG_1:7;
hence thesis by A2,FUNCT_2:25;
end;
theorem Th5:
for f be Element of UAAut UA holds f" in UAAut UA
proof
let f be Element of UAAut UA;
A1: f is_isomorphism 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 by A1,A2,ALG_1:10;
hence thesis by A2,Def1;
end;
theorem Th6:
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 & f2 is_isomorphism by Def1;
then f1 * f2 is_isomorphism by ALG_1:11;
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,set] 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 Th6;
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 BINOP_1:sch 3 (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
multMagma (# UAAut UA, UAAutComp UA #);
coherence
proof
set H = multMagma (# UAAut UA, UAAutComp UA #);
A1: 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 Th3;
take e;
let h be Element of H;
consider A be Element of UAAut UA such that
A2: A = h;
h * e = (id the carrier of UA) * A by A2,Def2
.= A by FUNCT_2:17;
hence h * e = h by A2;
e * h = A * (id the carrier of UA) by A2,Def2
.= A by FUNCT_2:17;
hence e * h = h by A2;
reconsider g = A" as Element of H by Th5;
take g;
A3: A is_isomorphism by Def1;
then
A4: A is one-to-one by ALG_1:7;
A is_epimorphism by A3;
then
A5: rng A = the carrier of UA;
thus h * g = A" * A by A2,Def2
.= e by A4,A5,FUNCT_2:29;
thus g * h = A * A" by A2,Def2
.= e by A4,A5,FUNCT_2:29;
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 UAAut UA;
A6: 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 A6,Def2;
end;
hence thesis by A1,GROUP_1:def 2,def 3;
end;
end;
registration
let UA;
cluster UAAutGroup UA -> strict;
coherence;
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;
A1: f is_isomorphism by Def1;
then dom f = the carrier of UA by ALG_1:8;
hence thesis by A1,ALG_1:8;
end;
theorem
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 by Def2;
theorem Th8:
id the carrier of UA = 1_UAAutGroup UA
proof
set f = the Element of UAAutGroup UA;
reconsider g = id the carrier of UA as Element of UAAutGroup UA by Th3;
consider g1 be Function of the carrier of UA, the carrier of UA such that
A1: g1 = g;
f is Element of UAAut UA;
then consider
f1 be Function of the carrier of UA, the carrier of UA such that
A2: f1 = f;
g * f = f1 * g1 by A1,A2,Def2
.= f by A1,A2,FUNCT_2:17;
hence thesis by GROUP_1:7;
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;
consider g1 be Element of UAAut UA such that
A1: g1 = g";
assume f = g;
then g1 * f = g * g" by A1,Def2;
then g1 * f = 1_UAAutGroup UA by GROUP_1:def 5;
then
A2: g1 * f = id the carrier of UA by Th8;
f is_isomorphism by Def1;
then f is_monomorphism;
then
A3: f is one-to-one;
rng f = dom f by Lm2
.= the carrier of UA by Lm2;
hence thesis by A1,A3,A2,FUNCT_2:30;
end;
begin
:: Some properties of Many Sorted Functions
reserve I for set,
A, B, C for ManySortedSet of I;
theorem
A is_transformable_to B & B is_transformable_to C implies A
is_transformable_to C
proof
assume that
A1: A is_transformable_to B and
A2: B is_transformable_to C;
let i be set;
assume
A3: i in I;
then B.i = {} implies A.i = {} by A1;
hence thesis by A2,A3;
end;
theorem Th11:
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 PARTFUN1:def 2;
then rng A = {A.x} by FUNCT_1:4;
hence thesis by A1,FUNCOP_1:9;
end;
theorem Th12:
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 PBOOLE:def 15;
g is one-to-one by A1,A2,MSUALG_3:1;
then g" is one-to-one;
hence (F"".i) is one-to-one by A1,A2,MSUALG_3:def 4;
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 reconsider g = F.i as Function of A.i, B.i by PBOOLE:def 15;
A4: g is one-to-one by A1,A3,MSUALG_3:1;
A.i = dom g by A3,FUNCT_2:def 1
.= rng (g") by A4,FUNCT_1:33;
hence thesis by A1,A3,MSUALG_3:def 4;
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 object;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
reconsider f9 = (F"").i as Function of B.i, A.i by A2,PBOOLE:def 15;
f is one-to-one by A1,A2,MSUALG_3:1;
then
A3: (f")" = f by FUNCT_1:43;
F"" is "1-1" "onto" by A1,Th12;
then (F"")"".i = f9" by A2,MSUALG_3:def 4;
hence (F"")"".i = F.i by A1,A2,A3,MSUALG_3:def 4;
end;
hence thesis by PBOOLE:3;
end;
theorem Th14:
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" and
A2: G is "1-1";
let i be set, f be Function such that
A3: i in dom (G**F) and
A4: (G**F).i = f;
A5: dom (G**F) = (dom G) /\ (dom F) by PBOOLE:def 19;
then i in dom F by A3,XBOOLE_0:def 4;
then
A6: F.i is one-to-one by A1;
i in dom G by A3,A5,XBOOLE_0:def 4;
then G.i is one-to-one by A2;
then (G.i)*(F.i) is one-to-one by A6;
hence thesis by A3,A4,PBOOLE:def 19;
end;
theorem Th15:
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
A1: F is "onto" & G is "onto";
now
let i be set;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
reconsider g = G.i as Function of B.i, C.i by A2,PBOOLE:def 15;
rng f = B.i & rng g = C.i by A1,A2;
then rng (g * f) = C.i by A2,FUNCT_2:14;
hence rng ((G ** F).i) = C.i by A2,MSUALG_3:2;
end;
hence thesis;
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 object;
assume
A3: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
A4: f is one-to-one by A1,A3,MSUALG_3:1;
reconsider g = G.i as Function of B.i, C.i by A3,PBOOLE:def 15;
A5: g is one-to-one by A2,A3,MSUALG_3:1;
(F"").i = f" & rng f = B.i by A1,A3,MSUALG_3:def 4;
then reconsider ff = (F"").i as Function of B.i, A.i by A4,FUNCT_2:25;
A6: (G ** F) is "1-1" "onto" by A1,A2,Th14,Th15;
(G ** F).i = g * f by A3,MSUALG_3:2;
then
A7: ((G ** F)"").i = (g * f)" by A3,A6,MSUALG_3:def 4;
(G"").i = g" & rng g = C.i by A2,A3,MSUALG_3:def 4;
then reconsider gg = (G"").i as Function of C.i, B.i by A5,FUNCT_2:25;
((F"") ** (G"")).i = ff * gg by A3,MSUALG_3:2
.= ff * (g") by A2,A3,MSUALG_3:def 4
.= f" * g" by A1,A3,MSUALG_3:def 4;
hence ((G ** F)"").i = ((F"") ** (G"")).i by A4,A5,A7,FUNCT_1:44;
end;
hence thesis by PBOOLE:3;
end;
theorem Th17:
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 that
A1: F is "1-1" and
A2: F is "onto" and
A3: G ** F = id A;
now
let i be object;
assume
A4: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
A5: f is one-to-one by A1,A4,MSUALG_3:1;
reconsider g = G.i as Function of B.i, A.i by A4,PBOOLE:def 15;
(G ** F).i = id (A.i) by A3,A4,MSUALG_3:def 1;
then
A6: g*f = id (A.i) by A4,MSUALG_3:2;
(F"").i = f" & rng f = B.i by A1,A2,A4,MSUALG_3:def 4;
hence G.i = (F"").i by A4,A6,A5,FUNCT_2:30;
end;
hence thesis by PBOOLE:3;
end;
theorem Th18:
A is_transformable_to B implies (Funcs)(A,B) is non-empty
proof
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;
hence thesis by FUNCT_2:8;
end;
for i be object st i in I holds (Funcs)(A,B).i <> {}
proof
let i be object;
assume
A3: i in I;
then (Funcs)(A,B).i = Funcs(A.i, B.i) by PBOOLE:def 17;
hence thesis by A2,A3;
end;
then for i be object st i in I holds (Funcs)(A,B).i is non empty;
hence thesis by PBOOLE:def 13;
end;
definition
let I, A, B;
assume
A1: A is_transformable_to B;
func MSFuncs(A,B) -> non empty set equals
:Def4:
product (Funcs)(A,B);
coherence
proof
(Funcs)(A,B) is non-empty by A1,Th18;
then not {} in rng (Funcs)(A,B) by PBOOLE:137;
hence thesis by CARD_3:26;
end;
end;
theorem Th19:
A is_transformable_to B implies
for x be set st x in MSFuncs(A,B) holds
x is ManySortedFunction of A,B
proof
assume
A1: A is_transformable_to B;
set f = (Funcs)(A,B);
let x be set;
assume x in MSFuncs(A,B);
then x in product f by A1,Def4;
then consider g be Function such that
A2: x = g and
A3: dom g = dom f and
A4: for i be object st i in dom f holds g.i in f.i by CARD_3:def 5;
A5: dom f = I by PARTFUN1:def 2;
A6: for i be set st i in I holds g.i in Funcs(A.i, B.i)
proof
let i be set;
assume
A7: i in I;
then (Funcs)(A,B).i = Funcs(A.i,B.i) by PBOOLE:def 17;
hence thesis by A4,A5,A7;
end;
A8: 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 A6;
hence thesis by FUNCT_2:def 2;
end;
A9: for i be object st i in I holds g.i is Function of A.i, B.i
proof
let i be object;
assume
A10: i in I;
ex F be Function st F = g.i & dom F = A.i & rng F c= B.i by A8,A10;
hence thesis by FUNCT_2:2;
end;
dom g = I by A3,PARTFUN1:def 2;
then g is ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
hence thesis by A2,A9,PBOOLE:def 15;
end;
theorem Th20:
A is_transformable_to B implies
for g be ManySortedFunction of A, B holds g in MSFuncs(A,B)
proof
assume
A1: A is_transformable_to B;
set f = (Funcs)(A,B);
let g be ManySortedFunction of A, B;
A2: dom f = I by PARTFUN1:def 2;
A3: now
let x be object;
assume
A4: x in dom f;
then reconsider i = x as Element of I by PARTFUN1:def 2;
A5: g.i is Function of A.i, B.i by A2,A4,PBOOLE:def 15;
B.i = {} implies A.i = {} by A1,A2,A4;
then g.i in Funcs(A.i, B.i) by A5,FUNCT_2:8;
hence g.x in f.x by A2,A4,PBOOLE:def 17;
end;
dom g = I by PARTFUN1:def 2;
then g in product f by A2,A3,CARD_3:9;
hence thesis by A1,Def4;
end;
registration
let I, A;
cluster (Funcs)(A,A) -> non-empty;
coherence
proof
for i be object st i in I holds (Funcs)(A,A).i is non empty
proof
let i be object;
assume
A1: i in I;
then (id A).i is Function of A.i, A.i by PBOOLE:def 15;
then (id A).i in Funcs(A.i, A.i) by FUNCT_2:9;
hence thesis by A1,PBOOLE:def 17;
end;
hence thesis by PBOOLE:def 13;
end;
end;
definition
let I be set;
let D be ManySortedSet of I;
let A be non empty Subset of MSFuncs(D,D);
redefine mode Element of A -> ManySortedFunction of D,D; :: redefines Element (SUBSET_1, definition)
coherence
proof
let f be Element of A;
thus thesis by Th19;
end;
end;
registration
let I,A;
cluster id A -> "onto";
coherence
proof
let i be set;
assume i in I;
then (id A).i = id (A.i) by MSUALG_3:def 1;
hence thesis by RELAT_1:45;
end;
cluster id A -> "1-1";
coherence
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;
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 S, U1, U2;
mode MSFunctionSet of U1, U2 is
non empty Subset of MSFuncs(the Sorts of U1, the Sorts of U2);
end;
theorem
id the Sorts of U1 in MSFuncs(the Sorts of U1, the Sorts of U1) by Th20;
definition
let S, U1;
set T = the Sorts of U1;
func MSAAut U1 -> MSFunctionSet of U1,U1 means
:Def5:
for h be ManySortedFunction of U1, U1 holds h in it iff
h is_isomorphism U1, U1;
existence
proof
defpred P[object] 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 object holds x in X iff x in MSFuncs(T,T) & P[x]
from XBOOLE_0:sch 1;
A2: X c= MSFuncs(T,T)
by A1;
id T in MSFuncs(T,T) & ex F be ManySortedFunction of U1, U1
st id T = F & F is_isomorphism U1, U1 by Th20,MSUALG_3:16;
then reconsider X as MSFunctionSet of U1,U1 by A1,A2;
take X;
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_isomorphism U1, U1 by A1;
hence h is_isomorphism U1, U1;
end;
h in MSFuncs(T,T) by Th20;
hence thesis by A1;
end;
uniqueness
proof
let F1, F2 be MSFunctionSet of U1,U1 such that
A3: for h be ManySortedFunction of U1, U1 holds h in F1 iff h
is_isomorphism U1, U1 and
A4: for h be ManySortedFunction of U1, U1 holds h in F2 iff h
is_isomorphism U1, U1;
thus F1 c= F2
proof
let q be object;
assume
A5: q in F1;
then reconsider h1 = q as ManySortedFunction of U1, U1 by Th19;
h1 is_isomorphism U1, U1 by A3,A5;
hence thesis by A4;
end;
let q be object;
assume
A6: q in F2;
then reconsider h1 = q as ManySortedFunction of U1, U1 by Th19;
h1 is_isomorphism U1, U1 by A4,A6;
hence thesis by A3;
end;
end;
theorem
for f be Element of MSAAut U1 holds
f in MSFuncs(the Sorts of U1, the Sorts of U1) by Th20;
theorem
MSAAut U1 c= MSFuncs(the Sorts of U1, the Sorts of U1);
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 Def5;
hence thesis by MSUALG_3:13;
end;
theorem Th24:
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 Def5;
end;
theorem Th25:
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 Def5;
then f"" is_isomorphism U1, U1 by MSUALG_3:14;
hence thesis by Def5;
end;
theorem Th26:
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 Def5;
then f1 ** f2 is_isomorphism U1, U1 by MSUALG_3:15;
hence thesis by Def5;
end;
theorem Th27:
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 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 Def5;
end;
definition
let S, U1;
func MSAAutComp U1 -> BinOp of MSAAut U1 means
:Def6:
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,set] 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 Th26;
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 BINOP_1:sch 3(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
multMagma (# MSAAut U1, MSAAutComp U1 #);
coherence
proof
set SO = the Sorts of U1;
set H = multMagma (# MSAAut U1, MSAAutComp U1 #);
A1: 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 Th24;
take e;
let h be Element of H;
consider A be Element of MSAAut U1 such that
A2: A = h;
h * e = (id SO) ** A by A2,Def6
.= A by MSUALG_3:4;
hence h * e = h by A2;
e * h = A ** (id SO) by A2,Def6
.= A by MSUALG_3:3;
hence e * h = h by A2;
reconsider g = A"" as Element of H by Th25;
take g;
A3: A is "onto" & A is "1-1" by Lm3;
thus h * g = (A"") ** A by A2,Def6
.= e by A3,MSUALG_3:5;
thus g * h = A ** (A"") by A2,Def6
.= e by A3,MSUALG_3:5;
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 MSAAut U1;
A4: g * h = C ** B by Def6;
f * g = B ** A by Def6;
hence (f * g) * h = C ** (B ** A) by Def6
.= (C ** B) ** A by PBOOLE:140
.= f * (g * h) by A4,Def6;
end;
hence thesis by A1,GROUP_1:def 2,def 3;
end;
end;
registration
let S, U1;
cluster MSAAutGroup U1 -> strict;
coherence;
end;
theorem
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 by Def6;
theorem Th29:
id the Sorts of U1 = 1_MSAAutGroup U1
proof
set T = the Sorts of U1;
set f = the Element of MSAAutGroup U1;
reconsider g = id T as Element of MSAAutGroup U1 by Th24;
consider g1 be ManySortedFunction of T, T such that
A1: g1 = g;
f is Element of MSAAut U1;
then consider f1 be ManySortedFunction of T, T such that
A2: f1 = f;
g * f = f1 ** g1 by A1,A2,Def6
.= f by A1,A2,MSUALG_3:3;
hence thesis by GROUP_1:7;
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;
consider g1 be Element of MSAAut U1 such that
A1: g1 = g";
assume f = g;
then g1 ** f = g * g" by A1,Def6;
then g1 ** f = 1_MSAAutGroup U1 by GROUP_1:def 5;
then
A2: g1 ** f = id the Sorts of U1 by Th29;
f is "1-1" & f is "onto" by Lm3;
hence thesis by A1,A2,Th17;
end;
begin
:: On the Relationship of Automorphisms of 1-Sorted and Many Sorted Algebras
theorem Th31:
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;
A1: 0 in {0} by TARSKI:def 1;
assume UA1, UA2 are_similar;
then MSSign UA1 = MSSign UA2 by MSUHOM_1:10;
then
A2: MSAlg UA2 = MSAlgebra (#MSSorts UA2, MSCharact UA2#) & MSAlg UA2 Over
MSSign UA1 = MSAlg UA2 by MSUALG_1:def 11,MSUHOM_1:9;
let F be ManySortedFunction of MSAlg UA1, (MSAlg UA2 Over MSSign UA1);
A3: the carrier of MSSign UA1 = {0} & MSAlg UA1 = MSAlgebra (#MSSorts UA1,
MSCharact UA1#) by MSUALG_1:def 8,def 11;
A4: (MSSorts UA2).0 = (0 .--> the carrier of UA2).0 by MSUALG_1:def 9
.= the carrier of UA2 by A1,FUNCOP_1:7;
(MSSorts UA1).0 = (0 .--> the carrier of UA1).0 by MSUALG_1:def 9
.= the carrier of UA1 by A1,FUNCOP_1:7;
hence thesis by A1,A3,A4,A2,PBOOLE:def 15;
end;
theorem Th32:
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 object 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 and
A2: for x be object st x in UAAut UA holds h.x = 0 .--> x;
thus rng h c= MSAAut (MSAlg UA)
proof
let x be object;
assume x in rng h;
then consider q be object such that
A3: q in dom h and
A4: x = h.q by FUNCT_1:def 3;
consider q9 be Element of UAAut UA such that
A5: q9 = q by A1,A3;
x = 0 .--> q & 0 .--> q is ManySortedFunction of MSAlg UA, MSAlg UA by A1
,A2,A3,A4,Th32;
then consider d be ManySortedFunction of MSAlg UA, MSAlg UA such that
A6: d = x;
q9 is_isomorphism by Def1;
then
A7: MSAlg q9 is_isomorphism MSAlg UA, MSAlg UA Over MSSign UA by MSUHOM_1:20;
MSAlg q9 = 0 .--> q by A5,MSUHOM_1:def 3
.= x by A1,A2,A3,A4;
then d is_isomorphism MSAlg UA, MSAlg UA by A6,A7,MSUHOM_1:9;
hence thesis by A6,Def5;
end;
let x be object;
assume
A8: x in MSAAut (MSAlg UA);
then reconsider f = x as ManySortedFunction of MSAlg UA, MSAlg UA by Th19;
the carrier of MSSign UA = {0} by MSUALG_1:def 8;
then
A9: f = 0 .--> f.0 by Th11;
A10: f is_isomorphism MSAlg UA, MSAlg UA by A8,Def5;
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 Th31;
MSAlg q9 = f by A9,MSUHOM_1:def 3;
then MSAlg q9 is_isomorphism MSAlg UA, (MSAlg UA Over MSSign UA) by A10,
MSUHOM_1:9;
then q9 is_isomorphism by MSUHOM_1:24;
hence q in dom h by A1,Def1;
hence thesis by A1,A2,A9;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th33:
for h be Function st (dom h = UAAut UA & for x be object 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 and
A2: for x be object st x in UAAut UA holds h.x = 0 .--> x;
set H = MSAAutGroup (MSAlg UA);
set G = UAAutGroup UA;
rng h c= the carrier of H by A1,A2,Lm4;
then reconsider h9 = h as Function of G,H by A1,FUNCT_2:def 1,RELSET_1:4;
now
let a, b be Element of UAAutGroup UA;
thus h9.(a * b) = (h9.a) * (h9.b)
proof
reconsider a9 = a, b9 = b as Element of UAAut UA;
A3: h9.(b9 * a9) = 0 .--> (b9 * a9) by A2,Th6;
reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of MSAlg
UA, MSAlg UA by Th32;
reconsider ha = h9.a, hb = h9.b as Element of MSAAut MSAlg UA;
reconsider A9 = A, B9 = B as Element of MSAAutGroup MSAlg UA by Th27;
A4: ha = A9 & hb = B9 by A2;
thus h9.(a * b) = h9.(b9 * a9) by Def2
.= MSAlg (b9 * a9) by A3,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 A4,Def6;
end;
end;
hence thesis by GROUP_6:def 6;
end;
theorem Th34:
for h be Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA)
st for x be object st x in UAAut UA holds h.x = 0 .--> x
holds h is bijective
proof
let h be Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA);
set G = UAAutGroup UA;
assume
A1: for x be object st x in UAAut 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
A2: h.a = h.b;
A3: h.b = 0 .--> b by A1
.= [:{0}, {b}:];
h.a = 0 .--> a by A1
.= [:{0}, {a}:];
then {a} = {b} by A2,A3,ZFMISC_1:110;
hence thesis by ZFMISC_1:3;
end;
then
A4: h is one-to-one by GROUP_6:1;
dom h = UAAut UA by FUNCT_2:def 1;
then rng h = the carrier of MSAAutGroup (MSAlg UA) by A1,Lm4;
then h is onto;
hence h is bijective by A4;
end;
theorem
UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
proof
deffunc F(object) = 0 .--> $1;
consider h be Function such that
A1: dom h = UAAut UA & for x be object st x in UAAut UA holds h.x = F(x)
from FUNCT_1:sch 3;
reconsider h as Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA)
by A1,Th33;
take h;
thus thesis by A1,Th34;
end;