:: Subalgebras of the Universal Algebra. Lattices of Subalgebras :: by Ewa Burakowska :: :: Received July 8, 1993 :: Copyright (c) 1993-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, XBOOLE_0, SUBSET_1, FINSEQ_2, TARSKI, UNIALG_1, FUNCT_2, PARTFUN1, RELAT_1, FINSEQ_1, FUNCOP_1, STRUCT_0, CQC_SIM1, FUNCT_1, CARD_1, ZFMISC_1, SETFAM_1, EQREL_1, BINOP_1, LATTICES, UNIALG_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, SETFAM_1, FUNCOP_1, PARTFUN1, FINSEQ_2, LATTICES, BINOP_1, UNIALG_1, MARGREL1; constructors SETFAM_1, BINOP_1, DOMAIN_1, FUNCOP_1, LATTICES, UNIALG_1, MARGREL1, FINSEQ_2, RELSET_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, FINSEQ_2, STRUCT_0, LATTICES, UNIALG_1, ORDINAL1, FINSEQ_1, CARD_1, MARGREL1; requirements BOOLE, SUBSET, NUMERALS; begin reserve U0,U1,U2,U3 for Universal_Algebra, n for Nat, x,y for set; definition let U1; mode PFuncsDomHQN of U1 is PFuncsDomHQN of (the carrier of U1); end; definition let U1 be UAStr; mode PartFunc of U1 is PartFunc of (the carrier of U1)*,the carrier of U1; end; definition let U1,U2; pred U1,U2 are_similar means :: UNIALG_2:def 1 signature (U1) = signature (U2); symmetry; reflexivity; end; theorem :: UNIALG_2:1 U1,U2 are_similar implies len the charact of(U1) = len the charact of( U2); theorem :: UNIALG_2:2 U1,U2 are_similar & U2,U3 are_similar implies U1,U3 are_similar; theorem :: UNIALG_2:3 rng the charact of(U0) is non empty Subset of PFuncs((the carrier of U0)*,the carrier of U0); definition let U0; func Operations(U0) -> PFuncsDomHQN of U0 equals :: UNIALG_2:def 2 rng the charact of(U0); end; definition let U1; mode operation of U1 is Element of Operations(U1); end; reserve A for non empty Subset of U0, o for operation of U0, x1,y1 for FinSequence of A; definition let U0 be Universal_Algebra, A be Subset of U0, o be operation of U0; pred A is_closed_on o means :: UNIALG_2:def 3 for s being FinSequence of A st len s = arity o holds o.s in A; end; definition let U0 be Universal_Algebra, A be Subset of U0; attr A is opers_closed means :: UNIALG_2:def 4 for o be operation of U0 holds A is_closed_on o; end; definition let U0,A,o; assume A is_closed_on o; func o/.A ->homogeneous quasi_total non empty PartFunc of A*,A equals :: UNIALG_2:def 5 o|((arity o)-tuples_on A); end; definition let U0,A; func Opers(U0,A) -> PFuncFinSequence of A means :: UNIALG_2:def 6 dom it = dom the charact of(U0) & for n being set,o st n in dom it & o =(the charact of(U0)).n holds it.n = o/.A; end; theorem :: UNIALG_2:4 for B being non empty Subset of U0 st B=the carrier of U0 holds B is opers_closed & for o holds o/.B = o; theorem :: UNIALG_2:5 for U1 be Universal_Algebra, A be non empty Subset of U1, o be operation of U1 st A is_closed_on o holds arity (o/.A) = arity o; definition let U0; mode SubAlgebra of U0 -> Universal_Algebra means :: UNIALG_2:def 7 the carrier of it is Subset of U0 & for B be non empty Subset of U0 st B=the carrier of it holds the charact of it = Opers(U0,B) & B is opers_closed; end; registration let U0 be Universal_Algebra; cluster strict for SubAlgebra of U0; end; theorem :: UNIALG_2:6 for U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be operation of U1, n be Nat st U0 is SubAlgebra of U1 & n in dom the charact of( U0) & o0 = (the charact of(U0)).n & o1 = (the charact of(U1)).n holds arity o0 = arity o1; theorem :: UNIALG_2:7 U0 is SubAlgebra of U1 implies dom the charact of(U0)=dom the charact of(U1); theorem :: UNIALG_2:8 U0 is SubAlgebra of U0; theorem :: UNIALG_2:9 U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is SubAlgebra of U2; theorem :: UNIALG_2:10 U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2 ; theorem :: UNIALG_2:11 for U1,U2 be SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds U1 is SubAlgebra of U2; theorem :: UNIALG_2:12 for U1,U2 be strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds U1 = U2; theorem :: UNIALG_2:13 U1 is SubAlgebra of U2 implies U1,U2 are_similar; theorem :: UNIALG_2:14 for A be non empty Subset of U0 holds UAStr (#A,Opers(U0,A)#) is strict Universal_Algebra; definition let U0 be Universal_Algebra, A be non empty Subset of U0; assume A is opers_closed; func UniAlgSetClosed(A) -> strict SubAlgebra of U0 equals :: UNIALG_2:def 8 UAStr (# A, Opers(U0,A) #); end; definition let U0; let U1,U2 be SubAlgebra of U0; assume the carrier of U1 meets the carrier of U2; func U1 /\ U2 -> strict SubAlgebra of U0 means :: UNIALG_2:def 9 the carrier of it = ( the carrier of U1) /\ (the carrier of U2) & for B be non empty Subset of U0 st B=the carrier of it holds the charact of(it) = Opers(U0,B) & B is opers_closed; end; definition let U0; func Constants(U0) -> Subset of U0 equals :: UNIALG_2:def 10 { a where a is Element of U0: ex o be operation of U0 st arity o=0 & a in rng o}; end; definition let IT be Universal_Algebra; attr IT is with_const_op means :: UNIALG_2:def 11 ex o being operation of IT st arity o =0; end; registration cluster with_const_op strict for Universal_Algebra; end; registration let U0 be with_const_op Universal_Algebra; cluster Constants(U0) -> non empty; end; theorem :: UNIALG_2:15 for U0 be Universal_Algebra, U1 be SubAlgebra of U0 holds Constants(U0) is Subset of U1; theorem :: UNIALG_2:16 for U0 be with_const_op Universal_Algebra, U1 be SubAlgebra of U0 holds Constants(U0) is non empty Subset of U1; theorem :: UNIALG_2:17 for U0 be with_const_op Universal_Algebra,U1,U2 be SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2; definition let U0 be Universal_Algebra, A be Subset of U0; assume Constants(U0) <> {} or A <> {}; func GenUnivAlg(A) -> strict SubAlgebra of U0 means :: UNIALG_2:def 12 A c= the carrier of it & for U1 be SubAlgebra of U0 st A c= the carrier of U1 holds it is SubAlgebra of U1; end; theorem :: UNIALG_2:18 for U0 be strict Universal_Algebra holds GenUnivAlg([#](the carrier of U0)) = U0; theorem :: UNIALG_2:19 for U0 be Universal_Algebra, U1 be strict SubAlgebra of U0, B be non empty Subset of U0 st B = the carrier of U1 holds GenUnivAlg(B) = U1; definition let U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0; func U1 "\/" U2 -> strict SubAlgebra of U0 means :: UNIALG_2:def 13 for A be non empty Subset of U0 st A = (the carrier of U1) \/ (the carrier of U2) holds it = GenUnivAlg(A); end; theorem :: UNIALG_2:20 for U0 be Universal_Algebra, U1 be SubAlgebra of U0, A,B be Subset of U0 st (A <> {} or Constants(U0) <> {}) & B = A \/ the carrier of U1 holds GenUnivAlg(A) "\/" U1 = GenUnivAlg(B); theorem :: UNIALG_2:21 for U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1; theorem :: UNIALG_2:22 for U0 be with_const_op Universal_Algebra,U1,U2 be strict SubAlgebra of U0 holds U1 /\ (U1"\/"U2) = U1; theorem :: UNIALG_2:23 for U0 be with_const_op Universal_Algebra,U1,U2 be strict SubAlgebra of U0 holds (U1 /\ U2)"\/"U2 = U2; definition let U0 be Universal_Algebra; func Sub(U0) -> set means :: UNIALG_2:def 14 for x being object holds x in it iff x is strict SubAlgebra of U0; end; registration let U0 be Universal_Algebra; cluster Sub(U0) -> non empty; end; definition let U0 be Universal_Algebra; func UniAlg_join(U0) -> BinOp of Sub(U0) means :: UNIALG_2:def 15 for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds it. (x,y) = U1 "\/" U2; end; definition let U0 be Universal_Algebra; func UniAlg_meet(U0) -> BinOp of Sub(U0) means :: UNIALG_2:def 16 for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds it. (x,y) = U1 /\ U2; end; theorem :: UNIALG_2:24 UniAlg_join(U0) is commutative; theorem :: UNIALG_2:25 UniAlg_join(U0) is associative; theorem :: UNIALG_2:26 for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0) is commutative; theorem :: UNIALG_2:27 for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0) is associative; definition let U0 be with_const_op Universal_Algebra; func UnSubAlLattice(U0) -> strict Lattice equals :: UNIALG_2:def 17 LattStr (# Sub(U0), UniAlg_join(U0), UniAlg_meet(U0) #); end;