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

theorem Th1: :: MSUALG_8:1

for n being 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{ F₁() -> Element of NAT , P₁[ object , object ] } :

ex p being FinSequence st
( dom p = Seg F₁() & ( for k being Element of NAT st k in Seg F₁() holds
P₁[k,p . k] ) )

provided

A1: for k being Element of NAT st k in Seg F₁() holds
ex x being object st P₁[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 Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) )

proof end;

:: 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 b₁ being Subset of (EqRelLatt (M . i)) holds
( b₁ = EqRelSet (,) iff for x being set holds
( x in b₁ 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 b₅ being Subset of (EqRelLatt (M . i)) holds
( b₅ = EqRelSet (X,i) iff for x being set holds
( x in b₅ 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;