:: Inverse Limits of Many Sorted Algebras
:: by Adam Grabowski
::
:: Received June 11, 1996
:: Copyright (c) 1996-2016 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;
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;
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;
end;
definition
let P, S;
mode OrderedAlgFam of P,S -> MSAlgebra-Family of the carrier of P,S means
:: MSALIMIT:def 1
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;
end;
reserve OAF for OrderedAlgFam of P, S;
definition
let P, S, OAF;
mode Binding of OAF -> ManySortedFunction of the InternalRel of P means
:: MSALIMIT:def 2
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;
end;
definition
let P, S, OAF;
let B be Binding of OAF, i,j;
assume
i >= j;
func bind (B,i,j) -> ManySortedFunction of OAF.i, OAF.j equals
:: MSALIMIT:def 3
B.(j,i
);
end;
reserve B for Binding of OAF;
theorem :: MSALIMIT:1
i >= j & j >= k implies bind (B,j,k) ** bind (B,i,j) = bind (B,i, k);
definition
let P, S, OAF;
let IT be Binding of OAF;
attr IT is normalized means
:: MSALIMIT:def 4
for i holds IT.(i,i) = id (the Sorts of OAF.i);
end;
theorem :: MSALIMIT:2
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;
definition
let P, S, OAF, B;
func Normalized B -> Binding of OAF means
:: MSALIMIT:def 5
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) );
end;
theorem :: MSALIMIT:3
for i, j st i >= j & i <> j holds B.(j,i) = (Normalized B).(j,i);
registration
let P, S, OAF, B;
cluster Normalized B -> normalized;
end;
registration
let P, S, OAF;
cluster normalized for Binding of OAF;
end;
theorem :: MSALIMIT:4
for NB be normalized Binding of OAF for i, j st i >= j holds (
Normalized NB).(j,i) = NB.(j,i);
definition
let P, S, OAF;
let B be Binding of OAF;
func InvLim B -> strict MSSubAlgebra of product OAF means
:: MSALIMIT:def 6
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;
end;
theorem :: MSALIMIT:5
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;
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
:: MSALIMIT:def 7
x in X implies x is strict non empty non void ManySortedSign;
end;
registration
cluster non empty MSS-membered for set;
end;
registration
cluster strict empty void for ManySortedSign;
end;
theorem :: MSALIMIT:6
for S be void ManySortedSign holds id the carrier of S, id the
carrier' of S form_morphism_between S,S;
definition
::$CD
let A;
func MSS_set A -> set means
:: MSALIMIT:def 9
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;
end;
registration
let A;
cluster MSS_set A -> non empty MSS-membered;
end;
definition
let A be non empty MSS-membered set;
redefine mode Element of A -> strict non empty non void ManySortedSign;
end;
definition
let S1,S2 be ManySortedSign;
func MSS_morph (S1,S2) -> set means
:: MSALIMIT:def 10
x in it iff ex f,g be Function st x = [f,g] & f
,g form_morphism_between S1,S2;
end;