:: On the Lattice of Subalgebras of a Universal Algebra :: by Miros{\l}aw Jan Paszek :: :: Received May 23, 1995 :: Copyright (c) 1995-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 UNIALG_1, UNIALG_2, XBOOLE_0, SUBSET_1, GROUP_2, STRUCT_0, ORDERS_3, FUNCT_1, ZFMISC_1, CARD_1, FINSEQ_1, TARSKI, PARTFUN1, RELAT_1, FINSEQ_2, NUMBERS, CQC_SIM1, SETFAM_1, PBOOLE, EQREL_1, XXREAL_2, LATTICES, REWRITE1, LATTICE3, VECTSP_8, UNIALG_3; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, SETFAM_1, RELAT_1, FUNCT_1, STRUCT_0, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_2, MARGREL1, LATTICES, LATTICE3, UNIALG_1, UNIALG_2; constructors BINOP_1, DOMAIN_1, LATTICE3, UNIALG_2, RELSET_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, UNIALG_2, ORDINAL1, FINSEQ_1, CARD_1; requirements BOOLE, SUBSET; begin reserve U0 for Universal_Algebra, U1 for SubAlgebra of U0, o for operation of U0; definition let U0; mode SubAlgebra-Family of U0 -> set means :: UNIALG_3:def 1 for U1 be set st U1 in it holds U1 is SubAlgebra of U0; end; registration let U0; cluster non empty for SubAlgebra-Family of U0; end; definition let U0; redefine func Sub(U0) -> non empty SubAlgebra-Family of U0; let U00 be non empty SubAlgebra-Family of U0; redefine mode Element of U00 -> SubAlgebra of U0; end; definition let U0; let u be Element of Sub(U0); func carr u -> Subset of U0 means :: UNIALG_3:def 2 ex U1 being SubAlgebra of U0 st u = U1 & it = the carrier of U1; end; definition let U0; func Carr U0 -> Function of Sub(U0), bool the carrier of U0 means :: UNIALG_3:def 3 for u being Element of Sub(U0) holds it.u = carr u; end; theorem :: UNIALG_3:1 for u being object holds u in Sub(U0) iff ex U1 be strict SubAlgebra of U0 st u = U1; theorem :: UNIALG_3:2 for H being non empty Subset of U0 for o holds arity o = 0 implies (H is_closed_on o iff o.{} in H); theorem :: UNIALG_3:3 for U1 be SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0; theorem :: UNIALG_3:4 for H being non empty Subset of U0 for o holds H is_closed_on o & arity o = 0 implies (o/.H) = o; theorem :: UNIALG_3:5 Constants(U0) = { o.{} where o is operation of U0: arity o = 0 }; theorem :: UNIALG_3:6 for U0 be with_const_op Universal_Algebra for U1 be SubAlgebra of U0 holds Constants(U0) = Constants(U1); registration let U0 be with_const_op Universal_Algebra; cluster -> with_const_op for SubAlgebra of U0; end; theorem :: UNIALG_3:7 for U0 be with_const_op Universal_Algebra for U1,U2 be SubAlgebra of U0 holds Constants(U1) = Constants(U2); definition let U0; redefine func Carr U0 means :: UNIALG_3:def 4 for u being Element of Sub(U0), U1 being SubAlgebra of U0 st u = U1 holds it.u = the carrier of U1; end; theorem :: UNIALG_3:8 for H being strict SubAlgebra of U0 for u being Element of U0 holds u in (Carr U0).H iff u in H; theorem :: UNIALG_3:9 for H be non empty Subset of Sub(U0) holds ((Carr U0).:H) is non empty; theorem :: UNIALG_3:10 for U0 being with_const_op Universal_Algebra for U1 being strict SubAlgebra of U0 holds Constants(U0) c= (Carr U0).U1; theorem :: UNIALG_3:11 for U0 being with_const_op Universal_Algebra for U1 be SubAlgebra of U0 for a be set holds a is Element of Constants(U0) implies a in the carrier of U1; theorem :: UNIALG_3:12 for U0 being with_const_op Universal_Algebra for H be non empty Subset of Sub(U0) holds meet ((Carr U0).:H) is non empty Subset of U0; theorem :: UNIALG_3:13 for U0 being with_const_op Universal_Algebra holds the carrier of UnSubAlLattice(U0) = Sub(U0); theorem :: UNIALG_3:14 for U0 being with_const_op Universal_Algebra for H be non empty Subset of Sub(U0) for S being non empty Subset of U0 st S = meet ((Carr U0).:H) holds S is opers_closed; definition let U0 be with_const_op strict Universal_Algebra; let H be non empty Subset of Sub(U0); func meet H -> strict SubAlgebra of U0 means :: UNIALG_3:def 5 the carrier of it = meet ((Carr U0).:H); end; theorem :: UNIALG_3:15 for U0 being with_const_op Universal_Algebra for l1,l2 being Element of UnSubAlLattice(U0), U1,U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds l1 [= l2 iff the carrier of U1 c= the carrier of U2; theorem :: UNIALG_3:16 for U0 being with_const_op Universal_Algebra for l1,l2 being Element of UnSubAlLattice(U0), U1,U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds l1 [= l2 iff U1 is SubAlgebra of U2; theorem :: UNIALG_3:17 for U0 being with_const_op strict Universal_Algebra holds UnSubAlLattice(U0) is bounded; registration let U0 be with_const_op strict Universal_Algebra; cluster UnSubAlLattice U0 -> bounded; end; theorem :: UNIALG_3:18 for U0 being with_const_op strict Universal_Algebra for U1 be strict SubAlgebra of U0 holds GenUnivAlg(Constants(U0)) /\ U1 = GenUnivAlg( Constants(U0)); theorem :: UNIALG_3:19 for U0 being with_const_op strict Universal_Algebra holds Bottom ( UnSubAlLattice(U0)) = GenUnivAlg(Constants(U0)); theorem :: UNIALG_3:20 for U0 being with_const_op strict Universal_Algebra for U1 be SubAlgebra of U0 for H be Subset of U0 st H = the carrier of U0 holds GenUnivAlg(H) "\/" U1 = GenUnivAlg(H); theorem :: UNIALG_3:21 for U0 being with_const_op strict Universal_Algebra for H be Subset of U0 st H = the carrier of U0 holds Top (UnSubAlLattice(U0)) = GenUnivAlg(H); theorem :: UNIALG_3:22 for U0 being with_const_op strict Universal_Algebra holds Top ( UnSubAlLattice(U0)) = U0; theorem :: UNIALG_3:23 for U0 being with_const_op strict Universal_Algebra holds UnSubAlLattice(U0) is complete; definition let U01,U02 be with_const_op Universal_Algebra; let F be Function of the carrier of U01, the carrier of U02; func FuncLatt F -> Function of the carrier of UnSubAlLattice(U01), the carrier of UnSubAlLattice(U02) means :: UNIALG_3:def 6 for U1 being strict SubAlgebra of U01, H being Subset of U02 st H = F.: the carrier of U1 holds it.U1 = GenUnivAlg(H); end; theorem :: UNIALG_3:24 for U0 being with_const_op strict Universal_Algebra for F being Function of the carrier of U0, the carrier of U0 st F = id the carrier of U0 holds FuncLatt F = id the carrier of UnSubAlLattice(U0);