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;