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