:: Algebraic and Arithmetic Lattices :: by Robert Milewski :: :: Received March 4, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users begin theorem Th1: :: WAYBEL13:1 for L being non empty reflexive transitive RelStr for x, y being Element of L st x <= y holds compactbelow x c= compactbelow y proofend; theorem Th2: :: WAYBEL13:2 for L being non empty reflexive RelStr for x being Element of L holds compactbelow x is Subset of (CompactSublatt L) proofend; theorem Th3: :: WAYBEL13:3 for L being RelStr for S being SubRelStr of L for X being Subset of S holds X is Subset of L proofend; theorem Th4: :: WAYBEL13:4 for L being non empty reflexive transitive with_suprema RelStr holds the carrier of L is Ideal of L proofend; theorem Th5: :: WAYBEL13:5 for L1 being non empty reflexive antisymmetric lower-bounded RelStr for L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) proofend; begin theorem Th6: :: WAYBEL13:6 for L being lower-bounded algebraic LATTICE for S being CLSubFrame of L holds S is algebraic proofend; theorem Th7: :: WAYBEL13:7 for X, E being set for L being CLSubFrame of BoolePoset X holds ( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) ) proofend; theorem Th8: :: WAYBEL13:8 for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L proofend; registration let L be non empty reflexive transitive RelStr ; cluster non empty directed lower principal for Element of K32( the carrier of L); existence ex b1 being Ideal of L st b1 is principal proofend; end; theorem Th9: :: WAYBEL13:9 for L being lower-bounded sup-Semilattice for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X proofend; theorem Th10: :: WAYBEL13:10 for S being lower-bounded sup-Semilattice holds InclPoset (Ids S) is algebraic proofend; theorem Th11: :: WAYBEL13:11 for S being lower-bounded sup-Semilattice for x being Element of (InclPoset (Ids S)) holds ( x is compact iff x is principal Ideal of S ) proofend; theorem Th12: :: WAYBEL13:12 for S being lower-bounded sup-Semilattice for x being Element of (InclPoset (Ids S)) holds ( x is compact iff ex a being Element of S st x = downarrow a ) proofend; theorem :: WAYBEL13:13 for L being lower-bounded sup-Semilattice for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds f is isomorphic proofend; theorem :: WAYBEL13:14 for S being lower-bounded LATTICE holds InclPoset (Ids S) is arithmetic proofend; theorem Th15: :: WAYBEL13:15 for L being lower-bounded sup-Semilattice holds CompactSublatt L is lower-bounded sup-Semilattice proofend; theorem Th16: :: WAYBEL13:16 for L being lower-bounded algebraic sup-Semilattice for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds f is isomorphic proofend; theorem :: WAYBEL13:17 for L being lower-bounded algebraic sup-Semilattice for x being Element of L holds ( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact ) proofend; begin theorem Th18: :: WAYBEL13:18 for L1, L2 being non empty RelStr for X being Subset of L1 for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_<=_than X iff f . x is_<=_than f .: X ) proofend; theorem Th19: :: WAYBEL13:19 for L1, L2 being non empty RelStr for X being Subset of L1 for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_>=_than X iff f . x is_>=_than f .: X ) proofend; theorem Th20: :: WAYBEL13:20 for L1, L2 being non empty antisymmetric RelStr for f being Function of L1,L2 st f is isomorphic holds ( f is infs-preserving & f is sups-preserving ) proofend; registration let L1, L2 be non empty antisymmetric RelStr ; cluster Function-like V21( the carrier of L1, the carrier of L2) isomorphic -> infs-preserving sups-preserving for Element of K32(K33( the carrier of L1, the carrier of L2)); coherence for b1 being Function of L1,L2 st b1 is isomorphic holds ( b1 is infs-preserving & b1 is sups-preserving ) by Th20; end; theorem Th21: :: WAYBEL13:21 for L1, L2, L3 being non empty transitive antisymmetric RelStr for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds ex g being Function of L1,L3 st ( f = g & g is infs-preserving ) proofend; theorem Th22: :: WAYBEL13:22 for L1, L2, L3 being non empty transitive antisymmetric RelStr for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds ex g being Function of L1,L3 st ( f = g & g is directed-sups-preserving ) proofend; theorem Th23: :: WAYBEL13:23 for L being lower-bounded sup-Semilattice holds InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L) proofend; theorem Th24: :: WAYBEL13:24 for L being lower-bounded algebraic LATTICE ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st ( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) ) proofend; theorem :: WAYBEL13:25 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) holds product J is lower-bounded algebraic LATTICE proofend; Lm1: for L being lower-bounded LATTICE st L is algebraic holds ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) proofend; theorem Th26: :: WAYBEL13:26 for L1, L2 being non empty RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds L1,L2 are_isomorphic proofend; Lm2: for L being LATTICE st ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) proofend; Lm3: for L being LATTICE st ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) proofend; Lm4: for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x, y being Element of L1 st x << y holds f . x << f . y proofend; theorem Th27: :: WAYBEL13:27 for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x, y being Element of L1 holds ( x << y iff f . x << f . y ) proofend; theorem Th28: :: WAYBEL13:28 for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x being Element of L1 holds ( x is compact iff f . x is compact ) proofend; theorem Th29: :: WAYBEL13:29 for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x) proofend; theorem Th30: :: WAYBEL13:30 for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is up-complete holds L2 is up-complete proofend; theorem Th31: :: WAYBEL13:31 for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K holds L2 is satisfying_axiom_K proofend; theorem Th32: :: WAYBEL13:32 for L1, L2 being sup-Semilattice st L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic holds L2 is algebraic proofend; Lm5: for L being LATTICE st ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) holds L is algebraic proofend; theorem :: WAYBEL13:33 for L being lower-bounded continuous sup-Semilattice holds ( SupMap L is infs-preserving & SupMap L is sups-preserving ) by WAYBEL_1:12, WAYBEL_1:57, WAYBEL_5:3; :: THEOREM 4.15. (1) iff (2) theorem :: WAYBEL13:34 for L being lower-bounded LATTICE holds ( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) ) proofend; :: THEOREM 4.15. (1) iff (3) theorem :: WAYBEL13:35 for L being lower-bounded LATTICE holds ( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) ) proofend;