Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras

by
Josef Urban

MML identifier: OSALG_2
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, PBOOLE, ZF_REFLE, BOOLE, CARD_3, AMI_1, MSUALG_1,
UNIALG_2, TDGROUP, QC_LANG1, PRALG_1, PROB_1, TARSKI, SETFAM_1, LATTICES,
BINOP_1, MSUALG_2, OSALG_1, ORDERS_1, SEQM_3, OSALG_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
SETFAM_1, LATTICES, BINOP_1, PROB_1, CARD_3, MBOOLEAN, PBOOLE, MSUALG_1,
ORDERS_1, MSUALG_2, YELLOW18, OSALG_1;
constructors MBOOLEAN, PROB_1, ORDERS_3, OSALG_1, YELLOW18, MSUALG_2;
clusters FUNCT_1, LATTICES, MSUALG_1, RELSET_1, STRUCT_0, RLSUB_2, SUBSET_1,
ORDERS_3, OSALG_1, MSUALG_2, MSAFREE, XBOOLE_0;
requirements BOOLE, SUBSET;

begin :: Auxiliary facts about Order Sorted Sets.

reserve x for set,
R for non empty Poset;

:: should be clusters, but that requires redef of the operation
theorem :: OSALG_2:1
for X,Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R;

theorem :: OSALG_2:2
for X,Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R;

definition let R be non empty Poset,
M be OrderSortedSet of R; :: can be for ManySortedSet
mode OrderSortedSubset of M -> ManySortedSubset of M means
:: OSALG_2:def 1
it is OrderSortedSet of R;
end;

definition let R be non empty Poset,
M be non-empty OrderSortedSet of R;
cluster non-empty OrderSortedSubset of M;
end;

begin
::
::  Constants of an Order Sorted Algebra.
::

definition let S be OrderSortedSign,
U0 be OSAlgebra of S;
mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means
:: OSALG_2:def 2
it is OrderSortedSet of S;
end;

:: very strange, the cluster in OSALG_1 should take care of this one
definition let S be OrderSortedSign;
cluster monotone strict non-empty OSAlgebra of S;
end;

definition
let S be OrderSortedSign,
U0 be non-empty OSAlgebra of S;
cluster non-empty OSSubset of U0;
end;

theorem :: OSALG_2:3
for S0 being non void all-with_const_op strict (non empty ManySortedSign)
holds OSSign S0 is all-with_const_op;

definition
cluster all-with_const_op strict OrderSortedSign;
end;

begin
::
::   Subalgebras of a Order Sorted Algebra.
::

theorem :: OSALG_2:4
for S being OrderSortedSign,
U0 being OSAlgebra of S holds
MSAlgebra (#the Sorts of U0,the Charact of U0#) is order-sorted;

definition let S be OrderSortedSign,
U0 be OSAlgebra of S; :: can't for ms!
cluster order-sorted MSSubAlgebra of U0;
end;

definition let S be OrderSortedSign,
U0 be OSAlgebra of S;
mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;
end;

definition let S be OrderSortedSign,
U0 be OSAlgebra of S;
cluster strict OSSubAlgebra of U0;
end;

definition let S be OrderSortedSign,
U0 be non-empty OSAlgebra of S;
cluster non-empty strict OSSubAlgebra of U0;
end;

:: the equivalent def, maybe not needed
theorem :: OSALG_2:5
for S being OrderSortedSign
for U0 being OSAlgebra of S
for U1 being MSAlgebra over S holds
U1 is OSSubAlgebra of U0 iff
the Sorts of U1 is OSSubset of U0 &
for B be OSSubset of U0 st B = the Sorts of U1 holds
B is opers_closed & the Charact of U1 = Opers(U0,B);

reserve S1 for OrderSortedSign,
OU0 for OSAlgebra of S1;
reserve s,s1,s2,s3,s4 for SortSymbol of S1;

definition let S1,OU0,s;
func OSConstants(OU0,s) -> Subset of (the Sorts of OU0).s equals
:: OSALG_2:def 3
union {Constants(OU0,s2) : s2 <= s};
end;

:: maybe
:: theorem S1 is discrete implies OSConstants(OU0,s) = Constants(OU0,s);

canceled 5;

theorem :: OSALG_2:11
Constants(OU0,s) c= OSConstants(OU0,s);

definition let S1;
let M be ManySortedSet of the carrier of S1;
func OSCl M -> OrderSortedSet of S1 means
:: OSALG_2:def 4
for s be SortSymbol of S1 holds it.s = union { M.s1: s1 <= s};
end;

theorem :: OSALG_2:12
for M being ManySortedSet of the carrier of S1 holds
M c= OSCl M;

theorem :: OSALG_2:13
for M being ManySortedSet of the carrier of S1,
A being OrderSortedSet of S1 holds
M c= A implies OSCl M c= A;

theorem :: OSALG_2:14
for S being OrderSortedSign,
X being OrderSortedSet of S holds OSCl X = X;

:: following should be rewritten to use OSCl Constants(OU0) instead;
:: maybe later
definition let S1,OU0;
func OSConstants (OU0) -> OSSubset of OU0 means
:: OSALG_2:def 5
for s be SortSymbol of S1 holds it.s = OSConstants(OU0,s);
end;

theorem :: OSALG_2:15
Constants(OU0) c= OSConstants(OU0);

theorem :: OSALG_2:16
for A being OSSubset of OU0 holds Constants(OU0) c= A implies
OSConstants(OU0) c= A;

theorem :: OSALG_2:17
for A being OSSubset of OU0 holds
OSConstants(OU0) = OSCl Constants(OU0);

theorem :: OSALG_2:18
for OU1 being OSSubAlgebra of OU0 holds
OSConstants(OU0) is OSSubset of OU1;

theorem :: OSALG_2:19
for S being all-with_const_op OrderSortedSign,
OU0 being non-empty OSAlgebra of S,
OU1 being non-empty OSSubAlgebra of OU0 holds
OSConstants(OU0) is non-empty OSSubset of OU1;

begin
::
::  Order Sorted Subsets of an Order Sorted Algebra.
::

:: this should be in MSUALG_2
theorem :: OSALG_2:20
for I being set
for M being ManySortedSet of I
for x being set holds
x is ManySortedSubset of M iff
x in product bool M;

:: Fraenkel should be improved, to allow more than just Element type
definition let R be non empty Poset,
M be OrderSortedSet of R;
func OSbool(M) -> set means
:: OSALG_2:def 6
for x being set holds x in it iff x is OrderSortedSubset of M;
end;

definition let S be OrderSortedSign,
U0 be OSAlgebra of S,
A be OSSubset of U0;
func OSSubSort(A) -> set equals
:: OSALG_2:def 7
{ x where x is Element of SubSort(A): x is OrderSortedSet of S};
end;

theorem :: OSALG_2:21
for A being OSSubset of OU0 holds OSSubSort(A) c= SubSort(A);

theorem :: OSALG_2:22
for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort(A);

definition let S1,OU0;
let A be OSSubset of OU0;
cluster OSSubSort(A) -> non empty;
end;

definition let S1,OU0;
func OSSubSort(OU0) -> set equals
:: OSALG_2:def 8
{ x where x is Element of SubSort(OU0): x is OrderSortedSet of S1};
end;

theorem :: OSALG_2:23
for A being OSSubset of OU0 holds OSSubSort(A) c= OSSubSort(OU0);

definition let S1,OU0;
cluster OSSubSort(OU0) -> non empty;
end;

:: new-def for order-sorted
definition let S1,OU0;
let e be Element of OSSubSort(OU0);
func @e -> OSSubset of OU0 equals
:: OSALG_2:def 9
e;
end;

:: maybe do another definition of ossort, saying that it contains
:: Elements of subsort which are order-sorted (or ossubsets)
theorem :: OSALG_2:24
for A,B be OSSubset of OU0 holds
B in OSSubSort(A) iff B is opers_closed &
OSConstants(OU0) c= B & A c= B;

theorem :: OSALG_2:25
for B be OSSubset of OU0 holds B in OSSubSort(OU0) iff B is opers_closed;

:: slices of members of OSsubsort
definition let S1,OU0;
let A be OSSubset of OU0,
s be Element of S1;
func OSSubSort(A,s) -> set means
:: OSALG_2:def 10
for x be set holds
x in it iff ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s;
end;

theorem :: OSALG_2:26
for A being OSSubset of OU0,
s1,s2 being SortSymbol of S1 holds
s1 <= s2 implies OSSubSort(A,s2) is_coarser_than OSSubSort(A,s1);

theorem :: OSALG_2:27
for A being OSSubset of OU0, s being SortSymbol of S1 holds
OSSubSort(A,s) c= SubSort(A,s);

theorem :: OSALG_2:28
for A being OSSubset of OU0, s being SortSymbol of S1 holds
(the Sorts of OU0).s in OSSubSort(A,s);

definition let S1,OU0;
let A be OSSubset of OU0,
s be SortSymbol of S1;
cluster OSSubSort(A,s) -> non empty;
end;

definition let S1,OU0;
let A be OSSubset of OU0;
func OSMSubSort(A) -> OSSubset of OU0 means
:: OSALG_2:def 11
for s be SortSymbol of S1 holds it.s = meet (OSSubSort(A,s));
end;

definition let S1,OU0;
canceled;
cluster opers_closed OSSubset of OU0;
end;

theorem :: OSALG_2:29
for A be OSSubset of OU0 holds OSConstants(OU0) \/ A c= OSMSubSort(A);

theorem :: OSALG_2:30
for A be OSSubset of OU0 st OSConstants(OU0) \/ A is non-empty holds
OSMSubSort(A) is non-empty;

theorem :: OSALG_2:31
for o be OperSymbol of S1
for A be OSSubset of OU0
for B be OSSubset of OU0 st B in OSSubSort(A) holds
((OSMSubSort A)# * (the Arity of S1)).o c= (B# * (the Arity of S1)).o;

theorem :: OSALG_2:32
for o be OperSymbol of S1
for A be OSSubset of OU0
for B be OSSubset of OU0 st B in OSSubSort(A) holds
rng (Den(o,OU0)|(((OSMSubSort A)# * (the Arity of S1)).o)) c=
(B * (the ResultSort of S1)).o;

theorem :: OSALG_2:33
for o be OperSymbol of S1
for A be OSSubset of OU0 holds
rng ((Den(o,OU0))|(((OSMSubSort A)# * (the Arity of S1)).o)) c=
((OSMSubSort A) * (the ResultSort of S1)).o;

theorem :: OSALG_2:34
for A be OSSubset of OU0 holds
OSMSubSort(A) is opers_closed & A c= OSMSubSort(A);

definition
let S1,OU0;
let A be OSSubset of OU0;
cluster OSMSubSort(A) -> opers_closed;
end;

begin :: Operations on Subalgebras of an Order Sorted Algebra.

definition let S1,OU0;
let A be opers_closed OSSubset of OU0;
cluster OU0|A -> order-sorted;
end;

definition let S1,OU0;
let OU1,OU2 be OSSubAlgebra of OU0;
cluster OU1 /\ OU2 -> order-sorted;
end;

:: generally, GenOSAlg can differ from GenMSAlg, example should be given
definition
let S1,OU0;
let A be OSSubset of OU0;
func GenOSAlg(A) -> strict OSSubAlgebra of OU0 means
:: OSALG_2:def 13
A is OSSubset of it &
for OU1 be OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
it is OSSubAlgebra of OU1;
end;

:: this should rather be a definition, but I want to keep
:: compatibility of the definition with MSUALG_2
theorem :: OSALG_2:35
for A be OSSubset of OU0 holds
GenOSAlg(A) = OU0 | OSMSubSort(A) &
the Sorts of GenOSAlg(A) = OSMSubSort(A);

:: this could simplify some proofs in MSUALG_2, I need it anyway
theorem :: OSALG_2:36
for S be non void non empty ManySortedSign
for U0 be MSAlgebra over S
for A be MSSubset of U0 holds
GenMSAlg(A) = U0 | MSSubSort(A) &
the Sorts of GenMSAlg(A) = MSSubSort(A);

theorem :: OSALG_2:37
for A being OSSubset of OU0 holds
the Sorts of GenMSAlg(A) c= the Sorts of GenOSAlg(A);

theorem :: OSALG_2:38
for A being OSSubset of OU0 holds
GenMSAlg(A) is MSSubAlgebra of GenOSAlg(A);

theorem :: OSALG_2:39
for OU0 being strict OSAlgebra of S1
for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg(B) = OU0;

theorem :: OSALG_2:40
for OU1 being strict OSSubAlgebra of OU0,
B being OSSubset of OU0 st B = the Sorts of OU1
holds GenOSAlg(B) = OU1;

theorem :: OSALG_2:41
for U0 be non-empty OSAlgebra of S1,
U1 be OSSubAlgebra of U0 holds
GenOSAlg(OSConstants(U0)) /\ U1 = GenOSAlg(OSConstants(U0));

definition let S1;
let U0 be non-empty OSAlgebra of S1,
U1,U2 be OSSubAlgebra of U0;
func U1 "\/"_os U2 -> strict OSSubAlgebra of U0 means
:: OSALG_2:def 14
for A be OSSubset of U0 st
A = (the Sorts of U1) \/ (the Sorts of U2) holds it = GenOSAlg(A);
end;

theorem :: OSALG_2:42
for U0 be non-empty OSAlgebra of S1,
U1 be OSSubAlgebra of U0, A,B be OSSubset of U0
st B = A \/ the Sorts of U1
holds GenOSAlg(A) "\/"_os U1 = GenOSAlg(B);

theorem :: OSALG_2:43
for U0 be non-empty OSAlgebra of S1,
U1 be OSSubAlgebra of U0, B be OSSubset of U0
st B = the Sorts of U0
holds GenOSAlg(B) "\/"_os U1 = GenOSAlg(B);

theorem :: OSALG_2:44
for U0 being non-empty OSAlgebra of S1,
U1,U2 be OSSubAlgebra of U0 holds
U1 "\/"_os U2 = U2 "\/"_os U1;

theorem :: OSALG_2:45
for U0 be non-empty OSAlgebra of S1,
U1,U2 be strict OSSubAlgebra of U0 holds
U1 /\ (U1"\/"_os U2) = U1;

theorem :: OSALG_2:46
for U0 be non-empty OSAlgebra of S1,
U1,U2 be strict OSSubAlgebra of U0
holds (U1 /\ U2) "\/"_os U2 = U2;

begin :: The Lattice of SubAlgebras of an Order Sorted Algebra.

:: ossub, ossubalgebra
definition let S1,OU0;
func OSSub(OU0) -> set means
:: OSALG_2:def 15
for x holds x in it iff x is strict OSSubAlgebra of OU0;
end;

theorem :: OSALG_2:47
OSSub(OU0) c= MSSub(OU0);

definition let S be OrderSortedSign,
U0 be OSAlgebra of S;
cluster OSSub(U0) -> non empty;
end;

definition let S1,OU0;
redefine func OSSub(OU0) -> Subset of MSSub(OU0);
end;

:: maybe show that e.g. for TrivialOSA(S,z,z1), OSSub(U0) is
:: proper subset of MSSub(U0), to have some counterexamples
definition let S1;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_join(U0) -> BinOp of (OSSub(U0)) means
:: OSALG_2:def 16
for x,y be Element of OSSub(U0) holds
for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
it.(x,y) = U1 "\/"_os U2;
end;

definition let S1;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_meet(U0) -> BinOp of (OSSub(U0)) means
:: OSALG_2:def 17
for x,y be Element of OSSub(U0) holds
for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
it.(x,y) = U1 /\ U2;
end;

theorem :: OSALG_2:48
for U0 being non-empty OSAlgebra of S1
for x,y being Element of OSSub(U0) holds
(OSAlg_meet(U0)).(x,y) = (MSAlg_meet(U0)).(x,y);

reserve U0 for non-empty OSAlgebra of S1;

theorem :: OSALG_2:49
OSAlg_join(U0) is commutative;

theorem :: OSALG_2:50
OSAlg_join(U0) is associative;

theorem :: OSALG_2:51
OSAlg_meet(U0) is commutative;

theorem :: OSALG_2:52
OSAlg_meet(U0) is associative;

definition let S1;
let U0 be non-empty OSAlgebra of S1;
func OSSubAlLattice(U0) -> strict Lattice equals
:: OSALG_2:def 18
LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #);
end;

theorem :: OSALG_2:53
for U0 be non-empty OSAlgebra of S1 holds OSSubAlLattice(U0) is bounded;

definition let S1;
let U0 be non-empty OSAlgebra of S1;
cluster OSSubAlLattice(U0) -> bounded;
end;

theorem :: OSALG_2:54
for U0 be non-empty OSAlgebra of S1
holds Bottom (OSSubAlLattice(U0)) = GenOSAlg(OSConstants(U0));

theorem :: OSALG_2:55
for U0 be non-empty OSAlgebra of S1,
B be OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice(U0)) = GenOSAlg(B);

theorem :: OSALG_2:56
for U0 be strict non-empty OSAlgebra of S1 holds
Top (OSSubAlLattice(U0)) = U0;

```