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


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 )
proof end;
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
proof end;
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 )
proof end;
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)
proof end;
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)
proof end;

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;
attr IT 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
proof end;

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))))
proof end;
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
proof end;
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 & i <> j holds
B . (j,i) = (Normalized B) . (j,i)
proof end;

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
proof end;
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 V45() normalized for Binding of OAF;
existence
ex b1 being Binding of OAF st b1 is normalized
proof end;
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)
proof end;

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 )
proof end;
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 ) ) & ( 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
proof end;
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
proof end;

definition
let X be set ;
attr X 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 & b1 is MSS-membered )
proof end;
end;

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

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

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

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

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

:: deftheorem MSALIMIT:def 8 :
canceled;

:: deftheorem Def8 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 object holds
( x in b2 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & 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 & MSS_set A is MSS-membered )
proof end;
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] & 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] & f,g form_morphism_between S1,S2 ) )
proof end;
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] & f,g form_morphism_between S1,S2 ) ) ) & ( for x being set holds
( x in b2 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) holds
b1 = b2
proof end;
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] & f,g form_morphism_between S1,S2 ) ) );