Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Ideals

by
Grzegorz Bancerek

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;

```