:: The Correspondence Between Lattices of Subalgebras of Universal
:: Algebras and Many Sorted Algebras
:: by Adam Naumowicz and Agnieszka Julia Marasik
::
:: Received September 22, 1998
:: Copyright (c) 1998-2019 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 NAT_1, PBOOLE, FUNCT_1, CARD_1, XBOOLE_0, FINSEQ_2, FINSEQ_1,
RELAT_1, TARSKI, NUMBERS, SUBSET_1, UNIALG_1, UNIALG_2, MSUALG_1,
FUNCOP_1, CQC_SIM1, STRUCT_0, MSUALG_2, MARGREL1, PARTFUN1, CARD_3,
FUNCT_2, ZFMISC_1, EQREL_1, INCPROJ, WELLORD1, GROUP_6, LATTICES,
SETLIM_2, LATTICE4;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, CARD_3, ORDINAL1, LATTICES,
LATTICE4, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0,
PBOOLE, UNIALG_1, UNIALG_2, NUMBERS, FINSEQ_1, FINSEQ_2, MARGREL1,
MSUALG_1, MSUALG_2;
constructors BINOP_1, FINSEQOP, FILTER_1, UNIALG_2, LATTICE4, MSUALG_2,
RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_2,
RELAT_1, PBOOLE, STRUCT_0, UNIALG_1, UNIALG_2, MSUALG_1, MSUALG_2,
FINSEQ_1, MARGREL1;
requirements NUMERALS, SUBSET, BOOLE;
begin
:: Preliminaries
reserve a for set,
i for Nat;
theorem :: MSSUBLAT:1
(*-->a).0 = {};
theorem :: MSSUBLAT:2
(*-->a).1 = <*a*>;
theorem :: MSSUBLAT:3
(*-->a).2 = <*a,a*>;
theorem :: MSSUBLAT:4
(*-->a).3 = <*a,a,a*>;
theorem :: MSSUBLAT:5
for f being FinSequence of {0} holds f = i |-> 0 iff len f = i;
theorem :: MSSUBLAT:6
for f be FinSequence st f = (*-->0).i holds len f = i;
begin
theorem :: MSSUBLAT:7
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSSign U1 = MSSign U2;
theorem :: MSSUBLAT:8
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 for B
being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 for o being OperSymbol
of MSSign U2 for a being OperSymbol of MSSign U1 st a = o holds Den(a,MSAlg U1)
= Den(o,MSAlg U2)|Args(a,MSAlg U1);
theorem :: MSSUBLAT:9
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
the Sorts of MSAlg U1 is MSSubset of MSAlg U2;
theorem :: MSSUBLAT:10
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 for
B being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 holds B is
opers_closed;
theorem :: MSSUBLAT:11
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2 for
B being MSSubset of MSAlg U2 st B = the Sorts of MSAlg U1 holds the Charact of
MSAlg U1 = Opers(MSAlg U2,B);
theorem :: MSSUBLAT:12
for U1,U2 being Universal_Algebra st U1 is SubAlgebra of U2
holds MSAlg U1 is MSSubAlgebra of MSAlg U2;
theorem :: MSSUBLAT:13
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 holds the carrier of U1 is Subset of U2;
theorem :: MSSUBLAT:14
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 for B being non empty Subset of U2 st B=the carrier of U1 holds B is
opers_closed;
theorem :: MSSUBLAT:15
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 for B being non empty Subset of U2 st B=the carrier of U1 holds the
charact of U1 = Opers(U2,B);
theorem :: MSSUBLAT:16
for U1,U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of
MSAlg U2 holds U1 is SubAlgebra of U2;
reserve MS for segmental non void 1-element ManySortedSign,
A for non-empty MSAlgebra over MS;
theorem :: MSSUBLAT:17
for B being non-empty MSSubAlgebra of A holds the carrier of
1-Alg B is Subset of 1-Alg A;
theorem :: MSSUBLAT:18
for B being non-empty MSSubAlgebra of A holds for S being non
empty Subset of 1-Alg A st S = the carrier of 1-Alg B holds S is opers_closed
;
theorem :: MSSUBLAT:19
for B being non-empty MSSubAlgebra of A holds for S being non
empty Subset of 1-Alg A st S = the carrier of 1-Alg B holds the charact of(
1-Alg B) = Opers(1-Alg A,S);
theorem :: MSSUBLAT:20
for B being non-empty MSSubAlgebra of A holds 1-Alg B is
SubAlgebra of 1-Alg A;
theorem :: MSSUBLAT:21
for S being non empty non void ManySortedSign, A,B being
MSAlgebra over S holds A is MSSubAlgebra of B iff A is MSSubAlgebra of the
MSAlgebra of B;
theorem :: MSSUBLAT:22
for A,B being Universal_Algebra holds signature A = signature B iff
MSSign A = MSSign B;
theorem :: MSSUBLAT:23
for A being non-empty MSAlgebra over MS st the carrier of MS = {
0} holds MSSign 1-Alg A = the ManySortedSign of MS;
theorem :: MSSUBLAT:24
for A,B being non-empty MSAlgebra over MS st 1-Alg A = 1-Alg B
holds the MSAlgebra of A = the MSAlgebra of B;
theorem :: MSSUBLAT:25
for A being non-empty MSAlgebra over MS st the carrier of MS = {0}
holds the Sorts of A = the Sorts of MSAlg (1-Alg A);
theorem :: MSSUBLAT:26
for A being non-empty MSAlgebra over MS st the carrier of MS = {
0} holds MSAlg (1-Alg A) = the MSAlgebra of A;
theorem :: MSSUBLAT:27
for A being Universal_Algebra, B being strict non-empty MSSubAlgebra
of MSAlg A st the carrier of MSSign A = {0} holds 1-Alg B is SubAlgebra of A;
begin
:: The Correspondence Between Lattices of Subalgebras of
:: Universal and Many Sorted Algebras
theorem :: MSSUBLAT:28
for A being Universal_Algebra, a1,b1 being strict SubAlgebra of
A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 =
MSAlg b1 holds (the Sorts of a2) (\/) (the Sorts of b2)
= 0 .--> ((the carrier of a1) \/ (the carrier of b1));
theorem :: MSSUBLAT:29
for A being Universal_Algebra, a1,b1 being strict non-empty
SubAlgebra of A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 =
MSAlg a1 & b2 = MSAlg b1 holds
(the Sorts of a2) (/\) (the Sorts of b2) = 0 .-->
((the carrier of a1) /\ (the carrier of b1));
theorem :: MSSUBLAT:30
for A being strict Universal_Algebra, a1,b1 be strict non-empty
SubAlgebra of A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 =
MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 "\/" b1) = a2 "\/" b2;
registration
let A be with_const_op Universal_Algebra;
cluster MSSign(A) -> non void strict segmental trivial all-with_const_op;
end;
theorem :: MSSUBLAT:31
for A being with_const_op Universal_Algebra, a1,b1 being strict
non-empty SubAlgebra of A, a2,b2 being strict non-empty MSSubAlgebra of MSAlg A
st a2 = MSAlg a1 & b2 = MSAlg b1 holds MSAlg (a1 /\ b1) = a2 /\ b2;
registration
let A be quasi_total UAStr;
cluster the UAStr of A -> quasi_total;
end;
registration
let A be partial UAStr;
cluster the UAStr of A -> partial;
end;
registration
let A be non-empty UAStr;
cluster the UAStr of A -> non-empty;
end;
registration
let A be with_const_op Universal_Algebra;
cluster the UAStr of A -> with_const_op;
end;
theorem :: MSSUBLAT:32
for A being with_const_op Universal_Algebra holds UnSubAlLattice the
UAStr of A, MSSubAlLattice MSAlg the UAStr of A are_isomorphic;