:: Homomorphisms of Many Sorted Algebras
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received April 25, 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 STRUCT_0, XBOOLE_0, MSUALG_1, NAT_1, PBOOLE, SUBSET_1, FUNCT_1,
RELAT_1, MEMBER_1, CARD_3, MARGREL1, TARSKI, FUNCT_6, NUMBERS, FINSEQ_4,
PARTFUN1, WELLORD1, GROUP_6, MSUALG_2, UNIALG_2, MSUALG_3;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
RELAT_1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3,
FUNCT_6, STRUCT_0, PRALG_1, MSUALG_1, MSUALG_2, PRALG_2;
constructors PRALG_1, MSUALG_2, PRALG_2, RELSET_1, FINSEQ_2, XTUPLE_0;
registrations FUNCT_2, FUNCOP_1, CARD_3, FUNCT_1, STRUCT_0, MSUALG_1,
MSUALG_2, ORDINAL1, RELAT_1, RELSET_1, PBOOLE, FINSEQ_1;
requirements BOOLE, SUBSET;
definitions TARSKI, MSUALG_2, XBOOLE_0;
equalities XBOOLE_0;
expansions TARSKI, MSUALG_2, XBOOLE_0;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, PBOOLE, CARD_3, MSUALG_1, PRALG_1,
MSUALG_2, RELAT_1, PRALG_2, FUNCT_6, FINSEQ_2, XBOOLE_0, FUNCOP_1,
PARTFUN1;
schemes FUNCT_1, CLASSES1;
begin
reserve S for non void non empty ManySortedSign,
U1,U2 for MSAlgebra over S,
o for OperSymbol of S,
n for Nat;
:: PRELIMINARIES - MANY SORTED FUNCTIONS
definition
let I be non empty set, A,B be ManySortedSet of I, F be ManySortedFunction
of A,B, i be Element of I;
redefine func F.i -> Function of A.i,B.i; :: redefines . (FUNCT_1, definition)
coherence by PBOOLE:def 15;
end;
definition
let S be non empty ManySortedSign;
let U1,U2 be MSAlgebra over S;
mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1,
the Sorts of U2;
end;
definition
let I be set,A be ManySortedSet of I;
func id A -> ManySortedFunction of A,A means
:Def1:
for i be set st i in I holds it.i = id (A.i);
existence
proof
deffunc F(object)=id (A.$1);
consider f being Function such that
A1: dom f = I & for i be object st i in I holds f.i = F(i) from FUNCT_1:
sch 3;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then f.x = id (A.x) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of I by FUNCOP_1:def 6;
for i be object st i in I holds f.i is Function of A.i,A.i
proof
let i be object;
assume i in I;
then f.i = id (A.i) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of A,A by PBOOLE:def 15;
take f;
thus thesis by A1;
end;
uniqueness
proof
let F,G be ManySortedFunction of A,A;
assume that
A2: for i be set st i in I holds F.i = id (A.i) and
A3: for i be set st i in I holds G.i = id (A.i);
A4: now
let i be object;
assume
A5: i in I;
then F.i = id (A.i) by A2;
hence F.i = G.i by A3,A5;
end;
dom F = I & dom G = I by PARTFUN1:def 2;
hence thesis by A4,FUNCT_1:2;
end;
end;
definition
let IT be Function;
attr IT is "1-1" means
for i be set, f be Function st i in dom IT & IT.i = f holds f is one-to-one;
end;
registration
let I be set;
cluster "1-1" for ManySortedFunction of I;
existence
proof
set A = the ManySortedSet of I;
take F = id A;
let i be set, f be Function;
A1: dom (id A) = I by PARTFUN1:def 2;
assume i in dom F & F.i = f;
then f = id (A.i) by A1,Def1;
hence thesis;
end;
end;
theorem Th1:
for I be set,F be ManySortedFunction of I holds F is "1-1" iff
for i be set st i in I holds F.i is one-to-one
proof
let I be set;
let F be ManySortedFunction of I;
A1: dom F = I by PARTFUN1:def 2;
hence F is "1-1" implies for i be set st i in I holds F.i is one-to-one;
assume for i be set st i in I holds F.i is one-to-one;
then for i be set, f being Function st i in dom F & f = F.i holds f is
one-to-one by A1;
hence thesis;
end;
definition
let I be set, A,B be ManySortedSet of I;
let IT be ManySortedFunction of A,B;
attr IT is "onto" means
for i be set st i in I holds rng(IT.i) = B.i;
end;
theorem Th2:
for I be set, A,B,C be ManySortedSet of I, F be
ManySortedFunction of A,B, G be ManySortedFunction of B,C holds dom (G ** F) =
I & for i be set st i in I holds (G**F).i = (G.i)*(F.i)
proof
let I be set, A,B,C be ManySortedSet of I, F be ManySortedFunction of A,B, G
be ManySortedFunction of B,C;
dom F = I & dom G = I by PARTFUN1:def 2;
then (dom F) /\ (dom G) = I;
hence
A1: dom (G ** F) = I by PBOOLE:def 19;
let i be set;
thus thesis by A1,PBOOLE:def 19;
end;
definition
let I be set, A be ManySortedSet of I, B,C be non-empty ManySortedSet of I,
F be ManySortedFunction of A,B, G be ManySortedFunction of B,C;
redefine func G**F -> ManySortedFunction of A,C; :: redefines ** (PBOOLE, definition)
coherence
proof
dom (G ** F) = I by Th2;
then reconsider fg = G ** F as ManySortedSet of I by PARTFUN1:def 2
,RELAT_1:def 18;
reconsider fg as ManySortedFunction of I;
for i be object st i in I holds fg.i is Function of A.i,C.i
proof
let i be object;
assume
A1: 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 A1,PBOOLE:def 15;
(G**F).i = g*f by A1,Th2;
hence thesis by A1;
end;
hence thesis by PBOOLE:def 15;
end;
end;
theorem
for I be set,A,B be ManySortedSet of I, F be ManySortedFunction of A,B
holds F**(id A) = F
proof
let I be set, A,B be ManySortedSet of I, F be ManySortedFunction of A,B;
dom (F**(id A)) = (dom F) /\ dom id A by PBOOLE:def 19
.= I /\ dom id A by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2
.= I;
then reconsider G = F**(id A) as ManySortedFunction of I by PARTFUN1:def 2
,RELAT_1:def 18;
now
let i be object;
assume
A1: i in I;
then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15;
reconsider g = (id A).i as Function of A.i,A.i by A1,PBOOLE:def 15;
A2: G.i = f*g by A1,Th2
.= f*(id (A.i)) by A1,Def1;
per cases;
suppose
B.i = {} implies A.i = {};
then dom f = A.i by FUNCT_2:def 1;
hence G.i = F.i by A2,RELAT_1:52;
end;
suppose
B.i = {} & A.i <> {};
then f = {};
hence G.i = F.i by A2;
end;
end;
hence thesis by PBOOLE:3;
end;
theorem Th4:
for I be set, A,B be ManySortedSet of I for F be
ManySortedFunction of A, B holds (id B)**F = F
proof
let I be set;
let A,B be ManySortedSet of I;
let F be ManySortedFunction of A, B;
dom ((id B)**F) = (dom id B) /\ dom F by PBOOLE:def 19
.= I /\ dom F by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2
.= I;
then reconsider G = (id B)**F as ManySortedFunction of I by PARTFUN1:def 2
,RELAT_1:def 18;
now
let i be object;
assume
A1: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
reconsider g = (id B).i as Function of B.i, B.i by A1,PBOOLE:def 15;
g = id (B.i) & G.i = g * f by A1,Def1,Th2;
hence G.i = F.i by FUNCT_2:17;
end;
hence thesis by PBOOLE:3;
end;
definition
let I be set, A,B be ManySortedSet of I, F be ManySortedFunction of A,B;
assume that
A1: F is "1-1" and
A2: F is "onto";
func F"" -> ManySortedFunction of B,A means
:Def4:
for i be set st i in I holds it.i = (F.i)";
existence
proof
defpred P[object,object] means $2 = (F.$1)";
A3: for i be object st i in I ex u be object st P[i,u];
consider H being Function such that
A4: dom H = I & for i be object st i in I holds P[i,H.i] from CLASSES1:
sch 1 (A3);
reconsider H as ManySortedSet of I by A4,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom H holds H.x is Function
proof
let x be object;
assume
A5: x in dom H;
then x in I by PARTFUN1:def 2;
then reconsider f = F.x as Function of A.x,B.x by PBOOLE:def 15;
H.x = f" by A4,A5;
hence thesis;
end;
then reconsider H as ManySortedFunction of I by FUNCOP_1:def 6;
for i be object st i in I holds H.i is Function of B.i,A.i
proof
let i be object;
assume
A6: i in I;
then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15;
i in dom F by A6,PARTFUN1:def 2;
then
A7: f is one-to-one by A1;
rng f = B.i by A2,A6;
then f" is Function of B.i,A.i by A7,FUNCT_2:25;
hence thesis by A4,A6;
end;
then reconsider H as ManySortedFunction of B,A by PBOOLE:def 15;
take H;
thus thesis by A4;
end;
uniqueness
proof
let H1,H2 be ManySortedFunction of B,A;
assume that
A8: for i be set st i in I holds H1.i = (F.i)" and
A9: for i be set st i in I holds H2.i = (F.i)";
now
let i be object;
assume
A10: i in I;
then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15;
H1.i = f" by A8,A10;
hence H1.i = H2.i by A9,A10;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th5:
for I be set,A,B be non-empty ManySortedSet of I, H be
ManySortedFunction of A,B, H1 be ManySortedFunction of B,A st H is "1-1" "onto"
& H1 = H"" holds H**H1 = id B & H1**H = id A
proof
let I be set, A,B be non-empty ManySortedSet of I, H be ManySortedFunction
of A,B, H1 be ManySortedFunction of B,A;
assume that
A1: H is "1-1" "onto" and
A2: H1 = H"";
A3: now
let i be set;
assume
A4: i in I;
then reconsider h = H.i as Function of A.i,B.i by PBOOLE:def 15;
reconsider h1 = H1.i as Function of B.i,A.i by A4,PBOOLE:def 15;
i in dom H by A4,PARTFUN1:def 2;
then
A5: h is one-to-one by A1;
h1 = h" by A1,A2,A4,Def4;
then h*h1 = id rng h by A5,FUNCT_1:39;
then h*h1 = id (B.i) by A1,A4;
hence (H**H1).i = id (B.i) by A4,Th2;
end;
for i be set st i in I holds (H1**H).i = id (A.i)
proof
let i be set;
assume
A6: i in I;
then reconsider h = H.i as Function of A.i,B.i by PBOOLE:def 15;
reconsider h1 = H1.i as Function of B.i,A.i by A6,PBOOLE:def 15;
i in dom H by A6,PARTFUN1:def 2;
then
A7: h is one-to-one by A1;
h1 = h" & dom h = A.i by A1,A2,A6,Def4,FUNCT_2:def 1;
then h1*h = id (A.i) by A7,FUNCT_1:39;
hence thesis by A6,Th2;
end;
hence thesis by A3,Def1;
end;
registration
let S;
let U1 be non-empty MSAlgebra over S;
let o;
cluster Args(o,U1) -> functional;
coherence
proof
Args(o,U1) = product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:3;
hence thesis;
end;
end;
begin :: Homomorphisms of Many Sorted Algebras
theorem Th6:
for U1 being MSAlgebra over S
for x be Function st x in Args(o,U1) holds
dom x = dom the_arity_of o &
for y be set st y in dom ((the Sorts of U1) * (the_arity_of o)) holds
x.y in ((the Sorts of U1) * (the_arity_of o)).y
proof
let U1 be MSAlgebra over S;
let x be Function;
A1: Args(o,U1) = product((the Sorts of U1) * (the_arity_of o)) by PRALG_2:3;
dom (the Sorts of U1) = (the carrier of S) by PARTFUN1:def 2;
then
A2: rng (the_arity_of o) c= dom (the Sorts of U1) by FINSEQ_1:def 4;
assume
A3: x in Args(o,U1);
then dom x = dom ((the Sorts of U1) * (the_arity_of o)) by A1,CARD_3:9;
hence thesis by A3,A1,A2,CARD_3:9,RELAT_1:27;
end;
definition
let S;
let U1,U2 be MSAlgebra over S;
let o;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1);
assume that
A1: Args(o,U1) <> {} and
A2: Args(o,U2) <> {};
func F # x -> Element of Args(o,U2) equals
:Def5:
(Frege(F*the_arity_of o)).
x;
coherence
proof
A3: dom((the Sorts of U1)*(the_arity_of o)) = dom(F*the_arity_of o)
proof
hereby
let e be object;
assume
A4: e in dom((the Sorts of U1)*(the_arity_of o));
then (the_arity_of o).e in dom the Sorts of U1 by FUNCT_1:11;
then (the_arity_of o).e in the carrier of S by PARTFUN1:def 2;
then
A5: (the_arity_of o).e in dom F by PARTFUN1:def 2;
e in dom the_arity_of o by A4,FUNCT_1:11;
then e in dom(F*the_arity_of o) by A5,FUNCT_1:11;
hence e in dom(F*the_arity_of o);
end;
let e be object;
assume e in dom(F*the_arity_of o);
then e in dom(F*the_arity_of o);
then
A6: e in dom the_arity_of o by FUNCT_1:11;
then reconsider f = e as Element of NAT;
(the_arity_of o).f in the carrier of S by A6,FINSEQ_2:11;
then (the_arity_of o).e in dom the Sorts of U1 by PARTFUN1:def 2;
hence thesis by A6,FUNCT_1:11;
end;
now
let e be object;
A7: product((the Sorts of U2)*(the_arity_of o)) <> {} by A2,PRALG_2:3;
assume e in dom(F*the_arity_of o);
then e in dom(F*the_arity_of o);
then
A8: e in dom the_arity_of o by FUNCT_1:11;
then reconsider f = e as Element of NAT;
(the_arity_of o).f in the carrier of S by A8,FINSEQ_2:11;
then (the_arity_of o).e in dom the Sorts of U2 by PARTFUN1:def 2;
then
A9: e in dom((the Sorts of U2)*(the_arity_of o)) by A8,FUNCT_1:11;
A10: ((the Sorts of U2)*(the_arity_of o)).e = (the Sorts of U2).((
the_arity_of o).e) by A8,FUNCT_1:13;
A11: now
assume (the Sorts of U2).((the_arity_of o).e) = {};
then {} in rng((the Sorts of U2)*(the_arity_of o)) by A9,A10,
FUNCT_1:def 3;
hence contradiction by A7,CARD_3:26;
end;
reconsider Foe = F.((the_arity_of o).e) as Function of (the Sorts of U1)
.((the_arity_of o).e), (the Sorts of U2).((the_arity_of o).e) by A8,FINSEQ_2:11
,PBOOLE:def 15;
thus ((the Sorts of U1)*(the_arity_of o)).e = (the Sorts of U1).((
the_arity_of o).e) by A8,FUNCT_1:13
.= dom Foe by A11,FUNCT_2:def 1
.= proj1 ((F*the_arity_of o).e) by A8,FUNCT_1:13;
end;
then
A12: (the Sorts of U1) * (the_arity_of o) = doms(F*the_arity_of o) by A3,
FUNCT_6:def 2;
x in Args(o,U1) by A1; then
A13: x in product((the Sorts of U1) * (the_arity_of o)) by PRALG_2:3;
then consider f being Function such that
A14: x = f and
a14: dom f = dom doms(F*the_arity_of o) and
A15: for e being object st e in dom doms(F*the_arity_of o) holds f.e in (
doms(F*the_arity_of o)).e by A12,CARD_3:def 5;
AA: dom doms (F*the_arity_of o) = dom (F*the_arity_of o) by FUNCT_6:def 2;
A16: dom((F*the_arity_of o)..f) = dom(F*the_arity_of o) /\ dom f
by PRALG_1:def 19
.= dom (F*the_arity_of o) by a14,AA;
A17: rng the_arity_of o c= the carrier of S by FINSEQ_1:def 4; then
A18: rng the_arity_of o c= dom the Sorts of U2 by PARTFUN1:def 2;
SS: rng the_arity_of o c= dom F by A17,PARTFUN1:def 2; then
A19: dom(F*the_arity_of o) = dom the_arity_of o by RELAT_1:27
.= dom((the Sorts of U2)*(the_arity_of o)) by A18,RELAT_1:27;
A20: now
let e be object;
A21: product((the Sorts of U2)*(the_arity_of o)) <> {} by A2,PRALG_2:3;
assume
A22: e in dom((the Sorts of U2)*(the_arity_of o)); then
A23: e in dom the_arity_of o by FUNCT_1:11;
then reconsider g = F.((the_arity_of o).e) as Function of
(the Sorts of U1).((the_arity_of o).e),
(the Sorts of U2).((the_arity_of o).e) by FINSEQ_2:11,PBOOLE:def 15;
dom f = dom the_arity_of o by A14,A1,Th6; then
AC: e in dom f by A23; then
e in dom the_arity_of o by A1,A14,Th6; then
e in dom (F*the_arity_of o) by SS,RELAT_1:27; then
e in dom (F*the_arity_of o) /\ dom f by AC,XBOOLE_0:def 4; then
AB: e in dom ((F*the_arity_of o)..f) by PRALG_1:def 19;
reconsider r = e as Element of NAT by A23;
g = (F*the_arity_of o).e by A19,A22,FUNCT_1:12; then
A24: ((F*the_arity_of o)..f).e = g.(f.e) by PRALG_1:def 19,AB;
A25: ((the Sorts of U2)*(the_arity_of o)).e = (the Sorts of U2).((
the_arity_of o).e) by A23,FUNCT_1:13;
A26: now
assume (the Sorts of U2).((the_arity_of o).e) = {};
then {} in rng((the Sorts of U2)*(the_arity_of o)) by A22,A25,
FUNCT_1:def 3;
hence contradiction by A21,CARD_3:26;
end;
(the_arity_of o).r in the carrier of S by A23,FINSEQ_2:11;
then (the_arity_of o).e in dom the Sorts of U1 by PARTFUN1:def 2;
then e in dom((the Sorts of U1)*(the_arity_of o)) by A23,FUNCT_1:11;
then f.e in (doms(F*the_arity_of o)).e by A12,A15;
then f.e in (the Sorts of U1).((the_arity_of o).e) by A12,A23,FUNCT_1:13;
then g.(f.e) in (the Sorts of U2).((the_arity_of o).e) by A26,FUNCT_2:5;
hence
((F*the_arity_of o)..f).e in ((the Sorts of U2)*(the_arity_of o)).e
by A22,A24,FUNCT_1:12;
end;
(Frege(F*the_arity_of o)).x = (F*the_arity_of o)..f by A13,A12,A14,
PRALG_2:def 2;
then (Frege(F*the_arity_of o)).x in product((the Sorts of U2)*(
the_arity_of o)) by A16,A19,A20,CARD_3:9;
hence thesis by PRALG_2:3;
end;
correctness;
end;
Lm1: now
let S;
let U1,U2 be MSAlgebra over S;
let o;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1), f,u be Function;
assume that
A1: f = x and
A2: x in Args(o,U1) and
A3: u in Args(o,U2);
A4: rng the_arity_of o c= the carrier of S by FINSEQ_1:def 4;
A6: F#x = (Frege(F*the_arity_of o)).x by A2,A3,Def5;
A7: dom((the Sorts of U1)*(the_arity_of o)) = dom(F*the_arity_of o)
proof
hereby
let e be object;
assume
A8: e in dom((the Sorts of U1)*(the_arity_of o));
then (the_arity_of o).e in dom the Sorts of U1 by FUNCT_1:11;
then (the_arity_of o).e in the carrier of S by PARTFUN1:def 2;
then
A9: (the_arity_of o).e in dom F by PARTFUN1:def 2;
e in dom the_arity_of o by A8,FUNCT_1:11;
then e in dom(F*the_arity_of o) by A9,FUNCT_1:11;
hence e in dom(F*the_arity_of o);
end;
let e be object;
assume e in dom(F*the_arity_of o); then
A10: e in dom the_arity_of o by FUNCT_1:11;
then reconsider f = e as Element of NAT;
(the_arity_of o).f in the carrier of S by A10,FINSEQ_2:11;
then (the_arity_of o).e in dom the Sorts of U1 by PARTFUN1:def 2;
hence thesis by A10,FUNCT_1:11;
end;
A11: Args(o,U2) = product((the Sorts of U2) * (the_arity_of o)) by PRALG_2:3;
then
A12: dom u = dom((the Sorts of U2) * (the_arity_of o)) by A3,CARD_3:9;
A13: Args(o,U1) = product((the Sorts of U1) * (the_arity_of o)) by PRALG_2:3;
A14: dom f = dom the_arity_of o by A1,A2,Th6;
rng the_arity_of o c= dom the Sorts of U2 by A4,PARTFUN1:def 2; then
A15: dom u = dom the_arity_of o by A12,RELAT_1:27;
set tao = the_arity_of o;
now
let e be object;
assume e in dom (F*tao); then
A16: e in dom tao by FUNCT_1:11;
then reconsider Foe = F.(tao.e) as Function of (the Sorts of U1).(
tao.e), (the Sorts of U2).(tao.e) by FINSEQ_2:11,PBOOLE:def 15;
((the Sorts of U2)*tao).e in rng ((the Sorts of U2)*
tao) by A12,A15,A16,FUNCT_1:def 3;
then
A17: ((the Sorts of U2)*tao).e <> {} by A3,A11,CARD_3:26;
((the Sorts of U1)*(tao)).e = (the Sorts of U1).((
the_arity_of o) .e) & ((the Sorts of U2)*tao).e = (the Sorts of U2
).(tao.e) by A16,FUNCT_1:13;
hence ((the Sorts of U1)*tao).e = dom Foe by A17,FUNCT_2:def 1
.= proj1 ((F*tao).e) by A16,FUNCT_1:13;
end;
then
A18: (the Sorts of U1) * tao = doms(F*the_arity_of o) by A7,FUNCT_6:def 2;
hereby
assume u = F#x; then
A19: u = (Frege(F*tao)).x by A2,A3,Def5;
let n;
assume
A20: n in dom f;
then tao.n in the carrier of S by A14,FINSEQ_2:11;
then tao.n in dom F by PARTFUN1:def 2; then
A21: n in dom(F*the_arity_of o) by A14,A20,FUNCT_1:11; then
n in dom(F*tao) /\ dom f by A20,XBOOLE_0:def 4; then
a21: n in dom ((F*the_arity_of o)..f) by PRALG_1:def 19;
A22: (F*the_arity_of o).n = F.((the_arity_of o).n) by FUNCT_1:12,A21
.= F.((the_arity_of o)/.n) by A14,A20,PARTFUN1:def 6;
thus u.n = ((F*the_arity_of o)..f).n by A1,A2,A13,A18,A19,PRALG_2:def 2
.= (F.((the_arity_of o)/.n)).(f.n) by A22,PRALG_1:def 19,a21;
end;
F#x is Element of product((the Sorts of U2) * (the_arity_of o)) by PRALG_2:3;
then reconsider g = F#x as Function;
A23: rng tao c= dom F by A4,PARTFUN1:def 2;
assume
A24: for n st n in dom f holds u.n = (F.((the_arity_of o)/.n)).(f.n);
A25: now
let e be object;
assume
A26: e in dom f;
then reconsider n = e as Nat by A14;
(the_arity_of o).n in the carrier of S by A14,A26,FINSEQ_2:11;
then tao.n in dom F by PARTFUN1:def 2; then
A27: n in dom(F*the_arity_of o) by A14,A26,FUNCT_1:11; then
n in dom(F*the_arity_of o) /\ dom f by A26,XBOOLE_0:def 4; then
a27: n in dom ((F*the_arity_of o)..f) by PRALG_1:def 19;
A28: (F*the_arity_of o).n = F.((the_arity_of o).n) by FUNCT_1:12,A27
.= (F.(tao/.n)) by A14,A26,PARTFUN1:def 6;
thus u.e = (F.((the_arity_of o)/.n)).(f.n) by A24,A26
.= ((F*tao)..f).n by a27,A28,PRALG_1:def 19
.= g.e by A1,A2,A13,A18,A6,PRALG_2:def 2;
end;
F#x = (F*tao)..f by A1,A2,A13,A18,A6,PRALG_2:def 2;
then dom g = dom (F*tao) /\ dom f by PRALG_1:def 19
.= dom tao /\ dom f by A23,RELAT_1:27;
hence u = F#x by A14,A15,A25,FUNCT_1:2;
end;
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
let o;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1);
redefine func F # x means :Def6: :: redefines # (MSUALG_3, definition)
for n st n in dom x holds it.n = (F.((the_arity_of o)/.n)).(x.n);
compatibility by Lm1;
end;
theorem Th7:
for S,o for U1 being MSAlgebra over S st Args(o,U1) <> {}
for x be Element of Args(o,U1) holds x = ((id (the Sorts of U1))#x)
proof
let S,o;
let U1 be MSAlgebra over S;
set F = id (the Sorts of U1);
assume
A1: Args(o,U1) <> {};
then reconsider AA = Args(o,U1) as non empty set;
let x be Element of Args(o,U1);
reconsider Fx = F#x as Element of AA;
A2: Args(o,U1) = product((the Sorts of U1) * (the_arity_of o)) by PRALG_2:3;
then consider g being Function such that
A3: Fx = g and
dom g = dom ((the Sorts of U1) * (the_arity_of o)) and
for x being object st x in dom ((the Sorts of U1)*the_arity_of o) holds g.x
in ((the Sorts of U1)*the_arity_of o).x by CARD_3:def 5;
consider f being Function such that
A4: x = f and
dom f = dom ((the Sorts of U1) * (the_arity_of o)) and
for x being object st x in dom ((the Sorts of U1)*the_arity_of o) holds f.x
in ((the Sorts of U1)*the_arity_of o).x by A1,A2,CARD_3:def 5;
A5: dom f = dom the_arity_of o by A4,A3,Th6;
A6: for y be object st y in dom f holds f.y = g.y
proof
let y be object;
assume
A7: y in dom f;
then reconsider n = y as Nat by A5;
set p = ((the_arity_of o)/.n);
dom (the Sorts of U1) = (the carrier of S) by PARTFUN1:def 2;
then rng (the_arity_of o) c= dom (the Sorts of U1) by FINSEQ_1:def 4;
then
A8: dom ((the Sorts of U1)*(the_arity_of o)) = dom the_arity_of o by
RELAT_1:27;
then f.n in ((the Sorts of U1) * (the_arity_of o)).n by A1,A4,A5,A7,Th6;
then f.n in (the Sorts of U1).((the_arity_of o).n) by A5,A7,A8,FUNCT_1:12;
then
A9: f.n in (the Sorts of U1).p by A5,A7,PARTFUN1:def 6;
A10: F.p = id ((the Sorts of U1).p) by Def1;
g.n = (F.((the_arity_of o)/.n)).(f.n) by A4,A3,A7,Lm1;
hence thesis by A10,A9,FUNCT_1:18;
end;
dom g = dom the_arity_of o by A3,Th6;
hence thesis by A4,A3,A6,Th6,FUNCT_1:2;
end;
theorem Th8:
for U1,U2,U3 being non-empty MSAlgebra over S
for H1 be ManySortedFunction of U1,U2,
H2 be ManySortedFunction of U2,U3,
x be Element of Args(o,U1) holds (H2**H1)#x = H2#(H1#x)
proof
let U1,U2,U3 be non-empty MSAlgebra over S;
let H1 be ManySortedFunction of U1,U2,H2 be ManySortedFunction of U2,U3;
let x be Element of Args(o,U1);
A1: dom x = dom the_arity_of o by Th6;
A2: dom (H1#x) = dom the_arity_of o by Th6;
A3: for y be object st y in dom (the_arity_of o)
holds ((H2**H1)#x).y = ((H2#(H1#x))).y
proof
rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
then rng the_arity_of o c= dom (the Sorts of U1) by PARTFUN1:def 2;
then
A4: dom ((the Sorts of U1)*(the_arity_of o)) = dom the_arity_of o by
RELAT_1:27;
let y be object;
assume
A5: y in dom the_arity_of o;
then reconsider n = y as Nat;
set F = H2**H1, p = (the_arity_of o)/.n;
A6: (F#x).n = (F.p).(x.n) by A1,A5,Def6;
p = (the_arity_of o).n by A5,PARTFUN1:def 6; then
A7: ((the Sorts of U1) * (the_arity_of o)).n =(the Sorts of U1).p
by A5,A4,FUNCT_1:12;
A8: F.p = (H2.p)*(H1.p) by Th2;
A9: dom (H1.p) = (the Sorts of U1).p by FUNCT_2:def 1;
then dom ((H2.p)*(H1.p)) = dom (H1.p) by FUNCT_2:def 1;
hence (F#x).y = (H2.p).((H1.p).(x.n)) by A5,A6,A4,A9,A7,A8,Th6,FUNCT_1:12
.= (H2.p).((H1#x).n) by A1,A5,Def6
.= (H2#(H1#x)).y by A2,A5,Def6;
end;
dom ((H2**H1)#x) = dom the_arity_of o & dom (H2#(H1#x)) = dom (
the_arity_of o) by Th6;
hence thesis by A3,FUNCT_1:2;
end;
definition
let S;
let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_homomorphism U1,U2 means
for o be OperSymbol of S st Args(o,U1) <> {}
for x be Element of Args(o,U1) holds
(F.(the_result_sort_of o)).(Den (o,U1).x) = Den(o,U2).(F#x);
end;
theorem Th9:
for U1 being MSAlgebra over S holds
id (the Sorts of U1) is_homomorphism U1,U1
proof
let U1 be MSAlgebra over S;
set F = id (the Sorts of U1);
let o be OperSymbol of S;
assume
A1: Args(o,U1) <> {};
let x be Element of Args(o,U1);
A2: F#x = x by A1,Th7;
set r = the_result_sort_of o;
A3: F.r = id ((the Sorts of U1).r) by Def1;
rng (the ResultSort of S) c= the carrier of S by RELAT_1:def 19;
then rng (the ResultSort of S) c= dom (the Sorts of U1) by PARTFUN1:def 2;
then
A4: Result(o,U1) = ((the Sorts of U1)*(the ResultSort of S)).o & dom ((the
Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort of S) by
MSUALG_1:def 5,RELAT_1:27;
o in the carrier' of S;
then o in dom (the ResultSort of S) by FUNCT_2:def 1;
then
A5: Result(o,U1) = (the Sorts of U1).((the ResultSort of S).o) by A4,FUNCT_1:12
.= (the Sorts of U1).r by MSUALG_1:def 2;
per cases;
suppose
Result(o,U1) <> {};
then dom Den(o,U1) = Args(o,U1) by FUNCT_2:def 1;
then rng Den(o,U1) c= Result(o,U1) & Den(o,U1).x in rng Den(o,U1) by A1,
FUNCT_1:def 3,RELAT_1:def 19;
hence thesis by A2,A3,A5,FUNCT_1:18;
end;
suppose
A6: Result(o,U1) = {};
then dom Den(o,U1) = {};
then
A7: Den(o,U1).x = {} by FUNCT_1:def 2;
dom (F.r) = {} by A5,A6;
then (F.r).{} = {} by FUNCT_1:def 2;
hence thesis by A1,A7,Th7;
end;
end;
theorem Th10:
for U1,U2,U3 being non-empty MSAlgebra over S for H1 be
ManySortedFunction of U1,U2, H2 be ManySortedFunction of U2,U3 st H1
is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism
U1,U3
proof
let U1,U2,U3 be non-empty MSAlgebra over S;
let H1 be ManySortedFunction of U1,U2,H2 be ManySortedFunction of U2,U3;
assume that
A1: H1 is_homomorphism U1,U2 and
A2: H2 is_homomorphism U2,U3;
let o be OperSymbol of S such that
Args(o,U1) <> {};
let x be Element of Args(o,U1);
set F = H2**H1, r = the_result_sort_of o;
(H1.r).(Den(o,U1).x) = Den(o,U2).(H1#x) by A1;
then
A3: (H2.r).((H1.r).(Den(o,U1).x)) = Den(o,U3).(H2#(H1#x)) by A2;
A4: F.r = (H2.r)*(H1.r) & dom (F.r) = (the Sorts of U1).r by Th2,FUNCT_2:def 1;
rng (the ResultSort of S) c= the carrier of S by RELAT_1:def 19;
then rng (the ResultSort of S) c= dom (the Sorts of U1) by PARTFUN1:def 2;
then
A5: Result(o,U1) = ((the Sorts of U1)*(the ResultSort of S)).o & dom ((the
Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort of S) by
MSUALG_1:def 5,RELAT_1:27;
o in the carrier' of S;
then o in dom (the ResultSort of S) by FUNCT_2:def 1;
then Result(o,U1) = (the Sorts of U1).((the ResultSort of S).o) by A5,
FUNCT_1:12
.= (the Sorts of U1).r by MSUALG_1:def 2;
then (F.r).(Den(o,U1).x) = Den(o,U3).(H2#(H1#x)) by A3,A4,FUNCT_1:12;
hence (F.r).(Den(o,U1).x) = Den(o,U3).(F#x) by Th8;
end;
definition
let S;
let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_epimorphism U1,U2 means
F is_homomorphism U1,U2 & F is "onto";
end;
theorem Th11:
for U1,U2,U3 being non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st
F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G**F is_epimorphism U1,U3
proof
let U1,U2,U3 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3;
assume that
A1: F is_epimorphism U1,U2 and
A2: G is_epimorphism U2,U3;
A3: G is "onto" by A2;
A4: F is "onto" by A1;
for i be set st i in (the carrier of S) holds rng((G**F).i) = (the Sorts
of U3).i
proof
let i be set;
assume
A5: i in the carrier of S;
then reconsider
f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by PBOOLE:def 15;
reconsider g = G.i as Function of (the Sorts of U2).i,(the Sorts of U3).i
by A5,PBOOLE:def 15;
rng f = (the Sorts of U2).i by A4,A5;
then
A6: dom g = rng f by A5,FUNCT_2:def 1;
rng g = (the Sorts of U3).i by A3,A5;
then rng (g*f) = (the Sorts of U3).i by A6,RELAT_1:28;
hence thesis by A5,Th2;
end;
then
A7: G**F is "onto";
F is_homomorphism U1,U2 & G is_homomorphism U2,U3 by A1,A2;
then G**F is_homomorphism U1,U3 by Th10;
hence thesis by A7;
end;
definition
let S;
let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_monomorphism U1,U2 means
F is_homomorphism U1,U2 & F is "1-1";
end;
theorem Th12:
for U1,U2,U3 being non-empty MSAlgebra over S for F be
ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st F
is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G**F is_monomorphism U1,
U3
proof
let U1,U2,U3 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3;
assume that
A1: F is_monomorphism U1,U2 and
A2: G is_monomorphism U2,U3;
A3: G is "1-1" by A2;
A4: F is "1-1" by A1;
for i be set, h be Function st i in dom (G**F) & (G**F).i = h holds h is
one-to-one
proof
let i be set,h be Function;
assume that
A5: i in dom (G**F) and
A6: (G**F).i = h;
A7: i in the carrier of S by A5,PARTFUN1:def 2;
then reconsider
g = G.i as Function of (the Sorts of U2).i,(the Sorts of U3).i
by PBOOLE:def 15;
reconsider f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by A7,PBOOLE:def 15;
i in dom G by A7,PARTFUN1:def 2;
then
A8: g is one-to-one by A3;
i in dom F by A7,PARTFUN1:def 2;
then f is one-to-one by A4;
then g*f is one-to-one by A8;
hence thesis by A6,A7,Th2;
end;
then
A9: G**F is "1-1";
F is_homomorphism U1,U2 & G is_homomorphism U2,U3 by A1,A2;
then G**F is_homomorphism U1,U3 by Th10;
hence thesis by A9;
end;
definition
let S;
let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_isomorphism U1,U2 means
F is_epimorphism U1,U2 & F is_monomorphism U1,U2;
end;
theorem Th13:
for F be ManySortedFunction of U1,U2 holds F is_isomorphism U1,
U2 iff F is_homomorphism U1,U2 & F is "onto" & F is "1-1"
proof
let F be ManySortedFunction of U1,U2;
thus F is_isomorphism U1,U2 implies F is_homomorphism U1,U2 & F is "onto" &
F is "1-1"
proof
assume F is_isomorphism U1,U2;
then F is_epimorphism U1,U2 & F is_monomorphism U1,U2;
hence thesis;
end;
assume F is_homomorphism U1,U2 & F is "onto" & F is "1-1";
then F is_epimorphism U1,U2 & F is_monomorphism U1,U2;
hence thesis;
end;
Lm2: for U1,U2 being non-empty MSAlgebra over S for H be ManySortedFunction of
U1,U2 st H is_isomorphism U1,U2 holds H"" is_homomorphism U2,U1
proof
let U1,U2 be non-empty MSAlgebra over S;
let H be ManySortedFunction of U1,U2;
set F = H"";
assume
A1: H is_isomorphism U1,U2;
then
A2: H is "onto" by Th13;
A3: H is "1-1" by A1,Th13;
A4: H is_homomorphism U1,U2 by A1,Th13;
for o be OperSymbol of S st Args(o,U2) <> {} for x be Element of Args(o,
U2) holds (F.(the_result_sort_of o)).(Den(o,U2).x) = Den(o,U1).(F#x)
proof
let o be OperSymbol of S such that
Args(o,U2) <> {};
let x be Element of Args(o,U2);
set r = the_result_sort_of o;
deffunc G(object)=(F#x).$1;
consider f being Function such that
A5: dom f = dom the_arity_of o & for n be object st n in dom (
the_arity_of o) holds f.n = G(n) from FUNCT_1:sch 3;
A6: dom (F#x) = dom the_arity_of o by Th6; then
A7: f = (F#x) by A5,FUNCT_1:2;
r in the carrier of S;
then r in dom H by PARTFUN1:def 2;
then
A8: H.r is one-to-one by A3;
dom (H.r) = (the Sorts of U1).r & F.r = (H.r)" by A2,A3,Def4,FUNCT_2:def 1;
then
A9: (F.r)*(H.r) = id ((the Sorts of U1).r) by A8,FUNCT_1:39;
A10: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
then
A11: dom ((the Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort
of S) by PARTFUN1:def 2;
A12: Result(o,U1) = ((the Sorts of U1)*(the ResultSort of S)).o by
MSUALG_1:def 5
.= (the Sorts of U1).((the ResultSort of S).o) by A10,A11,FUNCT_1:12
.= (the Sorts of U1).r by MSUALG_1:def 2;
reconsider f as Element of Args(o,U1) by A5,A6,FUNCT_1:2;
A13: dom ((F.r)*(H.r)) = (the Sorts of U1).r by FUNCT_2:def 1;
(H.r).(Den(o,U1).f) = Den(o,U2).(H#(F#x)) by A4,A7
.= Den(o,U2).((H**F)#x) by Th8
.= Den(o,U2).((id (the Sorts of U2))#x) by A2,A3,Th5
.= Den(o,U2).x by Th7;
then
(F.r).(Den(o,U2).x) = ((F.r)*(H.r)).(Den(o,U1).(F#x)) by A7,A13,A12,
FUNCT_1:12
.= Den(o,U1).(F#x) by A12,A9;
hence thesis;
end;
hence thesis;
end;
theorem Th14:
for U1,U2 being non-empty MSAlgebra over S for H be
ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U1 st H
is_isomorphism U1,U2 & H1 = H"" holds H1 is_isomorphism U2,U1
proof
let U1,U2 be non-empty MSAlgebra over S;
let H be ManySortedFunction of U1,U2,H1 be ManySortedFunction of U2,U1;
assume that
A1: H is_isomorphism U1,U2 and
A2: H1 = H"";
A3: H1 is_homomorphism U2,U1 by A1,A2,Lm2;
H is_monomorphism U1,U2 by A1;
then
A4: H is "1-1";
H is_epimorphism U1,U2 by A1;
then
A5: H is "onto";
for i be set, g be Function st i in dom H1 & g = H1.i holds g is one-to-one
proof
let i be set;
let g be Function;
assume that
A6: i in dom H1 and
A7: g = H1.i;
A8: i in the carrier of S by A6,PARTFUN1:def 2;
then reconsider
f = H.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by PBOOLE:def 15;
i in dom H by A8,PARTFUN1:def 2;
then f is one-to-one by A4;
then f" is one-to-one;
hence thesis by A2,A4,A5,A7,A8,Def4;
end;
then H1 is "1-1";
then
A9: H1 is_monomorphism U2,U1 by A3;
for i be set st i in (the carrier of S) holds rng(H1.i) = (the Sorts of U1).i
proof
let i be set;
assume
A10: i in (the carrier of S);
then reconsider
f = H.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by PBOOLE:def 15;
i in dom H by A10,PARTFUN1:def 2;
then f is one-to-one by A4;
then rng (f") = dom f by FUNCT_1:33;
then rng (f") = (the Sorts of U1).i by A10,FUNCT_2:def 1;
hence thesis by A2,A4,A5,A10,Def4;
end;
then H1 is "onto";
then H1 is_epimorphism U2,U1 by A3;
hence thesis by A9;
end;
theorem Th15:
for U1,U2,U3 being non-empty MSAlgebra over S for H be
ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U3 st H
is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,
U3
by Th11,Th12;
definition
let S;
let U1,U2 be MSAlgebra over S;
pred U1,U2 are_isomorphic means
ex F be ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;
end;
theorem Th16:
for U1 being MSAlgebra over S holds id the Sorts of U1
is_isomorphism U1,U1 & U1,U1 are_isomorphic
proof
let U1 be MSAlgebra over S;
A1: id (the Sorts of U1) is_homomorphism U1,U1 by Th9;
for i be set,f be Function st i in dom id (the Sorts of U1) & (id (the
Sorts of U1)).i = f holds f is one-to-one
proof
let i be set,f be Function;
assume that
A2: i in dom id (the Sorts of U1) and
A3: (id (the Sorts of U1)).i = f;
i in the carrier of S by A2,PARTFUN1:def 2;
then f = id ((the Sorts of U1).i) by A3,Def1;
hence thesis;
end;
then id (the Sorts of U1) is "1-1";
then
A4: id (the Sorts of U1) is_monomorphism U1,U1 by A1;
for i be set st i in (the carrier of S) holds rng((id (the Sorts of U1))
.i) = (the Sorts of U1).i
proof
let i be set;
assume i in (the carrier of S);
then (id (the Sorts of U1)).i = id ((the Sorts of U1).i) by Def1;
hence thesis;
end;
then id (the Sorts of U1) is "onto";
then
A5: id (the Sorts of U1) is_epimorphism U1,U1 by A1;
hence id (the Sorts of U1) is_isomorphism U1,U1 by A4;
take id (the Sorts of U1);
thus thesis by A4,A5;
end;
definition
let S;
let U1, U2 be MSAlgebra over S;
redefine pred U1, U2 are_isomorphic; :: redefines are_isomorphic (MSUALG_3, definition)
reflexivity by Th16;
end;
theorem
for U1,U2 being non-empty MSAlgebra over S holds U1,U2 are_isomorphic
implies U2,U1 are_isomorphic
proof
let U1,U2 be non-empty MSAlgebra over S;
assume U1,U2 are_isomorphic;
then consider F be ManySortedFunction of U1,U2 such that
A1: F is_isomorphism U1,U2;
reconsider G = F"" as ManySortedFunction of U2,U1;
G is_isomorphism U2,U1 by A1,Th14;
hence thesis;
end;
theorem
for U1,U2,U3 being non-empty MSAlgebra over S holds U1,U2
are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic
proof
let U1,U2,U3 be non-empty MSAlgebra over S;
assume that
A1: U1,U2 are_isomorphic and
A2: U2,U3 are_isomorphic;
consider F be ManySortedFunction of U1,U2 such that
A3: F is_isomorphism U1,U2 by A1;
consider G be ManySortedFunction of U2,U3 such that
A4: G is_isomorphism U2,U3 by A2;
reconsider H = G**F as ManySortedFunction of U1,U3;
H is_isomorphism U1,U3 by A3,A4,Th15;
hence thesis;
end;
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume
A1: F is_homomorphism U1,U2;
func Image F -> strict non-empty MSSubAlgebra of U2 means
:Def12:
the Sorts of it = F.:.:(the Sorts of U1);
existence
proof
set u2 = F.:.:(the Sorts of U1);
A2: now
let i be object;
reconsider f = F.i as Function;
assume
A3: i in the carrier of S;
then
A4: u2.i = f.:((the Sorts of U1).i) by PBOOLE:def 20;
reconsider f as Function of (the Sorts of U1).i,(the Sorts of U2).i by A3
,PBOOLE:def 15;
dom f = (the Sorts of U1).i by A3,FUNCT_2:def 1;
hence u2.i is non empty by A3,A4;
end;
now
let i be object;
reconsider f = F.i as Function;
assume
A5: i in the carrier of S;
then
A6: u2.i = f.:((the Sorts of U1).i) by PBOOLE:def 20;
reconsider f as Function of (the Sorts of U1).i,(the Sorts of U2).i by A5
,PBOOLE:def 15;
A7: rng f c= (the Sorts of U2).i by RELAT_1:def 19;
dom f = (the Sorts of U1).i by A5,FUNCT_2:def 1;
hence u2.i c= (the Sorts of U2).i by A6,A7,RELAT_1:113;
end;
then u2 c= the Sorts of U2 by PBOOLE:def 2;
then reconsider u2 as non-empty MSSubset of U2 by A2,PBOOLE:def 13,def 18;
set M = GenMSAlg(u2);
reconsider M9 = MSAlgebra (# u2, Opers(U2,u2) qua ManySortedFunction of u2
# * the Arity of S, u2 * the ResultSort of S #) as non-empty MSAlgebra over S
by MSUALG_1:def 3;
take M;
u2 is opers_closed
proof
let o be OperSymbol of S;
thus rng ((Den(o,U2))|((u2# * the Arity of S).o)) c= (u2 * the
ResultSort of S).o
proof
let x be object;
set D = Den(o,U2), X = (u2# * the Arity of S).o, ao = the_arity_of o,
ro = the_result_sort_of o, ut = u2 * ao, S1 = the Sorts of U1;
A8: rng ao c= the carrier of S by FINSEQ_1:def 4;
A9: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
then dom (u2# * (the Arity of S)) = dom (the Arity of S) by
PARTFUN1:def 2;
then
A10: X = u2#.((the Arity of S).o) by A9,FUNCT_1:12
.= u2#.(ao) by MSUALG_1:def 1
.= product(u2 * ao) by FINSEQ_2:def 5;
assume x in rng (D|X);
then consider a be object such that
A11: a in dom(D|X) and
A12: x = (D|X).a by FUNCT_1:def 3;
A13: x = D.a by A11,A12,FUNCT_1:47;
dom (D|X) c= dom D by RELAT_1:60;
then reconsider a as Element of Args(o,U2) by A11,FUNCT_2:def 1;
defpred P[object,object] means
for s be SortSymbol of S st s = ao.$1 holds
$2 in S1.s & (a).$1=(F.s).$2;
A14: dom (D|X) c= X by RELAT_1:58;
then
A15: dom a = dom ut by A11,A10,CARD_3:9;
A16: dom u2 = the carrier of S by PARTFUN1:def 2;
A17: for y be object st y in dom (a) ex i be object st P[y,i]
proof
let y be object;
assume
A18: y in dom (a);
then
A19: a.y in ut.y by A11,A14,A10,A15,CARD_3:9;
dom (u2 * ao) = dom ao by A16,A8,RELAT_1:27;
then ao.y in rng ao by A15,A18,FUNCT_1:def 3;
then reconsider s = ao.y as SortSymbol of S by A8;
A20: dom (F.s) = S1.s by FUNCT_2:def 1;
ut.y = u2.(ao.y) by A15,A18,FUNCT_1:12
.= (F.s).:(S1.s) by PBOOLE:def 20
.= rng (F.s) by A20,RELAT_1:113;
then consider i be object such that
A21: i in S1.s & (a).y = (F.s).i by A20,A19,FUNCT_1:def 3;
take i;
thus thesis by A21;
end;
consider f be Function such that
A22: dom f = dom a & for y be object st y in dom a holds P[y,f.y]
from CLASSES1:sch 1(A17);
dom S1 = the carrier of S by PARTFUN1:def 2;
then
A23: dom (S1 * ao) = dom ao by A8,RELAT_1:27;
A24: dom f = dom ao by A15,A16,A8,A22,RELAT_1:27;
A25: for y be object st y in dom(S1 * ao) holds f.y in (S1 * ao).y
proof
let y be object;
assume
A26: y in dom (S1 * ao);
then ao.y in rng ao by A23,FUNCT_1:def 3;
then reconsider s = ao.y as SortSymbol of S by A8;
f.y in S1.s by A22,A24,A23,A26;
hence thesis by A26,FUNCT_1:12;
end;
Args(o,U1) = product (S1 * ao) by PRALG_2:3;
then reconsider a1 = f as Element of Args(o,U1) by A24,A23,A25,CARD_3:9
;
A27: dom a1 = dom ao by Th6;
A28: now
let y be object;
assume
A29: y in dom ao;
then reconsider n = y as Nat;
ao.y in rng ao by A29,FUNCT_1:def 3;
then reconsider s = ao.y as SortSymbol of S by A8;
(F#a1).n = (F.(ao/.n)).(a1.n) by A27,A29,Def6
.= (F.s).(a1.n) by A29,PARTFUN1:def 6;
hence (F#a1).y = a.y by A22,A27,A29;
end;
dom (F#a1) = dom ao & dom a = dom ao by Th6;
then F#a1 = a by A28,FUNCT_1:2;
then
A30: (F.ro).(Den(o,U1).a1) = x by A1,A13;
reconsider g = F.ro as Function;
A31: dom (F.ro) = S1.ro by FUNCT_2:def 1;
A32: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
then
A33: dom (S1 * (the ResultSort of S)) = dom (the ResultSort of S) by
PARTFUN1:def 2;
Result(o,U1) = (S1 * (the ResultSort of S)).o by MSUALG_1:def 5
.= S1.((the ResultSort of S).o) by A32,A33,FUNCT_1:12
.= S1.ro by MSUALG_1:def 2;
then Den(o,U1).a1 in S1.ro;
then
A34: Den(o,U1).a1 in dom (F.ro) by FUNCT_2:def 1;
dom (u2 * the ResultSort of S) = dom (the ResultSort of S) by A32,
PARTFUN1:def 2;
then (u2 * the ResultSort of S).o = u2.((the ResultSort of S).o) by A32
,FUNCT_1:12
.= u2.ro by MSUALG_1:def 2
.= g.:(S1.ro) by PBOOLE:def 20
.= rng g by A31,RELAT_1:113;
hence thesis by A30,A34,FUNCT_1:def 3;
end;
end;
then for B be MSSubset of U2 st B = the Sorts of M9 holds B is
opers_closed & the Charact of M9 = Opers(U2,B);
then
A35: M9 is MSSubAlgebra of U2 by MSUALG_2:def 9;
u2 is MSSubset of M9 by PBOOLE:def 18;
then M is MSSubAlgebra of M9 by A35,MSUALG_2:def 17;
then the Sorts of M is MSSubset of M9 by MSUALG_2:def 9;
then
A36: the Sorts of M c= u2 by PBOOLE:def 18;
u2 is MSSubset of M by MSUALG_2:def 17;
then u2 c= the Sorts of M by PBOOLE:def 18;
hence thesis by A36,PBOOLE:146;
end;
uniqueness by MSUALG_2:9;
end;
theorem
for U1 being non-empty MSAlgebra over S, U2 being non-empty
MSAlgebra over S, F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2
holds F is_epimorphism U1,U2 iff Image F = the MSAlgebra of U2
proof
let U1 be non-empty MSAlgebra over S;
let U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1,
U2;
set FF = F.:.:(the Sorts of U1);
assume
A1: F is_homomorphism U1,U2;
thus F is_epimorphism U1,U2 implies Image F = the MSAlgebra of U2
proof
assume F is_epimorphism U1,U2;
then
A2: F is "onto";
now
let i be object;
assume
A3: i in the carrier of S;
then reconsider
f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).
i by PBOOLE:def 15;
A4: rng f = (the Sorts of U2).i by A2,A3;
reconsider f as Function;
FF.i = f.:((the Sorts of U1).i) & dom f = (the Sorts of U1).i by A3,
FUNCT_2:def 1,PBOOLE:def 20;
hence FF.i = (the Sorts of U2).i by A4,RELAT_1:113;
end;
then
A5: FF = the Sorts of U2 by PBOOLE:3;
the MSAlgebra of U2 is strict MSSubAlgebra of U2 by MSUALG_2:5;
hence thesis by A1,A5,Def12;
end;
assume Image F = the MSAlgebra of U2;
then
A6: FF = the Sorts of U2 by A1,Def12;
for i be set st i in the carrier of S holds rng(F.i) = (the Sorts of U2 ) . i
proof
let i be set;
assume i in the carrier of S;
then reconsider i as Element of S;
reconsider f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).i;
f.:((the Sorts of U1).i) = (the Sorts of U2).i & dom f = (the Sorts
of U1).i by A6,FUNCT_2:def 1,PBOOLE:def 20;
hence thesis by RELAT_1:113;
end;
then F is "onto";
hence thesis by A1;
end;
Lm3: for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction of
U1,U2 st F is_homomorphism U1,U2 holds F is ManySortedFunction of U1,Image F
proof
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume
A1: F is_homomorphism U1,U2;
for i be object st i in the carrier of S holds F.i is Function of (the
Sorts of U1).i,(the Sorts of Image F).i
proof
let i be object;
assume
A2: i in the carrier of S;
then reconsider
f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by PBOOLE:def 15;
A3: dom f = (the Sorts of U1).i by A2,FUNCT_2:def 1;
the Sorts of Image F = F.:.:(the Sorts of U1) by A1,Def12;
then (the Sorts of Image F).i = f.:((the Sorts of U1).i) by A2,
PBOOLE:def 20
.= rng f by A3,RELAT_1:113;
hence thesis by A3,FUNCT_2:1;
end;
hence thesis by PBOOLE:def 15;
end;
theorem Th20:
for U1,U2 being non-empty MSAlgebra over S for F be
ManySortedFunction of U1,U2, G be ManySortedFunction of U1,Image F st F = G & F
is_homomorphism U1,U2 holds G is_epimorphism U1,Image F
proof
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2, G be ManySortedFunction of U1,Image F;
assume that
A1: F = G and
A2: F is_homomorphism U1,U2;
for o be OperSymbol of S st Args(o,U1) <> {} for x be Element of Args(o,
U1) holds (G.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,Image F).(G#x)
proof
set IF = Image F;
reconsider SIF = the Sorts of IF as non-empty MSSubset of U2 by
MSUALG_2:def 9;
reconsider G1 = G as ManySortedFunction of U1,U2 by A1;
let o be OperSymbol of S such that
Args(o,U1) <> {};
let x be Element of Args(o,U1);
set SIFo = SIF * (the_arity_of o), Uo = (the Sorts of U2) * (the_arity_of
o), ao = the_arity_of o;
A3: dom Den(o,U2) = Args(o,U2) by FUNCT_2:def 1;
A4: rng ao c= the carrier of S by FINSEQ_1:def 4;
then rng ao c= dom SIF by PARTFUN1:def 2;
then
A5: dom SIFo = dom ao by RELAT_1:27;
rng ao c= dom (the Sorts of U2) by A4,PARTFUN1:def 2;
then
A6: dom SIFo = dom Uo by A5,RELAT_1:27;
A7: for x be object st x in dom SIFo holds SIFo.x c= Uo.x
proof
let x be object;
assume
A8: x in dom SIFo;
then ao.x in rng ao by A5,FUNCT_1:def 3;
then reconsider k = ao.x as Element of S by A4;
set f = F.k;
A9: dom f = (the Sorts of U1).k by FUNCT_2:def 1;
A10: rng f c= (the Sorts of U2).k by RELAT_1:def 19;
SIF = F.:.:(the Sorts of U1) by A2,Def12;
then SIFo.x = (F.:.:(the Sorts of U1)).k by A8,FUNCT_1:12
.= f.:((the Sorts of U1).k) by PBOOLE:def 20
.= rng f by A9,RELAT_1:113;
hence thesis by A6,A8,A10,FUNCT_1:12;
end;
A11: dom x = dom the_arity_of o by Th6;
A12: now
let a be object;
assume
A13: a in dom the_arity_of o;
then reconsider n = a as Nat;
(G#x).n = (G.((the_arity_of o)/.n)).(x.n) by A11,A13,Def6;
hence (G#x).a = (G1#x).a by A11,A13,Def6;
end;
dom (G#x) = dom the_arity_of o & dom (G1#x) = dom the_arity_of o
by Th6;
then G#x = G1#x by A12,FUNCT_1:2;
then
A14: (G.(the_result_sort_of o)).(Den(o,U1).x)= Den(o,U2).(G#x) by A1,A2;
SIF is opers_closed by MSUALG_2:def 9;
then
A15: SIF is_closed_on o;
Args(o,IF) = product(SIFo) & Args(o,U2) = product(Uo) by PRALG_2:3;
then Args(o,IF) c= Args(o,U2) by A6,A7,CARD_3:27;
then G#x in dom Den(o,U2) by A3;
then
A16: (SIF# * the Arity of S).o = Args(o,IF) & G#x in (dom Den(o,U2)) /\
Args(o,IF ) by MSUALG_1:def 4,XBOOLE_0:def 4;
the Charact of IF = Opers(U2,SIF) by MSUALG_2:def 9;
then Den(o,IF) = (Opers(U2,SIF)).o by MSUALG_1:def 6
.= o/.(SIF) by MSUALG_2:def 8
.= (Den(o,U2))|((SIF# * the Arity of S).o) by A15,MSUALG_2:def 7;
hence thesis by A14,A16,FUNCT_1:48;
end;
then
A17: G is_homomorphism U1,Image F;
for i be set st i in the carrier of S holds rng(G.i) = (the Sorts of
Image F).i
proof
let i be set;
assume i in the carrier of S;
then reconsider i as Element of S;
set g = G.i;
the Sorts of (Image F) = G.:.:(the Sorts of U1) by A1,A2,Def12;
then
A18: (the Sorts of Image F).i = g.:((the Sorts of U1).i) by PBOOLE:def 20;
dom g = (the Sorts of U1).i by FUNCT_2:def 1;
hence thesis by A18,RELAT_1:113;
end;
then G is "onto";
hence thesis by A17;
end;
theorem
for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction
of U1,U2 st F is_homomorphism U1,U2 ex G be ManySortedFunction of U1,Image F st
F = G & G is_epimorphism U1,Image F
proof
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume
A1: F is_homomorphism U1,U2;
then reconsider G = F as ManySortedFunction of U1,Image F by Lm3;
take G;
thus thesis by A1,Th20;
end;
Lm4: for U1,U2 being non-empty MSAlgebra over S for U3 be non-empty
MSSubAlgebra of U2, F be ManySortedFunction of U1,U2, G be ManySortedFunction
of U1,U3 st F = G & G is_homomorphism U1,U3 holds F is_homomorphism U1,U2
proof
let U1,U2 be non-empty MSAlgebra over S;
let U3 be non-empty MSSubAlgebra of U2, F be ManySortedFunction of U1,U2, G
be ManySortedFunction of U1,U3;
assume that
A1: F = G and
A2: G is_homomorphism U1,U3;
for o be OperSymbol of S st Args(o,U1) <> {} for x be Element of Args(o,
U1) holds (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U2).(F#x)
proof
reconsider S3 = the Sorts of U3 as non-empty MSSubset of U2 by
MSUALG_2:def 9;
let o be OperSymbol of S such that
Args(o,U1) <> {};
let x be Element of Args(o,U1);
for i be object st i in the carrier of S holds G.i is Function of (the
Sorts of U1).i, (the Sorts of U2).i
proof
reconsider S3 = the Sorts of U3 as non-empty MSSubset of U2 by
MSUALG_2:def 9;
let i be object;
assume
A3: i in the carrier of S;
then reconsider
g = G.i as Function of (the Sorts of U1).i,(the Sorts of U3).
i by PBOOLE:def 15;
the Sorts of U3 is MSSubset of U2 by MSUALG_2:def 9;
then the Sorts of U3 c= the Sorts of U2 by PBOOLE:def 18;
then S3.i c= (the Sorts of U2).i by A3,PBOOLE:def 2;
then g is Function of (the Sorts of U1).i,(the Sorts of U2).i by A3,
FUNCT_2:7;
hence thesis;
end;
then reconsider G1 = G as ManySortedFunction of U1,U2 by PBOOLE:def 15;
S3 is opers_closed by MSUALG_2:def 9;
then
A4: S3 is_closed_on o;
the Charact of U3 = Opers(U2,S3) by MSUALG_2:def 9;
then
A5: Den(o,U3) = (Opers(U2,S3)).o by MSUALG_1:def 6
.= o/.(S3) by MSUALG_2:def 8
.= (Den(o,U2))|((S3# * the Arity of S).o) by A4,MSUALG_2:def 7;
A6: dom x = dom the_arity_of o by Th6;
A7: now
let a be object;
assume
A8: a in dom the_arity_of o;
then reconsider n = a as Nat;
(G#x).n = (G.((the_arity_of o)/.n)).(x.n) by A6,A8,Def6;
hence (G#x).a = (G1#x).a by A6,A8,Def6;
end;
dom (G#x) = dom the_arity_of o & dom (G1#x) = dom the_arity_of o
by Th6;
then
A9: G#x = G1#x by A7,FUNCT_1:2;
dom Den(o,U2) = Args(o,U2) by FUNCT_2:def 1;
then
A10: (S3# * the Arity of S).o = Args(o,U3) & F#x in (dom Den(o,U2)) /\
Args(o,U3) by A1,A9,MSUALG_1:def 4,XBOOLE_0:def 4;
(F.(the_result_sort_of o)).(Den(o,U1).x)= Den(o,U3).(F#x) by A1,A2,A9;
hence thesis by A5,A10,FUNCT_1:48;
end;
hence thesis;
end;
theorem Th22:
for U1 being non-empty MSAlgebra over S for U2 be non-empty
MSSubAlgebra of U1, G be ManySortedFunction of U2,U1 st G = id (the Sorts of U2
) holds G is_monomorphism U2,U1
proof
let U1 be non-empty MSAlgebra over S;
let U2 be non-empty MSSubAlgebra of U1, G be ManySortedFunction of U2,U1;
set F = id (the Sorts of U2);
assume
A1: G =id (the Sorts of U2);
for i be set st i in the carrier of S holds G.i is one-to-one
proof
let i be set;
assume
A2: i in the carrier of S;
then reconsider
f = F.i as Function of (the Sorts of U2).i,(the Sorts of U2 ).i
by PBOOLE:def 15;
f = id ((the Sorts of U2).i) by A2,Def1;
hence thesis by A1;
end;
then
A3: G is "1-1" by Th1;
G is_homomorphism U2,U1 by A1,Lm4,Th9;
hence thesis by A3;
end;
theorem
for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction
of U1,U2 st F is_homomorphism U1,U2 ex F1 be ManySortedFunction of U1,Image F,
F2 be ManySortedFunction of Image F,U2 st F1 is_epimorphism U1,Image F & F2
is_monomorphism Image F,U2 & F = F2**F1
proof
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume
A1: F is_homomorphism U1,U2;
then reconsider F1 = F as ManySortedFunction of U1,Image F by Lm3;
for H be ManySortedFunction of Image F,Image F holds H is
ManySortedFunction of Image F,U2
proof
let H be ManySortedFunction of Image F,Image F;
for i be object st i in the carrier of S holds H.i is Function of (the
Sorts of Image F).i,(the Sorts of U2).i
proof
let i be object;
assume
A2: i in the carrier of S;
then reconsider
f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).
i by PBOOLE:def 15;
A3: dom f = (the Sorts of U1).i by A2,FUNCT_2:def 1;
reconsider h = H.i as Function of (the Sorts of Image F).i,(the Sorts of
Image F).i by A2,PBOOLE:def 15;
A4: rng f c= (the Sorts of U2).i by RELAT_1:def 19;
the Sorts of Image F = F.:.:(the Sorts of U1) by A1,Def12;
then (the Sorts of Image F).i = f.:((the Sorts of U1).i) by A2,
PBOOLE:def 20
.= rng f by A3,RELAT_1:113;
then
h is Function of (the Sorts of Image F).i,(the Sorts of U2).i by A4,
FUNCT_2:7;
hence thesis;
end;
hence thesis by PBOOLE:def 15;
end;
then reconsider
F2 = id (the Sorts of Image F) as ManySortedFunction of Image F,
U2;
take F1,F2;
thus F1 is_epimorphism U1,Image F by A1,Th20;
thus F2 is_monomorphism Image F,U2 by Th22;
thus thesis by Th4;
end;
theorem
for S for U1,U2 being MSAlgebra over S for o for F being
ManySortedFunction of U1,U2 for x being Element of Args(o,U1), f,u being
Function st x = f & x in Args(o,U1) & u in Args(o,U2) holds u = F#x iff for n
st n in dom f holds u.n = (F.((the_arity_of o)/.n)).(f.n) by Lm1;