:: On the Trivial Many Sorted Algebras and Many Sorted Congruences
:: by Artur Korni\l owicz
::
:: Received June 11, 1996
:: Copyright (c) 1996-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 XBOOLE_0, STRUCT_0, MSUALG_1, PBOOLE, FINSET_1, SUBSET_1,
CLOSURE2, TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, MARGREL1, NAT_1, PRALG_2,
CARD_3, RLVECT_2, MSAFREE, PRELAMB, ZFMISC_1, PRALG_1, MCART_1, EQREL_1,
FUNCOP_1, MSUALG_3, TREES_4, LANG1, NUMBERS, MSUALG_2, MEMBER_1, GROUP_6,
WELLORD1, PARTFUN1, FUNCT_6, FINSEQ_4, PZFMISC1, CARD_1, MSUALG_4,
MSUALG_5, SETFAM_1, FUNCT_4, RELAT_2, MSUALG_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
RELAT_2, STRUCT_0, SETFAM_1, FUNCT_1, PBOOLE, EQREL_1, RELSET_1,
PARTFUN1, FUNCT_2, FINSEQ_1, LANG1, XTUPLE_0, MCART_1, FINSET_1, CARD_3,
NAT_1, TREES_4, FUNCT_6, DTCONSTR, MSUALG_1, MSUALG_2, PRALG_1, MSUALG_3,
MSAFREE, PRALG_2, FUNCOP_1, MSAFREE2, MSUALG_4, PZFMISC1, MSSUBFAM,
CLOSURE2, MSUALG_5;
constructors BINOP_1, PZFMISC1, MSUALG_3, MSUALG_5, CLOSURE1, CLOSURE2,
PRALG_3, RELSET_1, CIRCUIT1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FINSET_1,
EQREL_1, PRE_CIRC, PZFMISC1, MSSUBFAM, STRUCT_0, FUNCT_1, MSUALG_1,
MSUALG_2, PRALG_2, MSUALG_3, MSAFREE, MSUALG_4, MSUALG_5, CLOSURE2,
CARD_3, RELSET_1, PRALG_1, PBOOLE, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions FINSEQ_1, FUNCT_1, FINSET_1, MSUALG_1, MSUALG_3, PBOOLE, TARSKI,
XBOOLE_0;
equalities MSUALG_1, MSUALG_4;
expansions FUNCT_1, MSAFREE2, MSUALG_1, MSUALG_3, PZFMISC1, MSUALG_4, PBOOLE;
theorems CARD_3, CLOSURE1, CLOSURE2, EXTENS_1, EQREL_1, FINSEQ_1, FUNCOP_1,
FUNCT_1, FUNCT_2, MCART_1, MSAFREE, MSAFREE2, MSSUBFAM, MSUALG_2,
MSUALG_3, MSUALG_4, MSUALG_5, MSUALG_6, MSUALG_7, PARTFUN1, PBOOLE,
PRALG_1, PRALG_2, PZFMISC1, RELAT_2, SETFAM_1, TARSKI, RELSET_1,
XBOOLE_0, XBOOLE_1, ORDERS_1, RELAT_1, ZFMISC_1;
schemes MSSUBFAM, PBOOLE, MSUALG_8;
begin :: Preliminaries
reserve a, I for set,
S for non empty non void ManySortedSign;
registration
let I be set, M be ManySortedSet of I;
cluster finite-yielding for Element of Bool M;
existence
proof
EmptyMS I c= M by PBOOLE:43;
then EmptyMS I is ManySortedSubset of M by PBOOLE:def 18;
then reconsider A = EmptyMS I as Element of Bool M by CLOSURE2:def 1;
take A;
thus thesis;
end;
end;
registration
let I be set, M be non-empty ManySortedSet of I;
cluster non-empty finite-yielding for ManySortedSubset of M;
existence
proof
defpred P[object,object] means ex a being Element of M.$1 st $2 = {a};
A1: now
let i be object such that
i in I;
set a = the Element of M.i;
reconsider j = {a} as object;
take j;
thus P[i,j];
end;
consider C being ManySortedSet of I such that
A2: for i be object st i in I holds P[i,C.i] from PBOOLE:sch 3(A1);
C is ManySortedSubset of M
proof
let i be object;
assume
A3: i in I;
then
A4: M.i is non empty;
let q be object;
consider a being Element of M.i such that
A5: C.i = {a} by A2,A3;
assume q in C.i;
then q = a by A5,TARSKI:def 1;
hence thesis by A4;
end;
then reconsider C as ManySortedSubset of M;
take C;
thus C is non-empty
proof
let i be object;
assume i in I;
then ex a being Element of M.i st C.i = {a} by A2;
hence thesis;
end;
let i be object;
assume i in I;
then ex a being Element of M.i st C.i = {a} by A2;
hence thesis;
end;
end;
registration
let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S,
o be OperSymbol of S;
cluster -> FinSequence-like for Element of Args(o,A);
coherence
proof
let x be Element of Args(o,A);
dom x = dom the_arity_of o by MSUALG_6:2;
then consider n being Nat such that
A1: dom x = Seg n by FINSEQ_1:def 2;
take n;
thus thesis by A1;
end;
end;
registration
let S be non void non empty ManySortedSign, I be set, s be SortSymbol of S,
F be MSAlgebra-Family of I, S;
cluster -> Function-like Relation-like for Element of (SORTS F).s;
coherence
proof
let x be Element of (SORTS F).s;
x is Element of product Carrier(F,s) by PRALG_2:def 10;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeGen X -> free non-empty;
coherence by MSAFREE:14,16;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeMSA X -> free;
coherence by MSAFREE:17;
end;
registration
let S be non empty non void ManySortedSign, A, B be non-empty MSAlgebra over
S;
cluster [:A,B:] -> non-empty;
coherence
proof
[:A,B:] = MSAlgebra (# [|the Sorts of A,the Sorts of B|], [[:the
Charact of A,the Charact of B:]] #) by PRALG_2:def 8;
hence the Sorts of [:A,B:] is non-empty;
end;
end;
theorem
for X, Y being set, f being Function st a in dom f & f.a in [:X,Y:]
holds f.a = [(pr1 f).a, (pr2 f).a]
proof
let X, Y be set, f be Function such that
A1: a in dom f and
A2: f.a in [:X,Y:];
(pr1 f).a = (f.a)`1 & (pr2 f).a = (f.a)`2 by A1,MCART_1:def 12,def 13;
hence thesis by A2,MCART_1:21;
end;
theorem Th2:
for X being non empty set, Y being set, f being Function of X, {Y
} holds rng f = {Y}
proof
let X be non empty set, Y be set, f be Function of X, {Y};
thus rng f c= {Y};
let q be object;
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
assume q in {Y};
then
A2: dom f = X & q = Y by FUNCT_2:def 1,TARSKI:def 1;
f.x = Y by A1,FUNCT_2:50;
hence thesis by A2,A1,FUNCT_1:def 3;
end;
theorem Th3:
Class(nabla I) c= {I}
proof
let q be object;
assume q in Class(nabla I);
then consider x being object such that
A1: x in I and
A2: q = Class(nabla I,x) by EQREL_1:def 3;
Class(nabla I,x) = I by A1,EQREL_1:26;
hence thesis by A2,TARSKI:def 1;
end;
theorem Th4:
for I being non empty set holds Class(nabla I) = {I}
proof
let I be non empty set;
consider a being object such that
A1: a in I by XBOOLE_0:def 1;
thus Class(nabla I) c= {I} by Th3;
let q be object;
assume q in {I};
then
A2: q = I by TARSKI:def 1;
Class(nabla I,a) = I by A1,EQREL_1:26;
hence thesis by A2,A1,EQREL_1:def 3;
end;
theorem Th5:
ex A being ManySortedSet of I st {A} = I --> {a}
proof
reconsider A = I --> a as ManySortedSet of I;
take A;
now
let i be object;
assume
A1: i in I;
hence {A}.i = {A.i} by PZFMISC1:def 1
.= {a} by A1,FUNCOP_1:7
.= (I --> {a}).i by A1,FUNCOP_1:7;
end;
hence thesis;
end;
theorem
for A being ManySortedSet of I ex B being non-empty ManySortedSet of I
st A c= B
proof
let A be ManySortedSet of I;
deffunc F(object) = {{}} \/ A.$1;
consider f being ManySortedSet of I such that
A1: for i be object st i in I holds f.i = F(i) from PBOOLE:sch 4;
f is non-empty
proof
let i be object;
assume i in I;
then f.i = {{}} \/ A.i by A1;
hence thesis;
end;
then reconsider f as non-empty ManySortedSet of I;
take f;
let i be object;
assume i in I;
then f.i = A.i \/ {{}} by A1;
hence thesis by XBOOLE_1:7;
end;
theorem
for M being non-empty ManySortedSet of I for B being finite-yielding
ManySortedSubset of M ex C being non-empty finite-yielding ManySortedSubset of
M st B c= C
proof
let M be non-empty ManySortedSet of I, B be finite-yielding ManySortedSubset
of M;
defpred P[object,object] means
ex a being Element of M.$1 st $2 = {a} \/ B.$1;
A1: now
let i be object such that
i in I;
set a = the Element of M.i;
reconsider j = {a} \/ B.i as object;
take j;
thus P[i,j];
end;
consider C being ManySortedSet of I such that
A2: for i be object st i in I holds P[i,C.i] from PBOOLE:sch 3(A1);
A3: C is ManySortedSubset of M
proof
let i be object;
assume
A4: i in I;
then consider a being Element of M.i such that
A5: C.i = {a} \/ B.i by A2;
let q be object;
assume q in C.i;
then
A6: q in {a} or q in B.i by A5,XBOOLE_0:def 3;
B c= M by PBOOLE:def 18;
then B.i c= M.i by A4;
then
A7: q = a or q in M.i by A6,TARSKI:def 1;
M.i is non empty by A4;
hence thesis by A7;
end;
A8: C is finite-yielding
proof
let i be object;
assume
A9: i in I;
reconsider b = B.i as finite set;
consider a being Element of M.i such that
A10: C.i = {a} \/ B.i by A2,A9;
thus thesis by A10;
end;
C is non-empty
proof
let i be object;
assume i in I;
then ex a being Element of M.i st C.i = {a} \/ B.i by A2;
hence thesis;
end;
then reconsider C as non-empty finite-yielding ManySortedSubset of M by A3,A8
;
take C;
let i be object;
assume i in I;
then ex a being Element of M.i st C.i = {a} \/ B.i by A2;
hence thesis by XBOOLE_1:7;
end;
theorem
for A, B being ManySortedSet of I for F, G being ManySortedFunction of
A, {B} holds F = G
proof
let A, B be ManySortedSet of I, F, G be ManySortedFunction of A, {B};
now
let i be object;
assume
A1: i in I;
then
A2: {B}.i = {B.i} by PZFMISC1:def 1;
F.i is Function of A.i, {B}.i & G.i is Function of A.i, {B}. i by A1,
PBOOLE:def 15;
hence F.i = G.i by A2,FUNCT_2:51;
end;
hence thesis;
end;
theorem Th9:
for A being non-empty ManySortedSet of I, B being ManySortedSet
of I for F being ManySortedFunction of A, {B} holds F is "onto"
proof
let A be non-empty ManySortedSet of I, B be ManySortedSet of I, F be
ManySortedFunction of A, {B};
let i be set;
assume
A1: i in I;
then {B}.i = {B.i} & F.i is Function of A.i, {B}.i by PBOOLE:def 15
,PZFMISC1:def 1;
hence thesis by A1,Th2;
end;
theorem Th10:
for A being ManySortedSet of I, B being non-empty ManySortedSet
of I for F being ManySortedFunction of {A}, B holds F is "1-1"
proof
let A be ManySortedSet of I, B be non-empty ManySortedSet of I, F be
ManySortedFunction of {A}, B;
now
let i be set;
assume i in I;
then {A}.i = {A.i} & F.i is Function of {A}.i, B.i by PBOOLE:def 15
,PZFMISC1:def 1;
hence F.i is one-to-one by PARTFUN1:17;
end;
hence thesis by MSUALG_3:1;
end;
theorem
for X being non-empty ManySortedSet of the carrier of S holds Reverse
X is "1-1"
proof
let X be non-empty ManySortedSet of the carrier of S;
for i being set st i in the carrier of S holds (Reverse X).i is one-to-one
proof
set D = DTConMSA X;
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
set f = (Reverse X).s;
let x1,x2 be object such that
A1: x1 in dom ((Reverse X).i) and
A2: x2 in dom ((Reverse X).i) and
A3: ((Reverse X).i).x1 = ((Reverse X).i).x2;
A4: f = Reverse(s,X) by MSAFREE:def 18;
then
A5: dom f = FreeGen(s,X) by FUNCT_2:def 1;
then consider a2 being set such that
A6: a2 in X.s and
A7: x2 = root-tree [a2,s] by A2,MSAFREE:def 15;
A8: [a2,s] in Terminals D by A6,MSAFREE:7;
then reconsider t2 = [a2,s] as Symbol of D;
t2`2 = s;
then root-tree t2 in {root-tree tt where tt is Symbol of D : tt in
Terminals D & tt`2 = s} by A8;
then root-tree t2 in FreeGen(s,X) by MSAFREE:13;
then
A9: f.x2 = [a2,s]`1 by A4,A7,MSAFREE:def 17
.= a2;
consider a1 being set such that
A10: a1 in X.s and
A11: x1 = root-tree [a1,s] by A1,A5,MSAFREE:def 15;
A12: [a1,s] in Terminals D by A10,MSAFREE:7;
then reconsider t1 = [a1,s] as Symbol of D;
t1`2 = s;
then root-tree t1 in {root-tree tt where tt is Symbol of D : tt in
Terminals D & tt`2 = s} by A12;
then root-tree t1 in FreeGen(s,X) by MSAFREE:13;
then f.x1 = [a1,s]`1 by A4,A11,MSAFREE:def 17
.= a1;
hence thesis by A3,A11,A7,A9;
end;
hence thesis by MSUALG_3:1;
end;
theorem
for A being non-empty finite-yielding ManySortedSet of I ex F being
ManySortedFunction of I --> NAT, A st F is "onto"
proof
let A be non-empty finite-yielding ManySortedSet of I;
defpred P[object,object] means
ex f being sequence of A.$1 st $2 = f & rng f = A.$1;
A1: for i being object st i in I ex j being object st P[i,j]
proof
let i be object;
assume
A2: i in I;
consider f being sequence of A.i such that
A3: rng f = A.i by A2,CARD_3:96;
take f;
thus thesis by A3;
end;
consider F being ManySortedSet of I such that
A4: for i being object st i in I holds P[i,F.i] from PBOOLE:sch 3(A1);
F is ManySortedFunction of I --> NAT, A
proof
let i be object;
assume i in I;
then (ex f being sequence of A.i st F.i = f & rng f = A.i )& (I -->
NAT).i = NAT by A4,FUNCOP_1:7;
hence thesis;
end;
then reconsider F as ManySortedFunction of I --> NAT, A;
take F;
let i be set;
assume i in I;
then ex f being sequence of A.i st F.i = f & rng f = A.i by A4;
hence thesis;
end;
theorem
for S being non empty ManySortedSign for A being non-empty MSAlgebra
over S for f, g being Element of product the Sorts of A
st for i being object
holds proj(the Sorts of A,i).f = proj(the Sorts of A,i).g holds f = g
proof
let S be non empty ManySortedSign, A be non-empty MSAlgebra over S, f, g be
Element of product the Sorts of A such that
A1: for i being object
holds proj(the Sorts of A,i).f = proj(the Sorts of A ,i).g;
set X = the Sorts of A;
now
thus dom f = dom X by CARD_3:9
.= dom g by CARD_3:9;
let x be object such that
x in dom f;
A2: dom (proj(X,x)) = product X by CARD_3:def 16;
hence f.x = proj(X,x).f by CARD_3:def 16
.= proj(X,x).g by A1
.= g.x by A2,CARD_3:def 16;
end;
hence thesis;
end;
theorem
for I being non empty set for s being Element of S for A being
MSAlgebra-Family of I,S for f, g being Element of product Carrier(A,s) st for a
being Element of I holds proj(Carrier(A,s),a).f = proj(Carrier(A,s),a).g holds
f = g
proof
let I be non empty set, s be Element of S, A be MSAlgebra-Family of I,S, f,
g be Element of product Carrier(A,s) such that
A1: for a being Element of I holds proj(Carrier(A,s),a).f = proj(Carrier
(A,s),a).g;
now
dom f = dom Carrier(A,s) by CARD_3:9;
hence dom f = dom g by CARD_3:9;
let x be object such that
A2: x in dom f;
A3: dom (proj(Carrier(A,s),x)) = product Carrier(A,s) by CARD_3:def 16;
hence f.x = proj(Carrier(A,s),x).f by CARD_3:def 16
.= proj(Carrier(A,s),x).g by A1,A2
.= g.x by A3,CARD_3:def 16;
end;
hence thesis;
end;
theorem
for A, B being non-empty MSAlgebra over S for C being non-empty
MSSubAlgebra of A for h1 being ManySortedFunction of B, C st h1 is_homomorphism
B, C for h2 being ManySortedFunction of B, A st h1 = h2 holds h2
is_homomorphism B, A
proof
let A, B be non-empty MSAlgebra over S, C be non-empty MSSubAlgebra of A, h1
be ManySortedFunction of B, C such that
A1: h1 is_homomorphism B, C;
the Sorts of C is ManySortedSubset of the Sorts of A by MSUALG_2:def 9;
then id (the Sorts of C) is ManySortedFunction of C, A by EXTENS_1:5;
then consider G be ManySortedFunction of C, A such that
A2: G = id (the Sorts of C);
G is_monomorphism C, A by A2,MSUALG_3:22;
then
A3: G is_homomorphism C, A;
A4: G ** h1 = h1 by A2,MSUALG_3:4;
let h2 be ManySortedFunction of B, A;
assume h1 = h2;
hence thesis by A1,A4,A3,MSUALG_3:10;
end;
theorem
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is_monomorphism A, B holds A, Image F
are_isomorphic
proof
let A, B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B;
assume
A1: F is_monomorphism A, B;
then F is_homomorphism A, B;
then consider G being ManySortedFunction of A, Image F such that
A2: G = F and
A3: G is_epimorphism A, Image F by MSUALG_3:21;
take G;
thus G is_epimorphism A, Image F by A3;
thus G is_homomorphism A, Image F by A3;
thus thesis by A1,A2;
end;
theorem Th17:
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is "onto" for o being OperSymbol of S for x
being Element of Args(o,B) holds ex y being Element of Args(o,A) st F # y = x
proof
let A, B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B such
that
A1: F is "onto";
let o be OperSymbol of S, t be Element of Args(o,B);
set D = len (the_arity_of o);
defpred P[object,object] means
ex y1 being Element of (the Sorts of A).((
the_arity_of o)/.$1) st (F.((the_arity_of o)/.$1)).y1 = t.$1 & $2 = y1;
A2: for k being Element of NAT st k in Seg D ex x being object st P[k,x]
proof
let k be Element of NAT;
assume k in Seg D;
then
A3: k in dom the_arity_of o by FINSEQ_1:def 3;
set s = (the_arity_of o)/.k;
A4: t.k in (the Sorts of B).s by A3,MSUALG_6:2;
rng (F.s) = (the Sorts of B).s by A1;
then consider y1 being object such that
A5: y1 in (the Sorts of A).s and
A6: F.s.y1 = t.k by A4,FUNCT_2:11;
reconsider y2 = y1 as Element of (the Sorts of A).s by A5;
take y1;
take y2;
thus thesis by A6;
end;
consider p being FinSequence such that
A7: dom p = Seg D and
A8: for k being Element of NAT st k in Seg D holds P[k,p.k] from
MSUALG_8:sch 1(A2);
A9: len p = len the_arity_of o by A7,FINSEQ_1:def 3;
for k being Nat st k in dom p holds p.k in (the Sorts of A).((
the_arity_of o)/.k)
proof
let k be Nat;
assume k in dom p;
then
ex y1 being Element of (the Sorts of A).((the_arity_of o)/.k ) st F.((
the_arity_of o)/.k).y1 = t.k & p.k = y1 by A7,A8;
hence thesis;
end;
then reconsider p as Element of Args(o,A) by A9,MSAFREE2:5;
set fp = F # p;
take p;
reconsider E = (the Sorts of B)*(the_arity_of o) as non-empty ManySortedSet
of dom (the_arity_of o);
A10: Args(o,B) = product E by PRALG_2:3;
A11: Seg D = dom the_arity_of o by FINSEQ_1:def 3
.= dom ((the Sorts of B)*(the_arity_of o)) by PRALG_2:3
.= dom t by A10,CARD_3:9;
A12: for k being Nat st k in dom t holds fp.k = t.k
proof
let k be Nat;
assume
A13: k in dom t;
then
ex y1 being Element of (the Sorts of A).((the_arity_of o)/.k) st (F.(
(the_arity_of o)/.k)).y1 = t.k & p.k = y1 by A11,A8;
hence thesis by A11,A7,A13,MSUALG_3:def 6;
end;
dom fp = dom ((the Sorts of B)*(the_arity_of o)) by A10,CARD_3:9
.= dom t by A10,CARD_3:9;
hence thesis by A12;
end;
theorem Th18:
for A being non-empty MSAlgebra over S, o being OperSymbol of S
for x being Element of Args(o,A) holds Den(o,A).x in (the Sorts of A).(
the_result_sort_of o)
proof
let A be non-empty MSAlgebra over S, o be OperSymbol of S, x be Element of
Args(o,A);
Den(o,A).x is Element of (the Sorts of A).((the ResultSort of S).o) by
FUNCT_2:15;
hence thesis;
end;
theorem Th19:
for A, B, C being non-empty MSAlgebra over S for F1 being
ManySortedFunction of A, B for F2 being ManySortedFunction of A, C st F1
is_epimorphism A, B & F2 is_homomorphism A, C for G being ManySortedFunction of
B, C st G ** F1 = F2 holds G is_homomorphism B, C
proof
let A, B, C be non-empty MSAlgebra over S, F1 be ManySortedFunction of A, B,
F2 be ManySortedFunction of A, C such that
A1: F1 is_epimorphism A, B and
A2: F2 is_homomorphism A, C;
let G be ManySortedFunction of B, C such that
A3: G ** F1 = F2;
let o be OperSymbol of S such that
Args(o,B) <> {};
let x be Element of Args(o,B);
F1 is "onto" by A1;
then consider y being Element of Args(o,A) such that
A4: F1 # y = x by Th17;
set r = the_result_sort_of o;
F1 is_homomorphism A, B by A1;
then
A5: (F1.r).(Den(o,A).y) = Den(o,B).x by A4;
A6: (F2.r).(Den(o,A).y) = (G.r * F1.r).(Den(o,A).y) by A3,MSUALG_3:2
.= (G.r).(Den(o,B).x) by A5,Th18,FUNCT_2:15;
(F2.r).(Den(o,A).y) = Den(o,C).((G ** F1) # y) by A2,A3
.= Den(o,C).(G # x) by A4,MSUALG_3:8;
hence (G.(the_result_sort_of o)).(Den(o,B).x) = Den(o,C).(G#x) by A6;
end;
reserve A, M for ManySortedSet of I,
B, C for non-empty ManySortedSet of I;
definition
let I be set;
let A be ManySortedSet of I;
let B, C be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, [|B,C|];
func Mpr1 F -> ManySortedFunction of A, B means
:Def1:
for i being set st i in I holds it.i = pr1 (F.i);
existence
proof
deffunc G(object) = pr1 (F.$1);
consider X be ManySortedSet of I such that
A1: for i be object st i in I holds X.i = G(i) from PBOOLE:sch 4;
X is ManySortedFunction of A, B
proof
let i be object;
assume
A2: i in I;
then reconsider Bi = B.i as non empty set;
A3: X.i = pr1 (F.i) by A1,A2;
then reconsider Xi = X.i as Function;
A4: F.i is Function of A.i, [|B,C|].i by A2,PBOOLE:def 15;
A5: rng Xi c= Bi
proof
let q be object;
assume q in rng Xi;
then consider x be object such that
A6: x in dom Xi and
A7: Xi.x = q by FUNCT_1:def 3;
x in dom (F.i) by A3,A6,MCART_1:def 12;
then
A8: Xi.x = (F.i.x)`1 & F.i.x in rng (F.i) by A3,FUNCT_1:def 3
,MCART_1:def 12;
rng (F.i) c= [|B,C|].i by A4,RELAT_1:def 19;
then
A9: rng (F.i) c= [:B.i,C.i:] by A2,PBOOLE:def 16;
assume not q in Bi;
hence contradiction by A7,A9,A8,MCART_1:10;
end;
dom (F.i) = A.i by A2,A4,FUNCT_2:def 1;
then dom Xi = A.i by A3,MCART_1:def 12;
hence thesis by A5,FUNCT_2:def 1,RELSET_1:4;
end;
then reconsider X as ManySortedFunction of A, B;
take X;
thus thesis by A1;
end;
uniqueness
proof
let M, N be ManySortedFunction of A, B such that
A10: for i be set st i in I holds M.i = pr1 (F.i) and
A11: for i be set st i in I holds N.i = pr1 (F.i);
now
let i be object;
assume
A12: i in I;
hence M.i = pr1 (F.i) by A10
.= N.i by A11,A12;
end;
hence M = N;
end;
func Mpr2 F -> ManySortedFunction of A, C means
:Def2:
for i being set st i in I holds it.i = pr2 (F.i);
existence
proof
deffunc G(object) =pr2 (F.$1);
consider X be ManySortedSet of I such that
A13: for i be object st i in I holds X.i = G(i) from PBOOLE:sch 4;
X is ManySortedFunction of A, C
proof
let i be object;
assume
A14: i in I;
then reconsider Ci = C.i as non empty set;
A15: X.i = pr2 (F.i) by A13,A14;
then reconsider Xi = X.i as Function;
A16: F.i is Function of A.i, [|B,C|].i by A14,PBOOLE:def 15;
A17: rng Xi c= Ci
proof
let q be object;
assume q in rng Xi;
then consider x be object such that
A18: x in dom Xi and
A19: Xi.x = q by FUNCT_1:def 3;
x in dom (F.i) by A15,A18,MCART_1:def 13;
then
A20: Xi.x = (F.i.x)`2 & F.i.x in rng (F.i) by A15,FUNCT_1:def 3
,MCART_1:def 13;
rng (F.i) c= [|B,C|].i by A16,RELAT_1:def 19;
then
A21: rng (F.i) c= [:B.i,C.i:] by A14,PBOOLE:def 16;
assume not q in Ci;
hence contradiction by A19,A21,A20,MCART_1:10;
end;
dom (F.i) = A.i by A14,A16,FUNCT_2:def 1;
then dom Xi = A.i by A15,MCART_1:def 13;
hence thesis by A17,FUNCT_2:def 1,RELSET_1:4;
end;
then reconsider X as ManySortedFunction of A, C;
take X;
thus thesis by A13;
end;
uniqueness
proof
let M, N be ManySortedFunction of A, C such that
A22: for i be set st i in I holds M.i = pr2 (F.i) and
A23: for i be set st i in I holds N.i = pr2 (F.i);
now
let i be object;
assume
A24: i in I;
hence M.i = pr2 (F.i) by A22
.= N.i by A23,A24;
end;
hence M = N;
end;
end;
theorem
for F being ManySortedFunction of A, [| I-->{a} , I-->{a} |] holds
Mpr1 F = Mpr2 F
proof
let F be ManySortedFunction of A, [| I-->{a} , I-->{a} |];
now
let i be object;
A1: dom (pr2 (F.i)) = dom (F.i) by MCART_1:def 13;
assume
A2: i in I;
A3: now
let y be object such that
A4: y in dom (F.i);
A5: (F.i).y in rng (F.i) by A4,FUNCT_1:def 3;
(F.i) is Function of A.i, [| I-->{a} , I-->{a} |].i by A2,PBOOLE:def 15;
then rng (F.i) c= [| I-->{a} , I-->{a} |].i by RELAT_1:def 19;
then
A6: rng (F.i) c= [: (I-->{a}).i, (I-->{a}).i :] by A2,PBOOLE:def 16;
then ((F.i).y)`1 in (I-->{a}).i by A5,MCART_1:10;
then
A7: ((F.i).y)`1 in {a} by A2,FUNCOP_1:7;
((F.i).y)`2 in (I-->{a}).i by A5,A6,MCART_1:10;
then
A8: ((F.i).y)`2 in {a} by A2,FUNCOP_1:7;
thus (pr2 (F.i)).y = ((F.i).y)`2 by A4,MCART_1:def 13
.= a by A8,TARSKI:def 1
.= ((F.i).y)`1 by A7,TARSKI:def 1;
end;
(Mpr1 F).i = pr1 (F.i) & (Mpr2 F).i = pr2 (F.i) by A2,Def1,Def2;
hence (Mpr1 F).i = (Mpr2 F).i by A1,A3,MCART_1:def 12;
end;
hence thesis;
end;
theorem
for F being ManySortedFunction of A, [|B,C|] st F is "onto" holds Mpr1
F is "onto"
proof
let F be ManySortedFunction of A, [|B,C|] such that
A1: F is "onto";
let i be set;
assume
A2: i in I;
then reconsider m = (Mpr1 F).i as Function of A.i, B.i by PBOOLE:def 15;
rng m = B.i
proof
thus rng m c= B.i;
let a be object such that
A3: a in B.i;
consider z be object such that
A4: z in [|B,C|].i by A2,XBOOLE_0:def 1;
set p = [a,z`2];
z in [:B.i,C.i:] by A2,A4,PBOOLE:def 16;
then
A5: p`2 in C.i by MCART_1:10;
p`1 in B.i by A3;
then p in [:B.i,C.i:] by A5,ZFMISC_1:def 2;
then
A6: p in [|B,C|].i by A2,PBOOLE:def 16;
A7: dom m = A.i by A2,FUNCT_2:def 1;
A8: (F.i) is Function of A.i, [|B,C|].i by A2,PBOOLE:def 15;
then
A9: dom (F.i) = A.i by A2,FUNCT_2:def 1;
rng (F.i) = [|B,C|].i by A1,A2;
then consider b be object such that
A10: b in A.i and
A11: (F.i).b = p by A8,A6,FUNCT_2:11;
m.b = (pr1 (F.i)).b by A2,Def1
.= p`1 by A10,A11,A9,MCART_1:def 12
.= a;
hence thesis by A10,A7,FUNCT_1:def 3;
end;
hence thesis;
end;
theorem
for F being ManySortedFunction of A, [|B,C|] st F is "onto" holds Mpr2
F is "onto"
proof
let F be ManySortedFunction of A, [|B,C|] such that
A1: F is "onto";
let i be set;
assume
A2: i in I;
then reconsider m = (Mpr2 F).i as Function of A.i, C.i by PBOOLE:def 15;
rng m = C.i
proof
thus rng m c= C.i;
let a be object such that
A3: a in C.i;
consider z be object such that
A4: z in [|B,C|].i by A2,XBOOLE_0:def 1;
set p = [z`1,a];
z in [:B.i,C.i:] by A2,A4,PBOOLE:def 16;
then
A5: p`1 in B.i by MCART_1:10;
p`2 in C.i by A3;
then p in [:B.i,C.i:] by A5,ZFMISC_1:def 2;
then
A6: p in [|B,C|].i by A2,PBOOLE:def 16;
A7: dom m = A.i by A2,FUNCT_2:def 1;
A8: (F.i) is Function of A.i, [|B,C|].i by A2,PBOOLE:def 15;
then
A9: dom (F.i) = A.i by A2,FUNCT_2:def 1;
rng (F.i) = [|B,C|].i by A1,A2;
then consider b be object such that
A10: b in A.i and
A11: (F.i).b = p by A8,A6,FUNCT_2:11;
m.b = (pr2 (F.i)).b by A2,Def2
.= p`2 by A10,A11,A9,MCART_1:def 13
.= a;
hence thesis by A10,A7,FUNCT_1:def 3;
end;
hence thesis;
end;
theorem
for F being ManySortedFunction of A, [|B,C|] st M in doms F holds for
i be set st i in I holds (F..M).i = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i]
proof
let F be ManySortedFunction of A, [|B,C|] such that
A1: M in doms F;
let i be set;
assume
A2: i in I;
then M.i in (doms F).i by A1;
then
A3: M.i in dom (F.i) by A2,MSSUBFAM:14;
A is_transformable_to [|B,C|];
then M in A by A1,MSSUBFAM:17;
then F..M in [|B,C|] by CLOSURE1:3;
then (F..M).i in [|B,C|].i by A2;
then (F..M).i in [:B.i,C.i:] by A2,PBOOLE:def 16;
then
A4: (F.i).(M.i) in [:B.i,C.i:] by A2,PRALG_1:def 20;
set z = (F.i).(M.i);
(Mpr2 F).i = pr2 (F.i) by A2,Def2;
then
A5: ((Mpr2 F)..M).i = (pr2 (F.i)).(M.i) by A2,PRALG_1:def 20
.= z`2 by A3,MCART_1:def 13;
(Mpr1 F).i = pr1 (F.i) by A2,Def1;
then ((Mpr1 F)..M).i = (pr1 (F.i)).(M.i) by A2,PRALG_1:def 20
.= z`1 by A3,MCART_1:def 12;
then z = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i] by A4,A5,MCART_1:21;
hence thesis by A2,PRALG_1:def 20;
end;
begin :: On the Trivial Many Sorted Algebras
registration
let S be non empty ManySortedSign;
cluster the Sorts of Trivial_Algebra S -> finite-yielding non-empty;
coherence
proof
ex A being ManySortedSet of the carrier of S st {A} = (the carrier of S
) --> {0} by Th5;
hence thesis by MSAFREE2:def 12;
end;
end;
registration
let S be non empty ManySortedSign;
cluster Trivial_Algebra S -> finite-yielding non-empty;
coherence;
end;
theorem Th24:
for A being non-empty MSAlgebra over S for F being
ManySortedFunction of A, Trivial_Algebra S for o being OperSymbol of S for x
being Element of Args(o,A) holds (F.the_result_sort_of o).(Den(o,A).x) = 0 &
Den(o,Trivial_Algebra S).(F#x) = 0
proof
let A be non-empty MSAlgebra over S, F be ManySortedFunction of A,
Trivial_Algebra S;
let o be OperSymbol of S;
let x be Element of Args(o,A);
set I = the carrier of S, SA = the Sorts of A, T = Trivial_Algebra S, ST =
the Sorts of T;
set r = the_result_sort_of o;
consider i being object such that
A1: i in I and
A2: Result(o,T) = ST.i by PBOOLE:138;
reconsider d = Den(o,A).x as Element of SA.r by FUNCT_2:15;
consider XX being ManySortedSet of I such that
A3: {XX} = I --> {0} by Th5;
A4: ST = {XX} by A3,MSAFREE2:def 12;
then
A5: ST.r = {0} by A3;
thus (F.r).(Den(o,A).x) = (F.r).d .= 0 by A5,TARSKI:def 1;
ST.i = {0} by A3,A4,A1,FUNCOP_1:7;
hence thesis by A2,TARSKI:def 1;
end;
theorem Th25:
for A being non-empty MSAlgebra over S for F being
ManySortedFunction of A, Trivial_Algebra S holds F is_epimorphism A,
Trivial_Algebra S
proof
let A be non-empty MSAlgebra over S, F be ManySortedFunction of A,
Trivial_Algebra S;
set I = the carrier of S;
consider XX being ManySortedSet of I such that
A1: {XX} = I --> {0} by Th5;
thus F is_homomorphism A, Trivial_Algebra S
proof
let o be OperSymbol of S such that
Args(o,A) <> {};
let x be Element of Args(o,A);
thus (F.the_result_sort_of o).(Den(o,A).x) = 0 by Th24
.= Den(o,Trivial_Algebra S).(F#x) by Th24;
end;
the Sorts of Trivial_Algebra S = {XX} by A1,MSAFREE2:def 12;
hence thesis by Th9;
end;
theorem
for A being MSAlgebra over S st ex X being ManySortedSet of the
carrier of S st the Sorts of A = {X} holds A, Trivial_Algebra S are_isomorphic
proof
let A be MSAlgebra over S such that
A1: ex X being ManySortedSet of the carrier of S st the Sorts of A = {X};
set I = the carrier of S, SB = the Sorts of A, ST = the Sorts of
Trivial_Algebra S;
consider X being ManySortedSet of I such that
A2: the Sorts of A = {X} by A1;
set F = the ManySortedFunction of SB, ST;
reconsider F1 = F as ManySortedFunction of {X}, ST by A2;
take F;
A is non-empty by A2;
hence F is_epimorphism A, Trivial_Algebra S by Th25;
hence F is_homomorphism A, Trivial_Algebra S;
F1 is "1-1" by Th10;
hence thesis;
end;
begin :: On the Many Sorted Congruences
theorem
for A being non-empty MSAlgebra over S for C being MSCongruence of A
holds C is ManySortedSubset of [|the Sorts of A, the Sorts of A|]
proof
let A be non-empty MSAlgebra over S, C be MSCongruence of A;
set SF = the Sorts of A;
let i be object such that
A1: i in the carrier of S;
C.i is Relation of SF.i, SF.i by A1,MSUALG_4:def 1;
then C.i c= [:SF.i, SF.i:];
hence thesis by A1,PBOOLE:def 16;
end;
theorem
for A being non-empty MSAlgebra over S for R being Subset of CongrLatt
A for F being SubsetFamily of [|the Sorts of A, the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
proof
let A be non-empty MSAlgebra over S, R be Subset of CongrLatt A, F be
SubsetFamily of [|the Sorts of A, the Sorts of A|] such that
A1: R = F;
set R0 = meet |:F:|, SF = the Sorts of A, I = the carrier of S;
per cases;
suppose
F is non empty;
then reconsider F1 = F as non empty SubsetFamily of [|SF,SF|];
A2: F1 c= the carrier of EqRelLatt SF
proof
let q be object;
assume q in F1;
then q is MSCongruence of A by A1,MSUALG_5:def 6;
hence thesis by MSUALG_5:def 5;
end;
then
A3: R0 is MSEquivalence_Relation-like ManySortedRelation of SF by MSUALG_7:8;
reconsider R0 as ManySortedRelation of A by A2,MSUALG_7:8;
R0 is MSEquivalence-like
by A3;
then reconsider R0 as MSEquivalence-like ManySortedRelation of A;
now
let o be OperSymbol of S;
let a,b be Element of Args(o,A) such that
A4: for n being Nat st n in dom a holds [a.n,b.n] in R0.((
the_arity_of o)/.n);
set r = the_result_sort_of o;
consider Q being Subset-Family of ([|SF,SF|].r) such that
A5: Q = |:F1:|.r and
A6: R0.r = Intersect Q by MSSUBFAM:def 1;
A7: Q = { s.r where s is Element of Bool [|SF,SF|] : s in F1 } by A5,
CLOSURE2:14;
now
let Y be set;
assume Y in Q;
then consider s being Element of Bool [|SF,SF|] such that
A8: Y = s.r and
A9: s in F1 by A7;
reconsider s as MSCongruence of A by A1,A9,MSUALG_5:def 6;
now
let n be Nat such that
A10: n in dom a;
set t = (the_arity_of o)/.n;
consider G being Subset-Family of ([|SF,SF|].t) such that
A11: G = |:F1:|.t and
A12: R0.t = Intersect G by MSSUBFAM:def 1;
G = { j.t where j is Element of Bool [|SF,SF|] : j in F1 } by A11,
CLOSURE2:14;
then
A13: s.t in G by A9;
[a.n,b.n] in Intersect G by A4,A10,A12;
then [a.n,b.n] in meet G by A11,SETFAM_1:def 9;
hence [a.n,b.n] in s.t by A13,SETFAM_1:def 1;
end;
hence [Den(o,A).a,Den(o,A).b] in Y by A8,MSUALG_4:def 4;
end;
then [Den(o,A).a,Den(o,A).b] in meet Q by A5,SETFAM_1:def 1;
hence [Den(o,A).a,Den(o,A).b] in R0.(the_result_sort_of o) by A5,A6,
SETFAM_1:def 9;
end;
hence thesis by MSUALG_4:def 4;
end;
suppose
F is empty;
then |:F:| = EmptyMS I;
then meet |:F:| = [|the Sorts of A, the Sorts of A|] by MSSUBFAM:41;
hence thesis by MSUALG_5:18;
end;
end;
theorem
for A being non-empty MSAlgebra over S for C being MSCongruence of A
st C = [|the Sorts of A, the Sorts of A|] holds the Sorts of QuotMSAlg (A,C) =
{the Sorts of A}
proof
let A be non-empty MSAlgebra over S, C be MSCongruence of A such that
A1: C = [|the Sorts of A, the Sorts of A|];
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
A2: C.s = [:(the Sorts of A).s, (the Sorts of A).s:] by A1,PBOOLE:def 16
.= nabla (the Sorts of A).s by EQREL_1:def 1;
thus (the Sorts of QuotMSAlg (A,C)).i = Class (C.s) by MSUALG_4:def 6
.= {(the Sorts of A).s} by A2,Th4
.= {the Sorts of A}.i by PZFMISC1:def 1;
end;
hence thesis;
end;
theorem Th30:
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is_homomorphism A, B holds MSHomQuot F **
MSNat_Hom(A,MSCng F) = F
proof
let A, B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B such
that
A1: F is_homomorphism A, B;
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
reconsider h = MSHomQuot(F,s) as Function of (Class MSCng F).s, (the Sorts
of B).s;
reconsider f = h * MSNat_Hom(A,MSCng F,s) as Function of (the Sorts of A).
s, (the Sorts of B).s;
A2: for c being Element of (the Sorts of A).s holds f.c = F.s.c
proof
let c be Element of (the Sorts of A).s;
thus f.c = h.((MSNat_Hom(A,MSCng F,s)).c) by FUNCT_2:15
.= h.(Class((MSCng F).s,c)) by MSUALG_4:def 15
.= h.(Class(MSCng(F,s),c)) by A1,MSUALG_4:def 18
.= F.s.c by A1,MSUALG_4:def 19;
end;
thus (MSHomQuot F ** MSNat_Hom(A,MSCng F)).i = ((MSHomQuot F).s) * ((
MSNat_Hom(A,MSCng F)).s) by MSUALG_3:2
.= MSHomQuot(F,s) * ((MSNat_Hom(A,MSCng F)).s) by MSUALG_4:def 20
.= MSHomQuot(F,s) * MSNat_Hom(A,MSCng F,s) by MSUALG_4:def 16
.= F.i by A2,FUNCT_2:63;
end;
hence thesis;
end;
theorem Th31:
for A being non-empty MSAlgebra over S for C being MSCongruence
of A for s being SortSymbol of S for a being Element of (the Sorts of QuotMSAlg
(A,C)).s ex x being Element of (the Sorts of A).s st a = Class(C,x)
proof
let A be non-empty MSAlgebra over S, C be MSCongruence of A, s be SortSymbol
of S, a be Element of (the Sorts of QuotMSAlg (A,C)).s;
a in (Class C).s;
then a in Class (C.s) by MSUALG_4:def 6;
then consider t being object such that
A1: t in (the Sorts of A).s and
A2: a = Class(C.s,t) by EQREL_1:def 3;
reconsider t as Element of (the Sorts of A).s by A1;
take t;
thus thesis by A2;
end;
theorem
for A being MSAlgebra over S for C1, C2 being MSEquivalence-like
ManySortedRelation of A st C1 c= C2 for i being Element of S for x, y being
Element of (the Sorts of A).i st [x,y] in C1.i holds Class (C1,x) c= Class (C2,
y) & (A is non-empty implies Class (C1,y) c= Class (C2,x))
proof
let A be MSAlgebra over S, C1, C2 be MSEquivalence-like ManySortedRelation
of A such that
A1: C1 c= C2;
let i be Element of S, x, y be Element of (the Sorts of A).i such that
A2: [x,y] in C1.i;
field(C1.i) = (the Sorts of A).i by ORDERS_1:12;
then
A3: C1.i is_transitive_in (the Sorts of A).i by RELAT_2:def 16;
A4: C1.i c= C2.i by A1;
thus Class (C1,x) c= Class (C2,y)
proof
let q be object;
assume
A5: q in Class (C1,x);
then [q,x] in C1.i by EQREL_1:19;
then [q,y] in C1.i by A2,A3,A5,RELAT_2:def 8;
hence thesis by A4,EQREL_1:19;
end;
assume A is non-empty;
then reconsider B = A as non-empty MSAlgebra over S;
field(C1.i) = (the Sorts of A).i by ORDERS_1:12;
then C1.i is_symmetric_in (the Sorts of B).i by RELAT_2:def 11;
then
A6: [y,x] in C1.i by A2,RELAT_2:def 3;
let q be object such that
A7: q in Class (C1,y);
[q,y] in C1.i by A7,EQREL_1:19;
then [q,x] in C1.i by A3,A7,A6,RELAT_2:def 8;
hence thesis by A4,EQREL_1:19;
end;
theorem
for A being non-empty MSAlgebra over S, C being MSCongruence of A for
s being SortSymbol of S, x, y being Element of (the Sorts of A).s holds (
MSNat_Hom(A,C)).s.x = (MSNat_Hom(A,C)).s.y iff [x,y] in C.s
proof
let A be non-empty MSAlgebra over S, C be MSCongruence of A, s be SortSymbol
of S, x, y be Element of (the Sorts of A).s;
set f = (MSNat_Hom(A,C)).s, g = MSNat_Hom(A,C,s);
A1: f = g by MSUALG_4:def 16;
hereby
assume
A2: (MSNat_Hom(A,C)).s.x = (MSNat_Hom(A,C)).s.y;
Class(C.s,x) = g.x by MSUALG_4:def 15
.= Class(C.s,y) by A1,A2,MSUALG_4:def 15;
hence [x,y] in C.s by EQREL_1:35;
end;
assume
A3: [x,y] in C.s;
thus (MSNat_Hom(A,C)).s.x = Class(C.s,x) by A1,MSUALG_4:def 15
.= Class(C.s,y) by A3,EQREL_1:35
.= (MSNat_Hom(A,C)).s.y by A1,MSUALG_4:def 15;
end;
Lm1: now
let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S,
C1, C2 be MSCongruence of A;
let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
A1: for i being Element of S for x being Element of (the Sorts of
QuotMSAlg (A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,
xx) holds G.i.x = Class(C2, xx);
thus G is "onto"
proof
let i be set;
set sL = the Sorts of QuotMSAlg (A,C1), sP = the Sorts of QuotMSAlg (A,C2);
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A2: dom (G.s) = sL.s by FUNCT_2:def 1;
rng(G.s) c= sP.s;
hence rng(G.i) c= sP.i;
let q be object;
assume q in sP.i;
then q in Class(C2.s) by MSUALG_4:def 6;
then consider a being object such that
A3: a in (the Sorts of A).s and
A4: q = Class(C2.s,a) by EQREL_1:def 3;
reconsider a as Element of (the Sorts of A).s by A3;
Class(C1.s,a) in Class (C1.s) by EQREL_1:def 3;
then reconsider x = Class(C1,a) as Element of sL.s by MSUALG_4:def 6;
G.s.x = Class(C2,a) by A1
.= Class(C2.s,a);
hence thesis by A4,A2,FUNCT_1:def 3;
end;
end;
theorem Th34:
for A being non-empty MSAlgebra over S for C1, C2 being
MSCongruence of A for G being ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg
(A,C2) st for i being Element of S for x being Element of (the Sorts of
QuotMSAlg (A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,
xx) holds G.i.x = Class(C2,xx) holds G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2)
proof
let A be non-empty MSAlgebra over S, C1, C2 be MSCongruence of A;
set sL = the Sorts of QuotMSAlg (A,C1);
let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
A1: for i being Element of S for x being Element of (the Sorts of
QuotMSAlg (A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,
xx) holds G.i.x = Class(C2,xx);
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A2: for c being Element of (the Sorts of A).s holds ((G.s) * (MSNat_Hom(A,
C1).s)).c = MSNat_Hom(A,C2).s.c
proof
let c be Element of (the Sorts of A).s;
Class(C1.s,c) in Class (C1.s) by EQREL_1:def 3;
then
A3: Class(C1,c) is Element of sL.s by MSUALG_4:def 6;
thus ((G.s) * (MSNat_Hom(A,C1).s)).c = (G.s).(MSNat_Hom(A,C1).s.c) by
FUNCT_2:15
.= (G.s).(MSNat_Hom(A,C1,s).c) by MSUALG_4:def 16
.= (G.s).Class(C1,c) by MSUALG_4:def 15
.= Class(C2,c) by A1,A3
.= MSNat_Hom(A,C2,s).c by MSUALG_4:def 15
.= MSNat_Hom(A,C2).s.c by MSUALG_4:def 16;
end;
thus (G ** MSNat_Hom(A,C1)).i = (G.s) * (MSNat_Hom(A,C1).s) by MSUALG_3:2
.= MSNat_Hom(A,C2).i by A2,FUNCT_2:63;
end;
hence thesis;
end;
theorem Th35:
for A being non-empty MSAlgebra over S for C1, C2 being
MSCongruence of A for G being ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg
(A,C2) st for i being Element of S for x being Element of (the Sorts of
QuotMSAlg (A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,
xx) holds G.i.x = Class(C2,xx) holds G is_epimorphism QuotMSAlg (A,C1),
QuotMSAlg (A,C2)
proof
let A be non-empty MSAlgebra over S, C1, C2 be MSCongruence of A;
MSNat_Hom(A,C2) is_epimorphism A, QuotMSAlg (A,C2) by MSUALG_4:3;
then
A1: MSNat_Hom(A,C2) is_homomorphism A, QuotMSAlg (A,C2);
let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
A2: for i being Element of S for x being Element of (the Sorts of
QuotMSAlg (A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,
xx) holds G.i.x = Class(C2,xx);
G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2) by A2,Th34;
hence G is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) by A1,Th19,
MSUALG_4:3;
thus thesis by A2,Lm1;
end;
theorem
for A, B being non-empty MSAlgebra over S for F being
ManySortedFunction of A, B st F is_homomorphism A, B for C1 being MSCongruence
of A st C1 c= MSCng F ex H being ManySortedFunction of QuotMSAlg (A,C1), B st H
is_homomorphism QuotMSAlg (A,C1), B & F = H ** MSNat_Hom(A,C1)
proof
let A, B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B such
that
A1: F is_homomorphism A, B;
MSHomQuot F is_monomorphism QuotMSAlg (A,MSCng F), B by A1,MSUALG_4:4;
then
A2: MSHomQuot F is_homomorphism QuotMSAlg (A,MSCng F), B;
let C1 be MSCongruence of A such that
A3: C1 c= MSCng F;
set G = MSNat_Hom(A,C1), I = the carrier of S, sQ = the Sorts of QuotMSAlg (
A,C1), sF = the Sorts of QuotMSAlg (A,MSCng F);
defpred P[object,object,object] means
ex s being Element of I, xx being Element of (
the Sorts of A).s st $3 = s & $2 = Class(C1,xx) & $1 = Class(MSCng F,xx);
A4: for i being object st i in I
for x being object st x in sQ.i ex y being object st y in sF.i & P[y,x,i]
proof
let i be object;
assume i in I;
then reconsider s = i as Element of I;
let x be object;
assume x in sQ.i;
then consider x1 being Element of (the Sorts of A).s such that
A5: x = Class(C1,x1) by Th31;
take y = Class(MSCng F,x1);
y in Class ((MSCng F).s) by EQREL_1:def 3;
hence y in sF.i by MSUALG_4:def 6;
thus thesis by A5;
end;
consider C12 being ManySortedFunction of sQ, sF such that
A6: for i being object st i in I holds ex f being Function of sQ.i, sF.i st
f = C12.i & for x being object st x in sQ.i holds P[f.x,x,i]
from MSSUBFAM:sch 1(
A4);
reconsider H = MSHomQuot F**C12 as ManySortedFunction of QuotMSAlg (A,C1), B;
take H;
A7: for i being Element of S for x being Element of (the Sorts of QuotMSAlg
(A,C1)).i for xx being Element of (the Sorts of A).i st x = Class(C1,xx) holds
C12.i.x = Class(MSCng F,xx)
proof
let i be Element of S, x be Element of (the Sorts of QuotMSAlg (A,C1)).i,
xx be Element of (the Sorts of A).i such that
A8: x = Class(C1,xx);
consider f being Function of sQ.i, sF.i such that
A9: f = C12.i and
A10: for x being object st x in sQ.i holds P[f.x,x,i] by A6;
consider s being Element of I, x1 being Element of (the Sorts of A).s such
that
A11: i = s and
A12: x = Class(C1,x1) and
A13: f.x = Class(MSCng F,x1) by A10;
xx in Class(C1.s,x1) by A8,A12,EQREL_1:23;
then
A14: [xx,x1] in C1.s by EQREL_1:19;
C1.s c= (MSCng F).s by A3;
then xx in Class((MSCng F).s,x1) by A14,EQREL_1:19;
hence thesis by A9,A11,A13,EQREL_1:23;
end;
then C12 is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,MSCng F) by Th35;
then C12 is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,MSCng F);
hence H is_homomorphism QuotMSAlg (A,C1), B by A2,MSUALG_3:10;
A15: now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A16: for x being Element of (the Sorts of A).s holds (C12.s * G.s).x = (
MSNat_Hom(A,MSCng F)).s.x
proof
let x be Element of (the Sorts of A).s;
Class(C1.s,x) in Class (C1.s) by EQREL_1:def 3;
then
A17: Class(C1,x) in (Class C1).s by MSUALG_4:def 6;
thus (C12.s * G.s).x = C12.s.(G.s.x) by FUNCT_2:15
.= C12.s.(MSNat_Hom(A,C1,s).x) by MSUALG_4:def 16
.= C12.s.(Class(C1,x)) by MSUALG_4:def 15
.= Class(MSCng F,x) by A7,A17
.= MSNat_Hom(A,MSCng F,s).x by MSUALG_4:def 15
.= (MSNat_Hom(A,MSCng F)).s.x by MSUALG_4:def 16;
end;
thus (C12 ** G).i = C12.s * G.s by MSUALG_3:2
.= (MSNat_Hom(A,MSCng F)).i by A16,FUNCT_2:63;
end;
thus F = MSHomQuot F ** MSNat_Hom(A,MSCng F) by A1,Th30
.= MSHomQuot F ** (C12 ** G) by A15,PBOOLE:3
.= H ** MSNat_Hom(A,C1) by PBOOLE:140;
end;