:: Lattice of Congruences in a Many Sorted Algebra
:: by Robert Milewski
::
:: Received January 11, 1996
:: Copyright (c) 1996-2017 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 NUMBERS, PBOOLE, RELAT_1, EQREL_1, TARSKI, XBOOLE_0, STRUCT_0,
LATTICES, FUNCT_1, SUBSET_1, BINOP_1, MSUALG_4, ZFMISC_1, CARD_3,
MSUALG_1, FINSEQ_1, MARGREL1, PARTFUN1, ARYTM_3, ORDINAL4, NAT_1,
XXREAL_0, CARD_1, RELAT_2, ARYTM_1, NAT_LAT, REALSET1, XXREAL_2,
MSUALG_5, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
REALSET1, ORDINAL1, NUMBERS, XCMPLX_0, FINSEQ_2, STRUCT_0, PARTFUN1,
FUNCT_2, RELSET_1, EQREL_1, BINOP_1, PBOOLE, MSUALG_1, MSUALG_3,
MSUALG_4, LATTICES, NAT_LAT, CARD_3, FINSEQ_1, NAT_1, XXREAL_0;
constructors BINOP_1, XXREAL_0, NAT_1, NAT_D, EQREL_1, REALSET1, NAT_LAT,
MSUALG_3, MSUALG_4, RELSET_1, PRALG_2, FUNCOP_1, FINSEQ_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1,
EQREL_1, PBOOLE, STRUCT_0, LATTICES, NAT_LAT, PRALG_1, MSUALG_1,
MSUALG_3, MSUALG_4, ORDINAL1, CARD_1, RELAT_2;
requirements NUMERALS, REAL, BOOLE, SUBSET;
begin
:: MORE OF EQUIVALENCE RELATIONS
reserve I,X,x,d,i for set;
reserve M for ManySortedSet of I;
reserve EqR1,EqR2 for Equivalence_Relation of X;
definition
let X be set, R be Relation of X;
func EqCl R -> Equivalence_Relation of X means
:: MSUALG_5:def 1
R c= it & for EqR2 be
Equivalence_Relation of X st R c= EqR2 holds it c= EqR2;
end;
theorem :: MSUALG_5:1
EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2);
theorem :: MSUALG_5:2
EqCl EqR1 = EqR1;
begin
:: LATTICE OF EQUIVALENCE RELATIONS ::
definition
let X be set;
func EqRelLatt X -> strict Lattice means
:: 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;
end;
begin
:: MANY SORTED EQUIVALENCE RELATIONS ::
registration
let I,M;
cluster MSEquivalence_Relation-like for ManySortedRelation of M;
end;
definition
let I,M;
mode Equivalence_Relation of M is MSEquivalence_Relation-like
ManySortedRelation of M;
end;
reserve I for non empty set;
reserve M for ManySortedSet of I;
reserve EqR,EqR1,EqR2,EqR3,EqR4 for Equivalence_Relation of M;
definition
let I be non empty set;
let M be ManySortedSet of I, R be ManySortedRelation of M;
func EqCl R -> Equivalence_Relation of M means
:: MSUALG_5:def 3
for i being Element of I holds it.i = EqCl(R.i);
end;
theorem :: MSUALG_5:3
EqCl EqR = EqR;
begin
:: LATTICE OF MANY SORTED EQUIVALENCE RELATIONS ::
definition
let I be non empty set, M be ManySortedSet of I;
let EqR1,EqR2 be Equivalence_Relation of M;
func EqR1 "\/" EqR2 -> Equivalence_Relation of M means
:: MSUALG_5:def 4
ex EqR3 being
ManySortedRelation of M st EqR3 = EqR1 (\/) EqR2 & it = EqCl EqR3;
commutativity;
end;
theorem :: MSUALG_5:4
EqR1 (\/) EqR2 c= EqR1 "\/" EqR2;
theorem :: MSUALG_5:5
for EqR be Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR;
theorem :: MSUALG_5:6
( EqR1 (\/) EqR2 c= EqR3 & for EqR be Equivalence_Relation of M st
EqR1 (\/) EqR2 c= EqR holds EqR3 c= EqR ) implies EqR3 = EqR1 "\/" EqR2;
theorem :: MSUALG_5:7
EqR "\/" EqR = EqR;
theorem :: MSUALG_5:8
(EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3);
theorem :: MSUALG_5:9
EqR1 (/\) (EqR1 "\/" EqR2) = EqR1;
theorem :: MSUALG_5:10
for EqR be Equivalence_Relation of M st EqR = EqR1 (/\) EqR2 holds
EqR1 "\/" EqR = EqR1;
theorem :: MSUALG_5:11
for EqR1,EqR2 be Equivalence_Relation of M holds EqR1 (/\) EqR2 is
Equivalence_Relation of M;
definition
let I be non empty set;
let M be ManySortedSet of I;
func EqRelLatt M -> strict Lattice means
:: 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;
end;
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 A;
end;
reserve S for non void non empty ManySortedSign;
reserve A for non-empty MSAlgebra over S;
theorem :: MSUALG_5:12
for o be OperSymbol of S for C1,C2 being MSCongruence of A for
x1,y1 be set for a1,b1 be FinSequence holds [x1,y1] in C1.((the_arity_of o)/.(
len a1 + 1)) \/ C2.((the_arity_of o)/.(len a1 + 1)) implies for x,y be 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);
theorem :: MSUALG_5:13
for o be OperSymbol of S for C1,C2 being MSCongruence of A for C
being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2
for x1,y1 be object
for n be Element of NAT for a1,a2,b1 being FinSequence st len a1 = n & len
a1 = len a2 & for k be Element of NAT st k in dom a1 holds [a1.k,a2.k] in C.((
the_arity_of o)/.k) holds ( [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))
implies for x be 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));
theorem :: MSUALG_5:14
for o be OperSymbol of S for C1,C2 being MSCongruence of A for C
being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 for x,y be
Element of Args(o,A) holds (( for n be Nat st n in dom x holds [x.n,y.n] in C.(
(the_arity_of o)/.n)) implies [Den(o,A).x,Den(o,A).y] in C.(the_result_sort_of
o));
theorem :: MSUALG_5:15
for C1,C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A;
theorem :: MSUALG_5:16
for C1,C2 being MSCongruence of A holds C1 (/\) C2 is MSCongruence of A;
definition
let S;
let A be non-empty MSAlgebra over S;
func CongrLatt A -> strict SubLattice of EqRelLatt the Sorts of A means
:: MSUALG_5:def 6
for
x being set holds x in the carrier of it iff x is MSCongruence of A;
end;
theorem :: MSUALG_5:17
id (the Sorts of A) is MSCongruence of A;
theorem :: MSUALG_5:18
[|the Sorts of A,the Sorts of A|] is MSCongruence of A;
registration
let S, A;
cluster CongrLatt A -> bounded;
end;
theorem :: MSUALG_5:19
Bottom CongrLatt A = id (the Sorts of A);
theorem :: MSUALG_5:20
Top CongrLatt A = [|the Sorts of A,the Sorts of A|];
:: from MSUALG_7, 2010.02.21, A.T
theorem :: MSUALG_5:21
for X be set holds x in the carrier of EqRelLatt X iff x is
Equivalence_Relation of X;