:: More on the Lattice of Congruences in a Many Sorted Algebra
:: by Robert Milewski
::
:: Received March 6, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PBOOLE, SUBSET_1, NUMBERS, FINSEQ_1, STRUCT_0,
MSUALG_1, RELAT_1, XXREAL_0, ARYTM_3, FUNCT_1, MSUALG_5, EQREL_1, TARSKI,
LATTICES, XXREAL_2, REWRITE1, LATTICE3, SETFAM_1, ZFMISC_1, CARD_1,
MSUALG_4, CLOSURE2, NAT_1, MARGREL1, PARTFUN1, FUNCT_4, FINSET_1, CARD_3,
MSUALG_6, MSUALG_7, MSUALG_8;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1,
DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, STRUCT_0, NAT_1, BINOP_1, FUNCT_1,
PARTFUN1, FUNCT_2, FINSET_1, FINSEQ_1, CARD_3, REWRITE1, EQREL_1,
LATTICES, LATTICE3, PBOOLE, MSSUBFAM, MSUALG_1, MSUALG_4, MSUALG_5,
CLOSURE2, MSUALG_6, MSUALG_7, XXREAL_0;
constructors BINOP_1, NAT_1, MEMBERED, REALSET1, REWRITE1, MSSUBFAM, LATTICE3,
MSUALG_5, CLOSURE2, MSUALG_6, MSUALG_7, RELSET_1, NUMBERS;
registrations SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, MEMBERED, EQREL_1,
PBOOLE, STRUCT_0, LATTICES, MSUALG_1, MSUALG_3, MSUALG_5, CLOSURE2,
MSUALG_6, MSUALG_7, FUNCT_1, XXREAL_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, EQREL_1;
expansions TARSKI, XBOOLE_0;
theorems XBOOLE_0, TARSKI, PBOOLE, NAT_LAT, MSUALG_4, MSUALG_5, MSUALG_7,
CLOSURE2, SETFAM_1, LATTICES, LATTICE3, MSSUBFAM, ZFMISC_1, FINSEQ_1,
SUBSET_1, REWRITE1, RELAT_1, MSUALG_6, FUNCT_2, NAT_1, EQREL_1, VECTSP_8,
CARD_3, XBOOLE_1, PARTFUN1;
schemes FINSEQ_1, PARTFUN1, CLASSES1;
begin
:: MORE ON THE LATTICE OF EQUIVALENCE RELATIONS ::
reserve I for non empty set;
reserve M for ManySortedSet of I;
reserve Y,x,y,y1,i,j for set;
reserve k for Element of NAT;
reserve p for FinSequence;
reserve S for non void non empty ManySortedSign;
reserve A for non-empty MSAlgebra over S;
theorem Th1:
for n be Nat, p be FinSequence holds 1 <= n & n <
len p iff n in dom p & n+1 in dom p
proof
let n be Nat;
let p be FinSequence;
thus 1 <= n & n < len p implies n in dom p & n+1 in dom p
proof
assume that
A1: 1 <= n and
A2: n < len p;
1 <= n + 1 & n + 1 <= len p by A2,NAT_1:11,13;
then
A3: n + 1 in Seg len p by FINSEQ_1:1;
n in Seg len p by A1,A2,FINSEQ_1:1;
hence thesis by A3,FINSEQ_1:def 3;
end;
thus n in dom p & n+1 in dom p implies 1 <= n & n < len p
proof
assume that
A4: n in dom p and
A5: n+1 in dom p;
n+1 in Seg len p by A5,FINSEQ_1:def 3;
then
A6: n+1 <= len p by FINSEQ_1:1;
n in Seg len p by A4,FINSEQ_1:def 3;
hence thesis by A6,FINSEQ_1:1,NAT_1:13;
end;
end;
scheme
NonUniqSeqEx{A()->(Element of NAT),P[object,object]}:
ex p st dom p = Seg A() & for k st k in Seg A() holds P[k,p.k]
provided
A1: for k st k in Seg A() ex x being object st P[k,x]
proof
A2: for x being object st x in Seg A() ex y being object st P[x,y] by A1;
consider f being Function such that
A3: dom f = Seg A() &
for x being object st x in Seg A() holds P[x,f.x] from CLASSES1
:sch 1(A2);
reconsider p = f as FinSequence by A3,FINSEQ_1:def 2;
take p;
thus thesis by A3;
end;
theorem Th2:
for a,b be Element of EqRelLatt Y for A,B be Equivalence_Relation
of Y st a = A & b = B holds a [= b iff A c= B
proof
let a,b be Element of EqRelLatt Y;
let A,B be Equivalence_Relation of Y;
assume that
A1: a = A and
A2: b = B;
thus a [= b implies A c= B
proof
assume
A3: a [= b;
A /\ B = (the L_meet of EqRelLatt Y).(A,B) by MSUALG_5:def 2
.= a "/\" b by A1,A2,LATTICES:def 2
.= A by A1,A3,LATTICES:4;
hence thesis by XBOOLE_1:17;
end;
thus A c= B implies a [= b
proof
assume
A4: A c= B;
a "/\" b = (the L_meet of EqRelLatt Y).(A,B) by A1,A2,LATTICES:def 2
.= A /\ B by MSUALG_5:def 2
.= a by A1,A4,XBOOLE_1:28;
hence thesis by LATTICES:4;
end;
end;
registration
let Y;
cluster EqRelLatt Y -> bounded;
coherence
proof
ex c being Element of EqRelLatt Y st for a being Element of EqRelLatt
Y holds c"\/"a = c & a"\/"c = c
proof
set c9 = nabla Y;
reconsider c = c9 as Element of EqRelLatt Y by MSUALG_5:21;
take c;
let a be Element of EqRelLatt Y;
reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21;
thus c"\/"a = (the L_join of EqRelLatt Y).(c,a) by LATTICES:def 1
.= c9 "\/" a9 by MSUALG_5:def 2
.= EqCl (c9 \/ a9) by MSUALG_5:1
.= EqCl c9 by EQREL_1:1
.= c by MSUALG_5:2;
hence thesis;
end;
then
A1: EqRelLatt Y is upper-bounded by LATTICES:def 14;
ex c being Element of EqRelLatt Y st for a being Element of EqRelLatt
Y holds c"/\"a = c & a"/\"c = c
proof
set c9 = id Y;
reconsider c = c9 as Element of EqRelLatt Y by MSUALG_5:21;
take c;
let a be Element of EqRelLatt Y;
reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21;
thus c"/\"a = (the L_meet of EqRelLatt Y).(c,a) by LATTICES:def 2
.= c9 /\ a9 by MSUALG_5:def 2
.= c by EQREL_1:10;
hence thesis;
end;
then EqRelLatt Y is lower-bounded by LATTICES:def 13;
hence thesis by A1;
end;
end;
theorem
Bottom EqRelLatt Y = id Y
proof
reconsider K = id Y as Element of EqRelLatt Y by MSUALG_5:21;
now
let a be Element of EqRelLatt Y;
reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21;
thus K "/\" a = (the L_meet of EqRelLatt Y).(K,a) by LATTICES:def 2
.= id Y /\ a9 by MSUALG_5:def 2
.= K by EQREL_1:10;
hence a "/\" K = K;
end;
hence thesis by LATTICES:def 16;
end;
theorem
Top EqRelLatt Y = nabla Y
proof
reconsider K = nabla Y as Element of EqRelLatt Y by MSUALG_5:21;
now
let a be Element of EqRelLatt Y;
reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5:21;
thus K "\/" a = (the L_join of EqRelLatt Y).(K,a) by LATTICES:def 1
.= nabla Y "\/" a9 by MSUALG_5:def 2
.= EqCl (nabla Y \/ a9) by MSUALG_5:1
.= EqCl (nabla Y) by EQREL_1:1
.= K by MSUALG_5:2;
hence a "\/" K = K;
end;
hence thesis by LATTICES:def 17;
end;
theorem Th5:
EqRelLatt Y is complete
proof
for X being Subset of EqRelLatt Y ex a being Element of EqRelLatt Y st a
is_less_than X & for b being Element of EqRelLatt Y st b is_less_than X holds b
[= a
proof
let X be Subset of EqRelLatt Y;
per cases;
suppose
A1: X is empty;
take a = Top EqRelLatt Y;
for q be Element of EqRelLatt Y st q in X holds a [= q by A1;
hence a is_less_than X by LATTICE3:def 16;
let b be Element of EqRelLatt Y;
assume b is_less_than X;
thus thesis by LATTICES:19;
end;
suppose
A2: X is non empty;
set a = meet X;
X c= bool [:Y,Y:]
proof
let x be object;
assume x in X;
then x is Equivalence_Relation of Y by MSUALG_5:21;
hence thesis;
end;
then reconsider X9 = X as Subset-Family of [:Y,Y:];
for Z be set st Z in X holds Z is Equivalence_Relation of Y by
MSUALG_5:21;
then meet X9 is Equivalence_Relation of Y by A2,EQREL_1:11;
then reconsider a as Equivalence_Relation of Y;
set a9 = a;
reconsider a as Element of EqRelLatt Y by MSUALG_5:21;
take a;
now
let q be Element of EqRelLatt Y;
reconsider q9 = q as Equivalence_Relation of Y by MSUALG_5:21;
assume q in X;
then a9 c= q9 by SETFAM_1:3;
hence a [= q by Th2;
end;
hence a is_less_than X by LATTICE3:def 16;
now
let b be Element of EqRelLatt Y;
reconsider b9 = b as Equivalence_Relation of Y by MSUALG_5:21;
assume
A3: b is_less_than X;
now
let x be object;
assume
A4: x in b9;
now
let Z be set;
assume
A5: Z in X;
then reconsider Z1 = Z as Element of EqRelLatt Y;
reconsider Z9 = Z1 as Equivalence_Relation of Y by MSUALG_5:21;
b [= Z1 by A3,A5,LATTICE3:def 16;
then b9 c= Z9 by Th2;
hence x in Z by A4;
end;
hence x in meet X by A2,SETFAM_1:def 1;
end;
then b9 c= meet X;
hence b [= a by Th2;
end;
hence thesis;
end;
end;
hence thesis by VECTSP_8:def 6;
end;
registration
let Y;
cluster EqRelLatt Y -> complete;
coherence by Th5;
end;
theorem Th6:
for Y be set for X be Subset of EqRelLatt Y holds union X is Relation of Y
proof
let Y be set;
let X be Subset of EqRelLatt Y;
now
let x be object;
assume x in union X;
then consider X9 be set such that
A1: x in X9 and
A2: X9 in X by TARSKI:def 4;
X9 is Equivalence_Relation of Y by A2,MSUALG_5:21;
hence x in [:Y,Y:] by A1;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th7:
for Y be set for X be Subset of EqRelLatt Y holds union X c= "\/" X
proof
let Y be set;
let X be Subset of EqRelLatt Y;
reconsider X9 = "\/" X as Equivalence_Relation of Y by MSUALG_5:21;
let x be object;
assume x in union X;
then consider X1 be set such that
A1: x in X1 and
A2: X1 in X by TARSKI:def 4;
reconsider X1 as Element of EqRelLatt Y by A2;
reconsider X2 = X1 as Equivalence_Relation of Y by MSUALG_5:21;
X is_less_than "\/" X by LATTICE3:def 21;
then X1 [= "\/" X by A2,LATTICE3:def 17;
then X2 c= X9 by Th2;
hence thesis by A1;
end;
theorem Th8:
for Y be set for X be Subset of EqRelLatt Y for R be Relation of
Y st R = union X holds "\/" X = EqCl R
proof
let Y be set;
let X be Subset of EqRelLatt Y;
let R be Relation of Y;
reconsider X1 = "\/" X as Equivalence_Relation of Y by MSUALG_5:21;
assume
A1: R = union X;
A2: now
let EqR be Equivalence_Relation of Y;
reconsider EqR1 = EqR as Element of EqRelLatt Y by MSUALG_5:21;
assume
A3: R c= EqR;
now
let q be Element of EqRelLatt Y;
reconsider q1 = q as Equivalence_Relation of Y by MSUALG_5:21;
assume
A4: q in X;
now
let x be object;
assume x in q1;
then x in union X by A4,TARSKI:def 4;
hence x in EqR by A1,A3;
end;
then q1 c= EqR;
hence q [= EqR1 by Th2;
end;
then X is_less_than EqR1 by LATTICE3:def 17;
then "\/" X [= EqR1 by LATTICE3:def 21;
hence X1 c= EqR by Th2;
end;
R c= "\/" X by A1,Th7;
hence thesis by A2,MSUALG_5:def 1;
end;
theorem Th9:
for Y be set for X be Subset of EqRelLatt Y for R be Relation st
R = union X holds R = R~
proof
let Y be set;
let X be Subset of EqRelLatt Y;
let R be Relation;
assume
A1: R = union X;
now
let x,y be object;
thus [x,y] in R implies [x,y] in R~
proof
assume [x,y] in R;
then consider Z be set such that
A2: [x,y] in Z and
A3: Z in X by A1,TARSKI:def 4;
reconsider Z as Equivalence_Relation of Y by A3,MSUALG_5:21;
[y,x] in Z by A2,EQREL_1:6;
then [y,x] in R by A1,A3,TARSKI:def 4;
hence thesis by RELAT_1:def 7;
end;
thus [x,y] in R~ implies [x,y] in R
proof
assume [x,y] in R~;
then [y,x] in R by RELAT_1:def 7;
then consider Z be set such that
A4: [y,x] in Z and
A5: Z in X by A1,TARSKI:def 4;
reconsider Z as Equivalence_Relation of Y by A5,MSUALG_5:21;
[x,y] in Z by A4,EQREL_1:6;
hence thesis by A1,A5,TARSKI:def 4;
end;
end;
hence thesis by RELAT_1:def 2;
end;
theorem Th10:
for Y be set for X be Subset of EqRelLatt Y holds x in Y & y in
Y implies ( [x,y] in "\/" X iff ex f being FinSequence st 1 <= len f & x = f.1
& y = f.(len f) & for i be Nat st 1 <= i & i < len f holds [f.i,f.(i
+1)] in union X )
proof
let Y be set;
let X be Subset of EqRelLatt Y;
assume that
A1: x in Y and
A2: y in Y;
reconsider Y9 = Y as non empty set by A1;
reconsider x9 = x, y9 = y as Element of Y9 by A1,A2;
reconsider R = union X as Relation of Y9 by Th6;
R = R~ by Th9;
then
A3: R \/ R~ = R;
A4: [x,y] in "\/" X implies R reduces x,y
proof
assume [x,y] in "\/" X;
then [x9,y9] in EqCl R by Th8;
then x,y are_convertible_wrt R by MSUALG_6:41;
hence thesis by A3,REWRITE1:def 4;
end;
thus [x,y] in "\/" X implies ex f being FinSequence st 1 <= len f & x = f.1
& y = f.(len f) & for i be Nat st 1 <= i & i < len f holds [f.i,f.(i
+1)] in union X
proof
assume [x,y] in "\/" X;
then consider f be FinSequence such that
A5: len f > 0 and
A6: x = f.1 & y = f.(len f) and
A7: for i be Nat st i in dom f & i+1 in dom f holds [f.i,f
.( i+1)] in R by A4,REWRITE1:11;
take f;
0 + 1 <= len f by A5,NAT_1:13;
hence 1 <= len f & x = f.1 & y = f.(len f) by A6;
let i be Nat;
assume 1 <= i & i < len f;
then i in dom f & i+1 in dom f by Th1;
hence thesis by A7;
end;
A8: R reduces x,y implies [x,y] in "\/" X
proof
assume R reduces x,y;
then x,y are_convertible_wrt R by REWRITE1:25;
then [x9,y9] in EqCl R by MSUALG_6:41;
hence thesis by Th8;
end;
thus ( ex f being FinSequence st 1 <= len f & x = f.1 & y = f.(len f) & for
i be Nat st 1 <= i & i < len f holds [f.i,f.(i+1)] in union X )
implies [x,y] in "\/" X
proof
given f be FinSequence such that
A9: 1 <= len f and
A10: x = f.1 & y = f.(len f) and
A11: for i be Nat st 1 <= i & i < len f holds [f.i,f.(i+1)]
in union X;
A12: now
let i be Nat;
assume i in dom f & i+1 in dom f;
then 1 <= i & i < len f by Th1;
hence [f.i,f.(i+1)] in union X by A11;
end;
0 + 1 <= len f by A9;
then len f > 0 by NAT_1:13;
hence thesis by A8,A10,A12,REWRITE1:11;
end;
end;
begin :: Lattice of Congruences in a Many Sorted Algebra as a Sublattice
:: of Lattice of Many Sorted Equivalence Relations Inheriting Sups and Infs
theorem Th11:
for B be Subset of CongrLatt A holds "/\" (B,EqRelLatt the Sorts
of A) is MSCongruence of A
proof
set M = the Sorts of A;
set E = EqRelLatt M;
set C = CongrLatt A;
let B be Subset of C;
set d9 = "/\" (B,E);
reconsider d = d9 as Equivalence_Relation of the Sorts of A by MSUALG_5:def 5
;
reconsider d as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
the carrier of C c= the carrier of E by NAT_LAT:def 12;
then reconsider B1 = B as Subset of E by XBOOLE_1:1;
reconsider B1 as SubsetFamily of [|M,M|] by MSUALG_7:5;
per cases;
suppose
B is empty;
then reconsider B9 = B as empty Subset of CongrLatt A;
for q being Element of E st q in B9 holds Top E [= q;
then
A1: Top E is_less_than B by LATTICE3:def 16;
for b be Element of E st b is_less_than B holds b [= Top E by LATTICES:19;
then "/\" (B,E) = Top E by A1,LATTICE3:34
.= [|M,M|] by MSUALG_7:4;
hence thesis by MSUALG_5:18;
end;
suppose
A2: B is non empty;
for o be OperSymbol of S, x,y be Element of Args(o,A) st (for n be Nat
st n in dom x holds [x.n,y.n] in d.((the_arity_of o)/.n)) holds [Den(o,A).x,Den
(o,A).y] in d.(the_result_sort_of o)
proof
reconsider B19 = B1 as non empty SubsetFamily of [|M,M|] by A2;
reconsider m = meet |:B1:| as Equivalence_Relation of M by A2,MSUALG_7:8;
let o be OperSymbol of S;
let x,y be Element of Args(o,A);
A3: |:B19:| is non-empty;
assume
A4: for n be Nat st n in dom x holds [x.n,y.n] in d.((the_arity_of o )/.n);
A5: now
let q be MSCongruence of A;
assume
A6: q in B;
now
let n be Nat;
assume n in dom x;
then [x.n,y.n] in d.((the_arity_of o)/.n) by A4;
then
A7: [x.n,y.n] in m.((the_arity_of o)/.n) by A2,MSUALG_7:10;
m c= q by A6,MSUALG_7:7;
then m.((the_arity_of o)/.n) c= q.((the_arity_of o)/.n) by
PBOOLE:def 2;
hence [x.n,y.n] in q.((the_arity_of o)/.n) by A7;
end;
hence [Den(o,A).x,Den(o,A).y] in q.(the_result_sort_of o) by
MSUALG_4:def 4;
end;
A8: |:B1:|.(the_result_sort_of o) = { x1.(the_result_sort_of o) where
x1 is Element of Bool [|M,M|] : x1 in B } by A2,CLOSURE2:14;
now
let Y be set;
assume Y in |:B1:|.(the_result_sort_of o);
then consider z be Element of Bool [|M,M|] such that
A9: Y = z.(the_result_sort_of o) and
A10: z in B by A8;
reconsider z9 = z as MSCongruence of A by A10,MSUALG_5:def 6;
[Den(o,A).x,Den(o,A).y] in z9.(the_result_sort_of o) by A5,A10;
hence [Den(o,A).x,Den(o,A).y] in Y by A9;
end;
then (ex Q be Subset-Family of ([|M,M|].(the_result_sort_of o)) st Q =
|:B1:|.( the_result_sort_of o) & m.(the_result_sort_of o) = Intersect Q )& [Den
(o,A).x,Den(o,A).y] in meet (|:B1:|.(the_result_sort_of o)) by A3,
MSSUBFAM:def 1,SETFAM_1:def 1;
then [Den(o,A).x,Den(o,A).y] in m.(the_result_sort_of o) by A3,
SETFAM_1:def 9;
hence thesis by A2,MSUALG_7:10;
end;
hence thesis by MSUALG_4:def 4;
end;
end;
definition
let S,A;
let E be Element of EqRelLatt the Sorts of A;
func CongrCl E -> MSCongruence of A equals
"/\" ({x where x is Element of
EqRelLatt the Sorts of A : x is MSCongruence of A & E [= x},EqRelLatt the Sorts
of A);
coherence
proof
set Z = {x where x is Element of EqRelLatt the Sorts of A : x is
MSCongruence of A & E [= x};
now
let z be object;
assume z in Z;
then ex z1 be Element of EqRelLatt the Sorts of A st z = z1 & z1 is
MSCongruence of A & E [= z1;
hence z in the carrier of CongrLatt A by MSUALG_5:def 6;
end;
then reconsider Z9 = Z as Subset of CongrLatt A by TARSKI:def 3;
"/\" (Z9,EqRelLatt the Sorts of A) is MSCongruence of A by Th11;
hence thesis;
end;
end;
definition
let S,A;
let X be Subset of EqRelLatt the Sorts of A;
func CongrCl X -> MSCongruence of A equals
"/\" ({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
proof
set Z = {x where x is Element of EqRelLatt the Sorts of A : x is
MSCongruence of A & X is_less_than x};
now
let z be object;
assume z in Z;
then ex z1 be Element of EqRelLatt the Sorts of A st z = z1 & z1 is
MSCongruence of A & X is_less_than z1;
hence z in the carrier of CongrLatt A by MSUALG_5:def 6;
end;
then reconsider Z9 = Z as Subset of CongrLatt A by TARSKI:def 3;
"/\" (Z9,EqRelLatt the Sorts of A) is MSCongruence of A by Th11;
hence thesis;
end;
end;
theorem
for C be Element of EqRelLatt the Sorts of A st C is MSCongruence of A
holds CongrCl C = C
proof
let C be Element of EqRelLatt the Sorts of A;
set Z = {x where x is Element of EqRelLatt the Sorts of A : x is
MSCongruence of A & C [= x};
now
let q be Element of EqRelLatt the Sorts of A;
assume q in Z;
then ex x be Element of EqRelLatt the Sorts of A st q = x & x is
MSCongruence of A & C [= x;
hence C [= q;
end;
then
A1: C is_less_than Z by LATTICE3:def 16;
assume C is MSCongruence of A;
then C in Z;
hence thesis by A1,LATTICE3:41;
end;
theorem
for X be Subset of EqRelLatt the Sorts of A holds CongrCl "\/" (X,
EqRelLatt the Sorts of A) = CongrCl X
proof
let X be Subset of EqRelLatt the Sorts of A;
set D1 = {x where x is Element of EqRelLatt the Sorts of A : x is
MSCongruence of A & "\/" (X,EqRelLatt the Sorts of A) [= x};
set D2 = {x where x is Element of EqRelLatt the Sorts of A : x is
MSCongruence of A & X is_less_than x};
A1: D1 c= D2
proof
let x1 be object;
assume x1 in D1;
then consider x be Element of EqRelLatt the Sorts of A such that
A2: x1 = x & x is MSCongruence of A and
A3: "\/" (X,EqRelLatt the Sorts of A) [= x;
now
let q be Element of EqRelLatt the Sorts of A;
A4: X is_less_than "\/" (X,EqRelLatt the Sorts of A) by LATTICE3:def 21;
assume q in X;
then q [= "\/" (X,EqRelLatt the Sorts of A) by A4,LATTICE3:def 17;
hence q [= x by A3,LATTICES:7;
end;
then X is_less_than x by LATTICE3:def 17;
hence thesis by A2;
end;
D2 c= D1
proof
let x1 be object;
assume x1 in D2;
then consider x be Element of EqRelLatt the Sorts of A such that
A5: x1 = x & x is MSCongruence of A and
A6: X is_less_than x;
"\/" (X,EqRelLatt the Sorts of A) [= x by A6,LATTICE3:def 21;
hence thesis by A5;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
for B1,B2 be Subset of CongrLatt A, C1,C2 be 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
let B1,B2 be Subset of CongrLatt A;
let C1,C2 be MSCongruence of A;
set C = EqRelLatt the Sorts of A;
assume
A1: C1 = "\/"(B1,EqRelLatt the Sorts of A) & C2 = "\/"(B2,EqRelLatt the
Sorts of A);
the carrier of CongrLatt A c= the carrier of EqRelLatt the Sorts of A by
NAT_LAT:def 12;
then reconsider D1 = B1, D2 = B2 as Subset of EqRelLatt the Sorts of A by
XBOOLE_1:1;
A2: { "\/" D1, "\/" D2 } c= {"\/" Y where Y is Subset of C: Y in { B1,B2 } }
proof
let x be object;
assume x in { "\/" D1, "\/" D2 };
then
A3: x = "\/" D1 or x = "\/" D2 by TARSKI:def 2;
D1 in { B1,B2 } & D2 in { B1,B2 } by TARSKI:def 2;
hence thesis by A3;
end;
{"\/" Y where Y is Subset of C: Y in { B1,B2 } } c= { "\/" D1, "\/" D2 }
proof
let x be object;
assume x in {"\/" Y where Y is Subset of C: Y in { B1,B2 } };
then consider X1 be Subset of C such that
A4: x = "\/" X1 and
A5: X1 in { B1,B2 };
X1 = B1 or X1 = B2 by A5,TARSKI:def 2;
hence thesis by A4,TARSKI:def 2;
end;
then
A6: {"\/" Y where Y is Subset of C: Y in { B1,B2 } } = { "\/" D1, "\/" D2 }
by A2;
now
let i be object;
assume i in { B1,B2 };
then i = D1 or i = D2 by TARSKI:def 2;
hence i in bool the carrier of C;
end;
then
A7: { B1,B2 } c= bool the carrier of C;
thus "\/" (B1 \/ B2,EqRelLatt the Sorts of A) = "\/" (union { B1,B2 }, C) by
ZFMISC_1:75
.= "\/" ({"\/" Y where Y is Subset of C: Y in { B1,B2 } }, C) by A7,
LATTICE3:48
.= ( "\/" D1 ) "\/" ( "\/" D2 ) by A6,LATTICE3:43
.= (the L_join of C).(C1,C2) by A1,LATTICES:def 1
.= C1 "\/" C2 by MSUALG_5:def 5;
end;
theorem
for X be 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
let X be Subset of CongrLatt A;
set E = EqRelLatt the Sorts of A;
set X1 = { X0 where X0 is Subset of E : X0 is finite Subset of X };
set B1 = { "\/"Y where Y is Subset of E : Y in X1 };
set B2 = { "\/" (X0,EqRelLatt the Sorts of A) where X0 is Subset of E : X0
is finite Subset of X };
A1: B2 c= B1
proof
let x be object;
assume x in B2;
then consider Y1 be Subset of E such that
A2: x = "\/" Y1 and
A3: Y1 is finite Subset of X;
Y1 in X1 by A3;
hence thesis by A2;
end;
A4: X c= union X1
proof
let x be object;
assume
A5: x in X;
then reconsider x9 = x as Element of CongrLatt A;
the carrier of CongrLatt A c= the carrier of E by NAT_LAT:def 12;
then reconsider x9 as Element of E;
{x9} is finite Subset of X by A5,SUBSET_1:41;
then x in {x} & {x9} in X1 by TARSKI:def 1;
hence thesis by TARSKI:def 4;
end;
union X1 c= X
proof
let x be object;
assume x in union X1;
then consider Y1 be set such that
A6: x in Y1 and
A7: Y1 in X1 by TARSKI:def 4;
ex Y2 be Subset of E st Y1 = Y2 & Y2 is finite Subset of X by A7;
hence thesis by A6;
end;
then
A8: X = union X1 by A4;
now
let i be object;
assume i in X1;
then ex I1 be Subset of E st i = I1 & I1 is finite Subset of X;
hence i in bool the carrier of E;
end;
then
A9: X1 c= bool the carrier of E;
B1 c= B2
proof
let x be object;
assume x in B1;
then consider Y1 be Subset of E such that
A10: x = "\/" Y1 and
A11: Y1 in X1;
ex Y2 be Subset of E st Y1 = Y2 & Y2 is finite Subset of X by A11;
hence thesis by A10;
end;
then B1 = B2 by A1;
hence thesis by A9,A8,LATTICE3:48;
end;
theorem Th16:
for i be Element of I for e be Equivalence_Relation of M.i ex E
be Equivalence_Relation of M st E.i = e & for j be Element of I st j <> i holds
E.j = nabla (M.j)
proof
let i be Element of I;
let e be Equivalence_Relation of M.i;
defpred C[object] means $1 = i;
deffunc F(object) = e;
deffunc G(object) = nabla (M.$1);
consider E being Function such that
A1: dom E = I and
A2: for j being object st j in I
holds ( C[j] implies E.j = F(j)) & (not C[j] implies
E.j = G(j)) from PARTFUN1:sch 1;
reconsider E as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
now
let k be set;
assume
A3: k in I;
per cases;
suppose
k = i;
hence E.k is Relation of M.k by A2;
end;
suppose
k <> i;
then E.k = nabla (M.k) by A2,A3;
hence E.k is Relation of M.k;
end;
end;
then reconsider E as ManySortedRelation of M by MSUALG_4:def 1;
now
let k be object, R be Relation of M.k;
assume that
A4: k in I and
A5: E.k = R;
per cases;
suppose
k = i;
hence R is Equivalence_Relation of M.k by A2,A5;
end;
suppose
k <> i;
then E.k = nabla (M.k) by A2,A4;
hence R is Equivalence_Relation of M.k by A5;
end;
end;
then reconsider E as Equivalence_Relation of M by MSUALG_4:def 2;
take E;
thus E.i = e by A2;
let j be Element of I;
assume j <> i;
hence thesis by A2;
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(X,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;
redefine func EqRelSet (X,i) -> Subset of EqRelLatt M.i means :: redefines EqRelSet (MSUALG_8, synonym) → pi (CARD_3, definition)
:Def3:
x in it iff ex Eq be Equivalence_Relation of M st x = Eq.i & Eq in X;
coherence
proof
pi(X,i) c= the carrier of EqRelLatt M.i
proof
let z be object;
assume z in pi(X,i);
then consider f be Function such that
A1: f in X and
A2: z = f.i by CARD_3:def 6;
reconsider f as Equivalence_Relation of M by A1,MSUALG_5:def 5;
f.i is Equivalence_Relation of M.i by MSUALG_4:def 2;
hence thesis by A2,MSUALG_5:21;
end;
hence thesis;
end;
compatibility
proof
thus for Y being Subset of EqRelLatt M.i holds Y = pi(X,i) iff for x holds
x in Y iff ex Eq be Equivalence_Relation of M st x = Eq.i & Eq in X
proof
let Y be Subset of EqRelLatt M.i;
thus Y = pi(X,i) implies for x holds x in Y iff ex Eq be
Equivalence_Relation of M st x = Eq.i & Eq in X
proof
assume
A3: Y = pi(X,i);
let x;
thus x in Y implies ex Eq be Equivalence_Relation of M st x = Eq.i &
Eq in X
proof
assume x in Y;
then consider f be Function such that
A4: f in X and
A5: x = f.i by A3,CARD_3:def 6;
reconsider f as Equivalence_Relation of M by A4,MSUALG_5:def 5;
take f;
thus thesis by A4,A5;
end;
thus thesis by A3,CARD_3:def 6;
end;
thus (for x holds x in Y iff ex Eq be Equivalence_Relation of M st x =
Eq.i & Eq in X) implies Y = pi(X,i)
proof
assume
A6: for x holds x in Y iff ex Eq be Equivalence_Relation of M st
x = Eq.i & Eq in X;
thus Y c= pi(X,i)
proof
let y1 be object;
assume y1 in Y;
then
ex Eq be Equivalence_Relation of M st y1 = Eq.i & Eq in X by A6;
hence thesis by CARD_3:def 6;
end;
thus pi(X,i) c= Y
proof
let y1 be object;
assume y1 in pi(X,i);
then consider f be Function such that
A7: f in X and
A8: y1 = f.i by CARD_3:def 6;
reconsider f as Equivalence_Relation of M by A7,MSUALG_5:def 5;
ex Eq be Equivalence_Relation of M st y1 = Eq.i & Eq in X
proof
take f;
thus thesis by A7,A8;
end;
hence thesis by A6;
end;
end;
end;
end;
end;
theorem Th17:
for i be Element of S for X be Subset of EqRelLatt the Sorts of
A for B be Equivalence_Relation of the Sorts of A st B = "\/" X holds B.i =
"\/" (EqRelSet (X,i) , EqRelLatt (the Sorts of A).i)
proof
let i be Element of S;
set M = the Sorts of A;
set E = EqRelLatt M;
set Ei = EqRelLatt M.i;
let X be Subset of E;
let B be Equivalence_Relation of M;
reconsider B9 = B as Element of E by MSUALG_5:def 5;
reconsider Bi = B.i as Equivalence_Relation of M.i by MSUALG_4:def 2;
reconsider Bi9 = Bi as Element of Ei by MSUALG_5:21;
assume
A1: B = "\/" X;
A2: now
let ri be Element of Ei;
reconsider ri9 = ri as Equivalence_Relation of M.i by MSUALG_5:21;
consider r9 be Equivalence_Relation of the Sorts of A such that
A3: r9.i = ri9 and
A4: for j be SortSymbol of S st j <> i holds r9.j = nabla ((the Sorts
of A).j) by Th16;
reconsider r = r9 as Element of E by MSUALG_5:def 5;
assume
A5: EqRelSet (X,i) is_less_than ri;
now
let c be Element of E;
reconsider c9 = c as Equivalence_Relation of M by MSUALG_5:def 5;
reconsider ci9 = c9.i as Equivalence_Relation of M.i by MSUALG_4:def 2;
reconsider ci = ci9 as Element of Ei by MSUALG_5:21;
assume c in X;
then ci in EqRelSet (X,i) by Def3;
then
A6: ci [= ri by A5,LATTICE3:def 17;
now
let j be object;
assume
A7: j in the carrier of S;
then reconsider j9 = j as Element of S;
reconsider rj9 = r9.j9, cj9 = c9.j9 as Equivalence_Relation of M.j by
MSUALG_4:def 2;
per cases;
suppose
j = i;
hence c9.j c= r9.j by A3,A6,Th2;
end;
suppose
j <> i;
then r9.j = nabla ((the Sorts of A).j) by A4,A7;
then cj9 /\ rj9 = cj9 by XBOOLE_1:28;
hence c9.j c= r9.j by XBOOLE_1:17;
end;
end;
then c9 c= r9 by PBOOLE:def 2;
hence c [= r by MSUALG_7:6;
end;
then X is_less_than r by LATTICE3:def 17;
then B9 [= r by A1,LATTICE3:def 21;
then B c= r9 by MSUALG_7:6;
then Bi c= ri9 by A3,PBOOLE:def 2;
hence Bi9 [= ri by Th2;
end;
now
let q9 be Element of Ei;
reconsider q = q9 as Equivalence_Relation of M.i by MSUALG_5:21;
assume q9 in EqRelSet (X,i);
then consider Eq be Equivalence_Relation of M such that
A8: q9 = Eq.i and
A9: Eq in X by Def3;
reconsider Eq9 = Eq as Element of E by MSUALG_5:def 5;
Eq9 [= B9 by A1,A9,LATTICE3:38;
then Eq c= B by MSUALG_7:6;
then q c= Bi by A8,PBOOLE:def 2;
hence q9 [= Bi9 by Th2;
end;
then EqRelSet (X,i) is_less_than Bi9 by LATTICE3:def 17;
hence thesis by A2,LATTICE3:def 21;
end;
theorem Th18:
for X be Subset of CongrLatt A holds "\/" (X,EqRelLatt the Sorts
of A) is MSCongruence of A
proof
let X9 be Subset of CongrLatt A;
set M = the Sorts of A;
set E = EqRelLatt M;
the carrier of CongrLatt A c= the carrier of EqRelLatt M by NAT_LAT:def 12;
then reconsider X = X9 as Subset of EqRelLatt M by XBOOLE_1:1;
reconsider V = "\/" (X,E) as Equivalence_Relation of M by MSUALG_5:def 5;
reconsider V as ManySortedRelation of A;
reconsider V as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for s1,s2 being SortSymbol of S for t being Function st t
is_e.translation_of A,s1,s2 for a,b being set st [a,b] in V.s1 holds [t.a, t.b]
in V.s2
proof
let s1,s2 be SortSymbol of S;
let t be Function;
assume
A1: t is_e.translation_of A,s1,s2;
then reconsider t9 = t as Function of M.s1,M.s2 by MSUALG_6:11;
let a,b be set;
assume
A2: [a,b] in V.s1;
then
A3: a in M.s1 by ZFMISC_1:87;
A4: b in M.s1 by A2,ZFMISC_1:87;
then
A5: t9.b in M.s2 by FUNCT_2:5;
[a,b] in "\/" EqRelSet (X,s1) by A2,Th17;
then consider f be FinSequence such that
A6: 1 <= len f and
A7: a = f.1 and
A8: b = f.(len f) and
A9: for i be Nat st 1 <= i & i < len f holds [f.i,f.(i+1)]
in union EqRelSet (X,s1) by A3,A4,Th10;
A10: ex g be FinSequence st 1 <= len g & t.a = g.1 & t.b = g.(len g) & for
i be Nat st 1 <= i & i < len g holds [g.i,g.(i+1)] in union EqRelSet
(X,s2)
proof
deffunc F(set)=t.(f.$1);
consider g be FinSequence such that
A11: len g = len f & for k be Nat st k in dom g holds g.k = F(k)
from FINSEQ_1:sch 2;
take g;
thus 1 <= len g by A6,A11;
A12: dom g = Seg len f by A11,FINSEQ_1:def 3;
1 in Seg len f by A6,FINSEQ_1:1;
hence g.1 = t.a by A7,A11,A12;
len g in Seg len f by A6,A11,FINSEQ_1:1;
hence g.(len g) = t.b by A8,A11,A12;
let j be Nat;
assume that
A13: 1 <= j and
A14: j < len g;
A15: 1 <= j+1 by A13,NAT_1:13;
[f.j,f.(j+1)] in union EqRelSet (X,s1) by A9,A11,A13,A14;
then consider Z be set such that
A16: [f.j,f.(j+1)] in Z and
A17: Z in EqRelSet (X,s1) by TARSKI:def 4;
consider Eq be Equivalence_Relation of M such that
A18: Z = Eq.s1 and
A19: Eq in X by A17,Def3;
reconsider Eq as ManySortedRelation of A;
reconsider Eq as MSEquivalence-like ManySortedRelation of A by
MSUALG_4:def 3;
Eq is MSCongruence of A by A19,MSUALG_5:def 6;
then reconsider
Eq as compatible MSEquivalence-like ManySortedRelation of A
by MSUALG_6:27;
ex W be set st [t.(f.j),t.(f.(j+1))] in W & W in EqRelSet (X,s2)
proof
take W = Eq.s2;
thus [t.(f.j),t.(f.(j+1))] in W by A1,A16,A18,MSUALG_6:def 8;
thus thesis by A19,Def3;
end;
then
A20: [t.(f.j),t.(f.(j+1))] in union EqRelSet (X,s2) by TARSKI:def 4;
j+1 <= len f by A11,A14,NAT_1:13;
then
A21: j+1 in Seg len f by A15,FINSEQ_1:1;
j in Seg len f by A11,A13,A14,FINSEQ_1:1;
then g.j = t.(f.j) by A11,A12;
hence thesis by A11,A12,A20,A21;
end;
t9.a in M.s2 by A3,FUNCT_2:5;
then [t.a,t.b] in "\/" EqRelSet (X,s2) by A5,A10,Th10;
hence thesis by Th17;
end;
then reconsider
V as invariant MSEquivalence-like ManySortedRelation of A by MSUALG_6:def 8;
V is compatible;
hence thesis by MSUALG_6:27;
end;
theorem Th19:
CongrLatt A is /\-inheriting
proof
set E = EqRelLatt the Sorts of A;
set C = CongrLatt A;
now
let B be Subset of C;
reconsider d = "/\" (B,E) as MSCongruence of A by Th11;
d in the carrier of C by MSUALG_5:def 6;
hence "/\" (B,E) in the carrier of C;
end;
hence thesis by MSUALG_7:def 2;
end;
theorem Th20:
CongrLatt A is \/-inheriting
proof
set E = EqRelLatt the Sorts of A;
set C = CongrLatt A;
now
let B be Subset of C;
reconsider d = "\/" (B,E) as MSCongruence of A by Th18;
d in the carrier of C by MSUALG_5:def 6;
hence "\/" (B,E) in the carrier of C;
end;
hence thesis by MSUALG_7:def 3;
end;
registration
let S,A;
cluster CongrLatt A -> /\-inheriting \/-inheriting;
coherence by Th19,Th20;
end;