:: Subalgebras of a Many Sorted Algebra. Lattice of Subalgebras :: by Ewa Burakowska :: :: Received April 25, 1994 :: Copyright (c) 1994-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 PBOOLE, RELAT_1, XBOOLE_0, FUNCT_1, SUBSET_1, CARD_3, TARSKI, STRUCT_0, MSUALG_1, UNIALG_2, FINSEQ_1, MARGREL1, PARTFUN1, FUNCT_2, ZFMISC_1, QC_LANG1, SETFAM_1, EQREL_1, BINOP_1, LATTICES, XXREAL_2, MSUALG_2, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, SETFAM_1, FINSEQ_2, LATTICES, BINOP_1, CARD_3, PBOOLE, MSUALG_1; constructors SETFAM_1, BINOP_1, CARD_3, LATTICES, MSUALG_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, STRUCT_0, LATTICES, MSUALG_1, FINSEQ_1, FUNCT_2, PARTFUN1, RELSET_1; requirements BOOLE, SUBSET; begin :: :: Auxiliary facts about Many Sorted Sets. :: reserve x,y for object; registration let I be set, X be ManySortedSet of I, Y be non-empty ManySortedSet of I; cluster X (\/) Y -> non-empty; cluster Y (\/) X -> non-empty; end; theorem :: MSUALG_2:1 for I be non empty set, X, Y be ManySortedSet of I, i be Element of I* holds product ((X (/\) Y)*i) = product(X * i) /\ product(Y * i); begin :: :: Constants of a Many Sorted Algebra. :: reserve S for non void non empty ManySortedSign, o for OperSymbol of S, U0,U1, U2 for MSAlgebra over S; definition let S be non empty ManySortedSign, U0 be MSAlgebra over S; mode MSSubset of U0 is ManySortedSubset of the Sorts of U0; end; definition let S be non empty ManySortedSign; let IT be SortSymbol of S; attr IT is with_const_op means :: MSUALG_2:def 1 ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = IT; end; definition let IT be non empty ManySortedSign; attr IT is all-with_const_op means :: MSUALG_2:def 2 for s be SortSymbol of IT holds s is with_const_op; end; registration let A be non empty set, B be set, a be Function of B,A*, r be Function of B, A; cluster ManySortedSign(#A,B,a,r#) -> non empty; end; registration cluster non void all-with_const_op strict for non empty ManySortedSign; end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, s be SortSymbol of S; func Constants(U0,s) -> Subset of (the Sorts of U0).s means :: MSUALG_2:def 3 ex A being non empty set st A =(the Sorts of U0).s & it = { a where a is Element of A: ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S). o = s & a in rng Den(o,U0)} if (the Sorts of U0).s <> {} otherwise it = {}; end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; func Constants (U0) -> MSSubset of U0 means :: MSUALG_2:def 4 for s be SortSymbol of S holds it.s = Constants(U0,s); end; registration let S be all-with_const_op non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S, s be SortSymbol of S; cluster Constants(U0,s) -> non empty; end; registration let S be non void all-with_const_op non empty ManySortedSign, U0 be non-empty MSAlgebra over S; cluster Constants(U0) -> non-empty; end; begin :: :: Subalgebras of a Many Sorted Algebra. :: definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be OperSymbol of S, A be MSSubset of U0; pred A is_closed_on o means :: MSUALG_2:def 5 rng ((Den(o,U0))|((A# * the Arity of S).o )) c= (A * the ResultSort of S).o; end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0; attr A is opers_closed means :: MSUALG_2:def 6 for o be OperSymbol of S holds A is_closed_on o; end; theorem :: MSUALG_2:2 for S be non void non empty ManySortedSign, o be OperSymbol of S, U0 be MSAlgebra over S, B0, B1 be MSSubset of U0 st B0 c= B1 holds ((B0# * the Arity of S).o) c= ((B1# * the Arity of S).o); definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be OperSymbol of S, A be MSSubset of U0; assume A is_closed_on o; func o/.A ->Function of (A# * the Arity of S).o, (A * the ResultSort of S).o equals :: MSUALG_2:def 7 (Den(o,U0)) | ((A# * the Arity of S).o); end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0; func Opers(U0,A) -> ManySortedFunction of (A# * the Arity of S),(A * the ResultSort of S) means :: MSUALG_2:def 8 for o be OperSymbol of S holds it.o = o/.A; end; theorem :: MSUALG_2:3 for U0 being MSAlgebra over S for B being MSSubset of U0 st B=the Sorts of U0 holds B is opers_closed & for o holds o/.B = Den(o,U0); theorem :: MSUALG_2:4 for B being MSSubset of U0 st B=the Sorts of U0 holds Opers(U0,B) = the Charact of U0; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; mode MSSubAlgebra of U0 -> MSAlgebra over S means :: MSUALG_2:def 9 the Sorts of it is MSSubset of U0 & for B be MSSubset of U0 st B = the Sorts of it holds B is opers_closed & the Charact of it = Opers(U0,B); end; registration let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; cluster strict for MSSubAlgebra of U0; end; registration let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S; cluster MSAlgebra (#the Sorts of U0,the Charact of U0#) -> non-empty; end; registration let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S; cluster non-empty strict for MSSubAlgebra of U0; end; theorem :: MSUALG_2:5 the MSAlgebra of U0 = the MSAlgebra of U1 implies U0 is MSSubAlgebra of U1; theorem :: MSUALG_2:6 U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is MSSubAlgebra of U2; theorem :: MSUALG_2:7 U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 implies the MSAlgebra of U1 = the MSAlgebra of U2; theorem :: MSUALG_2:8 for U1,U2 be MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds U1 is MSSubAlgebra of U2; theorem :: MSUALG_2:9 for U1,U2 be MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds the MSAlgebra of U1 = the MSAlgebra of U2; theorem :: MSUALG_2:10 for S be non void non empty ManySortedSign, U0 be MSAlgebra over S, U1 be MSSubAlgebra of U0 holds Constants(U0) is MSSubset of U1; theorem :: MSUALG_2:11 for S be non void all-with_const_op non empty ManySortedSign, U0 be non-empty MSAlgebra over S, U1 be non-empty MSSubAlgebra of U0 holds Constants( U0) is non-empty MSSubset of U1; theorem :: MSUALG_2:12 for S be non void all-with_const_op non empty ManySortedSign, U0 be non-empty MSAlgebra over S, U1,U2 be non-empty MSSubAlgebra of U0 holds (the Sorts of U1) (/\) (the Sorts of U2) is non-empty; begin :: :: Many Sorted Subsets of a Many Sorted Algebra. :: definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0; func SubSort(A) -> set means :: MSUALG_2:def 10 for x be object holds x in it iff x in Funcs(the carrier of S, bool (Union (the Sorts of U0))) & x is MSSubset of U0 & for B be MSSubset of U0 st B = x holds B is opers_closed & Constants(U0) c= B & A c= B; end; registration let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0; cluster SubSort(A) -> non empty; end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; func SubSort(U0) -> set means :: MSUALG_2:def 11 for x be object holds x in it iff x in Funcs(the carrier of S, bool Union the Sorts of U0) & x is MSSubset of U0 & for B be MSSubset of U0 st B = x holds B is opers_closed; end; registration let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; cluster SubSort(U0) -> non empty; end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, e be Element of SubSort(U0); func @e -> MSSubset of U0 equals :: MSUALG_2:def 12 e; end; theorem :: MSUALG_2:13 for A,B be MSSubset of U0 holds B in SubSort(A) iff B is opers_closed & Constants(U0) c= B & A c= B; theorem :: MSUALG_2:14 for B be MSSubset of U0 holds B in SubSort(U0) iff B is opers_closed; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0, s be SortSymbol of S; func SubSort(A,s) -> set means :: MSUALG_2:def 13 for x be object holds x in it iff ex B be MSSubset of U0 st B in SubSort(A) & x = B.s; end; registration let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0, s be SortSymbol of S; cluster SubSort(A,s) -> non empty; end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0; func MSSubSort(A) -> MSSubset of U0 means :: MSUALG_2:def 14 for s be SortSymbol of S holds it.s = meet (SubSort(A,s)); end; theorem :: MSUALG_2:15 for A be MSSubset of U0 holds Constants(U0) (\/) A c= MSSubSort(A); theorem :: MSUALG_2:16 for A be MSSubset of U0 st Constants(U0) (\/) A is non-empty holds MSSubSort(A) is non-empty; theorem :: MSUALG_2:17 for A be MSSubset of U0 for B be MSSubset of U0 st B in SubSort( A) holds ((MSSubSort A)# * (the Arity of S)).o c= (B# * (the Arity of S)).o; theorem :: MSUALG_2:18 for A be MSSubset of U0 for B be MSSubset of U0 st B in SubSort( A) holds rng (Den(o,U0)|(((MSSubSort A)# * (the Arity of S)).o)) c= (B * (the ResultSort of S)).o; theorem :: MSUALG_2:19 for A be MSSubset of U0 holds rng ((Den(o,U0))|(((MSSubSort A)# * (the Arity of S)).o)) c= ((MSSubSort A) * (the ResultSort of S)).o; theorem :: MSUALG_2:20 for A be MSSubset of U0 holds MSSubSort(A) is opers_closed & A c= MSSubSort(A); begin :: :: Operations on Subalgebras of a Many Sorted Algebra. :: definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0; assume A is opers_closed; func U0|A -> strict MSSubAlgebra of U0 equals :: MSUALG_2:def 15 MSAlgebra (#A, Opers( U0,A) qua ManySortedFunction of (A# * the Arity of S),(A * the ResultSort of S) #); end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, U1,U2 be MSSubAlgebra of U0; func U1 /\ U2 -> strict MSSubAlgebra of U0 means :: MSUALG_2:def 16 the Sorts of it = (the Sorts of U1) (/\) (the Sorts of U2) & for B be MSSubset of U0 st B=the Sorts of it holds B is opers_closed & the Charact of it = Opers(U0,B); end; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be MSSubset of U0; func GenMSAlg(A) -> strict MSSubAlgebra of U0 means :: MSUALG_2:def 17 A is MSSubset of it & for U1 be MSSubAlgebra of U0 st A is MSSubset of U1 holds it is MSSubAlgebra of U1; end; registration let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S , A be non-empty MSSubset of U0; cluster GenMSAlg(A) -> non-empty; end; theorem :: MSUALG_2:21 for S be non void non empty ManySortedSign, U0 be MSAlgebra over S, B be MSSubset of U0 st B = the Sorts of U0 holds GenMSAlg(B) = the MSAlgebra of U0; theorem :: MSUALG_2:22 for S be non void non empty ManySortedSign, U0 be MSAlgebra over S, U1 be MSSubAlgebra of U0, B be MSSubset of U0 st B = the Sorts of U1 holds GenMSAlg(B) = the MSAlgebra of U1; theorem :: MSUALG_2:23 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S, U1 be MSSubAlgebra of U0 holds GenMSAlg(Constants(U0)) /\ U1 = GenMSAlg(Constants(U0)); definition let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S , U1,U2 be MSSubAlgebra of U0; func U1 "\/" U2 -> strict MSSubAlgebra of U0 means :: MSUALG_2:def 18 for A be MSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of U2) holds it = GenMSAlg(A); end; theorem :: MSUALG_2:24 for S be non void non empty ManySortedSign,U0 be non-empty MSAlgebra over S, U1 be MSSubAlgebra of U0, A,B be MSSubset of U0 st B = A (\/) the Sorts of U1 holds GenMSAlg(A) "\/" U1 = GenMSAlg(B); theorem :: MSUALG_2:25 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S, U1 be MSSubAlgebra of U0, B be MSSubset of U0 st B = the Sorts of U0 holds GenMSAlg(B) "\/" U1 = GenMSAlg(B); theorem :: MSUALG_2:26 for S be non void non empty ManySortedSign,U0 be non-empty MSAlgebra over S, U1,U2 be MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1; theorem :: MSUALG_2:27 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S, U1,U2 be MSSubAlgebra of U0 holds U1 /\ (U1"\/"U2) = the MSAlgebra of U1; theorem :: MSUALG_2:28 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S, U1,U2 be MSSubAlgebra of U0 holds (U1 /\ U2)"\/"U2 = the MSAlgebra of U2; begin :: :: The Lattice of SubAlgebras of a Many Sorted Algebra. :: definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; func MSSub(U0) -> set means :: MSUALG_2:def 19 for x being object holds x in it iff x is strict MSSubAlgebra of U0; end; registration let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; cluster MSSub(U0) -> non empty; end; definition let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S; func MSAlg_join(U0) -> BinOp of (MSSub(U0)) means :: MSUALG_2:def 20 for x,y be Element of MSSub(U0) holds for U1,U2 be strict MSSubAlgebra of U0 st x = U1 & y = U2 holds it.(x,y) = U1 "\/" U2; end; definition let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S; func MSAlg_meet(U0) -> BinOp of (MSSub(U0)) means :: MSUALG_2:def 21 for x,y be Element of MSSub(U0) holds for U1,U2 be strict MSSubAlgebra of U0 st x = U1 & y = U2 holds it.(x,y) = U1 /\ U2; end; reserve U0 for non-empty MSAlgebra over S; theorem :: MSUALG_2:29 MSAlg_join(U0) is commutative; theorem :: MSUALG_2:30 MSAlg_join(U0) is associative; theorem :: MSUALG_2:31 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S holds MSAlg_meet(U0) is commutative; theorem :: MSUALG_2:32 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S holds MSAlg_meet(U0) is associative; definition let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S; func MSSubAlLattice(U0) -> strict Lattice equals :: MSUALG_2:def 22 LattStr (# MSSub(U0), MSAlg_join(U0), MSAlg_meet(U0) #); end; theorem :: MSUALG_2:33 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S holds MSSubAlLattice(U0) is bounded; registration let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S; cluster MSSubAlLattice(U0) -> bounded; end; theorem :: MSUALG_2:34 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S holds Bottom (MSSubAlLattice(U0)) = GenMSAlg(Constants(U0)); theorem :: MSUALG_2:35 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S, B be MSSubset of U0 st B = the Sorts of U0 holds Top ( MSSubAlLattice(U0)) = GenMSAlg(B); theorem :: MSUALG_2:36 for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S holds Top (MSSubAlLattice(U0)) = the MSAlgebra of U0; theorem :: MSUALG_2:37 for S being non void non empty ManySortedSign, U0 being MSAlgebra over S holds MSAlgebra (#the Sorts of U0,the Charact of U0#) is MSSubAlgebra of U0 ; theorem :: MSUALG_2:38 for S being non void non empty ManySortedSign, U0 being MSAlgebra over S, A being MSSubset of U0 holds the Sorts of U0 in SubSort(A); theorem :: MSUALG_2:39 for S being non void non empty ManySortedSign, U0 being MSAlgebra over S, A being MSSubset of U0 holds SubSort(A) c= SubSort(U0);