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