:: Lattice of Congruences in a Many Sorted Algebra
:: by Robert Milewski
::
:: Received January 11, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let X be set ;
let R be Relation of X;
func EqCl R ->  Equivalence_Relation of X means :Def1: :: MSUALG_5:def 1
( R c= it & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
it c= EqR2 ) );
existence
 ex b1 being Equivalence_Relation of X st
( R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b1 c= EqR2 ) ) by EQREL_1:12;
uniqueness
 for b1, b2 being Equivalence_Relation of X st R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b1 c= EqR2 ) & R c= b2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b2 c= EqR2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines EqCl MSUALG_5:def_1_:_
 for X being set
for R being Relation of X
for b3 being Equivalence_Relation of X holds
( b3 = EqCl R iff ( R c= b3 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b3 c= EqR2 ) ) );

theorem Th1: :: MSUALG_5:1
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
proofend;

theorem Th2: :: MSUALG_5:2
for X being set
for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1
proofend;

begin

:: LATTICE OF EQUIVALENCE RELATIONS ::
definition
let X be set ;
func EqRelLatt X ->  strict Lattice means :Def2: :: MSUALG_5:def 2
( the carrier of it =  {  x where x is Relation of X,X : x is Equivalence_Relation of X  }  & ( for x, y being Equivalence_Relation of X holds
( the L_meet of it . (x,y) = x /\ y & the L_join of it . (x,y) = x "\/" y ) ) );
existence
 ex b1 being strict Lattice st
( the carrier of b1 =  {  x where x is Relation of X,X : x is Equivalence_Relation of X  }  & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) )
proofend;
uniqueness
 for b1, b2 being strict Lattice st the carrier of b1 =  {  x where x is Relation of X,X : x is Equivalence_Relation of X  }  & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & the carrier of b2 =  {  x where x is Relation of X,X : x is Equivalence_Relation of X  }  & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines EqRelLatt MSUALG_5:def_2_:_
 for X being set
for b2 being strict Lattice holds
( b2 = EqRelLatt X iff ( the carrier of b2 =  {  x where x is Relation of X,X : x is Equivalence_Relation of X  }  & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) ) );

begin

:: MANY SORTED EQUIVALENCE RELATIONS ::
registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like I -defined Function-like total V95() MSEquivalence_Relation-like for ManySortedRelation of M,M;
existence
 ex b1 being ManySortedRelation of M st b1 is MSEquivalence_Relation-like
proofend;
end;

definition
let I be set ;
let M be ManySortedSet of I;
mode Equivalence_Relation of M is MSEquivalence_Relation-like ManySortedRelation of M;
end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
let R be ManySortedRelation of M;
func EqCl R ->  Equivalence_Relation of M means :Def3: :: MSUALG_5:def 3
 for i being Element of I holds it . i = EqCl (R . i);
existence
 ex b1 being Equivalence_Relation of M st
for i being Element of I holds b1 . i = EqCl (R . i)
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of M st ( for i being Element of I holds b1 . i = EqCl (R . i) ) & ( for i being Element of I holds b2 . i = EqCl (R . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines EqCl MSUALG_5:def_3_:_
 for I being non empty set
for M being ManySortedSet of I
for R being ManySortedRelation of M
for b4 being Equivalence_Relation of M holds
( b4 = EqCl R iff for i being Element of I holds b4 . i = EqCl (R . i) );

theorem :: MSUALG_5:3
for I being non empty set
for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqCl EqR = EqR
proofend;

begin

:: LATTICE OF MANY SORTED EQUIVALENCE RELATIONS ::
definition
let I be non empty set ;
let M be ManySortedSet of I;
let EqR1, EqR2 be Equivalence_Relation of M;
funcEqR1 "\/" EqR2 ->  Equivalence_Relation of M means :Def4: :: MSUALG_5:def 4
 ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & it = EqCl EqR3 );
existence
 ex b1 being Equivalence_Relation of M ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) & ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b2 = EqCl EqR3 ) holds
b1 = b2 ;
commutativity
 for b1, EqR1, EqR2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) holds
ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR2 \/ EqR1 & b1 = EqCl EqR3 ) ;
end;

:: deftheorem Def4 defines "\/" MSUALG_5:def_4_:_
 for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, b5 being Equivalence_Relation of M holds
( b5 = EqR1 "\/" EqR2 iff ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b5 = EqCl EqR3 ) );

theorem Th4: :: MSUALG_5:4
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2
proofend;

theorem Th5: :: MSUALG_5:5
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR
proofend;

theorem Th6: :: MSUALG_5:6
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR3 c= EqR ) holds
EqR3 = EqR1 "\/" EqR2
proofend;

theorem :: MSUALG_5:7
for I being non empty set
for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR
proofend;

theorem Th8: :: MSUALG_5:8
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proofend;

theorem Th9: :: MSUALG_5:9
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
proofend;

theorem Th10: :: MSUALG_5:10
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds
EqR1 "\/" EqR = EqR1
proofend;

theorem Th11: :: MSUALG_5:11
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M
proofend;

definition
let I be non empty set ;
let M be ManySortedSet of I;
func EqRelLatt M ->  strict Lattice means :Def5: :: MSUALG_5:def 5
( ( for x being set holds
( x in the carrier of it iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of it . (x,y) = x /\ y & the L_join of it . (x,y) = x "\/" y ) ) );
existence
 ex b1 being strict Lattice st
( ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) )
proofend;
uniqueness
 for b1, b2 being strict Lattice st ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & ( for x being set holds
( x in the carrier of b2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines EqRelLatt MSUALG_5:def_5_:_
 for I being non empty set
for M being ManySortedSet of I
for b3 being strict Lattice holds
( b3 = EqRelLatt M iff ( ( for x being set holds
( x in the carrier of b3 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b3 . (x,y) = x /\ y & the L_join of b3 . (x,y) = x "\/" y ) ) ) );

begin

:: LATTICE OF CONGRUENCES IN A MANY SORTED ALGEBRA ::
registration
let S be non empty ManySortedSign ;
let A be MSAlgebra over S;
cluster MSEquivalence-like  ->  MSEquivalence_Relation-like for ManySortedRelation of the Sorts of A, the Sorts of A;
coherence
 for b1 being ManySortedRelation of A st b1 is MSEquivalence-like holds
b1 is MSEquivalence_Relation-like by MSUALG_4:def_3;
end;

theorem Th12: :: MSUALG_5:12
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 &amp; y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
proofend;

theorem Th13: :: MSUALG_5:13
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n &amp; len a1 = len a2 &amp; ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) &amp; [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) &amp; [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
proofend;

theorem Th14: :: MSUALG_5:14
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
proofend;

theorem Th15: :: MSUALG_5:15
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A
proofend;

theorem Th16: :: MSUALG_5:16
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A
proofend;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
func CongrLatt A ->  strict SubLattice of EqRelLatt the Sorts of A means :Def6: :: MSUALG_5:def 6
 for x being set holds
( x in the carrier of it iff x is MSCongruence of A );
existence
 ex b1 being strict SubLattice of EqRelLatt the Sorts of A st
for x being set holds
( x in the carrier of b1 iff x is MSCongruence of A )
proofend;
uniqueness
 for b1, b2 being strict SubLattice of EqRelLatt the Sorts of A st ( for x being set holds
( x in the carrier of b1 iff x is MSCongruence of A ) ) &amp; ( for x being set holds
( x in the carrier of b2 iff x is MSCongruence of A ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines CongrLatt MSUALG_5:def_6_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for b3 being strict SubLattice of EqRelLatt the Sorts of A holds
( b3 = CongrLatt A iff for x being set holds
( x in the carrier of b3 iff x is MSCongruence of A ) );

theorem Th17: :: MSUALG_5:17
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds id the Sorts of A is MSCongruence of A
proofend;

theorem Th18: :: MSUALG_5:18
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds [| the Sorts of A, the Sorts of A|] is MSCongruence of A
proofend;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster CongrLatt A ->  strict bounded ;
coherence
 CongrLatt A is bounded
proofend;
end;

theorem :: MSUALG_5:19
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds Bottom (CongrLatt A) = id the Sorts of A
proofend;

theorem :: MSUALG_5:20
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]
proofend;

:: from MSUALG_7, 2010.02.21, A.T
theorem :: MSUALG_5:21
for x, X being set holds
( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X )
proofend;