:: Algebraic and Arithmetic Lattices :: by Robert Milewski :: :: Received March 4, 1997 :: Copyright (c) 1997-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 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 );