:: Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received March 4, 1997
:: Copyright (c) 1997-2018 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 XBOOLE_0, RELAT_2, ORDERS_2, SUBSET_1, XXREAL_0, WAYBEL_8,
TARSKI, RCOMP_1, STRUCT_0, YELLOW_0, LATTICE3, CARD_FIL, LATTICES,
WAYBEL_0, WAYBEL_5, GROUP_6, WAYBEL10, YELLOW_1, FINSET_1, SETFAM_1,
REWRITE1, RELAT_1, FUNCT_1, ZFMISC_1, CAT_1, EQREL_1, WELLORD2, ORDINAL2,
WAYBEL_3, SEQM_3, PBOOLE, CARD_3, WELLORD1, WAYBEL_1, YELLOW_2;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, RELAT_1,
ORDERS_1, ORDERS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0,
PBOOLE, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1,
WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10;
constructors DOMAIN_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_8,
WAYBEL10, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1,
STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1,
WAYBEL_3, WAYBEL_8, WAYBEL10;
requirements SUBSET, BOOLE;
begin :: Preliminaries
theorem :: WAYBEL13:1
for L be non empty reflexive transitive RelStr for x,y be Element
of L holds x <= y implies compactbelow x c= compactbelow y;
theorem :: WAYBEL13:2
for L be non empty reflexive RelStr for x be Element of L holds
compactbelow x is Subset of CompactSublatt L;
theorem :: WAYBEL13:3
for L be RelStr for S be SubRelStr of L for X be Subset of S
holds X is Subset of L;
theorem :: WAYBEL13:4
for L be with_suprema non empty reflexive transitive RelStr holds
the carrier of L is Ideal of L;
theorem :: WAYBEL13:5
for L1 be lower-bounded non empty reflexive antisymmetric RelStr
for L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the
RelStr of L2 & L1 is up-complete holds the carrier of CompactSublatt L1 = the
carrier of CompactSublatt L2;
begin :: Algebraic and Arithmetic Lattices
theorem :: WAYBEL13:6 :: COROLLARY 4.10.
for L be algebraic lower-bounded LATTICE for S be CLSubFrame of L
holds S is algebraic;
theorem :: WAYBEL13:7 :: EXAMPLES 4.11.(2)
for X,E be set for L be CLSubFrame of BoolePoset X holds E in the
carrier of CompactSublatt L iff ex F be Element of BoolePoset X st F is finite
& E = meet { Y where Y is Element of L : F c= Y } & F c= E;
theorem :: WAYBEL13:8
for L be lower-bounded sup-Semilattice holds InclPoset Ids L is
CLSubFrame of BoolePoset the carrier of L;
registration
let L be non empty reflexive transitive RelStr;
cluster principal for Ideal of L;
end;
theorem :: WAYBEL13:9
for L be lower-bounded sup-Semilattice for X be non empty
directed Subset of InclPoset Ids L holds sup X = union X;
theorem :: WAYBEL13:10 :: PROPOSITION 4.12.(i)
for S be lower-bounded sup-Semilattice holds InclPoset Ids S is algebraic;
theorem :: WAYBEL13:11 :: PROPOSITION 4.12.(i)
for S be lower-bounded sup-Semilattice for x be Element of
InclPoset Ids S holds x is compact iff x is principal Ideal of S;
theorem :: WAYBEL13:12
for S be lower-bounded sup-Semilattice for x be Element of
InclPoset Ids S holds x is compact iff ex a be Element of S st x = downarrow a;
theorem :: WAYBEL13:13 :: PROPOSITION 4.12.(ii)
for L be lower-bounded sup-Semilattice for f be Function of L,
CompactSublatt InclPoset Ids L st for x be Element of L holds f.x = downarrow x
holds f is isomorphic;
theorem :: WAYBEL13:14 :: PROPOSITION 4.12.(iii)
for S be lower-bounded LATTICE holds InclPoset Ids S is arithmetic;
theorem :: WAYBEL13:15 :: PROPOSITION 4.12.(iv)
for L be lower-bounded sup-Semilattice holds CompactSublatt L is
lower-bounded sup-Semilattice;
theorem :: WAYBEL13:16 :: PROPOSITION 4.12.(v)
for L be algebraic lower-bounded sup-Semilattice for f be
Function of L,InclPoset Ids CompactSublatt L st for x be Element of L holds f.x
= compactbelow x holds f is isomorphic;
theorem :: WAYBEL13:17 :: PROPOSITION 4.12.(vi)
for L be algebraic lower-bounded sup-Semilattice for x be Element of L
holds compactbelow x is principal Ideal of CompactSublatt L iff x is compact;
begin :: Maps
theorem :: WAYBEL13:18
for L1,L2 be non empty RelStr for X be Subset of L1, x be
Element of L1 for f be Function of L1,L2 st f is isomorphic holds x is_<=_than
X iff f.x is_<=_than f.:X;
theorem :: WAYBEL13:19
for L1,L2 be non empty RelStr for X be Subset of L1, x be
Element of L1 for f be Function of L1,L2 st f is isomorphic holds x is_>=_than
X iff f.x is_>=_than f.:X;
theorem :: WAYBEL13:20
for L1,L2 be non empty antisymmetric RelStr for f be Function of
L1,L2 holds f is isomorphic implies f is infs-preserving sups-preserving;
registration
let L1,L2 be non empty antisymmetric RelStr;
cluster isomorphic -> infs-preserving sups-preserving for Function of L1,L2;
end;
theorem :: WAYBEL13:21
for L1,L2,L3 be non empty transitive antisymmetric RelStr for f
be Function of L1,L2 st f is infs-preserving holds L2 is full infs-inheriting
SubRelStr of L3 & L3 is complete implies ex g be Function of L1,L3 st f = g & g
is infs-preserving;
theorem :: WAYBEL13:22
for L1,L2,L3 be non empty transitive antisymmetric RelStr for f
be Function of L1,L2 st f is monotone directed-sups-preserving holds L2 is full
directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g be
Function of L1,L3 st f = g & g is directed-sups-preserving;
theorem :: WAYBEL13:23
for L be lower-bounded sup-Semilattice holds InclPoset Ids
CompactSublatt L is CLSubFrame of BoolePoset the carrier of CompactSublatt L;
theorem :: WAYBEL13:24 :: COROLLARY 4.13.
for L be algebraic lower-bounded LATTICE ex g be Function of L,
BoolePoset the carrier of CompactSublatt L st g is infs-preserving & g is
directed-sups-preserving & g is one-to-one & for x be Element of L holds g.x =
compactbelow x;
theorem :: WAYBEL13:25 :: PROPOSITION 4.14.
for I be non empty set for J be RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i be Element of I holds J.i is
algebraic lower-bounded LATTICE holds product J is algebraic lower-bounded
LATTICE;
theorem :: WAYBEL13:26
for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr
of L2 holds L1,L2 are_isomorphic;
theorem :: WAYBEL13:27
for L1,L2 be up-complete non empty Poset for f be Function of
L1,L2 st f is isomorphic for x,y be Element of L1 holds x << y iff f.x << f.y
;
theorem :: WAYBEL13:28
for L1,L2 be up-complete non empty Poset for f be Function of
L1,L2 st f is isomorphic for x be Element of L1 holds x is compact iff f.x is
compact;
theorem :: WAYBEL13:29
for L1,L2 be up-complete non empty Poset for f be Function of
L1,L2 st f is isomorphic for x be Element of L1 holds f.:(compactbelow x) =
compactbelow f.x;
theorem :: WAYBEL13:30
for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is
up-complete holds L2 is up-complete;
theorem :: WAYBEL13:31
for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is
complete satisfying_axiom_K holds L2 is satisfying_axiom_K;
theorem :: WAYBEL13:32
for L1,L2 be sup-Semilattice st L1,L2 are_isomorphic & L1 is
lower-bounded algebraic holds L2 is algebraic;
theorem :: WAYBEL13:33
for L be continuous lower-bounded sup-Semilattice holds SupMap L is
infs-preserving sups-preserving;
:: THEOREM 4.15. (1) iff (2)
theorem :: WAYBEL13:34
for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be
non empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S
is directed-sups-inheriting & L,S are_isomorphic ) & (( ex X be set, S be full
SubRelStr of BoolePoset X st S is infs-inheriting & S is
directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic );
:: THEOREM 4.15. (1) iff (3)
theorem :: WAYBEL13:35
for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be
non empty set, c be closure Function of BoolePoset X,BoolePoset X st c is
directed-sups-preserving & L,Image c are_isomorphic ) & (( ex X be set, c be
closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving
& L,Image c are_isomorphic ) implies L is algebraic );