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