:: 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;

ex b_{1} being Equivalence_Relation of X st

( R c= b_{1} & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

b_{1} c= EqR2 ) )
by EQREL_1:12;

uniqueness

for b_{1}, b_{2} being Equivalence_Relation of X st R c= b_{1} & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

b_{1} c= EqR2 ) & R c= b_{2} & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

b_{2} c= EqR2 ) holds

b_{1} = b_{2}

end;
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 ( R c= it & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

it c= EqR2 ) );

ex b

( R c= b

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def1 defines EqCl MSUALG_5:def 1 :

for X being set

for R being Relation of X

for b_{3} being Equivalence_Relation of X holds

( b_{3} = EqCl R iff ( R c= b_{3} & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

b_{3} c= EqR2 ) ) );

for X being set

for R being Relation of X

for b

( b

b

theorem Th1: :: MSUALG_5:1

for X being set

for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)

for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)

proof end;

begin

:: LATTICE OF EQUIVALENCE RELATIONS ::

definition

let X be set ;

ex b_{1} being strict Lattice st

( the carrier of b_{1} = { 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 b_{1} . (x,y) = x /\ y & the L_join of b_{1} . (x,y) = x "\/" y ) ) )

for b_{1}, b_{2} being strict Lattice st the carrier of b_{1} = { 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 b_{1} . (x,y) = x /\ y & the L_join of b_{1} . (x,y) = x "\/" y ) ) & the carrier of b_{2} = { 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 b_{2} . (x,y) = x /\ y & the L_join of b_{2} . (x,y) = x "\/" y ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

( the L_meet of b

proof end;

uniqueness for b

( the L_meet of b

( the L_meet of b

b

proof end;

:: deftheorem Def2 defines EqRelLatt MSUALG_5:def 2 :

for X being set

for b_{2} being strict Lattice holds

( b_{2} = EqRelLatt X iff ( the carrier of b_{2} = { 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 b_{2} . (x,y) = x /\ y & the L_join of b_{2} . (x,y) = x "\/" y ) ) ) );

for X being set

for b

( b

( the L_meet of b

begin

:: MANY SORTED EQUIVALENCE RELATIONS ::

registration

let I be set ;

let M be ManySortedSet of I;

ex b_{1} being ManySortedRelation of M st b_{1} is MSEquivalence_Relation-like

end;
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 b

proof 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;
let M be ManySortedSet of I;

mode Equivalence_Relation of M is MSEquivalence_Relation-like ManySortedRelation of M;

definition

let I be non empty set ;

let M be ManySortedSet of I;

let R be ManySortedRelation of M;

ex b_{1} being Equivalence_Relation of M st

for i being Element of I holds b_{1} . i = EqCl (R . i)

for b_{1}, b_{2} being Equivalence_Relation of M st ( for i being Element of I holds b_{1} . i = EqCl (R . i) ) & ( for i being Element of I holds b_{2} . i = EqCl (R . i) ) holds

b_{1} = b_{2}

end;
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 for i being Element of I holds it . i = EqCl (R . i);

ex b

for i being Element of I holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Equivalence_Relation of M holds

( b_{4} = EqCl R iff for i being Element of I holds b_{4} . i = EqCl (R . i) );

for I being non empty set

for M being ManySortedSet of I

for R being ManySortedRelation of M

for b

( b

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

for M being ManySortedSet of I

for EqR being Equivalence_Relation of M holds EqCl EqR = EqR

proof end;

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;

ex b_{1} being Equivalence_Relation of M ex EqR3 being ManySortedRelation of M st

( EqR3 = EqR1 \/ EqR2 & b_{1} = EqCl EqR3 )

for b_{1}, b_{2} being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st

( EqR3 = EqR1 \/ EqR2 & b_{1} = EqCl EqR3 ) & ex EqR3 being ManySortedRelation of M st

( EqR3 = EqR1 \/ EqR2 & b_{2} = EqCl EqR3 ) holds

b_{1} = b_{2}
;

commutativity

for b_{1}, EqR1, EqR2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st

( EqR3 = EqR1 \/ EqR2 & b_{1} = EqCl EqR3 ) holds

ex EqR3 being ManySortedRelation of M st

( EqR3 = EqR2 \/ EqR1 & b_{1} = EqCl EqR3 )
;

end;
let M be ManySortedSet of I;

let EqR1, EqR2 be Equivalence_Relation of M;

func EqR1 "\/" 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 EqR3 being ManySortedRelation of M st

( EqR3 = EqR1 \/ EqR2 & it = EqCl EqR3 );

ex b

( EqR3 = EqR1 \/ EqR2 & b

proof end;

uniqueness for b

( EqR3 = EqR1 \/ EqR2 & b

( EqR3 = EqR1 \/ EqR2 & b

b

commutativity

for b

( EqR3 = EqR1 \/ EqR2 & b

ex EqR3 being ManySortedRelation of M st

( EqR3 = EqR2 \/ EqR1 & b

:: deftheorem Def4 defines "\/" MSUALG_5:def 4 :

for I being non empty set

for M being ManySortedSet of I

for EqR1, EqR2, b_{5} being Equivalence_Relation of M holds

( b_{5} = EqR1 "\/" EqR2 iff ex EqR3 being ManySortedRelation of M st

( EqR3 = EqR1 \/ EqR2 & b_{5} = EqCl EqR3 ) );

for I being non empty set

for M being ManySortedSet of I

for EqR1, EqR2, b

( b

( EqR3 = EqR1 \/ EqR2 & b

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

for M being ManySortedSet of I

for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2

proof end;

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

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

proof end;

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

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

proof end;

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

for M being ManySortedSet of I

for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR

proof end;

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)

for M being ManySortedSet of I

for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)

proof end;

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

for M being ManySortedSet of I

for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1

proof end;

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

for M being ManySortedSet of I

for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds

EqR1 "\/" EqR = EqR1

proof end;

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

for M being ManySortedSet of I

for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M

proof end;

definition

let I be non empty set ;

let M be ManySortedSet of I;

ex b_{1} being strict Lattice st

( ( for x being set holds

( x in the carrier of b_{1} iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of b_{1} . (x,y) = x /\ y & the L_join of b_{1} . (x,y) = x "\/" y ) ) )

for b_{1}, b_{2} being strict Lattice st ( for x being set holds

( x in the carrier of b_{1} iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of b_{1} . (x,y) = x /\ y & the L_join of b_{1} . (x,y) = x "\/" y ) ) & ( for x being set holds

( x in the carrier of b_{2} iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of b_{2} . (x,y) = x /\ y & the L_join of b_{2} . (x,y) = x "\/" y ) ) holds

b_{1} = b_{2}

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

ex b

( ( for x being set holds

( x in the carrier of b

( the L_meet of b

proof end;

uniqueness for b

( x in the carrier of b

( the L_meet of b

( x in the carrier of b

( the L_meet of b

b

proof end;

:: deftheorem Def5 defines EqRelLatt MSUALG_5:def 5 :

for I being non empty set

for M being ManySortedSet of I

for b_{3} being strict Lattice holds

( b_{3} = EqRelLatt M iff ( ( for x being set holds

( x in the carrier of b_{3} iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of b_{3} . (x,y) = x /\ y & the L_join of b_{3} . (x,y) = x "\/" y ) ) ) );

for I being non empty set

for M being ManySortedSet of I

for b

( b

( x in the carrier of b

( the L_meet of b

begin

:: LATTICE OF CONGRUENCES IN A MANY SORTED ALGEBRA ::

registration

let S be non empty ManySortedSign ;

let A be MSAlgebra over S;

for b_{1} being ManySortedRelation of A st b_{1} is MSEquivalence-like holds

b_{1} is MSEquivalence_Relation-like
by MSUALG_4:def 3;

end;
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 b

b

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 & 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))

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 & 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))

proof end;

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 & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [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)

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 & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds

[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [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)

proof end;

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)

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)

proof end;

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

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A

proof end;

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

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

ex b_{1} being strict SubLattice of EqRelLatt the Sorts of A st

for x being set holds

( x in the carrier of b_{1} iff x is MSCongruence of A )

for b_{1}, b_{2} being strict SubLattice of EqRelLatt the Sorts of A st ( for x being set holds

( x in the carrier of b_{1} iff x is MSCongruence of A ) ) & ( for x being set holds

( x in the carrier of b_{2} iff x is MSCongruence of A ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in the carrier of it iff x is MSCongruence of A );

ex b

for x being set holds

( x in the carrier of b

proof end;

uniqueness for b

( x in the carrier of b

( x in the carrier of b

b

proof 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 b_{3} being strict SubLattice of EqRelLatt the Sorts of A holds

( b_{3} = CongrLatt A iff for x being set holds

( x in the carrier of b_{3} iff x is MSCongruence of A ) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for b

( b

( x in the carrier of b

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

for A being non-empty MSAlgebra over S holds id the Sorts of A is MSCongruence of A

proof end;

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

for A being non-empty MSAlgebra over S holds [| the Sorts of A, the Sorts of A|] is MSCongruence of A

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

coherence

CongrLatt A is bounded

end;
let A be non-empty MSAlgebra over S;

coherence

CongrLatt A is bounded

proof 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

for A being non-empty MSAlgebra over S holds Bottom (CongrLatt A) = id the Sorts of A

proof end;

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|]

for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]

proof end;

:: from MSUALG_7, 2010.02.21, A.T