Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Algebraic Lattices

**by****Robert Milewski**- Received December 1, 1996
- MML identifier: WAYBEL_8

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_2, ORDERS_1, CAT_1, YELLOW_0, COMPTS_1, WELLORD1, LATTICES, BHSP_3, WAYBEL_0, WAYBEL_3, WAYBEL_6, FILTER_0, LATTICE3, ORDINAL2, BOOLE, QUANTAL1, FINSET_1, REALSET1, WAYBEL_4, COHSP_1, WAYBEL_7, WAYBEL_1, PRE_TOPC, GROUP_6, RELAT_1, SUBSET_1, BINOP_1, SEQM_3, FUNCT_1, YELLOW_1, FILTER_1, SETFAM_1, TARSKI, WAYBEL_8; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FINSET_1, RELAT_1, REALSET1, STRUCT_0, ORDERS_1, TOLER_1, FUNCT_1, LATTICE3, PRE_TOPC, QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, GRCAT_1; constructors TOLER_1, ORDERS_3, QUANTAL1, YELLOW_3, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, GRCAT_1; clusters STRUCT_0, RELSET_1, FINSET_1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: The Subset of All Compact Elements definition :: DEFINITION 4.1 let L be non empty reflexive RelStr; func CompactSublatt L -> strict full SubRelStr of L means :: WAYBEL_8:def 1 for x be Element of L holds x in the carrier of it iff x is compact; end; definition let L be lower-bounded non empty reflexive antisymmetric RelStr; cluster CompactSublatt L -> non empty; end; theorem :: WAYBEL_8:1 for L be complete LATTICE for x,y,k be Element of L holds x <= k & k <= y & k in the carrier of CompactSublatt L implies x << y; theorem :: WAYBEL_8:2 :: REMARK 4.2 for L be complete LATTICE for x be Element of L holds uparrow x is Open Filter of L iff x is compact; theorem :: WAYBEL_8:3 :: REMARK 4.3 for L be lower-bounded with_suprema non empty Poset holds CompactSublatt L is join-inheriting & Bottom L in the carrier of CompactSublatt L; 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}; end; theorem :: WAYBEL_8:4 for L be non empty reflexive RelStr for x,y be Element of L holds y in compactbelow x iff x >= y & y is compact; theorem :: WAYBEL_8:5 for L be non empty reflexive RelStr for x be Element of L holds compactbelow x = downarrow x /\ the carrier of CompactSublatt L; theorem :: WAYBEL_8:6 for L be non empty reflexive transitive RelStr for x be Element of L holds compactbelow x c= waybelow x; definition let L be non empty lower-bounded reflexive antisymmetric RelStr; let x be Element of L; cluster compactbelow x -> non empty; end; begin :: Algebraic Lattices definition let L be non empty reflexive RelStr; attr L is satisfying_axiom_K means :: WAYBEL_8:def 3 for x be Element of L holds x = sup compactbelow x; end; definition :: DEFINITION 4.4 let L be non empty reflexive RelStr; attr L is algebraic means :: WAYBEL_8:def 4 (for x being Element of L holds compactbelow x is non empty directed) & L is up-complete satisfying_axiom_K; end; theorem :: WAYBEL_8:7 :: PROPOSITION 4.5 for L be LATTICE holds L is algebraic iff ( L is continuous & for x,y be Element of L st x << y ex k be Element of L st k in the carrier of CompactSublatt L & x <= k & k <= y ); definition cluster algebraic -> continuous LATTICE; end; definition cluster algebraic -> up-complete satisfying_axiom_K (non empty reflexive RelStr); end; definition let L be non empty with_suprema Poset; cluster CompactSublatt L -> join-inheriting; end; definition let L be non empty reflexive RelStr; attr L is arithmetic means :: WAYBEL_8:def 5 L is algebraic & CompactSublatt L is meet-inheriting; end; begin :: Arithmetic Lattices definition cluster arithmetic -> algebraic LATTICE; end; definition cluster trivial -> arithmetic LATTICE; end; definition cluster trivial strict LATTICE; end; theorem :: WAYBEL_8:8 for L1,L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the RelStr of L2 & L1 is up-complete for x1,y1 be Element of L1 for x2,y2 be Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds x2 << y2; theorem :: WAYBEL_8:9 for L1,L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the RelStr of L2 & L1 is up-complete for x be Element of L1 for y be Element of L2 st x = y & x is compact holds y is compact; theorem :: WAYBEL_8:10 for L1,L2 be up-complete (non empty reflexive antisymmetric RelStr) st the RelStr of L1 = the RelStr of L2 for x be Element of L1 for y be Element of L2 st x = y holds compactbelow x = compactbelow y; theorem :: WAYBEL_8:11 for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is non empty holds L2 is non empty; theorem :: WAYBEL_8:12 for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 & L1 is reflexive holds L2 is reflexive; theorem :: WAYBEL_8:13 for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is transitive holds L2 is transitive; theorem :: WAYBEL_8:14 for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is antisymmetric holds L2 is antisymmetric; theorem :: WAYBEL_8:15 for L1,L2 be non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 & L1 is up-complete holds L2 is up-complete; theorem :: WAYBEL_8:16 for L1,L2 be up-complete (non empty reflexive antisymmetric RelStr) st the RelStr of L1 = the RelStr of L2 & L1 is satisfying_axiom_K & for x be Element of L1 holds compactbelow x is non empty directed holds L2 is satisfying_axiom_K; theorem :: WAYBEL_8:17 for L1,L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the RelStr of L2 & L1 is algebraic holds L2 is algebraic; theorem :: WAYBEL_8:18 for L1,L2 be LATTICE st the RelStr of L1 = the RelStr of L2 & L1 is arithmetic holds L2 is arithmetic; definition let L be non empty RelStr; cluster the RelStr of L -> non empty; end; definition let L be non empty reflexive RelStr; cluster the RelStr of L -> reflexive; end; definition let L be transitive RelStr; cluster the RelStr of L -> transitive; end; definition let L be antisymmetric RelStr; cluster the RelStr of L -> antisymmetric; end; definition let L be with_infima RelStr; cluster the RelStr of L -> with_infima; end; definition let L be with_suprema RelStr; cluster the RelStr of L -> with_suprema; end; definition let L be up-complete (non empty reflexive RelStr); cluster the RelStr of L -> up-complete; end; definition let L be algebraic (non empty reflexive antisymmetric RelStr); cluster the RelStr of L -> algebraic; end; definition let L be arithmetic LATTICE; cluster the RelStr of L -> arithmetic; end; theorem :: WAYBEL_8:19 for L be non empty transitive RelStr for S be non empty full SubRelStr of L for X be Subset of S st ex_sup_of X,L & "\/"(X,L) is Element of S holds ex_sup_of X,S & sup X = "\/"(X,L); theorem :: WAYBEL_8:20 for L be non empty transitive RelStr for S be non empty full SubRelStr of L for X be Subset of S st ex_inf_of X,L & "/\"(X,L) is Element of S holds ex_inf_of X,S & inf X = "/\"(X,L); theorem :: WAYBEL_8:21 :: PROPOSITION 4.7 a) for L be algebraic LATTICE holds L is arithmetic iff CompactSublatt L is LATTICE; theorem :: WAYBEL_8:22 :: PROPOSITION 4.7 b) for L be algebraic lower-bounded LATTICE holds L is arithmetic iff L-waybelow is multiplicative; theorem :: WAYBEL_8:23 :: COROLLARY 4.8.a) for L be arithmetic lower-bounded LATTICE, p be Element of L holds p is pseudoprime implies p is prime; theorem :: WAYBEL_8:24 :: COROLLARY 4.8.b) for L be algebraic distributive lower-bounded LATTICE st for p being Element of L st p is pseudoprime holds p is prime holds L is arithmetic; definition let L be algebraic LATTICE; let c be closure map of L,L; cluster non empty directed Subset of Image c; end; theorem :: WAYBEL_8:25 for L be algebraic LATTICE for c be closure map of L,L st c is directed-sups-preserving holds c.:([#]CompactSublatt L) c= [#]CompactSublatt Image c; theorem :: WAYBEL_8:26 :: PROPOSITION 4.9.(i) for L be algebraic lower-bounded LATTICE for c be closure map of L,L st c is directed-sups-preserving holds Image c is algebraic LATTICE; theorem :: WAYBEL_8:27 :: PROPOSITION 4.9.(ii) for L be algebraic lower-bounded LATTICE, c be closure map of L,L st c is directed-sups-preserving holds c.:([#]CompactSublatt L) = [#]CompactSublatt Image c; begin :: Boolean Posets as Algebraic Lattices theorem :: WAYBEL_8:28 for X,x be set holds x is Element of BoolePoset X iff x c= X; theorem :: WAYBEL_8:29 for X be set for x,y be Element of BoolePoset X holds x << y iff for Y be Subset-Family of X st y c= union Y ex Z be finite Subset of Y st x c= union Z; theorem :: WAYBEL_8:30 for X be set for x be Element of BoolePoset X holds x is finite iff x is compact; theorem :: WAYBEL_8:31 for X be set for x be Element of BoolePoset X holds compactbelow x = {y where y is finite Subset of x : not contradiction}; theorem :: WAYBEL_8:32 :: EXAMPLES 4.11.(1a) for X be set for F be Subset of X holds F in the carrier of CompactSublatt BoolePoset X iff F is finite; definition let X be set; let x be Element of BoolePoset X; cluster compactbelow x -> lower directed; end; theorem :: WAYBEL_8:33 :: EXAMPLES 4.11.(1b) for X be set holds BoolePoset X is algebraic; definition let X be set; cluster BoolePoset X -> algebraic; end;

Back to top