MSUALG_5: Lattice of Congruences in a Many Sorted Algebra

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

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 by EQREL_1:12;
uniqueness

proof end;

end;

:: deftheorem Def1 defines EqCl MSUALG_5:def 1 :

theorem Th1: :: MSUALG_5:1

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

proof end;

theorem Th2: :: MSUALG_5:2

for X being set
for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines EqRelLatt MSUALG_5:def 2 :

:: MANY SORTED EQUIVALENCE RELATIONS ::

registration

let I be set ;
let M be ManySortedSet of I;

cluster Relation-like I -defined Function-like total V101() MSEquivalence_Relation-like for ManySortedRelation of M,M;

existence

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines EqCl MSUALG_5:def 3 :

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

proof end;

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

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

proof end;

uniqueness ;
commutativity ;

end;

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

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

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

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

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

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)

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

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

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

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines EqRelLatt MSUALG_5:def 5 :

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

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

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

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines CongrLatt MSUALG_5:def 6 :

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

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

proof end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;

cluster CongrLatt A -> strict bounded ;

coherence

proof end;

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

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

proof end;

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

proof end;