Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Prime Ideals and Filters

**by****Grzegorz Bancerek**- Received December 1, 1996
- MML identifier: WAYBEL_7

- [ Mizar article, MML identifier index ]

environ vocabulary BHSP_3, WAYBEL_0, FILTER_2, LATTICES, ORDERS_1, FILTER_0, YELLOW_0, YELLOW_1, WELLORD2, RELAT_2, REALSET1, BOOLE, COLLSP, FINSET_1, SETFAM_1, ZF_LANG, QUANTAL1, TARSKI, ORDINAL2, CANTOR_1, LATTICE3, SUBSET_1, OPPCAT_1, RELAT_1, WAYBEL_6, SUB_METR, ZFMISC_1, PRE_TOPC, WAYBEL_3, FUNCT_1, COMPTS_1, COHSP_1, WAYBEL_4, CAT_1, MCART_1, FUNCT_5, WAYBEL_7, RLVECT_3, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, REALSET1, STRUCT_0, PRE_TOPC, TOPS_2, TEX_2, CANTOR_1, ORDINAL1, ORDERS_1, LATTICE3, ALG_1, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_3, YELLOW_7, WAYBEL_6, WAYBEL_4; constructors REALSET1, TOPS_2, TEX_2, CANTOR_1, YELLOW_3, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_6, WAYBEL_4; clusters FINSET_1, PRE_TOPC, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_3, CANTOR_1, YELLOW_2, YELLOW_3, WAYBEL_1, YELLOW_7, WAYBEL_6, WAYBEL_4, SUBSET_1, XBOOLE_0, ZFMISC_1; requirements SUBSET, BOOLE; begin canceled 2; theorem :: WAYBEL_7:3 for L being complete LATTICE, X,Y being set st X c= Y holds "\/"(X,L) <= "\/"(Y,L) & "/\"(X,L) >= "/\"(Y,L); theorem :: WAYBEL_7:4 for X being set holds the carrier of BoolePoset X = bool X; theorem :: WAYBEL_7:5 for L being bounded antisymmetric (non empty RelStr) holds L is trivial iff Top L = Bottom L; definition let X be set; cluster BoolePoset X -> Boolean; end; definition let X be non empty set; cluster BoolePoset X -> non trivial; end; canceled 2; theorem :: WAYBEL_7:8 for L being lower-bounded (non empty Poset), F being Filter of L holds F is proper iff not Bottom L in F; definition cluster non trivial Boolean strict LATTICE; end; definition let X be set; cluster finite non empty Subset-Family of X; end; definition let S be 1-sorted; cluster finite non empty Subset-Family of S; end; definition let L be non trivial upper-bounded (non empty Poset); cluster proper Filter of L; end; theorem :: WAYBEL_7:9 for X being set, a being Element of BoolePoset X holds 'not' a = X \ a; theorem :: WAYBEL_7:10 for X being set, Y being Subset of BoolePoset X holds Y is lower iff for x,y being set st x c= y & y in Y holds x in Y; theorem :: WAYBEL_7:11 for X being set, Y being Subset of BoolePoset X holds Y is upper iff for x,y being set st x c= y & y c= X & x in Y holds y in Y; theorem :: WAYBEL_7:12 for X being set, Y being lower Subset of BoolePoset X holds Y is directed iff for x,y being set st x in Y & y in Y holds x \/ y in Y; theorem :: WAYBEL_7:13 for X being set, Y being upper Subset of BoolePoset X holds Y is filtered iff for x,y being set st x in Y & y in Y holds x /\ y in Y; theorem :: WAYBEL_7:14 for X being set, Y being non empty lower Subset of BoolePoset X holds Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds union Z in Y; theorem :: WAYBEL_7:15 for X being set, Y being non empty upper Subset of BoolePoset X holds Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y; begin :: Prime ideals and filters definition let L be with_infima Poset; let I be Ideal of L; attr I is prime means :: WAYBEL_7:def 1 for x,y being Element of L st x"/\"y in I holds x in I or y in I; end; theorem :: WAYBEL_7:16 for L being with_infima Poset, I being Ideal of L holds I is prime iff for A being finite non empty Subset of L st inf A in I ex a being Element of L st a in A & a in I; definition let L be LATTICE; cluster prime Ideal of L; end; theorem :: WAYBEL_7:17 for L1, L2 being LATTICE st the RelStr of L1 = the RelStr of L2 for x being set st x is prime Ideal of L1 holds x is prime Ideal of L2; definition let L be with_suprema Poset; let F be Filter of L; attr F is prime means :: WAYBEL_7:def 2 for x,y being Element of L st x"\/"y in F holds x in F or y in F; end; theorem :: WAYBEL_7:18 for L being with_suprema Poset, F being Filter of L holds F is prime iff for A being finite non empty Subset of L st sup A in F ex a being Element of L st a in A & a in F; definition let L be LATTICE; cluster prime Filter of L; end; theorem :: WAYBEL_7:19 for L1, L2 being LATTICE st the RelStr of L1 = the RelStr of L2 for x being set st x is prime Filter of L1 holds x is prime Filter of L2; theorem :: WAYBEL_7:20 for L being LATTICE, x being set holds x is prime Ideal of L iff x is prime Filter of L opp; theorem :: WAYBEL_7:21 for L being LATTICE, x being set holds x is prime Filter of L iff x is prime Ideal of L opp; :: Remark 3.16: (3) iff (2) theorem :: WAYBEL_7:22 for L being with_infima Poset, I being Ideal of L holds I is prime iff I` is Filter of L or I` = {}; :: Remark 3.16: (3) iff (1) theorem :: WAYBEL_7:23 for L being LATTICE, I being Ideal of L holds I is prime iff I in PRIME InclPoset Ids L; theorem :: WAYBEL_7:24 for L being Boolean LATTICE, F being Filter of L holds F is prime iff for a being Element of L holds a in F or 'not' a in F; :: Remark 3.18: (1) iff (2) theorem :: WAYBEL_7:25 for X being set, F being Filter of BoolePoset X holds F is prime iff for A being Subset of X holds A in F or X\A in F; definition let L be non empty Poset; let F be Filter of L; attr F is ultra means :: WAYBEL_7:def 3 F is proper & for G being Filter of L st F c= G holds F = G or G = the carrier of L; end; definition let L be non empty Poset; cluster ultra -> proper Filter of L; end; :: Remark 3.18: (1)+proper iff (3) theorem :: WAYBEL_7:26 for L being Boolean LATTICE, F being Filter of L holds F is proper prime iff F is ultra; :: Lemma 3.19 theorem :: WAYBEL_7:27 for L being distributive LATTICE, I being Ideal of L, F being Filter of L st I misses F ex P being Ideal of L st P is prime & I c= P & P misses F; theorem :: WAYBEL_7:28 for L being distributive LATTICE, I being Ideal of L, x being Element of L st not x in I ex P being Ideal of L st P is prime & I c= P & not x in P; theorem :: WAYBEL_7:29 for L being distributive LATTICE, I being Ideal of L, F being Filter of L st I misses F ex P being Filter of L st P is prime & F c= P & I misses P; theorem :: WAYBEL_7:30 for L being non trivial Boolean LATTICE, F being proper Filter of L ex G being Filter of L st F c= G & G is ultra; begin :: Cluster points of a filter of sets definition let T be TopSpace; let F,x be set; pred x is_a_cluster_point_of F,T means :: WAYBEL_7:def 4 for A being Subset of T st A is open & x in A for B being set st B in F holds A meets B; pred x is_a_convergence_point_of F,T means :: WAYBEL_7:def 5 for A being Subset of T st A is open & x in A holds A in F; end; definition let X be non empty set; cluster ultra Filter of BoolePoset X; end; theorem :: WAYBEL_7:31 for T being non empty TopSpace for F being ultra Filter of BoolePoset the carrier of T for p being set holds p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T; :: Proposition 3.20 (1) => (2) theorem :: WAYBEL_7:32 for T being non empty TopSpace for x,y being Element of InclPoset the topology of T st x << y for F being proper Filter of BoolePoset the carrier of T st x in F ex p being Element of T st p in y & p is_a_cluster_point_of F,T; :: Proposition 3.20: (1) => (3) theorem :: WAYBEL_7:33 for T being non empty TopSpace for x,y being Element of InclPoset the topology of T st x << y for F being ultra Filter of BoolePoset the carrier of T st x in F ex p being Element of T st p in y & p is_a_convergence_point_of F,T; :: Proposition 3.20: (3) => (1) theorem :: WAYBEL_7:34 for T being non empty TopSpace for x,y being Element of InclPoset the topology of T st x c= y & for F being ultra Filter of BoolePoset the carrier of T st x in F ex p being Element of T st p in y & p is_a_convergence_point_of F,T holds x << y; :: Proposition 3.21 theorem :: WAYBEL_7:35 for T being non empty TopSpace for B being prebasis of T for x,y being Element of InclPoset the topology of T st x c= y holds x << y iff for F being Subset of B st y c= union F ex G being finite Subset of F st x c= union G; :: Proposition 3.22 theorem :: WAYBEL_7:36 for L being distributive complete LATTICE for x,y being Element of L holds x << y iff for P being prime Ideal of L st y <= sup P holds x in P; theorem :: WAYBEL_7:37 for L being LATTICE, p being Element of L st p is prime holds downarrow p is prime; begin :: Pseudo prime elements definition :: Definition 3.23 let L be LATTICE; let p be Element of L; attr p is pseudoprime means :: WAYBEL_7:def 6 ex P being prime Ideal of L st p = sup P; end; theorem :: WAYBEL_7:38 for L being LATTICE for p being Element of L st p is prime holds p is pseudoprime; :: Proposition 3.24: (1) => (2) theorem :: WAYBEL_7:39 for L being continuous LATTICE for p being Element of L st p is pseudoprime for A being finite non empty Subset of L st inf A << p ex a being Element of L st a in A & a <= p; :: Proposition 3.24: (2)+? => (3) theorem :: WAYBEL_7:40 for L being continuous LATTICE for p being Element of L st (p <> Top L or Top L is not compact) & for A being finite non empty Subset of L st inf A << p ex a being Element of L st a in A & a <= p holds uparrow fininfs (downarrow p)` misses waybelow p; :: It is not true that: Proposition 3.24: (2) => (3) theorem :: WAYBEL_7:41 for L being continuous LATTICE st Top L is compact holds (for A being finite non empty Subset of L st inf A << Top L ex a being Element of L st a in A & a <= Top L) & uparrow fininfs (downarrow Top L)` meets waybelow Top L; theorem :: WAYBEL_7:42 :: Proposition 3.24: (2) <= (3) for L being continuous LATTICE for p being Element of L st uparrow fininfs (downarrow p)` misses waybelow p for A being finite non empty Subset of L st inf A << p ex a being Element of L st a in A & a <= p; theorem :: WAYBEL_7:43 :: Proposition 3.24: (3) => (1) for L being distributive continuous LATTICE for p being Element of L st uparrow fininfs (downarrow p)` misses waybelow p holds p is pseudoprime; definition let L be non empty RelStr; let R be Relation of the carrier of L; attr R is multiplicative means :: WAYBEL_7:def 7 for a,x,y being Element of L st [a,x] in R & [a,y] in R holds [a,x"/\" y] in R; end; definition let L be lower-bounded sup-Semilattice; let R be auxiliary Relation of L; let x be Element of L; cluster R-above x -> upper; end; theorem :: WAYBEL_7:44 :: Lemma 3.25: (1) iff (2)-[non empty] for L being lower-bounded LATTICE, R being auxiliary Relation of L holds R is multiplicative iff for x being Element of L holds R-above x is filtered; :: Lemma 3.25: (1) iff (3) theorem :: WAYBEL_7:45 for L being lower-bounded LATTICE, R being auxiliary Relation of L holds R is multiplicative iff for a,b,x,y being Element of L st [a,x] in R & [b,y] in R holds [a"/\"b,x"/\"y] in R; theorem :: WAYBEL_7:46 :: Lemma 3.25: (1) iff (4) for L being lower-bounded LATTICE, R being auxiliary Relation of L holds R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting; theorem :: WAYBEL_7:47 :: Lemma 3.25: (1) iff (5) for L being lower-bounded LATTICE, R being auxiliary Relation of L holds R is multiplicative iff R-below is meet-preserving; theorem :: WAYBEL_7:48 for L being continuous lower-bounded LATTICE st L-waybelow is multiplicative for p being Element of L holds p is pseudoprime iff for a,b being Element of L st a"/\"b << p holds a <= p or b <= p; theorem :: WAYBEL_7:49 for L being continuous lower-bounded LATTICE st L-waybelow is multiplicative for p being Element of L st p is pseudoprime holds p is prime; theorem :: WAYBEL_7:50 for L being distributive continuous lower-bounded LATTICE st for p being Element of L st p is pseudoprime holds p is prime holds L-waybelow is multiplicative;

Back to top