:: The Correspondence Between Homomorphisms of Universal Algebra &
:: Many Sorted Algebra
:: by Adam Grabowski
::
:: 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, NAT_1, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, SUBSET_1,
FINSEQ_1, FUNCOP_1, PBOOLE, CARD_3, MSUALG_1, XXREAL_0, STRUCT_0,
FINSEQ_2, PARTFUN1, CQC_SIM1, CARD_1, UNIALG_2, MARGREL1, NUMBERS,
MSUALG_3, MEMBER_1, MSUHOM_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, CARD_3, FUNCOP_1, FINSEQ_1,
STRUCT_0, UNIALG_1, UNIALG_2, FINSEQ_2, ALG_1, MSUALG_3, MSUALG_1,
XXREAL_0;
constructors FINSEQOP, ALG_1, MSUALG_3, XREAL_0, RELSET_1, NAT_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
XREAL_0, PRE_CIRC, STRUCT_0, MSUALG_1, MSUALG_3, RELAT_1, PBOOLE,
FINSEQ_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions ALG_1, MSUALG_3, TARSKI;
equalities FUNCOP_1, FINSEQ_2, UNIALG_2;
expansions ALG_1, MSUALG_3, TARSKI, UNIALG_2;
theorems TARSKI, FINSEQ_2, MSUALG_1, UNIALG_2, MSUALG_3, FUNCOP_1, FINSEQ_1,
FUNCT_1, FUNCT_2, UNIALG_1, PBOOLE, MONOID_1, CARD_3, RELAT_1, XBOOLE_0,
XBOOLE_1, PARTFUN1, FINSEQ_3;
begin
reserve U1,U2,U3 for Universal_Algebra,
m,n for Nat,
a for set,
A for non empty set,
h for Function of U1,U2;
theorem Th1:
for f,g be Function, C be set st rng f c= C holds (g|C)*f = g*f
proof
let f,g be Function, C be set such that
A1: rng f c= C;
(g|C)*f = g*(C|`f) by MONOID_1:1
.= g*f by A1,RELAT_1:94;
hence thesis;
end;
theorem Th2:
for I be set, C be Subset of I holds C* c= I*
proof
let I be set, C be Subset of I;
thus C* c= I*
proof
let a be object;
assume a in C*;
then reconsider p = a as FinSequence of C by FINSEQ_1:def 11;
rng p c= I by XBOOLE_1:1;
then p is FinSequence of I by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
end;
theorem
for f be Function, C be set st f is Function-yielding holds f|C is
Function-yielding;
theorem Th4:
for I be set, C be Subset of I, M be ManySortedSet of I holds (M|
C)# = M#|(C*)
proof
let I be set, C be Subset of I, M be ManySortedSet of I;
dom (M# ) = I* by PARTFUN1:def 2;
then dom (M#|(C*)) = C* by Th2,RELAT_1:62;
then reconsider D = M#|(C*) as ManySortedSet of C* by PARTFUN1:def 2;
A1: C* c= I* by Th2;
for i being Element of C* holds (M#|(C*)).i = product((M|C)*i)
proof
let i be Element of C*;
A2: rng i c= C;
i in C*;
then
A3: i in dom D by PARTFUN1:def 2;
A4: i in I* by A1;
for a being object holds
a in (D.i) iff ex g be Function st a = g & dom g = dom ((M|C)*i) & for
a being object st a in dom ((M|C)*i) holds g.a in ((M|C)*i).a
proof let a be object;
hereby
assume a in (D.i);
then a in M#.i by A3,FUNCT_1:47;
then a in product(M*i) by A4,FINSEQ_2:def 5;
then consider g be Function such that
A5: a = g and
A6: dom g = dom (M*i) and
A7: for x be object st x in dom (M*i) holds g.x in (M*i).x
by CARD_3:def 5;
take g;
thus a = g by A5;
rng i c= C;
hence dom g = dom ((M|C)*i) by A6,Th1;
thus for a being object st a in dom ((M|C)*i) holds g.a in ((M|C)*i).a
proof
A8: rng i c= C;
let a be object;
assume a in dom ((M|C)*i);
then a in dom (M*i) by A8,Th1;
then g.a in (M*i).a by A7;
hence thesis by A8,Th1;
end;
end;
given g be Function such that
A9: a = g and
A10: dom g = dom ((M|C)*i) and
A11: for a being object st a in dom ((M|C)*i) holds g.a in ((M|C)*i).a;
A12: for a being object st a in dom (M*i) holds g.a in (M*i).a
proof
let a be object;
assume a in dom (M*i);
then a in dom ((M|C)*i) by A2,Th1;
then g.a in ((M|C)*i).a by A11;
hence thesis by A2,Th1;
end;
dom g = dom (M*i) by A2,A10,Th1;
then a in product(M*i) by A9,A12,CARD_3:def 5;
then a in M#.i by A4,FINSEQ_2:def 5;
hence thesis by A3,FUNCT_1:47;
end;
hence thesis by CARD_3:def 5;
end;
hence (M|C)# = D by FINSEQ_2:def 5
.= M#|(C*);
end;
definition
let S,S9 be non empty ManySortedSign;
pred S <= S9 means
the carrier of S c= the carrier of S9 & the
carrier' of S c= the carrier' of S9 & (the Arity of S9)|the carrier' of S = the
Arity of S & (the ResultSort of S9)|the carrier' of S = the ResultSort of S;
reflexivity;
end;
theorem
for S,S9,S99 be non empty ManySortedSign st S <= S9 & S9 <= S99 holds
S <= S99
proof
let S,S9,S99 be non empty ManySortedSign;
assume that
A1: S <= S9 and
A2: S9 <= S99;
the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier
of S99 by A1,A2;
hence the carrier of S c= the carrier of S99;
A3: the carrier' of S c= the carrier' of S9 by A1;
the carrier' of S9 c= the carrier' of S99 by A2;
hence the carrier' of S c= the carrier' of S99 by A3;
thus (the Arity of S99)|the carrier' of S = (the Arity of S99)|((the
carrier' of S9)/\(the carrier' of S)) by A3,XBOOLE_1:28
.= the Arity of S by A1,A2,RELAT_1:71;
thus (the ResultSort of S99)|the carrier' of S = (the ResultSort of S99)|((
the carrier' of S9) /\ (the carrier' of S)) by A3,XBOOLE_1:28
.= the ResultSort of S by A1,A2,RELAT_1:71;
end;
theorem
for S,S9 be strict non empty ManySortedSign st S <= S9 & S9 <= S holds S = S9
proof
let S,S9 be strict non empty ManySortedSign;
assume that
A1: S <= S9 and
A2: S9 <= S;
A3: the carrier' of S9 c= the carrier' of S by A2;
A4: dom (the ResultSort of S9) = the carrier' of S9 by FUNCT_2:def 1;
(the ResultSort of S9)|the carrier' of S = the ResultSort of S by A1;
then
A5: the ResultSort of S = the ResultSort of S9 by A3,A4,RELAT_1:68;
A6: dom (the Arity of S9) = the carrier' of S9 by FUNCT_2:def 1;
(the Arity of S9)|the carrier' of S = the Arity of S by A1;
then
A7: the Arity of S = the Arity of S9 by A3,A6,RELAT_1:68;
the carrier' of S c= the carrier' of S9 by A1;
then
A8: the carrier' of S = the carrier' of S9 by A3,XBOOLE_0:def 10;
the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier
of S by A1,A2;
hence thesis by A8,A7,A5,XBOOLE_0:def 10;
end;
theorem
for g be Function, a be Element of A for k be Nat st 1 <= k & k <= n
holds (a .--> g).((n |-> a)/.k) = g
proof
let g be Function;
let a be Element of A;
let k be Nat;
assume 1 <= k & k <= n;
then
A1: k in Seg n by FINSEQ_1:1;
then k in dom (n |-> a);
then (n |-> a)/.k = (n |-> a).k by PARTFUN1:def 6
.= a by A1,FUNCOP_1:7;
hence thesis by FUNCOP_1:72;
end;
theorem Th8:
for I be set,I0 be Subset of I, A,B be ManySortedSet of I, F be
ManySortedFunction of A,B for A0,B0 be ManySortedSet of I0 st A0 = A | I0 & B0
= B | I0 holds F|I0 is ManySortedFunction of A0,B0
proof
let I be set, I0 be Subset of I, A,B be ManySortedSet of I, F be
ManySortedFunction of A,B;
let A0,B0 be ManySortedSet of I0 such that
A1: A0 = A | I0 and
A2: B0 = B | I0;
reconsider G = F|I0 as ManySortedFunction of I0;
A3: dom A0 = I0 & dom (F|I0) = I0 by PARTFUN1:def 2;
A4: dom B0 = I0 by PARTFUN1:def 2;
now
let i be object;
assume
A5: i in I0;
then
A6: B.i = B0.i by A2,A4,FUNCT_1:47;
G.i = F.i & A.i = A0.i by A1,A3,A5,FUNCT_1:47;
hence G.i is Function of A0.i,B0.i by A5,A6,PBOOLE:def 15;
end;
hence thesis by PBOOLE:def 15;
end;
definition
let S,S9 be strict non void non empty ManySortedSign;
let A be non-empty strict MSAlgebra over S9;
assume
A1: S <= S9;
func A Over S -> non-empty strict MSAlgebra over S means
:Def2:
the Sorts of
it = (the Sorts of A)|the carrier of S & the Charact of it = (the Charact of A)
|the carrier' of S;
existence
proof
set D = (the Charact of A)|the carrier' of S;
set C = (the Sorts of A)|the carrier of S;
A2: rng (the Arity of S) c= (the carrier of S)*;
A3: the carrier' of S c= the carrier' of S9 by A1;
then reconsider D as ManySortedSet of the carrier' of S;
A4: the carrier of S c= the carrier of S9 by A1;
then reconsider C as ManySortedSet of the carrier of S;
rng (the ResultSort of S) c= the carrier of S;
then
A5: C * the ResultSort of S = (the Sorts of A) * the ResultSort of S by Th1
.= ((the Sorts of A) * the ResultSort of S9)|the carrier' of S by
RELAT_1:83,A1;
C# * the Arity of S = ((the Sorts of A)#|((the carrier of S)*)) * the
Arity of S by A4,Th4
.= (the Sorts of A)# * ((the Arity of S9)|the carrier' of S)
by A1,A2,Th1
.= ((the Sorts of A)# * the Arity of S9)|the carrier' of S by RELAT_1:83;
then reconsider D as ManySortedFunction of C# * the Arity of S, C * the
ResultSort of S by A3,A5,Th8;
reconsider B = MSAlgebra(#C,D#) as non-empty strict MSAlgebra over S by
MSUALG_1:def 3;
take B;
thus thesis;
end;
uniqueness;
end;
theorem Th9:
for S be strict non void non empty ManySortedSign, A be non-empty
strict MSAlgebra over S holds A = A Over S
proof
let S be strict non void non empty ManySortedSign;
let A be non-empty strict MSAlgebra over S;
A1: the Charact of A Over S = (the Charact of A)|the carrier' of S by Def2
.= the Charact of A;
the Sorts of A Over S = (the Sorts of A)|the carrier of S by Def2
.= the Sorts of A;
hence thesis by A1;
end;
theorem Th10:
for U1,U2 st U1,U2 are_similar holds MSSign U1 = MSSign U2
proof
let U1,U2 such that
A1: U1,U2 are_similar;
reconsider f = (*-->0)*(signature U1) as Function of dom signature(U1), {0}*
by MSUALG_1:2;
A2: the carrier of MSSign U1 = {0} & the Arity of MSSign U1 = f by
MSUALG_1:def 8;
reconsider f = (*-->0)*(signature U2) as Function of dom signature(U2), {0}*
by MSUALG_1:2;
A3: the Arity of MSSign U2 = f & the ResultSort of MSSign U2 = dom signature
U2 -->0 by MSUALG_1:def 8;
A4: the ResultSort of MSSign U1 = dom signature U1-->0 & the carrier of
MSSign U2 = {0} by MSUALG_1:def 8;
the carrier' of MSSign U1 = dom signature U1 & the carrier' of MSSign U2
= dom signature U2 by MSUALG_1:def 8;
then the carrier' of MSSign U1 = the carrier' of MSSign U2 by A1;
hence thesis by A1,A2,A4,A3;
end;
definition
let U1,U2 be Universal_Algebra, h be Function of U1,U2;
assume
A1: MSSign U1 = MSSign U2;
func MSAlg h -> ManySortedFunction of MSAlg U1, ((MSAlg U2) Over MSSign U1)
equals
:Def3:
0 .--> h;
coherence
proof
the carrier of MSSign U2 = {0} by MSUALG_1:def 8;
then reconsider Z2 = the Sorts of MSAlg U2 as ManySortedSet of {0};
set f = 0 .--> h;
MSAlg U2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
then
A2: (the Sorts of MSAlg U2).0 = (0 .--> the carrier of U2).0 by MSUALG_1:def 9
.= the carrier of U2 by FUNCOP_1:72;
A3: the carrier of MSSign U1 = {0} by MSUALG_1:def 8;
then reconsider Z1 = the Sorts of MSAlg U1 as ManySortedSet of {0};
MSAlg U1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
then
A4: (the Sorts of MSAlg U1).0 = (0 .--> the carrier of U1).0 by MSUALG_1:def 9
.= the carrier of U1 by FUNCOP_1:72;
now
let a be object;
assume a in {0};
then a = 0 by TARSKI:def 1;
hence
f.a is Function of (the Sorts of MSAlg U1).a,(the Sorts of MSAlg U2
).a by A4,A2,FUNCOP_1:72;
end;
then f is ManySortedFunction of Z1,Z2 by PBOOLE:def 15;
hence thesis by A1,A3,Th9;
end;
end;
theorem Th11:
for U1,U2,h st U1,U2 are_similar for o be OperSymbol of MSSign
U1 holds ((MSAlg h).(the_result_sort_of o)) = h
proof
let U1,U2,h such that
A1: U1,U2 are_similar;
set f = MSAlg h;
let o be OperSymbol of MSSign U1;
A2: the carrier' of MSSign U1 = dom signature U1 & the ResultSort of MSSign
U1 = dom signature U1-->0 by MSUALG_1:def 8;
A3: 0 in {0} by TARSKI:def 1;
thus (f.(the_result_sort_of o)) = (f.((the ResultSort of MSSign U1).o)) by
MSUALG_1:def 2
.= (( 0.--> h ).0 ) by A1,A2,Def3,Th10
.= h by A3,FUNCOP_1:7;
end;
theorem Th12:
for o be OperSymbol of MSSign U1 holds Den(o,MSAlg U1) = (the
charact of U1).o
proof
let o be OperSymbol of MSSign U1;
MSAlg U1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
hence Den(o,MSAlg U1) = ((MSCharact U1).o) by MSUALG_1:def 6
.= ((the charact of U1).o) by MSUALG_1:def 10;
end;
Lm1: for U1 be Universal_Algebra holds dom signature U1 = dom the charact of U1
proof
let U1 be Universal_Algebra;
thus dom signature U1 = Seg len signature U1 by FINSEQ_1:def 3
.= Seg len the charact of U1 by UNIALG_1:def 4
.= dom the charact of U1 by FINSEQ_1:def 3;
end;
theorem Th13:
for o be OperSymbol of MSSign U1 holds Den(o,MSAlg U1) is operation of U1
proof
let o be OperSymbol of MSSign U1;
A1: dom signature U1 = dom the charact of U1 by Lm1;
Den(o,MSAlg U1) = (the charact of U1).o & the carrier' of MSSign U1 =
dom signature U1 by Th12,MSUALG_1:def 8;
hence thesis by A1,FUNCT_1:def 3;
end;
Lm2: for U1,U2 st U1,U2 are_similar for o be OperSymbol of MSSign U1 holds Den
(o,MSAlg U2 Over MSSign U1) is operation of U2
proof
let U1,U2;
set A = MSAlg U2 Over MSSign U1;
A1: MSAlg U2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
assume
A2: U1,U2 are_similar;
then
A3: MSSign U1 = MSSign U2 by Th10;
let o be OperSymbol of MSSign U1;
A4: Den(o,A) = ((the Charact of A).o) by MSUALG_1:def 6
.= ((MSCharact U2).o) by A3,A1,Th9
.= ((the charact of U2).o) by MSUALG_1:def 10;
A5: dom signature U1 = dom the charact of U1 by Lm1;
signature U1 = signature U2 by A2;
then the carrier' of MSSign U1 = dom signature U1 & dom the charact of U1 =
dom the charact of U2 by A5,Lm1,MSUALG_1:def 8;
hence thesis by A4,A5,FUNCT_1:def 3;
end;
theorem Th14:
for o be OperSymbol of MSSign U1 for y be Element of Args(o,
MSAlg U1) holds y is FinSequence of the carrier of U1
proof
let o be OperSymbol of MSSign U1;
let y be Element of Args(o,MSAlg U1);
set O1 = Den(o,MSAlg U1);
A1: O1 = (the charact of U1).o & the carrier' of MSSign U1 = dom signature
U1 by Th12,MSUALG_1:def 8;
dom signature U1 = dom the charact of U1 by Lm1;
then reconsider O1 as operation of U1 by A1,FUNCT_1:def 3;
Args(o,MSAlg U1) = dom O1 by FUNCT_2:def 1;
then y in (the carrier of U1)* by TARSKI:def 3;
hence thesis by FINSEQ_1:def 11;
end;
theorem Th15:
for U1,U2,h st U1,U2 are_similar for o be OperSymbol of MSSign
U1,y be Element of Args(o,MSAlg U1) holds (MSAlg h)#y = h * y
proof
let U1,U2,h;
assume
A1: U1,U2 are_similar;
reconsider f1 = (*-->0)*(signature U1) as Function of dom signature(U1), {0}
* by MSUALG_1:2;
let o be OperSymbol of MSSign U1;
A2: the carrier' of MSSign U2 = dom signature U2 by MSUALG_1:def 8;
MSSign U1 = MSSign U2 by A1,Th10;
then o in dom signature U2 by A2;
then
A3: o in dom signature U1 by A1;
then o in dom f1 by FUNCT_2:def 1;
then
A4: ((*-->0)*(signature U1)).o = (*-->0).((signature U1).o) by FUNCT_1:12;
let y be Element of Args(o,MSAlg U1);
set f = MSAlg h;
A5: the carrier of MSSign U1 = {0} by MSUALG_1:def 8;
set X = dom (h*y);
A6: dom h = the carrier of U1 by FUNCT_2:def 1;
A7: y is FinSequence of the carrier of U1 by Th14;
then rng y c= the carrier of U1 by FINSEQ_1:def 4;
then reconsider p = h*y as FinSequence by A7,A6,FINSEQ_1:16;
A8: X = dom y by A7,FINSEQ_3:120;
the Arity of MSSign U1 = f1 by MSUALG_1:def 8;
then
A9: the_arity_of o = ((*-->0)*(signature U1)).o by MSUALG_1:def 1;
(signature U1).o in rng signature U1 by A3,FUNCT_1:def 3;
then consider n being Element of NAT such that
A10: n = ((signature U1).o);
A11: 0 in {0} by TARSKI:def 1;
A12: now
0 is Element of {0} by TARSKI:def 1;
then n |-> 0 is FinSequence of {0} by FINSEQ_2:63;
then reconsider
l = n |-> 0 as Element of (the carrier of MSSign U1)* by A5,FINSEQ_1:def 11;
let m;
A13: (the_arity_of o)/.m = l/.m & dom (n |-> 0) = Seg n by A9,A4,A10,
FINSEQ_2:def 6;
assume m in dom y;
then m in dom (the_arity_of o) by MSUALG_3:6;
then
A14: m in dom (n |-> 0) by A9,A4,A10,FINSEQ_2:def 6;
then l/.m = l.m by PARTFUN1:def 6;
then (the_arity_of o)/.m = 0 by A14,A13,FUNCOP_1:7;
hence (f.((the_arity_of o)/.m)) = (( 0.--> h ).0) by A1,Def3,Th10
.= h by A11,FUNCOP_1:7;
end;
A15: now
let m be Nat;
assume
A16: m in dom y;
then
A17: m in dom (h*y) by A7,FINSEQ_3:120;
(f#y).m = (f.((the_arity_of o)/.m)).(y.m) by A16,MSUALG_3:def 6;
hence (f#y).m = h.(y.m) by A12,A16
.= p.m by A7,A17,FINSEQ_3:120;
end;
dom (f#y) = dom (the_arity_of o) by MSUALG_3:6
.= dom (n |-> 0) by A9,A4,A10,FINSEQ_2:def 6
.= Seg n;
then
A18: f#y is FinSequence by FINSEQ_1:def 2;
A19: dom y = dom (the_arity_of o) by MSUALG_3:6
.= dom (n |-> 0) by A9,A4,A10,FINSEQ_2:def 6
.= Seg n;
dom (f#y) = dom (the_arity_of o) by MSUALG_3:6
.= dom (n |-> 0) by A9,A4,A10,FINSEQ_2:def 6
.= X by A7,A19,FINSEQ_3:120;
hence thesis by A18,A15,A8,FINSEQ_1:13;
end;
theorem Th16:
h is_homomorphism implies MSAlg h is_homomorphism MSAlg U1
,(MSAlg U2 Over MSSign U1)
proof
set f = MSAlg h;
set A = MSAlg U2 Over MSSign U1;
A1: MSAlg U2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
consider m such that
A2: the carrier' of MSSign U1 = Seg m by MSUALG_1:def 7;
assume
A3: h is_homomorphism;
then
A4: U1,U2 are_similar;
then
A5: MSSign U1 = MSSign U2 by Th10;
let o be OperSymbol of MSSign U1 such that
Args (o,MSAlg U1) <> {};
o in Seg m by A2;
then reconsider k = o as Element of NAT;
reconsider O2 = Den(o,A) as operation of U2 by A4,Lm2;
Den(o,A) = ((the Charact of A).o) by MSUALG_1:def 6
.= ((MSCharact U2).o) by A5,A1,Th9
.= ((the charact of U2).o) by MSUALG_1:def 10;
then
A6: O2 = (the charact of U2).k;
set O1 = Den(o,MSAlg U1);
let y be Element of Args(o,MSAlg U1);
A7: O1 = (the charact of U1).o & the carrier' of MSSign U1 = dom signature
U1 by Th12,MSUALG_1:def 8;
reconsider O1 as operation of U1 by Th13;
A8: y is FinSequence of the carrier of U1 by Th14;
dom signature U1 = dom the charact of U1 & Args(o,MSAlg U1) = dom O1 by Lm1,
FUNCT_2:def 1;
then h.(O1.y) = O2.(h*y) by A3,A7,A6,A8
.= Den(o,A).(f#y) by A4,Th15;
hence thesis by A4,Th11;
end;
Lm3: for n be Nat st n in dom the charact of U1 holds n is OperSymbol of
MSSign U1
proof
A1: dom signature U1 = dom the charact of U1 by Lm1;
let n be Nat;
assume n in dom the charact of U1;
hence thesis by A1,MSUALG_1:def 8;
end;
theorem Th17:
U1,U2 are_similar implies MSAlg h is ManySortedSet of {0}
proof
assume U1,U2 are_similar;
then MSAlg h = 0 .--> h by Def3,Th10;
hence thesis;
end;
theorem Th18:
h is_epimorphism implies MSAlg h is_epimorphism MSAlg U1,
(MSAlg U2 Over MSSign U1)
proof
set f = MSAlg h;
set A = MSAlg U2 Over MSSign U1;
A1: 0 in {0} by TARSKI:def 1;
MSSorts U2 = 0 .--> the carrier of U2 by MSUALG_1:def 9;
then
A2: the carrier of MSSign U1 = {0} & (MSSorts U2).0 = the carrier of U2 by A1,
FUNCOP_1:7,MSUALG_1:def 8;
A3: MSAlg U2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
assume
A4: h is_epimorphism;
then
A5: rng h = the carrier of U2;
A6: h is_homomorphism by A4;
then
A7: U1,U2 are_similar;
then MSSign U1 = MSSign U2 by Th10;
then
A8: the Sorts of A = MSSorts U2 by A3,Th9;
thus f is_homomorphism MSAlg U1,A by A6,Th16;
let i be set;
assume i in the carrier of MSSign U1;
then reconsider i9=i as Element of MSSign U1;
reconsider h9 = f.i as Function of (the Sorts of MSAlg U1).i9, (the Sorts of
A).i9 by PBOOLE:def 15;
f.0 = (0.--> h).0 by A7,Def3,Th10
.= h by A1,FUNCOP_1:7;
then the carrier of MSSign U1 = {0} & rng h9 = (the Sorts of A).0 by A5,A8,A2
,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem Th19:
h is_monomorphism implies MSAlg h is_monomorphism MSAlg
U1,(MSAlg U2 Over MSSign U1)
proof
set f = MSAlg h;
the carrier of MSSign U1 = {0} by MSUALG_1:def 8;
then
A1: dom f = {0} by PARTFUN1:def 2;
assume
A2: h is_monomorphism;
then
A3: h is_homomorphism;
hence MSAlg h is_homomorphism MSAlg U1,(MSAlg U2 Over MSSign U1) by Th16;
U1,U2 are_similar by A3;
then f = 0 .--> h by Def3,Th10;
then
A4: f.0 = h by FUNCOP_1:72;
let i be set, h9 be Function;
assume i in dom f & f.i = h9;
then h = h9 by A4,A1,TARSKI:def 1;
hence thesis by A2;
end;
theorem
h is_isomorphism implies MSAlg h is_isomorphism MSAlg U1,(MSAlg
U2 Over MSSign U1)
by Th18,Th19;
theorem Th21:
for U1,U2,h st U1,U2 are_similar holds MSAlg h is_homomorphism
MSAlg U1,(MSAlg U2 Over MSSign U1) implies h is_homomorphism
proof
let U1,U2,h such that
A1: U1,U2 are_similar;
A2: MSSign U1 = MSSign U2 by A1,Th10;
set A = MSAlg U2 Over MSSign U1;
set f = MSAlg h;
assume
A3: f is_homomorphism MSAlg U1,A;
thus U1,U2 are_similar by A1;
let n be Nat;
assume n in dom the charact of U1;
then reconsider o = n as OperSymbol of MSSign U1 by Lm3;
let O1 be operation of U1, O2 be operation of U2 such that
A4: O1 = (the charact of U1).n and
A5: O2 = (the charact of U2).n;
A6: O1 = Den(o,MSAlg U1) by A4,Th12;
let x be FinSequence of U1;
assume x in dom O1;
then reconsider y = x as Element of Args(o,MSAlg U1) by A6,FUNCT_2:def 1;
A7: (f.(the_result_sort_of o)).(Den(o,MSAlg U1).y) = h.(O1.y) by A1,A6,Th11;
A8: (f.(the_result_sort_of o)).(Den(o,MSAlg U1).y) = Den(o,A).(f#y) by A3;
A9: MSAlg U2 = MSAlgebra(#MSSorts U2,MSCharact U2#) by MSUALG_1:def 11;
Den(o,A) = ((the Charact of A).o) by MSUALG_1:def 6
.= ((MSCharact U2).o) by A2,A9,Th9
.= O2 by A5,MSUALG_1:def 10;
hence thesis by A1,A7,A8,Th15;
end;
theorem Th22:
for U1,U2,h st U1, U2 are_similar holds MSAlg h is_epimorphism
MSAlg U1, (MSAlg U2 Over MSSign U1) implies h is_epimorphism
proof
let U1, U2, h;
set B = the Sorts of (MSAlg U2 Over MSSign U1);
set I = the carrier of MSSign U1;
A1: 0 in {0} by TARSKI:def 1;
MSSorts U2 = 0 .--> the carrier of U2 by MSUALG_1:def 9;
then
A2: (MSSorts U2).0 = the carrier of U2 by A1,FUNCOP_1:7;
A3: I = {0} & MSAlg U2 = MSAlgebra (#MSSorts U2, MSCharact U2#) by
MSUALG_1:def 8,def 11;
assume
A4: U1, U2 are_similar;
then MSSign U1 = MSSign U2 by Th10;
then
A5: B = the Sorts of MSAlg U2 by Th9;
assume
A6: MSAlg h is_epimorphism MSAlg U1, (MSAlg U2 Over MSSign U1);
then
A7: MSAlg h is "onto";
MSAlg h is_homomorphism MSAlg U1, (MSAlg U2 Over MSSign U1) by A6;
then
A8: h is_homomorphism by A4,Th21;
(MSAlg h).0 = (0.--> h).0 by A4,Def3,Th10
.= h by A1,FUNCOP_1:7;
then rng h = the carrier of U2 by A7,A1,A2,A5,A3;
hence h is_epimorphism by A8;
end;
theorem Th23:
for U1, U2, h st U1, U2 are_similar holds MSAlg h
is_monomorphism MSAlg U1, (MSAlg U2 Over MSSign U1) implies h is_monomorphism
proof
let U1,U2,h;
assume
A1: U1,U2 are_similar;
assume
A2: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2 Over MSSign U1);
then
A3: MSAlg h is "1-1";
MSAlg h is_homomorphism MSAlg U1,(MSAlg U2 Over MSSign U1) by A2;
then
A4: h is_homomorphism by A1,Th21;
A5: the carrier of MSSign U1 = {0} by MSUALG_1:def 8;
A6: 0 in {0} by TARSKI:def 1;
(MSAlg h).0 = (0.--> h).0 by A1,Def3,Th10
.= h by A6,FUNCOP_1:7;
then h is one-to-one by A3,A5,A6,MSUALG_3:1;
hence thesis by A4;
end;
theorem
for U1, U2, h st U1, U2 are_similar holds MSAlg h is_isomorphism MSAlg
U1, (MSAlg U2 Over MSSign U1) implies h is_isomorphism
by Th23,Th22;
theorem
MSAlg (id the carrier of U1) = (id the Sorts of MSAlg U1)
proof
set f = (id the Sorts of MSAlg U1);
set h = id the carrier of U1;
A1: the carrier of MSSign U1 = {0} by MSUALG_1:def 8;
then reconsider Z1 = the Sorts of MSAlg U1 as ManySortedSet of {0};
A2: now
let i be set;
MSAlg U1 = MSAlgebra(#MSSorts U1,MSCharact U1#) by MSUALG_1:def 11;
then
A3: Z1.0 = (0 .--> the carrier of U1).0 by MSUALG_1:def 9
.= the carrier of U1 by FUNCOP_1:72;
assume
A4: i in {0};
then i = 0 by TARSKI:def 1;
hence f.0 = h by A1,A4,A3,MSUALG_3:def 1;
end;
MSAlg h = 0 .--> h by Def3;
then
A5: (MSAlg h).0 = h by FUNCOP_1:72;
now
let a be object;
assume
A6: a in {0};
then a = 0 by TARSKI:def 1;
hence f.a = (MSAlg h).a by A2,A5,A6;
end;
hence f = MSAlg h by A1,PBOOLE:3;
end;
theorem
for U1,U2,U3 st U1,U2 are_similar & U2,U3 are_similar for h1 be
Function of U1,U2, h2 be Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) =
MSAlg (h2*h1)
proof
let U1,U2,U3 such that
A1: U1,U2 are_similar and
A2: U2,U3 are_similar;
let h1 be Function of U1,U2, h2 be Function of U2,U3;
A3: MSAlg h1 is ManySortedSet of {0} by A1,Th17;
MSAlg h2 is ManySortedSet of {0} by A2,Th17;
then
A4: dom MSAlg h2 = {0} by PARTFUN1:def 2;
A5: dom ((MSAlg h2)**(MSAlg h1)) = (dom MSAlg h1) /\ (dom MSAlg h2) by
PBOOLE:def 19
.= {0} /\ {0} by A3,A4,PARTFUN1:def 2
.= {0};
A6: now
let a be set ,f be Function, g be Function such that
A7: a in dom ((MSAlg h2) ** (MSAlg h1)) and
A8: f = (MSAlg h1).a and
A9: g = (MSAlg h2).a;
A10: g = (MSAlg h2).0 by A5,A7,A9,TARSKI:def 1
.= (0 .--> h2).0 by A2,Def3,Th10
.= h2 by FUNCOP_1:72;
f = (MSAlg h1).0 by A5,A7,A8,TARSKI:def 1
.= (0 .--> h1).0 by A1,Def3,Th10
.= h1 by FUNCOP_1:72;
hence ((MSAlg h2)**(MSAlg h1)).a = h2*h1 by A7,A8,A9,A10,PBOOLE:def 19;
end;
set h = h2*h1;
A11: MSAlg h is ManySortedSet of {0} by A1,A2,Th17,UNIALG_2:2;
A12: MSSign U2 = MSSign U3 by A2,Th10;
A13: now
let a be set;
assume a in dom MSAlg h;
then
A14: a in {0} by A11,PARTFUN1:def 2;
(MSAlg (h2*h1)).0 = (0 .--> (h2*h1)).0 by A1,A12,Def3,Th10
.= h2*h1 by FUNCOP_1:72;
hence (MSAlg (h2*h1)).a = h2*h1 by A14,TARSKI:def 1;
end;
A15: dom (MSAlg (h2*h1)) = {0} by A11,PARTFUN1:def 2;
A16: now
let a be set, f,g be Function such that
A17: a in dom (MSAlg (h2*h1)) and
A18: f = (MSAlg h1).a & g = (MSAlg h2).a;
thus (MSAlg (h2*h1)).a = h2*h1 by A13,A17
.= ((MSAlg h2)**(MSAlg h1)).a by A5,A6,A15,A17,A18;
end;
A19: dom MSAlg (h2*h1) = {0} by A11,PARTFUN1:def 2;
A20: for a being object st a in {0}
holds ((MSAlg h2)**(MSAlg h1)).a = (MSAlg (h2*h1)).a
proof
let a be object;
A21: (MSAlg h1).a is Function & (MSAlg h2).a is Function;
assume a in {0};
hence thesis by A19,A16,A21;
end;
((MSAlg h2)**(MSAlg h1)) is ManySortedSet of {0} by A5,PARTFUN1:def 2
,RELAT_1:def 18;
hence thesis by A11,A20,PBOOLE:3;
end;