:: Algebraic Lattices :: by Robert Milewski :: :: Received December 1, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin definition let L be non empty reflexive RelStr ; func CompactSublatt L -> strict full SubRelStr of L means :Def1: :: WAYBEL_8:def 1 for x being Element of L holds ( x in the carrier of it iff x is compact ); existence ex b1 being strict full SubRelStr of L st for x being Element of L holds ( x in the carrier of b1 iff x is compact ) proofend; uniqueness for b1, b2 being strict full SubRelStr of L st ( for x being Element of L holds ( x in the carrier of b1 iff x is compact ) ) & ( for x being Element of L holds ( x in the carrier of b2 iff x is compact ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines CompactSublatt WAYBEL_8:def_1_:_ for L being non empty reflexive RelStr for b2 being strict full SubRelStr of L holds ( b2 = CompactSublatt L iff for x being Element of L holds ( x in the carrier of b2 iff x is compact ) ); registration let L be non empty reflexive antisymmetric lower-bounded RelStr ; cluster CompactSublatt L -> non empty strict full ; coherence not CompactSublatt L is empty proofend; end; theorem :: WAYBEL_8:1 for L being complete LATTICE for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds x << y proofend; theorem :: WAYBEL_8:2 for L being complete LATTICE for x being Element of L holds ( uparrow x is Open Filter of L iff x is compact ) proofend; theorem :: WAYBEL_8:3 for L being non empty with_suprema lower-bounded Poset holds ( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) ) proofend; definition let L be non empty reflexive RelStr ; let x be Element of L; func compactbelow x -> Subset of L equals :: WAYBEL_8:def 2 { y where y is Element of L : ( x >= y & y is compact ) } ; coherence { y where y is Element of L : ( x >= y & y is compact ) } is Subset of L proofend; end; :: deftheorem defines compactbelow WAYBEL_8:def_2_:_ for L being non empty reflexive RelStr for x being Element of L holds compactbelow x = { y where y is Element of L : ( x >= y & y is compact ) } ; theorem Th4: :: WAYBEL_8:4 for L being non empty reflexive RelStr for x, y being Element of L holds ( y in compactbelow x iff ( x >= y & y is compact ) ) proofend; theorem Th5: :: WAYBEL_8:5 for L being non empty reflexive RelStr for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) proofend; theorem Th6: :: WAYBEL_8:6 for L being non empty reflexive transitive RelStr for x being Element of L holds compactbelow x c= waybelow x proofend; registration let L be non empty reflexive antisymmetric lower-bounded RelStr ; let x be Element of L; cluster compactbelow x -> non empty ; coherence not compactbelow x is empty proofend; end; begin definition let L be non empty reflexive RelStr ; attrL is satisfying_axiom_K means :Def3: :: WAYBEL_8:def 3 for x being Element of L holds x = sup (compactbelow x); end; :: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def_3_:_ for L being non empty reflexive RelStr holds ( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) ); definition let L be non empty reflexive RelStr ; attrL is algebraic means :Def4: :: WAYBEL_8:def 4 ( ( for x being Element of L holds ( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ); end; :: deftheorem Def4 defines algebraic WAYBEL_8:def_4_:_ for L being non empty reflexive RelStr holds ( L is algebraic iff ( ( for x being Element of L holds ( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) ); theorem Th7: :: WAYBEL_8:7 for L being LATTICE holds ( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) ) proofend; registration cluster reflexive transitive antisymmetric with_suprema with_infima algebraic -> continuous for RelStr ; coherence for b1 being LATTICE st b1 is algebraic holds b1 is continuous by Th7; end; registration cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K for RelStr ; coherence for b1 being non empty reflexive RelStr st b1 is algebraic holds ( b1 is up-complete & b1 is satisfying_axiom_K ) by Def4; end; registration let L be non empty with_suprema Poset; cluster CompactSublatt L -> strict full join-inheriting ; coherence CompactSublatt L is join-inheriting proofend; end; definition let L be non empty reflexive RelStr ; attrL is arithmetic means :Def5: :: WAYBEL_8:def 5 ( L is algebraic & CompactSublatt L is meet-inheriting ); end; :: deftheorem Def5 defines arithmetic WAYBEL_8:def_5_:_ for L being non empty reflexive RelStr holds ( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) ); begin registration cluster reflexive transitive antisymmetric with_suprema with_infima arithmetic -> algebraic for RelStr ; coherence for b1 being LATTICE st b1 is arithmetic holds b1 is algebraic by Def5; end; registration cluster trivial reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ; coherence for b1 being LATTICE st b1 is trivial holds b1 is arithmetic proofend; end; registration cluster non empty 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( b1 is 1 -element & b1 is strict ) proofend; end; theorem Th8: :: WAYBEL_8:8 for L1, 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 for x1, y1 being Element of L1 for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds x2 << y2 proofend; theorem Th9: :: WAYBEL_8:9 for L1, 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 for x being Element of L1 for y being Element of L2 st x = y & x is compact holds y is compact proofend; theorem Th10: :: WAYBEL_8:10 for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for x being Element of L1 for y being Element of L2 st x = y holds compactbelow x = compactbelow y proofend; theorem :: WAYBEL_8:11 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & not L1 is empty holds not L2 is empty ; theorem Th12: :: WAYBEL_8:12 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive holds L2 is reflexive proofend; theorem Th13: :: WAYBEL_8:13 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive holds L2 is transitive proofend; theorem Th14: :: WAYBEL_8:14 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric holds L2 is antisymmetric proofend; theorem Th15: :: WAYBEL_8:15 for L1, L2 being non empty reflexive 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 L2 is up-complete proofend; theorem Th16: :: WAYBEL_8:16 for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds ( not compactbelow x is empty & compactbelow x is directed ) ) holds L2 is satisfying_axiom_K proofend; theorem Th17: :: WAYBEL_8:17 for L1, 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 algebraic holds L2 is algebraic proofend; theorem Th18: :: WAYBEL_8:18 for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic holds L2 is arithmetic proofend; registration let L be non empty RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> non empty ; coherence not RelStr(# the carrier of L, the InternalRel of L #) is empty ; end; registration let L be non empty reflexive RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> reflexive ; coherence RelStr(# the carrier of L, the InternalRel of L #) is reflexive by Th12; end; registration let L be transitive RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> transitive ; coherence RelStr(# the carrier of L, the InternalRel of L #) is transitive by Th13; end; registration let L be antisymmetric RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> antisymmetric ; coherence RelStr(# the carrier of L, the InternalRel of L #) is antisymmetric by Th14; end; registration let L be with_infima RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_infima ; coherence RelStr(# the carrier of L, the InternalRel of L #) is with_infima by YELLOW_7:14; end; registration let L be with_suprema RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_suprema ; coherence RelStr(# the carrier of L, the InternalRel of L #) is with_suprema by YELLOW_7:15; end; registration let L be non empty reflexive up-complete RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> up-complete ; coherence RelStr(# the carrier of L, the InternalRel of L #) is up-complete by Th15; end; registration let L be non empty reflexive antisymmetric algebraic RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> algebraic ; coherence RelStr(# the carrier of L, the InternalRel of L #) is algebraic by Th17; end; registration let L be arithmetic LATTICE; cluster RelStr(# the carrier of L, the InternalRel of L #) -> arithmetic ; coherence RelStr(# the carrier of L, the InternalRel of L #) is arithmetic by Th18; end; theorem :: WAYBEL_8:19 for L being algebraic LATTICE holds ( L is arithmetic iff CompactSublatt L is LATTICE ) proofend; theorem Th20: :: WAYBEL_8:20 for L being lower-bounded algebraic LATTICE holds ( L is arithmetic iff L -waybelow is multiplicative ) proofend; theorem :: WAYBEL_8:21 for L being lower-bounded arithmetic LATTICE for p being Element of L st p is pseudoprime holds p is prime proofend; theorem :: WAYBEL_8:22 for L being lower-bounded distributive algebraic LATTICE st ( for p being Element of L st p is pseudoprime holds p is prime ) holds L is arithmetic proofend; registration let L be algebraic LATTICE; let c be closure Function of L,L; cluster non empty directed for Element of bool the carrier of (Image c); existence ex b1 being Subset of (Image c) st ( not b1 is empty & b1 is directed ) proofend; end; theorem Th23: :: WAYBEL_8:23 for L being algebraic LATTICE for c being closure Function of L,L st c is directed-sups-preserving holds c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) proofend; theorem :: WAYBEL_8:24 for L being lower-bounded algebraic LATTICE for c being closure Function of L,L st c is directed-sups-preserving holds Image c is algebraic LATTICE proofend; theorem :: WAYBEL_8:25 for L being lower-bounded algebraic LATTICE for c being closure Function of L,L st c is directed-sups-preserving holds c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) proofend; begin theorem Th26: :: WAYBEL_8:26 for X, x being set holds ( x is Element of (BoolePoset X) iff x c= X ) proofend; theorem Th27: :: WAYBEL_8:27 for X being set for x, y being Element of (BoolePoset X) holds ( x << y iff for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ) proofend; theorem Th28: :: WAYBEL_8:28 for X being set for x being Element of (BoolePoset X) holds ( x is finite iff x is compact ) proofend; theorem Th29: :: WAYBEL_8:29 for X being set for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum } proofend; theorem :: WAYBEL_8:30 for X being set for F being Subset of X holds ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite ) proofend; registration let X be set ; let x be Element of (BoolePoset X); cluster compactbelow x -> directed lower ; coherence ( compactbelow x is lower & compactbelow x is directed ) proofend; end; theorem Th31: :: WAYBEL_8:31 for X being set holds BoolePoset X is algebraic proofend; registration let X be set ; cluster BoolePoset X -> algebraic ; coherence BoolePoset X is algebraic by Th31; end;