:: Inverse Limits of Many Sorted Algebras
:: by Adam Grabowski
::
:: 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, ORDERS_2, SUBSET_1, STRUCT_0, MSUALG_1, PRALG_2,
FUNCT_1, RELAT_1, CARD_3, RLVECT_2, PBOOLE, XXREAL_0, MEMBER_1, MSUALG_3,
FUNCOP_1, RELAT_2, MCART_1, MSUALG_2, TARSKI, UNIALG_2, MARGREL1,
FUNCT_6, FINSEQ_1, FUNCT_2, COMPLEX1, PARTFUN1, FINSEQ_4, NAT_1, FUNCT_5,
NATTRA_1, PUA2MSS1, ZFMISC_1, MSALIMIT;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XTUPLE_0, MCART_1,
RELAT_1, FUNCT_1, STRUCT_0, RELAT_2, FUNCT_2, FINSEQ_1, FINSEQ_2,
ORDERS_2, FUNCOP_1, RELSET_1, PARTFUN1, CARD_3, BINOP_1, FUNCT_5,
FUNCT_6, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, PRALG_2,
PUA2MSS1, ORDERS_3;
constructors PRALG_1, PRALG_2, MSUALG_3, PUA2MSS1, ORDERS_3, RELSET_1,
FUNCT_5, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE,
STRUCT_0, ORDERS_2, MSUALG_1, MSUALG_2, PRALG_2, MSUALG_3, ORDERS_3,
PRALG_3, ORDINAL1, CARD_3, RELSET_1, FINSEQ_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities TARSKI, BINOP_1, XTUPLE_0;
expansions TARSKI, XBOOLE_0;
theorems CARD_3, FUNCOP_1, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCT_5, FUNCT_7,
MCART_1, MSUALG_1, MSUALG_2, MSUALG_3, MSUHOM_1, ORDERS_2, ORDERS_3,
PARTFUN1, PBOOLE, PRALG_1, PRALG_2, PUA2MSS1, RELAT_1, RELAT_2, TARSKI,
ZFMISC_1, RELSET_1, XBOOLE_0, ORDERS_1, FUNCT_6, FINSEQ_2, XTUPLE_0;
schemes FRAENKEL, PBOOLE, TARSKI, XBOOLE_0;
begin :: Inverse Limits of Many Sorted Algebras
reserve P for non empty Poset,
i, j, k for Element of P;
reserve S for non void non empty ManySortedSign;
registration
let I be non empty set, S;
let AF be MSAlgebra-Family of I,S;
let i be Element of I;
let o be OperSymbol of S;
cluster ((OPER AF).i).o -> Function-like Relation-like;
coherence
proof
ex U0 being MSAlgebra over S st U0 = AF.i & (OPER AF).i = the Charact
of U0 by PRALG_2:def 11;
hence thesis;
end;
end;
registration
let I be non empty set, S;
let AF be MSAlgebra-Family of I,S;
let s be SortSymbol of S;
cluster (SORTS AF).s -> functional;
coherence
proof
(SORTS AF).s = product Carrier (AF,s) by PRALG_2:def 10;
hence thesis;
end;
end;
definition
let P, S;
mode OrderedAlgFam of P,S -> MSAlgebra-Family of the carrier of P,S means
:
Def1: ex
F be ManySortedFunction of the InternalRel of P st for i,j,k st i >= j
& j >= k ex f1 be ManySortedFunction of it.i, it.j, f2 be ManySortedFunction of
it.j, it.k st f1 = F.(j,i) & f2 = F.(k,j) & F.(k,i) = f2 ** f1 & f1
is_homomorphism it.i, it.j;
existence
proof
reconsider T1 = the InternalRel of P as Relation of the carrier of P;
set A = the non-empty MSAlgebra over S;
reconsider Z = (the carrier of P) --> A as ManySortedSet of the carrier of
P;
for i be object st i in the carrier of P holds Z.i is non-empty MSAlgebra
over S by FUNCOP_1:7;
then reconsider Z as MSAlgebra-Family of the carrier of P, S by
PRALG_2:def 5;
take Z;
set G = (the InternalRel of P) --> id (the Sorts of A);
reconsider G as ManySortedFunction of the InternalRel of P;
take G;
let i, j, k;
consider F2 be ManySortedFunction of Z.j, Z.k such that
A2: F2 = id (the Sorts of A);
assume i >= j & j >= k;
then
A3: [j,i] in the InternalRel of P & [k,j] in the InternalRel of P by
ORDERS_2:def 5;
field T1 = the carrier of P by ORDERS_1:12;
then T1 is_transitive_in the carrier of P by RELAT_2:def 16;
then
A4: [k,i] in T1 by A3,RELAT_2:def 8;
consider F1 be ManySortedFunction of Z.i, Z.j such that
A6: F1 = id (the Sorts of A);
take F1;
take F2;
F2 ** F1 = id (the Sorts of A) by A6,A2,MSUALG_3:3;
hence thesis by A3,A6,A2,A4,FUNCOP_1:7,MSUALG_3:9;
end;
end;
reserve OAF for OrderedAlgFam of P, S;
definition
let P, S, OAF;
mode Binding of OAF -> ManySortedFunction of the InternalRel of P means
:
Def2: for
i,j,k st i >= j & j >= k ex f1 be ManySortedFunction of OAF.i, OAF.j,
f2 be ManySortedFunction of OAF.j, OAF.k st f1 = it.(j,i) & f2 = it.(k,j) & it.
(k,i) = f2 ** f1 & f1 is_homomorphism OAF.i, OAF.j;
existence by Def1;
end;
definition
let P, S, OAF;
let B be Binding of OAF, i,j;
assume
A1: i >= j;
func bind (B,i,j) -> ManySortedFunction of OAF.i, OAF.j equals
:Def3:
B.(j,i
);
coherence
proof
j >= j by ORDERS_2:1;
then ex f1 be ManySortedFunction of OAF.i, OAF.j, f2 be ManySortedFunction
of OAF.j, OAF.j st f1 = B.(j,i) & f2 = B.(j,j) & B.(j,i) = f2 ** f1 & f1
is_homomorphism OAF.i, OAF.j by A1,Def2;
hence thesis;
end;
end;
reserve B for Binding of OAF;
theorem Th1:
i >= j & j >= k implies bind (B,j,k) ** bind (B,i,j) = bind (B,i, k)
proof
assume
A1: i >= j & j >= k;
then
A2: ex f1 be ManySortedFunction of OAF.i, OAF.j, f2 be ManySortedFunction of
OAF.j, OAF.k st f1 = B.(j,i) & f2 = B.(k,j) & B.(k,i) = f2 ** f1 & f1
is_homomorphism OAF.i, OAF.j by Def2;
bind (B,j,k) = B.(k,j) & bind (B,i,j) = B.(j,i) by A1,Def3;
hence thesis by A1,A2,Def3,ORDERS_2:3;
end;
definition
let P, S, OAF;
let IT be Binding of OAF;
attr IT is normalized means
:Def4:
for i holds IT.(i,i) = id (the Sorts of OAF.i);
end;
theorem Th2:
for P,S,OAF,B,i,j st i >= j for f be ManySortedFunction of OAF.i,
OAF.j st f = bind (B,i,j) holds f is_homomorphism OAF.i,OAF.j
proof
let P,S,OAF,B,i,j;
assume
A1: i >= j;
let f be ManySortedFunction of OAF.i,OAF.j;
assume
A2: f = bind (B,i,j);
j >= j by ORDERS_2:1;
then
ex f1 be ManySortedFunction of OAF.i, OAF.j, f2 be ManySortedFunction of
OAF.j, OAF.j st f1 = B.(j,i) & f2 = B.(j,j) & B.(j,i) = f2 ** f1 & f1
is_homomorphism OAF.i, OAF.j by A1,Def2;
hence thesis by A1,A2,Def3;
end;
definition
let P, S, OAF, B;
func Normalized B -> Binding of OAF means
:Def5:
for i, j st i >= j holds it
.(j,i) = IFEQ (j, i, id (the Sorts of OAF.i), bind (B,i,j) ** id (the Sorts of
OAF.i) );
existence
proof
defpred P[object,object] means
ex i,j st $1 = [j,i] & $2 = IFEQ (j, i, id (the
Sorts of OAF.i), bind (B,i,j) ** id (the Sorts of OAF.i) );
A1: now
let ij be object;
assume
A2: ij in the InternalRel of P;
then reconsider i2 = ij`1, i1 = ij`2 as Element of P by MCART_1:10;
reconsider i1, i2 as Element of P;
deffunc Z(object)=
IFEQ (i2, i1, id (the Sorts of OAF.i1), bind (B,i1,i2)
** id (the Sorts of OAF.i1) );
consider A be ManySortedSet of the InternalRel of P such that
A3: for ij be object st ij in the InternalRel of P holds A.ij = Z(ij)
from PBOOLE:sch 4;
take x = A.ij;
take i1,i2;
thus ij = [i2,i1] & x = IFEQ (i2, i1, id (the Sorts of OAF.i1), bind (B,
i1,i2) ** id (the Sorts of OAF.i1) ) by A2,A3,MCART_1:21;
end;
A4: for z being object st z in the InternalRel of P
ex y being object st P[z,y]
proof let z be object;
assume z in the InternalRel of P;
then ex y being set st P[z,y] by A1;
hence thesis;
end;
consider A be ManySortedSet of the InternalRel of P such that
A5: for ij being object st ij in the InternalRel of P holds P[ij,A.ij]
from PBOOLE:sch 3(A4);
for z be object st z in dom A holds A.z is Function
proof
let z be object;
assume z in dom A;
then z in the InternalRel of P;
then consider i1,i2 be Element of P such that
z = [i2,i1] and
A6: A.z = IFEQ (i2, i1, id (the Sorts of OAF.i1), bind (B,i1,i2) **
id (the Sorts of OAF.i1) ) by A5;
per cases;
suppose
i1 = i2;
hence thesis by A6,FUNCOP_1:def 8;
end;
suppose
i1 <> i2;
hence thesis by A6,FUNCOP_1:def 8;
end;
end;
then reconsider A as ManySortedFunction of the InternalRel of P by
FUNCOP_1:def 6;
now
let i,j,k;
assume that
A7: i >= j and
A8: j >= k;
consider kl be set such that
A9: kl = [j,i];
kl in the InternalRel of P by A7,A9,ORDERS_2:def 5;
then consider i1,j1 be Element of P such that
A10: [j1,i1] = kl and
A11: A.kl = IFEQ (j1, i1, id (the Sorts of OAF.i1), bind (B,i1,j1)
** id (the Sorts of OAF.i1) ) by A5;
A12: i1 = i & j1 = j by A9,A10,XTUPLE_0:1;
A.(j,i) is ManySortedFunction of OAF.i,OAF.j
proof
per cases;
suppose
i = j;
hence thesis by A10,A11,A12,FUNCOP_1:def 8;
end;
suppose
i <> j;
hence thesis by A10,A11,A12,FUNCOP_1:def 8;
end;
end;
then reconsider f1 = A.(j,i) as ManySortedFunction of OAF.i,OAF.j;
consider lm be set such that
A13: lm = [k,j];
lm in the InternalRel of P by A8,A13,ORDERS_2:def 5;
then consider i2,j2 be Element of P such that
A14: [j2,i2] = lm and
A15: A.lm = IFEQ (j2, i2, id (the Sorts of OAF.i2), bind (B,i2,j2)
** id (the Sorts of OAF.i2) ) by A5;
A16: j2 = k & i2 = j by A13,A14,XTUPLE_0:1;
A.(k,j) is ManySortedFunction of OAF.j,OAF.k
proof
per cases;
suppose
j = k;
hence thesis by A14,A15,A16,FUNCOP_1:def 8;
end;
suppose
j <> k;
hence thesis by A14,A15,A16,FUNCOP_1:def 8;
end;
end;
then reconsider f2 = A.(k,j) as ManySortedFunction of OAF.j,OAF.k;
A17: for i,j st i >= j & i <> j holds A.(j,i) = bind (B,i,j)
proof
let i,j;
assume that
A18: i >= j and
A19: i <> j;
consider lm be set such that
A20: lm = [j,i];
lm in the InternalRel of P by A18,A20,ORDERS_2:def 5;
then consider i2,j2 be Element of P such that
A21: [j2,i2] = lm and
A22: A.lm = IFEQ (j2, i2, id (the Sorts of OAF.i2), bind (B,i2,j2)
** id (the Sorts of OAF.i2) ) by A5;
i2 = i & j2 = j by A20,A21,XTUPLE_0:1;
then
A.(j,i) = bind (B,i,j) ** id (the Sorts of OAF.i) by A19,A21,A22,
FUNCOP_1:def 8;
hence thesis by MSUALG_3:3;
end;
A23: A.(k,i) = f2 ** f1
proof
per cases;
suppose
A24: i = j & j = k;
then f2 = id (the Sorts of OAF.j) by A14,A15,A16,FUNCOP_1:def 8;
hence thesis by A24,MSUALG_3:3;
end;
suppose
A25: i = j & j <> k;
then f1 = id (the Sorts of OAF.i) by A10,A11,A12,FUNCOP_1:def 8;
hence thesis by A25,MSUALG_3:3;
end;
suppose
A26: i <> j & j = k;
then f2 = id (the Sorts of OAF.j) by A14,A15,A16,FUNCOP_1:def 8;
hence thesis by A26,MSUALG_3:4;
end;
suppose
A27: i <> j & j <> k;
then i > j & j > k by A7,A8,ORDERS_2:def 6;
then
A28: i <> k by ORDERS_2:5;
f2 = bind (B,j,k) ** id (the Sorts of OAF.j) by A14,A15,A16,A27,
FUNCOP_1:def 8;
then
A29: f2 = bind (B,j,k) by MSUALG_3:3;
f1 = bind (B,i,j) ** id (the Sorts of OAF.i) by A10,A11,A12,A27,
FUNCOP_1:def 8;
then f1 = bind (B,i,j) by MSUALG_3:3;
then f2 ** f1 = bind (B,i,k) by A7,A8,A29,Th1;
hence thesis by A7,A8,A17,A28,ORDERS_2:3;
end;
end;
A30: for i,j st i = j holds A.(j,i) = id (the Sorts of OAF.i)
proof
let i,j;
consider lm be set such that
A31: lm = [j,i];
assume
A32: i = j;
then i >= j by ORDERS_2:1;
then lm in the InternalRel of P by A31,ORDERS_2:def 5;
then consider i2,j2 be Element of P such that
A33: [j2,i2] = lm and
A34: A.lm = IFEQ (j2, i2, id (the Sorts of OAF.i2), bind (B,i2,j2)
** id (the Sorts of OAF.i2) ) by A5;
i2 = i & j2 = j by A31,A33,XTUPLE_0:1;
hence thesis by A32,A33,A34,FUNCOP_1:def 8;
end;
f1 is_homomorphism OAF.i, OAF.j
proof
per cases;
suppose
A35: i = j;
then A.(i,j) = id (the Sorts of OAF.i) by A30;
hence thesis by A35,MSUALG_3:9;
end;
suppose
i <> j;
then A.(j,i) = bind (B,i,j) by A7,A17;
hence thesis by A7,Th2;
end;
end;
hence ex f1 be ManySortedFunction of OAF.i, OAF.j, f2 be
ManySortedFunction of OAF.j, OAF.k st f1 = A.(j,i) & f2 = A.(k,j) & A.(k,i) =
f2 ** f1 & f1 is_homomorphism OAF.i, OAF.j by A23;
end;
then reconsider A as Binding of OAF by Def2;
take A;
let i, j;
consider kl be set such that
A36: kl = [j,i];
assume i >= j;
then kl in the InternalRel of P by A36,ORDERS_2:def 5;
then consider i1,j1 be Element of P such that
A37: [j1,i1] = kl and
A38: A.kl = IFEQ (j1, i1, id (the Sorts of OAF.i1), bind (B,i1,j1) **
id (the Sorts of OAF.i1) ) by A5;
i1 = i & j1 = j by A36,A37,XTUPLE_0:1;
hence thesis by A37,A38;
end;
uniqueness
proof
let N1, N2 be Binding of OAF such that
A39: for i,j st i >= j holds N1.(j,i) = IFEQ (j, i, id (the Sorts of
OAF.i), bind (B,i,j) ** id (the Sorts of OAF.i) ) and
A40: for i,j st i >= j holds N2.(j,i) = IFEQ (j, i, id (the Sorts of
OAF.i), bind (B,i,j) ** id (the Sorts of OAF.i) );
now
let ij be object;
assume
A41: ij in the InternalRel of P;
then reconsider i2 = ij`1 , i1 = ij`2 as Element of P by MCART_1:10;
reconsider i1, i2 as Element of P;
A42: N2.ij = N2.(i2,i1) by A41,MCART_1:21;
ij = [ij`1,ij`2] by A41,MCART_1:21;
then
A43: i2 <= i1 by A41,ORDERS_2:def 5;
N1.ij = N1.(i2,i1) by A41,MCART_1:21;
then N1.ij = IFEQ (i2, i1, id (the Sorts of OAF.i1), bind (B,i1,i2) **
id (the Sorts of OAF.i1) ) by A39,A43;
hence N1.ij = N2.ij by A40,A43,A42;
end;
hence N1 = N2 by PBOOLE:3;
end;
end;
theorem Th3:
for i, j st i >= j & i <> j holds B.(j,i) = (Normalized B).(j,i)
proof
let i, j;
assume that
A1: i >= j and
A2: i <> j;
(Normalized B).(j,i) = IFEQ (j, i, id (the Sorts of OAF.i), bind (B,i,j)
** id (the Sorts of OAF.i) ) & IFEQ (j, i, id (the Sorts of OAF.i), bind (B,i,j
) ** id (the Sorts of OAF.i) ) = bind (B,i,j) ** id (the Sorts of OAF.i) by A1
,A2,Def5,FUNCOP_1:def 8;
then (Normalized B).(j,i) = bind (B,i,j) by MSUALG_3:3;
hence thesis by A1,Def3;
end;
registration
let P, S, OAF, B;
cluster Normalized B -> normalized;
coherence
proof
let i be Element of P;
i >= i by ORDERS_2:1;
then
(Normalized B).(i,i) = IFEQ (i, i, id (the Sorts of OAF.i), bind (B,i,
i) ** id (the Sorts of OAF.i) ) by Def5;
hence thesis by FUNCOP_1:def 8;
end;
end;
registration
let P, S, OAF;
cluster normalized for Binding of OAF;
existence
proof
set B = the Binding of OAF;
take Normalized B;
thus thesis;
end;
end;
theorem
for NB be normalized Binding of OAF for i, j st i >= j holds (
Normalized NB).(j,i) = NB.(j,i)
proof
let NB be normalized Binding of OAF;
let i, j;
assume
A1: i >= j;
per cases;
suppose
i <> j;
hence thesis by A1,Th3;
end;
suppose
A2: i = j;
(Normalized NB).(j,i) = IFEQ (j, i, id (the Sorts of OAF.i), bind (NB,
i,j) ** id (the Sorts of OAF.i) ) by A1,Def5;
then (Normalized NB).(j,i) = id (the Sorts of OAF.i) by A2,FUNCOP_1:def 8;
hence thesis by A2,Def4;
end;
end;
definition
let P, S, OAF;
let B be Binding of OAF;
func InvLim B -> strict MSSubAlgebra of product OAF means
:Def6:
for s be
SortSymbol of S for f be Element of (SORTS OAF).s holds f in (the Sorts of it).
s iff for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f.j;
existence
proof
reconsider L = product OAF as non-empty MSAlgebra over S;
deffunc F(SortSymbol of S) = { f where f is Element of product Carrier (
OAF,$1) : for i,j st i >= j holds (bind (B,i,j).$1).(f.i) = f.j };
consider C be ManySortedSet of the carrier of S such that
A1: for s be SortSymbol of S holds C.s = F(s) from PBOOLE:sch 5;
for i be object st i in the carrier of S holds C.i c= (SORTS OAF).i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
defpred P[Element of product Carrier (OAF,s)] means for i,j st i >= j
holds (bind (B,i,j).s).($1.i) = $1.j;
A2: { f where f is Element of product Carrier (OAF,s) : P[f] } c=
product Carrier (OAF,s) from FRAENKEL:sch 10;
(SORTS OAF).s = product Carrier (OAF,s) by PRALG_2:def 10;
hence thesis by A1,A2;
end;
then C c= SORTS OAF by PBOOLE:def 2;
then reconsider C as ManySortedSubset of SORTS OAF by PBOOLE:def 18;
reconsider C as MSSubset of product OAF by PRALG_2:12;
for o be OperSymbol of S holds C is_closed_on o
proof
let o be OperSymbol of S;
rng ( (Den(o,product OAF)) | ((C# * the Arity of S).o) ) c= (C * the
ResultSort of S).o
proof
reconsider MS = C as ManySortedSet of (the carrier of S);
reconsider K = ( (Den(o,product OAF)) | ((C# * the Arity of S).o) ) as
Function;
let x be object;
A3: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
assume
A4: x in rng ( (Den(o,product OAF)) | ((C# * the Arity of S).o) );
then consider y be object such that
A5: y in dom K and
A6: x = K.y by FUNCT_1:def 3;
A7: dom K = (dom (Den (o,product OAF))) /\ ((C# * the Arity of S).o)
by RELAT_1:61;
then y in ((C# * the Arity of S).o) by A5,XBOOLE_0:def 4;
then y in C# . ((the Arity of S).o) by A3,FUNCT_1:13;
then y in C# . the_arity_of o by MSUALG_1:def 1;
then
A8: y in product (MS * the_arity_of o) by FINSEQ_2:def 5;
x in Result (o,product OAF) by A4;
then dom (the ResultSort of S) = the carrier' of S & x in ((the Sorts
of product OAF) * the ResultSort of S).o by FUNCT_2:def 1,MSUALG_1:def 5;
then x in (the Sorts of product OAF).((the ResultSort of S).o) by
FUNCT_1:13;
then
A9: x in (SORTS OAF).((the ResultSort of S).o) by PRALG_2:12;
then reconsider x1 = x as Function;
x in (SORTS OAF).(the_result_sort_of o) by A9,MSUALG_1:def 2;
then
A10: x
is Element of product Carrier (OAF,the_result_sort_of o) by PRALG_2:def 10;
A11: y in (dom (Den (o,product OAF))) by A5,A7,XBOOLE_0:def 4;
now
let s be SortSymbol of S;
for i,j st i >= j holds (bind (B,i,j).the_result_sort_of o). (
x1.i) = x1.j
proof
reconsider OPE = (OPS OAF).o as Function;
A12: Den (o,product OAF) = (the Charact of product OAF).o by
MSUALG_1:def 6
.= (OPS OAF).o by PRALG_2:12;
reconsider y as Function by A8;
let i,j;
assume
A13: i >= j;
reconsider Co = commute y as Function;
set y1 = (commute y).i;
A14: dom y = dom (MS*the_arity_of o) by A8,CARD_3:9;
A15: rng (the_arity_of o) c= dom MS
proof
let i be object;
assume i in rng (the_arity_of o);
then i in the carrier of S;
hence thesis by PARTFUN1:def 2;
end;
then
A16: dom y = dom the_arity_of o by A14,RELAT_1:27;
then
A17: dom y = Seg len (the_arity_of o) by FINSEQ_1:def 3;
rng y c= Funcs(the carrier of P,|.OAF.|)
proof
let z be object;
assume z in rng y;
then consider n be object such that
A18: n in dom y and
A19: z = y.n by FUNCT_1:def 3;
A20: n in dom (MS*the_arity_of o) by A8,A18,CARD_3:9;
then n in dom (the_arity_of o) by A15,RELAT_1:27;
then (the_arity_of o).n = (the_arity_of o)/.n by PARTFUN1:def 6;
then reconsider Pa = ((the_arity_of o).n) as SortSymbol of S;
z in (MS*the_arity_of o).n by A8,A19,A20,CARD_3:9;
then z in MS.((the_arity_of o).n) by A20,FUNCT_1:12;
then z in { f where f is Element of product Carrier (OAF,Pa) :
for i,j st i >= j holds (bind (B,i,j).Pa).(f.i) = f.j } by A1;
then
A21: ex z9 be Element of product Carrier(OAF,Pa) st z9 = z & for
i,j st i >= j holds (bind (B,i,j).Pa).(z9.i) = z9.j;
then reconsider z as Function;
A22: dom z = dom Carrier (OAF,Pa) by A21,CARD_3:9
.= the carrier of P by PARTFUN1:def 2;
rng z c= |.OAF.|
proof
let p be object;
assume p in rng z;
then consider r be object such that
A23: r in dom z and
A24: z.r = p by FUNCT_1:def 3;
reconsider r9 = r as Element of P by A22,A23;
reconsider r9 as Element of P;
r9 in the carrier of P;
then
A25: ex U0 be MSAlgebra over S st U0 = OAF.r & (Carrier (OAF,
Pa)).r = (the Sorts of U0).Pa by PRALG_2:def 9;
|.OAF.r9.| in the set of all |.OAF.k.| where k is Element of P;
then |.OAF.r9.| c= union the set of all |.OAF.k.| where
k is Element of P by ZFMISC_1:74; then
A26: |.OAF.r9.| c= |.OAF.| by PRALG_2:def 7;
dom (the Sorts of (OAF.r9)) = the carrier of S
by PARTFUN1:def 2; then
A27: (the Sorts of (OAF.r9)).Pa in rng (the Sorts of (OAF.r9))
by FUNCT_1:def 3;
dom z = dom Carrier (OAF,Pa) by A21,CARD_3:9;
then p in (Carrier (OAF,Pa)).r by A21,A23,A24,CARD_3:9;
then p in union (rng the Sorts of OAF.r9)
by A25,A27,TARSKI:def 4;
then p in |.OAF.r9.| by PRALG_2:def 6;
hence thesis by A26;
end;
hence thesis by A22,FUNCT_2:def 2;
end;
then
A28: y in Funcs(Seg len (the_arity_of o),Funcs(the carrier of P,|.
OAF.|)) by A17,FUNCT_2:def 2;
per cases;
suppose
A29: the_arity_of o <> {};
A30: for t be object st t in dom doms(OAF?.o) holds Co.t in (doms(
OAF?.o)).t
proof
let t be object;
assume t in dom doms(OAF?.o);
then reconsider t as Element of P by PRALG_2:11;
reconsider yt = Co.t as Function;
dom the_arity_of o <> {} by A29;
then
WW: Seg len (the_arity_of o) <> {} by FINSEQ_1:def 3;
then Co in Funcs(the carrier of P,Funcs (Seg len(the_arity_of
o), |.OAF.|)) by A28,FUNCT_6:55;
then
A31: ex ss be Function st ss = Co & dom ss = the carrier of P &
rng ss c= Funcs (Seg len(the_arity_of o),|.OAF.|) by FUNCT_2:def 2;
A32: Co.t in product ((the Sorts of OAF.t)*(the_arity_of o))
proof
A33: dom ((the Sorts of OAF.t)*(the_arity_of o)) = dom (
the_arity_of o) by PRALG_2:3
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
A34: dom y = Seg len (the_arity_of o) by A16,FINSEQ_1:def 3;
A35: for w be object st w in dom ((the Sorts of OAF.t)*(
the_arity_of o)) holds yt.w in ((the Sorts of OAF.t)*(the_arity_of o)).w
proof
A36: y = commute commute y by WW,A28,FUNCT_6:57;
let w be object;
reconsider Pi = (the_arity_of o)/.w as SortSymbol of S;
A37: dom (Carrier (OAF,(the_arity_of o)/.w)) = the
carrier of P by PARTFUN1:def 2;
assume
A38: w in dom ((the Sorts of OAF.t)*(the_arity_of o));
then
A39: w in dom (the_arity_of o) by A33,FINSEQ_1:def 3;
y.w in (MS*the_arity_of o).w by A8,A14,A33,A34,A38,CARD_3:9
;
then
A40: y.w in MS.((the_arity_of o).w) by A39,FUNCT_1:13;
reconsider y as Function-yielding Function by A36;
reconsider yw = y.w as Function;
y.w in MS.((the_arity_of o)/.w) by A39,A40,PARTFUN1:def 6;
then yw in { ff where ff is Element of product Carrier (
OAF,Pi) : for i,j st i >= j holds (bind (B,i,j).Pi).(ff.i) = ff.j } by A1;
then ex jg be Element of product Carrier(OAF,Pi) st jg =
yw & for i,j st i >= j holds (bind (B,i,j).Pi).(jg.i) = jg.j;
then
A41: yw .t in (Carrier (OAF,(the_arity_of o)/.w)).t by A37,
CARD_3:9;
ex U0 be MSAlgebra over S st U0 = OAF.t & (Carrier (
OAF,( the_arity_of o)/.w)).t = (the Sorts of U0).(( the_arity_of o)/.w) by
PRALG_2:def 9;
then (Carrier (OAF,(the_arity_of o)/.w)).t = (the Sorts
of (OAF.t)) . ((the_arity_of o).w) by A39,PARTFUN1:def 6
.= ((the Sorts of (OAF.t)) * (the_arity_of o)).w by A39,
FUNCT_1:13;
hence thesis by A28,A33,A38,A41,FUNCT_6:56;
end;
Co.t in rng Co by A31,FUNCT_1:def 3;
then ex ts be Function st ts = Co.t & dom ts = Seg len (
the_arity_of o) & rng ts c= |.OAF.| by A31,FUNCT_2:def 2;
hence thesis by A33,A35,CARD_3:9;
end;
(doms(OAF?.o)).t = Args (o,OAF.t) by PRALG_2:11;
hence thesis by A32,PRALG_2:3;
end;
dom (the_arity_of o) <> {} by A29;
then Seg len (the_arity_of o) <> {} by FINSEQ_1:def 3;
then Co in Funcs (the carrier of P,Funcs(Seg len (
the_arity_of o),|. OAF.|)) by A28,FUNCT_6:55;
then consider Co9 be Function such that
AA: Co9 = Co & dom Co9 = the carrier of P &
rng Co9 c= Funcs(Seg len (the_arity_of o),|.OAF.|)
by FUNCT_2:def 2;
dom Co = dom doms (OAF?.o) by AA,PRALG_2:11; then
A42: Co in product doms (OAF?.o) by A30,CARD_3:9;
A43: OPE = IFEQ(the_arity_of o,{},commute(OAF?.o),Commute Frege
(OAF?.o)) by PRALG_2:def 13;
then
A44: y in dom Commute Frege(OAF?.o) by A11,A12,A29,FUNCOP_1:def 8;
reconsider y1 as Function;
A45: dom (OAF?.o) = the carrier of P by PARTFUN1:def 2;
S: dom Co = the carrier of P by AA; then
i in dom (OAF?.o) /\ dom Co by A45; then
a45: i in dom ((OAF?.o)..commute y) by PRALG_1:def 19;
j in dom (OAF?.o) /\ dom Co by A45,S; then
b45: j in dom ((OAF?.o)..commute y) by PRALG_1:def 19;
A46: x1 = OPE.y by A5,A6,A12,FUNCT_1:47
.= (Commute Frege(OAF?.o)).y by A29,A43,FUNCOP_1:def 8
.= ((Frege (OAF?.o)).commute y) by A44,PRALG_2:def 1
.= ((OAF?.o)..commute y) by A42,PRALG_2:def 2;
then
A47: x1.i = ((OAF?.o).i).((commute y).i) by PRALG_1:def 19,a45
.= (Den(o,OAF.i)).y1 by PRALG_2:7;
dom (the_arity_of o) <> {} by A29;
then Seg len (the_arity_of o) <> {} by FINSEQ_1:def 3;
then
Co in Funcs(the carrier of P,Funcs (Seg len(the_arity_of o)
, |.OAF.|)) by A28,FUNCT_6:55;
then
A48: ex ss be Function st ss = Co & dom ss = the carrier of P &
rng ss c= Funcs (Seg len(the_arity_of o),|.OAF.|) by FUNCT_2:def 2;
y1 in product ((the Sorts of OAF.i)*(the_arity_of o))
proof
A49: dom ((the Sorts of OAF.i)*(the_arity_of o)) = dom (
the_arity_of o) by PRALG_2:3
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
A50: for w be object st w in dom ((the Sorts of OAF.i)*(
the_arity_of o)) holds y1.w in ((the Sorts of OAF.i)*(the_arity_of o)).w
proof
dom (the_arity_of o) <> {} by A29;
then Seg len (the_arity_of o) <> {} by FINSEQ_1:def 3;
then
A51: y = commute commute y by A28,FUNCT_6:57;
let w be object;
reconsider Pi = (the_arity_of o)/.w as SortSymbol of S;
A52: dom (Carrier (OAF,(the_arity_of o)/.w)) = the carrier
of P by PARTFUN1:def 2;
assume
A53: w in dom ((the Sorts of OAF.i)*(the_arity_of o));
then
A54: w in dom (the_arity_of o) by A49,FINSEQ_1:def 3;
w in dom y by A16,A49,A53,FINSEQ_1:def 3;
then y.w in (MS*the_arity_of o).w by A8,A14,CARD_3:9;
then
A55: y.w in MS.((the_arity_of o).w) by A54,FUNCT_1:13;
reconsider y as Function-yielding Function by A51;
reconsider yw = y.w as Function;
y.w in MS.((the_arity_of o)/.w) by A54,A55,PARTFUN1:def 6;
then
yw in { ff where ff is Element of product Carrier (OAF,
Pi) : for i,j st i >= j holds (bind (B,i,j).Pi).(ff.i) = ff.j } by A1;
then
ex jg be Element of product Carrier(OAF,Pi) st jg = yw &
for i,j st i >= j holds (bind (B,i,j).Pi).(jg.i) = jg.j;
then
A56: yw .i in (Carrier (OAF,(the_arity_of o)/.w)).i by A52,
CARD_3:9;
ex U0 be MSAlgebra over S st U0 = OAF.i & (Carrier (OAF,
( the_arity_of o)/.w)).i = (the Sorts of U0).(( the_arity_of o)/.w) by
PRALG_2:def 9;
then
(Carrier (OAF,(the_arity_of o)/.w)).i = (the Sorts of (
OAF.i)) . ((the_arity_of o).w) by A54,PARTFUN1:def 6
.= ((the Sorts of (OAF.i)) * (the_arity_of o)).w by A54,
FUNCT_1:13;
hence thesis by A28,A49,A53,A56,FUNCT_6:56;
end;
Co.i in rng Co by A48,FUNCT_1:def 3;
then ex ts be Function st ts = Co.i & dom ts = Seg len (
the_arity_of o) & rng ts c= |.OAF.| by A48,FUNCT_2:def 2;
hence thesis by A49,A50,CARD_3:9;
end;
then reconsider y19 = y1 as Element of Args(o,OAF.i) by PRALG_2:3
;
A57: bind (B,i,j) is_homomorphism OAF.i,OAF.j by A13,Th2;
(bind (B,i,j))#y19 = (commute y).j
proof
A58: dom ((bind (B,i,j))#y19) = dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
then reconsider One = ((bind (B,i,j))#y19) as FinSequence by
FINSEQ_1:def 2;
dom (the_arity_of o) <> {} by A29; then
A59: Seg len the_arity_of o <> {} by FINSEQ_1:def 3;
then y = commute commute y by A28,FUNCT_6:57;
then reconsider y as Function-yielding Function;
reconsider y2 = ((commute y).j) as Function;
Co in Funcs(the carrier of P,Funcs (Seg len(the_arity_of
o), |.OAF.|)) by A28,A59,FUNCT_6:55;
then
A60: ex ss be Function st ss = Co & dom ss = the carrier of P
& rng ss c= Funcs (Seg len(the_arity_of o),|.OAF.|) by FUNCT_2:def 2;
then Co.j in rng Co by FUNCT_1:def 3;
then
A61: ex ts be Function st ts = Co.j & dom ts = Seg len (
the_arity_of o) & rng ts c= |.OAF.| by A60,FUNCT_2:def 2;
then reconsider Two = y2 as FinSequence by FINSEQ_1:def 2;
A62: Co.i in rng Co by A60,FUNCT_1:def 3;
now
let n be Nat;
reconsider yn = y.n as Function;
reconsider Pi = (the_arity_of o)/.n as SortSymbol of S;
A63: ex ts9 be Function st ts9 = Co.i & dom ts9 = Seg len (
the_arity_of o) & rng ts9 c= |.OAF.| by A60,A62,FUNCT_2:def 2;
assume
A64: n in dom y2;
then
A65: y.n in (MS*the_arity_of o).n by A8,A14,A17,A61,CARD_3:9;
A66: n in dom (the_arity_of o) by A61,A64,FINSEQ_1:def 3;
then (the_arity_of o)/.n = (the_arity_of o).n by
PARTFUN1:def 6;
then yn in MS.Pi by A66,A65,FUNCT_1:13;
then yn in { f where f is Element of product Carrier (OAF,
Pi) : for i,j st i >= j holds (bind (B,i,j).Pi).(f.i) = f.j } by A1;
then
A67: ex yn9 be Element of product Carrier(OAF,Pi) st yn9 =
yn & for i,j st i >= j holds (bind (B,i,j).Pi).(yn9.i) = yn9.j;
(y19.n) = yn.i by A28,A61,A64,FUNCT_6:56;
then ((bind (B,i,j))#y19).n = ((bind (B,i,j)).((
the_arity_of o)/.n)).(yn.i) by A61,A64,A63,MSUALG_3:def 6
.= yn.j by A13,A67;
hence ((bind (B,i,j))#y19).n = y2.n by A28,A61,A64,FUNCT_6:56
;
end;
then for n be Nat st n in Seg len (the_arity_of o) holds One.
n = Two.n by A61;
hence thesis by A61,A58,FINSEQ_1:13;
end;
then (Den(o,OAF.j)).((bind (B,i,j))#y19) = ((OAF?.o).j).((
commute y).j) by PRALG_2:7
.= x1.j by A46,PRALG_1:def 19,b45;
hence thesis by A57,A47,MSUALG_3:def 7;
end;
suppose
A68: the_arity_of o = {};
reconsider co = ((commute (OAF?.o)).y) as Function;
A69: MS * {} = {};
A70: co = ((curry' uncurry (OAF?.o)).y) by FUNCT_6:def 10;
A71: dom (OAF?.o) = the carrier of P by PARTFUN1:def 2;
A72: (Den (o,product OAF)) = (the Charact of product OAF).o
by MSUALG_1:def 6
.= (OPS OAF).o by PRALG_2:12
.= IFEQ(the_arity_of o,{},commute(OAF?.o),Commute Frege(OAF
?.o)) by PRALG_2:def 13
.= (commute (OAF?.o)) by A68,FUNCOP_1:def 8;
A73: for d be Element of P holds x1.d = (Den (o,OAF.d)).{}
proof
reconsider co9 = ((curry' uncurry (OAF?.o)).y) as Function by
A70;
let d be Element of P;
reconsider g = (OAF?.o).d as Function;
A74: x1 = (commute (OAF?.o)).y by A5,A6,A72,FUNCT_1:47;
g = Den(o,OAF.d) by PRALG_2:7;
then dom g = Args (o,OAF.d) by FUNCT_2:def 1
.= {{}} by A68,PRALG_2:4; then
A75: y in dom g by A8,A68,CARD_3:10; then
A76: [d,y] in dom (uncurry (OAF?.o)) by A71,FUNCT_5:38;
co.d = co9.d by FUNCT_6:def 10
.= (uncurry (OAF?.o)).(d,y) by A76,FUNCT_5:22
.= g.y by A71,A75,FUNCT_5:38;
then x1.d = (Den (o,OAF.d)).y by A74,PRALG_2:7
.= (Den (o,OAF.d)).{} by A8,A68,A69,CARD_3:10,TARSKI:def 1;
hence thesis;
end; then
A77: x1.i = Den (o,OAF.i).{};
Args(o,OAF.i) = {{}} by A68,PRALG_2:4;
then reconsider E = {} as Element of Args(o,OAF.i)
by TARSKI:def 1;
set F = bind (B,i,j);
A78: Args(o,OAF.j) = {{}} by A68,PRALG_2:4;
bind (B,i,j) is_homomorphism OAF.i,OAF.j by A13,Th2;
then
A79: (F.the_result_sort_of o).(x1.i) = Den (o,OAF.j).(F#E)
by A77,MSUALG_3:def 7;
x1.j = Den (o,OAF.j).{} by A73;
hence thesis by A79,A78,TARSKI:def 1;
end;
end;
then x in { f where f is Element of product Carrier (OAF,
the_result_sort_of o) : for i,j st i >= j holds (bind (B,i,j).(
the_result_sort_of o)). (f.i) = f.j } by A10;
hence x in C.the_result_sort_of o by A1;
end;
then x in C.the_result_sort_of o;
then
A80: x in C.((the ResultSort of S).o) by MSUALG_1:def 2;
dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
hence thesis by A80,FUNCT_1:13;
end;
hence thesis by MSUALG_2:def 5;
end;
then
A81: C is opers_closed by MSUALG_2:def 6;
reconsider C as MSSubset of L;
set MSA = L|C;
A82: MSA = MSAlgebra (#C, Opers(L,C)#) by A81,MSUALG_2:def 15;
now
let s be SortSymbol of S;
let f be Element of (SORTS OAF).s;
A83: f is Element of product Carrier(OAF,s) by PRALG_2:def 10;
thus f in (the Sorts of MSA).s iff for i,j st i >= j holds (bind (B,i,j)
.s).(f.i) = f.j
proof
hereby
assume f in (the Sorts of MSA).s;
then f in { g where g is Element of product Carrier (OAF,s) : for i
,j st i >= j holds (bind (B,i,j).s).(g.i) = g.j } by A1,A82;
then ex k be Element of product Carrier (OAF,s) st k = f & for i,j
st i >= j holds (bind (B,i,j).s).(k.i) = k.j;
hence for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f.j;
end;
assume for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f.j;
then f in { h where h is Element of product Carrier (OAF,s) : for i,j
st i >= j holds (bind (B,i,j).s).(h.i) = h.j } by A83;
hence thesis by A1,A82;
end;
end;
hence thesis;
end;
uniqueness
proof
let A1,A2 be strict MSSubAlgebra of product OAF such that
A84: for s be SortSymbol of S for f be Element of (SORTS OAF).s holds
f in (the Sorts of A1).s iff for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f
.j and
A85: for s be SortSymbol of S for f be Element of (SORTS OAF).s holds
f in (the Sorts of A2).s iff for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f
.j;
for s be object st s in the carrier of S holds (the Sorts of A1).s = (
the Sorts of A2).s
proof
let a be object;
assume a in the carrier of S;
then reconsider s = a as SortSymbol of S;
thus (the Sorts of A1).a c= (the Sorts of A2).a
proof
let e be object;
assume
A86: e in (the Sorts of A1).a;
(the Sorts of A1) is MSSubset of product OAF by MSUALG_2:def 9;
then (the Sorts of A1) c= the Sorts of product OAF by PBOOLE:def 18;
then (the Sorts of A1) c= SORTS OAF by PRALG_2:12;
then (the Sorts of A1).s c= (SORTS OAF).s by PBOOLE:def 2;
then reconsider f = e as Element of (SORTS OAF).s by A86;
for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f.j by A84,A86;
hence thesis by A85;
end;
let e be object;
assume
A87: e in (the Sorts of A2).a;
(the Sorts of A2) is MSSubset of product OAF by MSUALG_2:def 9;
then (the Sorts of A2) c= the Sorts of product OAF by PBOOLE:def 18;
then (the Sorts of A2) c= SORTS OAF by PRALG_2:12;
then (the Sorts of A2).s c= (SORTS OAF).s by PBOOLE:def 2;
then reconsider f = e as Element of (SORTS OAF).s by A87;
for i,j st i >= j holds (bind (B,i,j).s).(f.i) = f.j by A85,A87;
hence thesis by A84;
end;
hence thesis by MSUALG_2:9,PBOOLE:3;
end;
end;
theorem
for DP be discrete non empty Poset, S for OAF be OrderedAlgFam of DP,S
for B be normalized Binding of OAF holds InvLim B = product OAF
proof
let DP be discrete non empty Poset, S;
let OAF be OrderedAlgFam of DP,S;
let B be normalized Binding of OAF;
A1: for s be object st s in the carrier of S holds (the Sorts of InvLim B).s =
(the Sorts of product OAF).s
proof
let a be object;
assume a in the carrier of S;
then reconsider s = a as SortSymbol of S;
thus (the Sorts of InvLim B).a c= (the Sorts of product OAF).a
proof
let e be object;
(the Sorts of InvLim B) is MSSubset of product OAF by MSUALG_2:def 9;
then (the Sorts of InvLim B) c= the Sorts of product OAF by PBOOLE:def 18
;
then
A2: (the Sorts of InvLim B).s c= (the Sorts of product OAF).s by PBOOLE:def 2
;
assume e in (the Sorts of InvLim B).a;
hence thesis by A2;
end;
let e be object;
assume e in (the Sorts of product OAF).a;
then reconsider f = e as Element of (SORTS OAF).s by PRALG_2:12;
for i,j be Element of DP st i >= j holds (bind (B,i,j).s).(f.i) = f.j
proof
let i,j be Element of DP;
assume i >= j;
then
A3: i = j by ORDERS_3:1;
f in (SORTS OAF).s;
then dom (Carrier (OAF,s)) = the carrier of DP & f in product Carrier (
OAF,s) by PARTFUN1:def 2,PRALG_2:def 10;
then
A4: f.i in (Carrier (OAF,s)).i by CARD_3:9;
bind (B,i,i) = B.(i,i) by Def3,ORDERS_2:1
.= id (the Sorts of OAF.i) by Def4; then
A5: (bind (B,i,i).s) = id ((the Sorts of OAF.i).s) by MSUALG_3:def 1;
ex U0 being MSAlgebra over S st U0 = OAF.i & (Carrier ( OAF,s)).i =
((the Sorts of U0).s) by PRALG_2:def 9;
hence thesis by A3,A5,A4,FUNCT_1:18;
end;
hence thesis by Def6;
end;
product OAF is MSSubAlgebra of product OAF by MSUALG_2:5;
hence thesis by A1,MSUALG_2:9,PBOOLE:3;
end;
begin :: Sets and Morphisms of Many Sorted Signatures
reserve x for set,
A for non empty set;
definition
let X be set;
attr X is MSS-membered means
:Def7:
x in X implies x is strict non empty non void ManySortedSign;
end;
registration
cluster non empty MSS-membered for set;
existence
proof
set S = the strict non empty non void ManySortedSign;
set A = {S};
for x be set st x in A holds x is strict non empty non void
ManySortedSign by TARSKI:def 1;
then A is MSS-membered;
hence thesis;
end;
end;
registration
cluster strict empty void for ManySortedSign;
existence
proof
dom ({} --> {}) = {} & rng ({} --> {}) = {};
then reconsider g = {} --> {} as Function of {},{} by RELSET_1:4;
{} in {}* by FINSEQ_1:49;
then reconsider f = {}-->{} as Function of {},{}* by FUNCOP_1:46;
take ManySortedSign(#{},{},f,g#);
thus thesis;
end;
end;
Lm1: for S be empty void ManySortedSign holds id the carrier of S, id the
carrier' of S form_morphism_between S,S
proof
let S be empty void ManySortedSign;
set f = id the carrier of S;
{}*the ResultSort of S = (the ResultSort of S)*{} & for o be set, p be
Function st o in the carrier' of S & p = (the Arity of S).o holds f*p = (the
Arity of S).(f.o);
hence thesis by PUA2MSS1:def 12,RELAT_1:38;
end;
Lm2: for S be non empty void ManySortedSign holds id the carrier of S, id the
carrier' of S form_morphism_between S,S
proof
let S be non empty void ManySortedSign;
set f = id the carrier of S, g = id the carrier' of S;
A1: rng f c= the carrier of S & rng g c= the carrier' of S;
A2: f*the ResultSort of S = {} & (the ResultSort of S)*g = {};
A3: for o be set, p be Function st o in the carrier' of S & p = (the Arity
of S).o holds f*p = (the Arity of S).(g.o);
dom f = the carrier of S & dom g = the carrier' of S;
hence thesis by A1,A2,A3,PUA2MSS1:def 12;
end;
theorem
for S be void ManySortedSign holds id the carrier of S, id the
carrier' of S form_morphism_between S,S
proof
let S be void ManySortedSign;
per cases;
suppose
S is empty;
hence thesis by Lm1;
end;
suppose
S is non empty;
hence thesis by Lm2;
end;
end;
definition
::$CD
let A;
func MSS_set A -> set means
:Def8:
for x being object holds x in it iff ex S be strict non empty non void
ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A;
existence
proof
defpred P[object,object] means
ex S be strict non empty non void ManySortedSign
st S = $2 & $1 = [the carrier of S, the carrier' of S, the Arity of S, the
ResultSort of S];
A1: for x,y,z be object st P[x,y] & P[x,z] holds y = z
proof
let x,y,z be object;
assume ( P[x,y])& P[x,z];
then consider
S1, S2 be strict non empty non void ManySortedSign such that
A2: S1 = y and
A3: x = [the carrier of S1, the carrier' of S1, the Arity of S1, the
ResultSort of S1] and
A4: S2 = z and
A5: x = [the carrier of S2, the carrier' of S2, the Arity of S2, the
ResultSort of S2] and
S2 is empty implies S2 is void;
A6: the Arity of S1 = the Arity of S2 by A3,A5,XTUPLE_0:5;
the carrier of S1 = the carrier of S2 & the carrier' of S1 = the
carrier' of S2 by A3,A5,XTUPLE_0:5;
hence thesis by A2,A3,A4,A5,A6,XTUPLE_0:5;
end;
consider X be set such that
A7: for x being object holds x in X iff
ex y be object st y in [:bool A, bool A,
PFuncs(A,A*), PFuncs(A,A):] & P[y,x] from TARSKI:sch 1 (A1);
take X;
let x be object;
thus x in X iff ex S be strict non empty non void ManySortedSign st x = S
& the carrier of S c= A & the carrier' of S c= A
proof
thus x in X implies ex S be strict non empty non void ManySortedSign st
x = S & the carrier of S c= A & the carrier' of S c= A
proof
assume x in X;
then consider y be object such that
A8: y in [:bool A, bool A, PFuncs(A,A*), PFuncs(A,A):] and
A9: P[y,x] by A7;
consider S be strict non empty non void ManySortedSign such that
A10: S = x and
y = [the carrier of S, the carrier' of S, the Arity of S, the
ResultSort of S] by A9;
take S;
the carrier of S in bool A & the carrier' of S in bool A by A8,A9,A10,
MCART_1:80;
hence thesis by A10;
end;
given S be strict non empty non void ManySortedSign such that
A11: x = S and
A12: the carrier of S c= A and
A13: the carrier' of S c= A;
dom the ResultSort of S = the carrier' of S & rng the ResultSort of
S c= A by A12,FUNCT_2:def 1;
then
A14: the ResultSort of S in PFuncs (A,A) by A13,PARTFUN1:def 3;
reconsider C = the carrier of S as Subset of A by A12;
consider y be set such that
A15: y = [the carrier of S,the carrier' of S,the Arity of S, the
ResultSort of S];
C* c= A* by MSUHOM_1:2;
then
A16: rng the Arity of S c= A*;
dom the Arity of S c= A by A13;
then the Arity of S in PFuncs (A,A*) by A16,PARTFUN1:def 3;
then y in [:bool A, bool A, PFuncs(A,A*), PFuncs(A,A):] by A12,A13,A15
,A14,MCART_1:80;
hence thesis by A7,A11,A15;
end;
end;
uniqueness
proof
let A1, A2 be set such that
A17: for x being object holds
x in A1 iff ex S be strict non empty non void ManySortedSign st x
= S & the carrier of S c= A & the carrier' of S c= A and
A18: for x being object holds
x in A2 iff ex S be strict non empty non void ManySortedSign st x
= S & the carrier of S c= A & the carrier' of S c= A;
thus A1 c= A2
proof
let x be object;
assume x in A1;
then ex S be strict non empty non void ManySortedSign st x = S & the
carrier of S c= A & the carrier' of S c= A by A17;
hence thesis by A18;
end;
thus A2 c= A1
proof
let x be object;
assume x in A2;
then ex S be strict non empty non void ManySortedSign st x = S & the
carrier of S c= A & the carrier' of S c= A by A18;
hence thesis by A17;
end;
end;
end;
registration
let A;
cluster MSS_set A -> non empty MSS-membered;
coherence
proof
set X = MSS_set A;
set a = the Element of A;
dom ({a} --> a) = {a} & rng ({a} --> a) c= {a} by FUNCOP_1:13;
then reconsider g = {a} --> a as Function of {a},{a} by FUNCT_2:2;
a in {a} by TARSKI:def 1;
then <*a*> in {a}* by FUNCT_7:18;
then reconsider f = {a}--><*a*> as Function of {a},{a}* by FUNCOP_1:46;
A1: {a} c= A by ZFMISC_1:31;
ManySortedSign(#{a},{a},f,g#) in X
proof
set SI = ManySortedSign(#{a},{a},f,g#);
SI is non void non empty;
hence thesis by A1,Def8;
end;
hence X is non empty;
thus X is MSS-membered
proof
let x be set;
assume x in X;
then ex S be strict non empty non void ManySortedSign st x = S & the
carrier of S c= A & the carrier' of S c= A by Def8;
hence thesis;
end;
end;
end;
definition
let A be non empty MSS-membered set;
redefine mode Element of A -> strict non empty non void ManySortedSign; :: redefines Element (SUBSET_1, definition)
coherence by Def7;
end;
definition
let S1,S2 be ManySortedSign;
func MSS_morph (S1,S2) -> set means
x in it iff ex f,g be Function st x = [f,g] & f
,g form_morphism_between S1,S2;
existence
proof
defpred P[object] means ex f,g be Function st $1 = [f,g] & f,g
form_morphism_between S1,S2;
consider X be set such that
A1: for x being object holds
x in X iff x in [:PFuncs (the carrier of S1, the carrier of S2),
PFuncs (the carrier' of S1, the carrier' of S2):] & P[x] from XBOOLE_0:sch 1;
take X;
thus x in X iff ex f,g be Function st x = [f,g] & f,g
form_morphism_between S1,S2
proof
thus x in X implies ex f,g be Function st x = [f,g] & f,g
form_morphism_between S1,S2 by A1;
given f,g be Function such that
A2: x = [f,g] and
A3: f,g form_morphism_between S1,S2;
dom g = the carrier' of S1 & rng g c= the carrier' of S2 by A3,
PUA2MSS1:def 12;
then
A4: g in PFuncs (the carrier' of S1, the carrier' of S2) by PARTFUN1:def 3;
dom f = the carrier of S1 & rng f c= the carrier of S2 by A3,
PUA2MSS1:def 12;
then f in PFuncs (the carrier of S1, the carrier of S2) by PARTFUN1:def 3
;
then x in [:PFuncs (the carrier of S1, the carrier of S2), PFuncs (the
carrier' of S1, the carrier' of S2):] by A2,A4,ZFMISC_1:87;
hence thesis by A1,A2,A3;
end;
end;
uniqueness
proof
let A1,A2 be set;
assume that
A5: x in A1 iff ex f,g be Function st x = [f,g] & f,g
form_morphism_between S1,S2 and
A6: x in A2 iff ex f,g be Function st x = [f,g] & f,g
form_morphism_between S1,S2;
A7: A2 c= A1
proof
let x be object;
assume x in A2;
then ex f,g be Function st x = [f,g] & f,g form_morphism_between S1,S2
by A6;
hence thesis by A5;
end;
A1 c= A2
proof
let x be object;
assume x in A1;
then ex f,g be Function st x = [f,g] & f,g form_morphism_between S1,S2
by A5;
hence thesis by A6;
end;
hence A1 = A2 by A7;
end;
end;