:: Prime Ideals and Filters :: by Grzegorz Bancerek :: :: Received December 1, 1996 :: Copyright (c) 1996-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 REWRITE1, WAYBEL_0, TARSKI, EQREL_1, XXREAL_0, LATTICES, YELLOW_0, STRUCT_0, YELLOW_1, ZFMISC_1, ORDERS_2, WELLORD2, XXREAL_2, RELAT_2, XBOOLE_0, SUBSET_1, CARD_FIL, XBOOLEAN, FINSET_1, SETFAM_1, ORDINAL2, LATTICE3, INT_2, ARYTM_0, RELAT_1, WAYBEL_6, METRIC_1, ORDINAL1, PRE_TOPC, RCOMP_1, WAYBEL_3, FUNCT_1, CANTOR_1, RLVECT_3, MSSUBFAM, WAYBEL_4, CAT_1, MCART_1, WAYBEL_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, FUNCT_2, DOMAIN_1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_2, CANTOR_1, ORDINAL1, ORDERS_2, LATTICE3, ALG_1, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, YELLOW_7, WAYBEL_6, WAYBEL_4; constructors SETFAM_1, DOMAIN_1, TOPS_2, TEX_2, CANTOR_1, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6; registrations XBOOLE_0, SUBSET_1, FINSET_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_4, YELLOW_7, WAYBEL_6, RELAT_1; requirements SUBSET, BOOLE; begin theorem :: WAYBEL_7:1 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:2 for X being set holds the carrier of BoolePoset X = bool X; theorem :: WAYBEL_7:3 for L being bounded antisymmetric non empty RelStr holds L is trivial iff Top L = Bottom L; registration let X be set; cluster BoolePoset X -> Boolean; end; registration let X be non empty set; cluster BoolePoset X -> non trivial; end; theorem :: WAYBEL_7:4 for L being lower-bounded non empty Poset, F being Filter of L holds F is proper iff not Bottom L in F; registration cluster non trivial Boolean strict for LATTICE; end; registration let L be upper-bounded non trivial Poset; cluster proper for Filter of L; end; theorem :: WAYBEL_7:5 for X being set, a being Element of BoolePoset X holds 'not' a = X \ a; theorem :: WAYBEL_7:6 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:7 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:8 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:9 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:10 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:11 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:12 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; registration let L be LATTICE; cluster prime for Ideal of L; end; theorem :: WAYBEL_7:13 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:14 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; registration let L be LATTICE; cluster prime for Filter of L; end; theorem :: WAYBEL_7:15 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:16 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:17 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:18 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:19 for L being LATTICE, I being Ideal of L holds I is prime iff I in PRIME InclPoset Ids L; theorem :: WAYBEL_7:20 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:21 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; registration let L be non empty Poset; cluster ultra -> proper for Filter of L; end; :: Remark 3.18: (1)+proper iff (3) theorem :: WAYBEL_7:22 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:23 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:24 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:25 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:26 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 be set,x be object; 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; registration let X be non empty set; cluster ultra for Filter of BoolePoset X; end; theorem :: WAYBEL_7:27 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:28 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:29 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:30 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 ::$N Alexander's Lemma theorem :: WAYBEL_7:31 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:32 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:33 for L being LATTICE, p being Element of L st p is prime holds downarrow p is prime; begin :: Pseudo prime elements definition 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:34 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:35 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:36 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:37 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; :: Proposition 3.24: (2) <= (3) theorem :: WAYBEL_7:38 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; :: Proposition 3.24: (3) => (1) theorem :: WAYBEL_7:39 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; registration 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; :: Lemma 3.25: (1) iff (2)-[non empty] theorem :: WAYBEL_7:40 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:41 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; :: Lemma 3.25: (1) iff (4) theorem :: WAYBEL_7:42 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; :: Lemma 3.25: (1) iff (5) theorem :: WAYBEL_7:43 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:44 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:45 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:46 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;