:: Prime Ideals and Filters :: by Grzegorz Bancerek :: :: Received December 1, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin theorem Th1: :: WAYBEL_7:1 for L being complete LATTICE for X, Y being set st X c= Y holds ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) proofend; theorem Th2: :: WAYBEL_7:2 for X being set holds the carrier of (BoolePoset X) = bool X proofend; theorem Th3: :: WAYBEL_7:3 for L being non empty antisymmetric bounded RelStr holds ( L is trivial iff Top L = Bottom L ) proofend; registration let X be set ; cluster BoolePoset X -> Boolean ; coherence BoolePoset X is Boolean ; end; registration let X be non empty set ; cluster BoolePoset X -> non trivial ; coherence not BoolePoset X is trivial proofend; end; theorem Th4: :: WAYBEL_7:4 for L being non empty lower-bounded Poset for F being Filter of L holds ( F is proper iff not Bottom L in F ) proofend; registration cluster non empty non trivial strict reflexive transitive antisymmetric Boolean non void with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( not b1 is trivial & b1 is Boolean & b1 is strict ) proofend; end; registration let L be non trivial upper-bounded Poset; cluster non empty proper filtered upper for Element of bool the carrier of L; existence ex b1 being Filter of L st b1 is proper proofend; end; theorem Th5: :: WAYBEL_7:5 for X being set for a being Element of (BoolePoset X) holds 'not' a = X \ a proofend; theorem :: WAYBEL_7:6 for X being set for 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 ) proofend; theorem Th7: :: WAYBEL_7:7 for X being set for 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 ) proofend; theorem :: WAYBEL_7:8 for X being set for 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 ) proofend; theorem Th9: :: WAYBEL_7:9 for X being set for 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 ) proofend; theorem :: WAYBEL_7:10 for X being set for 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 ) proofend; theorem Th11: :: WAYBEL_7:11 for X being set for 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 ) proofend; begin definition let L be with_infima Poset; let I be Ideal of L; attrI is prime means :Def1: :: WAYBEL_7:def 1 for x, y being Element of L holds ( not x "/\" y in I or x in I or y in I ); end; :: deftheorem Def1 defines prime WAYBEL_7:def_1_:_ for L being with_infima Poset for I being Ideal of L holds ( I is prime iff for x, y being Element of L holds ( not x "/\" y in I or x in I or y in I ) ); theorem Th12: :: WAYBEL_7:12 for L being with_infima Poset for I being Ideal of L holds ( I is prime iff for A being non empty finite Subset of L st inf A in I holds ex a being Element of L st ( a in A & a in I ) ) proofend; registration let L be LATTICE; cluster non empty directed lower prime for Element of bool the carrier of L; existence ex b1 being Ideal of L st b1 is prime proofend; end; theorem :: WAYBEL_7:13 for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for x being set st x is prime Ideal of L1 holds x is prime Ideal of L2 proofend; definition let L be with_suprema Poset; let F be Filter of L; attrF is prime means :Def2: :: WAYBEL_7:def 2 for x, y being Element of L holds ( not x "\/" y in F or x in F or y in F ); end; :: deftheorem Def2 defines prime WAYBEL_7:def_2_:_ for L being with_suprema Poset for F being Filter of L holds ( F is prime iff for x, y being Element of L holds ( not x "\/" y in F or x in F or y in F ) ); theorem :: WAYBEL_7:14 for L being with_suprema Poset for F being Filter of L holds ( F is prime iff for A being non empty finite Subset of L st sup A in F holds ex a being Element of L st ( a in A & a in F ) ) proofend; registration let L be LATTICE; cluster non empty filtered upper prime for Element of bool the carrier of L; existence ex b1 being Filter of L st b1 is prime proofend; end; theorem Th15: :: WAYBEL_7:15 for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for x being set st x is prime Filter of L1 holds x is prime Filter of L2 proofend; theorem Th16: :: WAYBEL_7:16 for L being LATTICE for x being set holds ( x is prime Ideal of L iff x is prime Filter of (L opp) ) proofend; theorem Th17: :: WAYBEL_7:17 for L being LATTICE for x being set holds ( x is prime Filter of L iff x is prime Ideal of (L opp) ) proofend; :: Remark 3.16: (3) iff (2) theorem :: WAYBEL_7:18 for L being with_infima Poset for I being Ideal of L holds ( I is prime iff ( I ` is Filter of L or I ` = {} ) ) proofend; :: Remark 3.16: (3) iff (1) theorem :: WAYBEL_7:19 for L being LATTICE for I being Ideal of L holds ( I is prime iff I in PRIME (InclPoset (Ids L)) ) proofend; theorem Th20: :: WAYBEL_7:20 for L being Boolean LATTICE for 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 ) ) proofend; :: Remark 3.18: (1) iff (2) theorem Th21: :: WAYBEL_7:21 for X being set for 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 ) ) proofend; definition let L be non empty Poset; let F be Filter of L; attrF is ultra means :Def3: :: WAYBEL_7:def 3 ( F is proper & ( for G being Filter of L holds ( not F c= G or F = G or G = the carrier of L ) ) ); end; :: deftheorem Def3 defines ultra WAYBEL_7:def_3_:_ for L being non empty Poset for F being Filter of L holds ( F is ultra iff ( F is proper & ( for G being Filter of L holds ( not F c= G or F = G or G = the carrier of L ) ) ) ); registration let L be non empty Poset; cluster non empty filtered upper ultra -> proper for Element of bool the carrier of L; coherence for b1 being Filter of L st b1 is ultra holds b1 is proper by Def3; end; Lm1: for L being with_infima Poset for F being Filter of L for X being non empty finite Subset of L for x being Element of L st x in uparrow (fininfs (F \/ X)) holds ex a being Element of L st ( a in F & x >= a "/\" (inf X) ) proofend; :: Remark 3.18: (1)+proper iff (3) theorem Th22: :: WAYBEL_7:22 for L being Boolean LATTICE for F being Filter of L holds ( ( F is proper & F is prime ) iff F is ultra ) proofend; Lm2: for L being with_suprema Poset for I being Ideal of L for X being non empty finite Subset of L for x being Element of L st x in downarrow (finsups (I \/ X)) holds ex i being Element of L st ( i in I & x <= i "\/" (sup X) ) proofend; :: Lemma 3.19 theorem Th23: :: WAYBEL_7:23 for L being distributive LATTICE for I being Ideal of L for F being Filter of L st I misses F holds ex P being Ideal of L st ( P is prime & I c= P & P misses F ) proofend; theorem Th24: :: WAYBEL_7:24 for L being distributive LATTICE for I being Ideal of L for x being Element of L st not x in I holds ex P being Ideal of L st ( P is prime & I c= P & not x in P ) proofend; theorem Th25: :: WAYBEL_7:25 for L being distributive LATTICE for I being Ideal of L for F being Filter of L st I misses F holds ex P being Filter of L st ( P is prime & F c= P & I misses P ) proofend; theorem Th26: :: WAYBEL_7:26 for L being non trivial Boolean LATTICE for F being proper Filter of L ex G being Filter of L st ( F c= G & G is ultra ) proofend; begin definition let T be TopSpace; let F, x be set ; predx is_a_cluster_point_of F,T means :Def4: :: WAYBEL_7:def 4 for A being Subset of T st A is open & x in A holds for B being set st B in F holds A meets B; predx is_a_convergence_point_of F,T means :Def5: :: WAYBEL_7:def 5 for A being Subset of T st A is open & x in A holds A in F; end; :: deftheorem Def4 defines is_a_cluster_point_of WAYBEL_7:def_4_:_ for T being TopSpace for F, x being set holds ( x is_a_cluster_point_of F,T iff for A being Subset of T st A is open & x in A holds for B being set st B in F holds A meets B ); :: deftheorem Def5 defines is_a_convergence_point_of WAYBEL_7:def_5_:_ for T being TopSpace for F, x being set holds ( x is_a_convergence_point_of F,T iff for A being Subset of T st A is open & x in A holds A in F ); registration let X be non empty set ; cluster non empty filtered upper ultra for Element of bool the carrier of (BoolePoset X); existence ex b1 being Filter of (BoolePoset X) st b1 is ultra proofend; end; theorem Th27: :: 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 ) proofend; :: Proposition 3.20 (1) => (2) theorem Th28: :: WAYBEL_7:28 for T being non empty TopSpace for x, y being Element of (InclPoset the topology of T) st x << y holds for F being proper Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_cluster_point_of F,T ) proofend; :: 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 holds for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) proofend; :: Proposition 3.20: (3) => (1) theorem Th30: :: 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 holds ex p being Element of T st ( p in y & p is_a_convergence_point_of F,T ) ) holds x << y proofend; :: Proposition 3.21 :: [WP: ] 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 holds ex G being finite Subset of F st x c= union G ) proofend; :: 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 ) proofend; theorem Th33: :: WAYBEL_7:33 for L being LATTICE for p being Element of L st p is prime holds downarrow p is prime proofend; begin definition let L be LATTICE; let p be Element of L; attrp is pseudoprime means :Def6: :: WAYBEL_7:def 6 ex P being prime Ideal of L st p = sup P; end; :: deftheorem Def6 defines pseudoprime WAYBEL_7:def_6_:_ for L being LATTICE for p being Element of L holds ( p is pseudoprime iff ex P being prime Ideal of L st p = sup P ); theorem Th34: :: WAYBEL_7:34 for L being LATTICE for p being Element of L st p is prime holds p is pseudoprime proofend; :: Proposition 3.24: (1) => (2) theorem Th35: :: WAYBEL_7:35 for L being continuous LATTICE for p being Element of L st p is pseudoprime holds for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) proofend; :: 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 not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) ) holds uparrow (fininfs ((downarrow p) `)) misses waybelow p proofend; :: 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 non empty finite Subset of L st inf A << Top L holds ex a being Element of L st ( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) ) proofend; :: 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 holds for A being non empty finite Subset of L st inf A << p holds ex a being Element of L st ( a in A & a <= p ) proofend; :: 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 proofend; definition let L be non empty RelStr ; let R be Relation of the carrier of L; attrR is multiplicative means :Def7: :: 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; :: deftheorem Def7 defines multiplicative WAYBEL_7:def_7_:_ for L being non empty RelStr for R being Relation of the carrier of L holds ( R is multiplicative iff for a, x, y being Element of L st [a,x] in R & [a,y] in R holds [a,(x "/\" y)] in R ); registration let L be lower-bounded sup-Semilattice; let R be auxiliary Relation of L; let x be Element of L; clusterR -above x -> upper ; coherence R -above x is upper proofend; end; :: Lemma 3.25: (1) iff (2)-[non empty] theorem :: WAYBEL_7:40 for L being lower-bounded LATTICE for R being auxiliary Relation of L holds ( R is multiplicative iff for x being Element of L holds R -above x is filtered ) proofend; :: Lemma 3.25: (1) iff (3) theorem Th41: :: WAYBEL_7:41 for L being lower-bounded LATTICE for 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 ) proofend; :: Lemma 3.25: (1) iff (4) theorem :: WAYBEL_7:42 for L being lower-bounded LATTICE for 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 ) proofend; :: Lemma 3.25: (1) iff (5) theorem :: WAYBEL_7:43 for L being lower-bounded LATTICE for R being auxiliary Relation of L holds ( R is multiplicative iff R -below is meet-preserving ) proofend; Lm3: now__::_thesis:_for_L_being_lower-bounded_continuous_LATTICE for_p_being_Element_of_L_st_L_-waybelow_is_multiplicative_&_(_for_a,_b_being_Element_of_L_holds_ (_not_a_"/\"_b_<<_p_or_a_<=_p_or_b_<=_p_)_)_holds_ p_is_prime let L be lower-bounded continuous LATTICE; ::_thesis: for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) holds p is prime let p be Element of L; ::_thesis: ( L -waybelow is multiplicative & ( for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) implies p is prime ) assume that A1: L -waybelow is multiplicative and A2: for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) and A3: not p is prime ; ::_thesis: contradiction consider x, y being Element of L such that A4: x "/\" y <= p and A5: not x <= p and A6: not y <= p by A3, WAYBEL_6:def_6; A7: for a being Element of L holds ( not waybelow a is empty & waybelow a is directed ) ; then consider u being Element of L such that A8: u << x and A9: not u <= p by A5, WAYBEL_3:24; consider v being Element of L such that A10: v << y and A11: not v <= p by A6, A7, WAYBEL_3:24; A12: [v,y] in L -waybelow by A10, WAYBEL_4:def_1; [u,x] in L -waybelow by A8, WAYBEL_4:def_1; then [(u "/\" v),(x "/\" y)] in L -waybelow by A1, A12, Th41; then u "/\" v << x "/\" y by WAYBEL_4:def_1; then u "/\" v << p by A4, WAYBEL_3:2; hence contradiction by A2, A9, A11; ::_thesis: verum end; theorem Th44: :: WAYBEL_7:44 for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds for p being Element of L holds ( p is pseudoprime iff for a, b being Element of L holds ( not a "/\" b << p or a <= p or b <= p ) ) proofend; theorem :: WAYBEL_7:45 for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds for p being Element of L st p is pseudoprime holds p is prime proofend; theorem :: WAYBEL_7:46 for L being lower-bounded distributive continuous LATTICE st ( for p being Element of L st p is pseudoprime holds p is prime ) holds L -waybelow is multiplicative proofend;