:: Inverse Limits of Many Sorted Algebras
:: by Adam Grabowski
::
:: Received June 11, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

registration
let I be non empty set ;
let S be non empty non void ManySortedSign ;
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 ->  Relation-like Function-like ;
coherence
 ( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like )
proofend;
end;

registration
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
let s be SortSymbol of S;
cluster(SORTS AF) . s ->  functional ;
coherence
 (SORTS AF) . s is functional
proofend;
end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
mode OrderedAlgFam of P,S ->  MSAlgebra-Family of the carrier of P,S means :Def1: :: MSALIMIT:def 1
 ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (it . i),(it . j) ex f2 being 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
 ex b1 being MSAlgebra-Family of the carrier of P,S ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (b1 . i),(b1 . j) ex f2 being ManySortedFunction of (b1 . j),(b1 . k) st
( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b1 . i,b1 . j )
proofend;
end;

:: deftheorem Def1 defines OrderedAlgFam MSALIMIT:def_1_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of the carrier of P,S holds
( b3 is OrderedAlgFam of P,S iff ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (b3 . i),(b3 . j) ex f2 being ManySortedFunction of (b3 . j),(b3 . k) st
( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b3 . i,b3 . j ) );

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
mode Binding of OAF ->  ManySortedFunction of the InternalRel of P means :Def2: :: MSALIMIT:def 2
 for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being 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
 ex b1 being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = b1 . (j,i) & f2 = b1 . (k,j) & b1 . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by Def1;
end;

:: deftheorem Def2 defines Binding MSALIMIT:def_2_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for b4 being ManySortedFunction of the InternalRel of P holds
( b4 is Binding of OAF iff for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = b4 . (j,i) & f2 = b4 . (k,j) & b4 . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) );

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
let i, j be Element of P;
assume A1: i >= j ;
func bind (B,i,j) ->  ManySortedFunction of (OAF . i),(OAF . j) equals :Def3: :: MSALIMIT:def 3
B . (j,i);
coherence
 B . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)
proofend;
end;

:: deftheorem Def3 defines bind MSALIMIT:def_3_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
bind (B,i,j) = B . (j,i);

theorem Th1: :: MSALIMIT:1
for P being non empty Poset
for i, j, k being Element of P
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)
proofend;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let IT be Binding of OAF;
attrIT is normalized  means :Def4: :: MSALIMIT:def 4
 for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i);
end;

:: deftheorem Def4 defines normalized MSALIMIT:def_4_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for IT being Binding of OAF holds
( IT is normalized iff for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i) );

theorem Th2: :: MSALIMIT:2
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j
proofend;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
func Normalized B ->  Binding of OAF means :Def5: :: MSALIMIT:def 5
 for i, j being Element of P 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
 ex b1 being Binding of OAF st
for i, j being Element of P st i >= j holds
b1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))))
proofend;
uniqueness
 for b1, b2 being Binding of OAF st ( for i, j being Element of P st i >= j holds
b1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) & ( for i, j being Element of P st i >= j holds
b2 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines Normalized MSALIMIT:def_5_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B, b5 being Binding of OAF holds
( b5 = Normalized B iff for i, j being Element of P st i >= j holds
b5 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) );

theorem Th3: :: MSALIMIT:3
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j &amp; i <> j holds
B . (j,i) = (Normalized B) . (j,i)
proofend;

registration
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
cluster Normalized B ->  normalized ;
coherence
 Normalized B is normalized
proofend;
end;

registration
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
cluster Relation-like the InternalRel of P -defined Function-like total Function-yielding V42() normalized for Binding of OAF;
existence
 ex b1 being Binding of OAF st b1 is normalized
proofend;
end;

theorem :: MSALIMIT:4
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
(Normalized NB) . (j,i) = NB . (j,i)
proofend;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
func InvLim B ->  strict MSSubAlgebra of product OAF means :Def6: :: MSALIMIT:def 6
 for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of it . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j );
existence
 ex b1 being strict MSSubAlgebra of product OAF st
for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )
proofend;
uniqueness
 for b1, b2 being strict MSSubAlgebra of product OAF st ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) &amp; ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b2 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines InvLim MSALIMIT:def_6_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for b5 being strict MSSubAlgebra of product OAF holds
( b5 = InvLim B iff for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b5 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) );

theorem :: MSALIMIT:5
for DP being non empty discrete Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of DP,S
for B being normalized Binding of OAF holds InvLim B = product OAF
proofend;

begin

definition
let X be set ;
attrX is MSS-membered  means :Def7: :: MSALIMIT:def 7
 for x being set st x in X holds
x is non empty non void strict ManySortedSign ;
end;

:: deftheorem Def7 defines MSS-membered MSALIMIT:def_7_:_
 for X being set holds
( X is MSS-membered iff for x being set st x in X holds
x is non empty non void strict ManySortedSign );

registration
cluster non empty MSS-membered for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is MSS-membered )
proofend;
end;

definition
func TrivialMSSign  ->  strict ManySortedSign  means :Def8: :: MSALIMIT:def 8
( it is empty &amp; it is void );
existence
 ex b1 being strict ManySortedSign st
( b1 is empty &amp; b1 is void )
proofend;
uniqueness
 for b1, b2 being strict ManySortedSign st b1 is empty &amp; b1 is void &amp; b2 is empty &amp; b2 is void holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines TrivialMSSign MSALIMIT:def_8_:_
 for b1 being strict ManySortedSign holds
( b1 = TrivialMSSign iff ( b1 is empty &amp; b1 is void ) );

registration
cluster TrivialMSSign  ->  empty void strict ;
coherence
 ( TrivialMSSign is empty &amp; TrivialMSSign is void ) by Def8;
end;

registration
cluster empty void strict for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( b1 is strict &amp; b1 is empty &amp; b1 is void )
proofend;
end;

Lm1:  for S being empty void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proofend;

Lm2:  for S being non empty void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proofend;

theorem :: MSALIMIT:6
for S being void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proofend;

definition
let A be non empty set ;
func MSS_set A ->  set  means :Def9: :: MSALIMIT:def 9
 for x being set holds
( x in it iff ex S being non empty non void strict ManySortedSign st
( x = S &amp; the carrier of S c= A &amp; the carrier' of S c= A ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex S being non empty non void strict ManySortedSign st
( x = S &amp; the carrier of S c= A &amp; the carrier' of S c= A ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex S being non empty non void strict ManySortedSign st
( x = S &amp; the carrier of S c= A &amp; the carrier' of S c= A ) ) ) &amp; ( for x being set holds
( x in b2 iff ex S being non empty non void strict ManySortedSign st
( x = S &amp; the carrier of S c= A &amp; the carrier' of S c= A ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines MSS_set MSALIMIT:def_9_:_
 for A being non empty set
for b2 being set holds
( b2 = MSS_set A iff for x being set holds
( x in b2 iff ex S being non empty non void strict ManySortedSign st
( x = S &amp; the carrier of S c= A &amp; the carrier' of S c= A ) ) );

registration
let A be non empty set ;
cluster MSS_set A ->  non empty MSS-membered ;
coherence
 ( not MSS_set A is empty &amp; MSS_set A is MSS-membered )
proofend;
end;

definition
let A be non empty MSS-membered set ;
:: original:Element
redefine mode Element of A ->  non empty non void strict ManySortedSign ;
coherence
 for b1 being Element of A holds b1 is non empty non void strict ManySortedSign by Def7;
end;

definition
let S1, S2 be ManySortedSign ;
func MSS_morph (S1,S2) ->  set  means :: MSALIMIT:def 10
 for x being set holds
( x in it iff ex f, g being Function st
( x = [f,g] &amp; f,g form_morphism_between S1,S2 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f, g being Function st
( x = [f,g] &amp; f,g form_morphism_between S1,S2 ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f, g being Function st
( x = [f,g] &amp; f,g form_morphism_between S1,S2 ) ) ) &amp; ( for x being set holds
( x in b2 iff ex f, g being Function st
( x = [f,g] &amp; f,g form_morphism_between S1,S2 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines MSS_morph MSALIMIT:def_10_:_
 for S1, S2 being ManySortedSign
for b3 being set holds
( b3 = MSS_morph (S1,S2) iff for x being set holds
( x in b3 iff ex f, g being Function st
( x = [f,g] &amp; f,g form_morphism_between S1,S2 ) ) );