:: More on the Lattice of Congruences in a Many Sorted Algebra
:: by Robert Milewski
::
:: Received March 6, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

theorem Th1: :: MSUALG_8:1
for n being Element of NAT
for p being FinSequence holds
( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) )
proof end;

scheme :: MSUALG_8:sch 1
NonUniqSeqEx{ F1() -> Element of NAT , P1[ set , set ] } :
ex p being FinSequence st
( dom p = Seg F1() & ( for k being Element of NAT st k in Seg F1() holds
P1[k,p . k] ) )
provided
A1: for k being Element of NAT st k in Seg F1() holds
ex x being set st P1[k,x]
proof end;

theorem Th2: :: MSUALG_8:2
for Y being set
for a, b being Element of (EqRelLatt Y)
for A, B being Equivalence_Relation of Y st a = A & b = B holds
( a [= b iff A c= B )
proof end;

registration
let Y be set ;
cluster EqRelLatt Y -> bounded ;
coherence
EqRelLatt Y is bounded
proof end;
end;

theorem :: MSUALG_8:3
for Y being set holds Bottom (EqRelLatt Y) = id Y
proof end;

theorem :: MSUALG_8:4
for Y being set holds Top (EqRelLatt Y) = nabla Y
proof end;

theorem Th5: :: MSUALG_8:5
for Y being set holds EqRelLatt Y is complete
proof end;

registration
let Y be set ;
cluster EqRelLatt Y -> complete ;
coherence
EqRelLatt Y is complete by Th5;
end;

theorem Th6: :: MSUALG_8:6
for Y being set
for X being Subset of (EqRelLatt Y) holds union X is Relation of Y
proof end;

theorem Th7: :: MSUALG_8:7
for Y being set
for X being Subset of (EqRelLatt Y) holds union X c= "\/" X
proof end;

theorem Th8: :: MSUALG_8:8
for Y being set
for X being Subset of (EqRelLatt Y)
for R being Relation of Y st R = union X holds
"\/" X = EqCl R
proof end;

theorem Th9: :: MSUALG_8:9
for Y being set
for X being Subset of (EqRelLatt Y)
for R being Relation st R = union X holds
R = R ~
proof end;

theorem Th10: :: MSUALG_8:10
for x, y, Y being set
for X being Subset of (EqRelLatt Y) st x in Y & y in Y holds
( [x,y] in "\/" X iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) )
proof end;

begin

:: of Lattice of Many Sorted Equivalence Relations Inheriting Sups and Infs
theorem Th11: :: MSUALG_8:11
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A
proof end;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let E be Element of (EqRelLatt the Sorts of A);
func CongrCl E -> MSCongruence of A equals :: MSUALG_8:def 1
 "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A));
coherence
"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A
proof end;
end;

:: deftheorem defines CongrCl MSUALG_8:def 1 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for E being Element of (EqRelLatt the Sorts of A) holds CongrCl E = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A));

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let X be Subset of (EqRelLatt the Sorts of A);
func CongrCl X -> MSCongruence of A equals :: MSUALG_8:def 2
 "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A));
coherence
"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A
proof end;
end;

:: deftheorem defines CongrCl MSUALG_8:def 2 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl X = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A));

theorem :: MSUALG_8:12
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds
CongrCl C = C
proof end;

theorem :: MSUALG_8:13
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X
proof end;

theorem :: MSUALG_8:14
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for B1, B2 being Subset of (CongrLatt A)
for C1, C2 being MSCongruence of A st C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) holds
C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A))
proof end;

theorem :: MSUALG_8:15
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A))
proof end;

theorem Th16: :: MSUALG_8:16
for I being non empty set
for M being ManySortedSet of I
for i being Element of I
for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st
( E . i = e & ( for j being Element of I st j <> i holds
E . j = nabla (M . j) ) )
proof end;

notation
let I be non empty set ;
let M be ManySortedSet of I;
let i be Element of I;
let X be Subset of (EqRelLatt M);
synonym EqRelSet (X,i) for pi (M,I);
end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
let i be Element of I;
let X be Subset of (EqRelLatt M);
:: original: EqRelSet
redefine func EqRelSet (X,i) -> Subset of (EqRelLatt (M . i)) means :Def3: :: MSUALG_8:def 3
 for x being set holds
( x in it iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) );
coherence
EqRelSet (,) is Subset of (EqRelLatt (M . i))
proof end;
compatibility
for b1 being Subset of (EqRelLatt (M . i)) holds
( b1 = EqRelSet (,) iff for x being set holds
( x in b1 iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) )
proof end;
end;

:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :
for I being non empty set
for M being ManySortedSet of I
for i being Element of I
for X being Subset of (EqRelLatt M)
for b5 being Subset of (EqRelLatt (M . i)) holds
( b5 = EqRelSet (X,i) iff for x being set holds
( x in b5 iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) );

theorem Th17: :: MSUALG_8:17
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for i being Element of S
for X being Subset of (EqRelLatt the Sorts of A)
for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds
B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))
proof end;

theorem Th18: :: MSUALG_8:18
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A
proof end;

theorem Th19: :: MSUALG_8:19
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds CongrLatt A is /\-inheriting
proof end;

theorem Th20: :: MSUALG_8:20
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds CongrLatt A is \/-inheriting
proof end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster CongrLatt A -> /\-inheriting \/-inheriting ;
coherence
( CongrLatt A is /\-inheriting & CongrLatt A is \/-inheriting ) by Th19, Th20;
end;