The abstract of the Mizar article:

Ideals

by

Grzegorz Bancerek

Received October 24, 1994

MML identifier: FILTER_2

[ Mizar article, MML identifier index ]

environ

 vocabulary BINOP_1, RELAT_1, FUNCT_1, LATTICE2, LATTICES, SUBSET_1, LATTICE4,
      FILTER_0, BOOLE, NAT_LAT, ZF_LANG, FILTER_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, FUNCT_1, DOMAIN_1,
      BINOP_1, LATTICES, NAT_LAT, FILTER_0, LATTICE2, MCART_1, RELSET_1,
      LATTICE4;
 constructors DOMAIN_1, BINOP_1, NAT_LAT, FILTER_0, LATTICE2, LATTICE4,
      XBOOLE_0;
 clusters LATTICES, FILTER_0, NAT_LAT, LATTICE2, FUNCT_1, STRUCT_0, RLSUB_2,
      RELSET_1, LATTICE4, SUBSET_1, XBOOLE_0, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin :: Some Properties of the Restriction of Binary Operations

theorem :: FILTER_2:1
 for D being non empty set, S being non empty Subset of D,
  f being BinOp of D, g being BinOp of S st g = f|[:S,S:] holds
   (f is commutative implies g is commutative) &
   (f is idempotent implies g is idempotent) &
   (f is associative implies g is associative);

theorem :: FILTER_2:2
   for D being non empty set, S being non empty Subset of D,
   f being BinOp of D, g being BinOp of S
  for d being Element of D, d' being Element of S st
   g = f|[:S,S:] & d' = d holds
    (d is_a_left_unity_wrt f implies d' is_a_left_unity_wrt g) &
    (d is_a_right_unity_wrt f implies d' is_a_right_unity_wrt g) &
    (d is_a_unity_wrt f implies d' is_a_unity_wrt g);

theorem :: FILTER_2:3
 for D being non empty set, S being non empty Subset of D,
  f1,f2 being BinOp of D, g1,g2 being BinOp of S st
   g1 = f1|[:S,S:] & g2 = f2|[:S,S:] holds
    (f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2) &
    (f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2);

theorem :: FILTER_2:4
   for D being non empty set, S being non empty Subset of D,
  f1,f2 being BinOp of D, g1,g2 being BinOp of S st
   g1 = f1|[:S,S:] & g2 = f2|[:S,S:] holds
    f1 is_distributive_wrt f2 implies g1 is_distributive_wrt g2;

theorem :: FILTER_2:5
 for D being non empty set, S being non empty Subset of D,
  f1,f2 being BinOp of D, g1,g2 being BinOp of S st
   g1 = f1|[:S,S:] & g2 = f2|[:S,S:] holds
    f1 absorbs f2 implies g1 absorbs g2;

begin :: Closed Subsets of a Lattice

definition let D be non empty set, X1,X2 be Subset of D;
 redefine pred X1 = X2 means
:: FILTER_2:def 1
    for x being Element of D holds x in X1 iff x in X2;
end;

 reserve L for Lattice,
  p,q,r for Element of L,
  p',q',r' for Element of L.:,
  x,y for set;

theorem :: FILTER_2:6
 for L1,L2 being LattStr st the LattStr of L1 = the LattStr of L2 holds
   L1.: = L2.:;

theorem :: FILTER_2:7
 L.:.: = the LattStr of L;

theorem :: FILTER_2:8
 for L1,L2 being non empty LattStr st the LattStr of L1 = the LattStr of L2
  for a1,b1 being Element of L1,
      a2,b2 being Element of L2 st
   a1 = a2 & b1 = b2 holds
    a1"\/"b1 = a2"\/"b2 & a1"/\"b1 = a2"/\"b2 & (a1 [= b1 iff a2 [= b2);

theorem :: FILTER_2:9
 for L1,L2 being 0_Lattice st the LattStr of L1 = the LattStr of L2 holds
   Bottom L1 = Bottom L2;

theorem :: FILTER_2:10
 for L1,L2 being 1_Lattice st the LattStr of L1 = the LattStr of L2 holds
   Top L1 = Top L2;

theorem :: FILTER_2:11
 for L1,L2 being C_Lattice st the LattStr of L1 = the LattStr of L2
  for a1,b1 being Element of L1,
      a2,b2 being Element of L2 st
   a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
    a2 is_a_complement_of b2;

theorem :: FILTER_2:12
   for L1,L2 being B_Lattice st the LattStr of L1 = the LattStr of L2
  for a being Element of L1,
      b being Element of L2 st a = b
   holds a` = b`;

theorem :: FILTER_2:13
   for X being Subset of L
    st for p,q holds p in X & q in X iff p"/\"q in X holds
   X is ClosedSubset of L;

theorem :: FILTER_2:14
 for X being Subset of L
    st for p,q holds p in X & q in X iff p"\/"q in X holds
   X is ClosedSubset of L;

definition let L;
 redefine mode Filter of L -> non empty ClosedSubset of L;
end;

definition let L;
 redefine func <.L.) -> Filter of L;
 let p be Element of L;
 func <.p.) -> Filter of L;
end;

definition let L; let D be non empty Subset of L;
 redefine func <.D.) -> Filter of L;
end;

definition let L be D_Lattice; let F1,F2 be Filter of L;
 redefine func F1 "/\" F2 -> Filter of L;
end;

definition let L;
 canceled;

 mode Ideal of L -> non empty ClosedSubset of L means
:: FILTER_2:def 3
  p in it & q in it iff p "\/" q in it;
end;

theorem :: FILTER_2:15
 for X being non empty Subset of L st
   for p,q holds p in X & q in X iff p "\/" q in X holds X is Ideal of L;

theorem :: FILTER_2:16
 for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2
   for x st x is Filter of L1 holds x is Filter of L2;

theorem :: FILTER_2:17
 for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2
   for x st x is Ideal of L1 holds x is Ideal of L2;

definition let L,p;
 func p.: -> Element of L.: equals
:: FILTER_2:def 4
   p;
end;

definition let L; let p be Element of L.:;
 func .:p -> Element of L equals
:: FILTER_2:def 5
   p;
end;

theorem :: FILTER_2:18
 .:(p.:) = p & ( .:p').: = p';

theorem :: FILTER_2:19
 p"/\"q = p.:"\/"q.: & p"\/"q = p.:"/\"q.: & p'"/\"q' = .:p'"\/".:
q' & p'"\/"q' = .:p' "/\".:q';

theorem :: FILTER_2:20
 (p [= q iff q.: [= p.:) & (p' [= q' iff .:q' [= .:p');

theorem :: FILTER_2:21
 x is Ideal of L iff x is Filter of L.:;

 definition let L; let X be Subset of L;
  func X.: -> Subset of L.: equals
:: FILTER_2:def 6
    X;
 end;

 definition let L; let X be Subset of L.:;
  func .:X -> Subset of L equals
:: FILTER_2:def 7
    X;
 end;

definition let L; let D be non empty Subset of L;
 cluster D.: -> non empty;
end;

definition let L; let D be non empty Subset of L.:;
 cluster .:D -> non empty;
end;

definition let L; let S be ClosedSubset of L;
 redefine func S.: -> ClosedSubset of L.:;
end;

definition let L; let S be non empty ClosedSubset of L;
 redefine func S.: -> non empty ClosedSubset of L.:;
end;

definition let L; let S be ClosedSubset of L.:;
 redefine func .:S -> ClosedSubset of L;
end;

definition let L; let S be non empty ClosedSubset of L.:;
 redefine func .:S -> non empty ClosedSubset of L;
end;

definition let L; let F be Filter of L;
 redefine func F.: -> Ideal of L.:;
end;

definition let L; let F be Filter of L.:;
 redefine func .:F -> Ideal of L;
end;

definition let L; let I be Ideal of L;
 redefine func I.: -> Filter of L.:;
end;

definition let L; let I be Ideal of L.:;
 redefine func .:I -> Filter of L;
end;

theorem :: FILTER_2:22
  for D being non empty Subset of L holds D is Ideal of L
 iff
  (for p,q st p in D & q in D holds p "\/" q in D) &
   for p,q st p in D & q [= p holds q in D;

 reserve I,J for Ideal of L, F for Filter of L;

theorem :: FILTER_2:23
 p in I implies p"/\"q in I & q"/\"p in I;

theorem :: FILTER_2:24
   ex p st p in I;

theorem :: FILTER_2:25
   L is lower-bounded implies Bottom L in I;

theorem :: FILTER_2:26
   L is lower-bounded implies {Bottom L} is Ideal of L;

theorem :: FILTER_2:27
   {p} is Ideal of L implies L is lower-bounded;

begin :: Ideals Generated by Subsets of a Lattice

theorem :: FILTER_2:28
  the carrier of L is Ideal of L;

 definition let L;
  func (.L.> -> Ideal of L equals
:: FILTER_2:def 8
    the carrier of L;
 end;

 definition let L,p;
  func (.p.> -> Ideal of L equals
:: FILTER_2:def 9
    { q : q [= p };
 end;

theorem :: FILTER_2:29
 q in (.p.> iff q [= p;

theorem :: FILTER_2:30
  (.p.> = <.p.:.) & (.p.:.> = <.p.);

theorem :: FILTER_2:31
   p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.>;

theorem :: FILTER_2:32
   L is upper-bounded implies (.L.> = (.Top L.>;

 definition let L,I;
  pred I is_max-ideal means
:: FILTER_2:def 10
     I <> the carrier of L & for J st I c= J & J <> the carrier of L
     holds I = J;
 end;

theorem :: FILTER_2:33
  I is_max-ideal iff I.: is_ultrafilter;

theorem :: FILTER_2:34
   L is upper-bounded implies for I st I <> the carrier of L
   ex J st I c= J & J is_max-ideal;

theorem :: FILTER_2:35
   (ex r st p "\/" r <> p) implies (.p.> <> the carrier of L;

theorem :: FILTER_2:36
   L is upper-bounded & p <> Top L implies ex I st p in I & I is_max-ideal;

 reserve D for non empty Subset of L,
  D' for non empty Subset of L.:;

 definition let L,D;
  func (.D.> -> Ideal of L means
:: FILTER_2:def 11
   D c= it & for I st D c= I holds it c= I;
 end;

theorem :: FILTER_2:37
  <.D.:.) = (.D.> & <.D.) = (.D.:.> & <..:D'.) = (.D'.> & <.D'.) = (..:
D'.>;

theorem :: FILTER_2:38
  (.I.> = I;

 reserve D1,D2 for non empty Subset of L,
  D1',D2' for non empty Subset of L.:;

theorem :: FILTER_2:39
   (D1 c= D2 implies (.D1.> c= (.D2.>) & (.(.D.>.> c= (.D.>;

theorem :: FILTER_2:40
   p in D implies (.p.> c= (.D.>;

theorem :: FILTER_2:41
   D = {p} implies (.D.> = (.p.>;

theorem :: FILTER_2:42
 L is upper-bounded & Top
L in D implies (.D.> = (.L.> & (.D.> = the carrier of L;

theorem :: FILTER_2:43
   L is upper-bounded & Top L in I implies I = (.L.> & I = the carrier of L;

 definition let L,I;
  attr I is prime means
:: FILTER_2:def 12
     p "/\" q in I iff p in I or q in I;
 end;

theorem :: FILTER_2:44
 I is prime iff I.: is prime;

 definition let L,D1,D2;
  func D1 "\/" D2 -> Subset of L equals
:: FILTER_2:def 13
    { p"\/"q : p in D1 & q in D2 };
 end;

 definition let L,D1,D2;
  cluster D1 "\/" D2 -> non empty;
 end;

theorem :: FILTER_2:45
  D1 "\/" D2 = D1.: "/\" D2.: & D1.: "\/" D2.: = D1 "/\" D2 &
   D1' "\/" D2' = .:D1' "/\" .:D2' & .:D1' "\/" .:D2' = D1' "/\" D2';

theorem :: FILTER_2:46
   p in D1 & q in D2 implies p"\/"q in D1 "\/" D2 & q"\/"p in D1 "\/" D2;

theorem :: FILTER_2:47
   x in D1 "\/" D2 implies ex p,q st x = p"\/"q & p in D1 & q in D2;

theorem :: FILTER_2:48
   D1 "\/" D2 = D2 "\/" D1;

 definition let L be D_Lattice; let I1,I2 be Ideal of L;
  redefine func I1 "\/" I2 -> Ideal of L;
 end;

theorem :: FILTER_2:49
   (.D1 \/ D2.> = (.(.D1.> \/ D2.> & (.D1 \/ D2.> = (.D1 \/ (.D2.>.>;

theorem :: FILTER_2:50
   (.I \/ J.> = { r : ex p,q st r [= p"\/"q & p in I & q in J };

theorem :: FILTER_2:51
   I c= I "\/" J & J c= I "\/" J;

theorem :: FILTER_2:52
   (.I \/ J.> = (.I "\/" J.>;

 reserve B for B_Lattice, I_B,J_B for Ideal of B,
    a,b for Element of B;

theorem :: FILTER_2:53
  L is C_Lattice iff L.: is C_Lattice;

theorem :: FILTER_2:54
 L is B_Lattice iff L.: is B_Lattice;


definition let B be B_Lattice;
 cluster B.: -> Boolean Lattice-like;
end;

reserve a' for Element of (B qua Lattice).:;

theorem :: FILTER_2:55
 a.:` = a` & ( .:a')` = a'`;

theorem :: FILTER_2:56
   (.I_B \/ J_B.> = I_B "\/" J_B;

theorem :: FILTER_2:57
   I_B is_max-ideal iff
   I_B <> the carrier of B & for a holds a in I_B or a` in I_B;

theorem :: FILTER_2:58
   I_B <> (.B.> & I_B is prime iff I_B is_max-ideal;

theorem :: FILTER_2:59
   I_B is_max-ideal implies for a holds a in I_B iff not a` in I_B;

theorem :: FILTER_2:60
   a <> b implies ex I_B st I_B is_max-ideal &
   (a in I_B & not b in I_B or not a in I_B & b in I_B);

 reserve P for non empty ClosedSubset of L,
  o1,o2 for BinOp of P;

theorem :: FILTER_2:61
  (the L_join of L)|[:P,P:] is BinOp of P &
  (the L_meet of L)|[:P,P:] is BinOp of P;

theorem :: FILTER_2:62
 o1 = (the L_join of L)|[:P,P:] & o2 = (the L_meet of L)|[:P,P:] implies
  o1 is commutative & o1 is associative &
   o2 is commutative & o2 is associative &
    o1 absorbs o2 & o2 absorbs o1;

 definition let L,p,q; assume
 p [= q;
  func [#p,q#] -> non empty ClosedSubset of L equals
:: FILTER_2:def 14
    {r: p [= r & r [= q};
 end;

theorem :: FILTER_2:63
 p [= q implies (r in [#p,q#] iff p [= r & r [= q);

theorem :: FILTER_2:64
  p [= q implies p in [#p,q#] & q in [#p,q#];

theorem :: FILTER_2:65
   [#p,p#] = {p};

theorem :: FILTER_2:66
   L is upper-bounded implies <.p.) = [#p,Top L#];

theorem :: FILTER_2:67
   L is lower-bounded implies (.p.> = [#Bottom L,p#];

theorem :: FILTER_2:68
   for L1,L2 being Lattice
  for F1 being Filter of L1, F2 being Filter of L2 st
   the LattStr of L1 = the LattStr of L2 & F1 = F2 holds latt F1 = latt F2;

begin :: Sublattices

definition let L;
 redefine mode SubLattice of L means
:: FILTER_2:def 15
   ex P,o1,o2 st o1 = (the L_join of L)|[:P,P:] &
    o2 = (the L_meet of L)|[:P,P:] & the LattStr of it = LattStr (#P, o1, o2#);
 synonym Sublattice of L;
end;

theorem :: FILTER_2:69
 for K being Sublattice of L, a being Element of K
 holds a is Element of L;

 definition let L,P;
  func latt (L,P) -> Sublattice of L means
:: FILTER_2:def 16
   ex o1,o2 st o1 = (the L_join of L)|[:P,P:] &
    o2 = (the L_meet of L)|[:P,P:] & it = LattStr (#P, o1, o2#);
 end;

 definition let L,P;
  cluster latt (L,P) -> strict;
 end;

definition let L; let l be Sublattice of L;
 redefine func l.: -> strict Sublattice of L.:;
end;

theorem :: FILTER_2:70
 latt F = latt (L,F);

theorem :: FILTER_2:71
 latt (L,P) = (latt (L.:,P.:)).:;

theorem :: FILTER_2:72
   latt (L,(.L.>) = the LattStr of L & latt (L,<.L.)) = the LattStr of L;

theorem :: FILTER_2:73
 the carrier of latt (L,P) = P &
 the L_join of latt (L,P) = (the L_join of L)|[:P,P:] &
 the L_meet of latt (L,P) = (the L_meet of L)|[:P,P:];

theorem :: FILTER_2:74
 for p,q for p',q' being Element of latt (L,P) st
   p = p' & q = q' holds p"\/"q = p'"\/"q' & p"/\"q = p'"/\"q';

theorem :: FILTER_2:75
 for p,q for p',q' being Element of latt (L,P) st
   p = p' & q = q' holds p [= q iff p' [= q';

theorem :: FILTER_2:76
   L is lower-bounded implies latt (L,I) is lower-bounded;

theorem :: FILTER_2:77
   L is modular implies latt (L,P) is modular;

theorem :: FILTER_2:78
 L is distributive implies latt (L,P) is distributive;

theorem :: FILTER_2:79
   L is implicative & p [= q implies latt (L,[#p,q#]) is implicative;

theorem :: FILTER_2:80
 latt (L,(.p.>) is upper-bounded;

theorem :: FILTER_2:81
 Top latt (L,(.p.>) = p;

theorem :: FILTER_2:82
 L is lower-bounded implies
   latt (L,(.p.>) is lower-bounded & Bottom latt (L,(.p.>) = Bottom L;

theorem :: FILTER_2:83
 L is lower-bounded implies latt (L,(.p.>) is bounded;

theorem :: FILTER_2:84
 p [= q implies latt (L,[#p,q#]) is bounded &
   Top latt (L,[#p,q#]) = q & Bottom latt (L,[#p,q#]) = p;

theorem :: FILTER_2:85
   L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice;

theorem :: FILTER_2:86
 L is C_Lattice & L is modular & p [= q implies
   latt (L,[#p,q#]) is C_Lattice;

theorem :: FILTER_2:87
   L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice;