:: Ideals
:: by Grzegorz Bancerek
::
:: Received October 24, 1994
:: Copyright (c) 1994-2018 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 XBOOLE_0, SUBSET_1, BINOP_1, REALSET1, RELAT_1, ZFMISC_1,
FUNCT_1, LATTICE2, LATTICES, STRUCT_0, EQREL_1, PBOOLE, LATTICE4,
FILTER_0, CARD_FIL, CAT_1, TARSKI, INT_2, YELLOW11, LATTICE5, NAT_LAT,
XBOOLEAN, XXREAL_2, FILTER_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
DOMAIN_1, BINOP_1, REALSET1, LATTICES, NAT_LAT, FILTER_0, LATTICE2,
MCART_1, LATTICE4;
constructors BINOP_1, REALSET1, FILTER_0, LATTICE2, NAT_LAT, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, LATTICES,
FILTER_0, LATTICE2, NAT_LAT;
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 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, d9 being Element of S
st g = f||S & d9 = d holds (d is_a_left_unity_wrt f implies d9
is_a_left_unity_wrt g) & (d is_a_right_unity_wrt f implies d9
is_a_right_unity_wrt g) & (d is_a_unity_wrt f implies d9 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 & g2 = f2||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 & g2 = f2||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 & g2 = f2||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,
p9,q9,r9 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;
mode Ideal of L is non empty initial join-closed Subset of L;
end;
theorem :: FILTER_2:15
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:16
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 2
p;
end;
definition
let L;
let p be Element of L.:;
func .:p -> Element of L equals
:: FILTER_2:def 3
p;
end;
theorem :: FILTER_2:17
.:(p.:) = p & ( .:p9).: = p9;
theorem :: FILTER_2:18
p"/\"q = p.:"\/"q.: & p"\/"q = p.:"/\"q.: & p9"/\"q9 = .:p9"\/".: q9 &
p9"\/"q9 = .:p9 "/\".:q9;
theorem :: FILTER_2:19
(p [= q iff q.: [= p.:) & (p9 [= q9 iff .:q9 [= .:p9);
definition
let L;
let X be Subset of L;
func X.: -> Subset of L.: equals
:: FILTER_2:def 4
X;
end;
definition
let L;
let X be Subset of L.:;
func .:X -> Subset of L equals
:: FILTER_2:def 5
X;
end;
registration
let L;
let D be non empty Subset of L;
cluster D.: -> non empty;
end;
registration
let L;
let D be non empty Subset of L.:;
cluster .:D -> non empty;
end;
registration
let L;
let S be meet-closed Subset of L;
cluster S.: -> join-closed for Subset of L.:;
end;
registration
let L;
let S be join-closed Subset of L;
cluster S.: -> meet-closed for Subset of L.:;
end;
registration
let L;
let S be meet-closed Subset of L.:;
cluster .:S -> join-closed for Subset of L;
end;
registration
let L;
let S be join-closed Subset of L.:;
cluster .:S -> meet-closed for Subset of L;
end;
registration
let L;
let F be final Subset of L;
cluster F.: -> initial for Subset of L.:;
end;
registration
let L;
let F be initial Subset of L;
cluster F.: -> final for Subset of L.:;
end;
registration
let L;
let F be final Subset of L.:;
cluster .:F -> initial for Subset of L;
end;
registration
let L;
let F be initial Subset of L.:;
cluster F.: -> final for Subset of L;
end;
theorem :: FILTER_2:20
x is Ideal of L iff x is Filter of L.:;
theorem :: FILTER_2:21
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:22
p in I implies p"/\"q in I & q"/\"p in I;
theorem :: FILTER_2:23
ex p st p in I;
theorem :: FILTER_2:24
L is lower-bounded implies Bottom L in I;
theorem :: FILTER_2:25
L is lower-bounded implies {Bottom L} is Ideal of L;
theorem :: FILTER_2:26
{p} is Ideal of L implies L is lower-bounded;
begin :: Ideals Generated by Subsets of a Lattice
theorem :: FILTER_2:27
the carrier of L is Ideal of L;
definition
let L;
func (.L.> -> Ideal of L equals
:: FILTER_2:def 6
the carrier of L;
end;
definition
let L,p;
func (.p.> -> Ideal of L equals
:: FILTER_2:def 7
{ q : q [= p };
end;
theorem :: FILTER_2:28
q in (.p.> iff q [= p;
theorem :: FILTER_2:29
(.p.> = <.p.:.) & (.p.:.> = <.p.);
theorem :: FILTER_2:30
p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.>;
theorem :: FILTER_2:31
L is upper-bounded implies (.L.> = (.Top L.>;
definition
let L,I;
attr I is max-ideal means
:: FILTER_2:def 8
I <> the carrier of L & for J st I c= J & J <> the carrier of L holds I = J;
end;
theorem :: FILTER_2:32
I is max-ideal iff I.: is being_ultrafilter;
theorem :: FILTER_2:33
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:34
(ex r st p "\/" r <> p) implies (.p.> <> the carrier of L;
theorem :: FILTER_2:35
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,
D9 for non empty Subset of L.:;
definition
let L,D;
func (.D.> -> Ideal of L means
:: FILTER_2:def 9
D c= it & for I st D c= I holds it c= I;
end;
theorem :: FILTER_2:36
<.D.:.) = (.D.> & <.D.) = (.D.:.> & <..:D9.) = (.D9.> & <.D9.) = (..: D9.>;
theorem :: FILTER_2:37
(.I.> = I;
reserve D1,D2 for non empty Subset of L,
D19,D29 for non empty Subset of L.:;
theorem :: FILTER_2:38
(D1 c= D2 implies (.D1.> c= (.D2.>) & (.(.D.>.> c= (.D.>;
theorem :: FILTER_2:39
p in D implies (.p.> c= (.D.>;
theorem :: FILTER_2:40
D = {p} implies (.D.> = (.p.>;
theorem :: FILTER_2:41
L is upper-bounded & Top L in D implies (.D.> = (.L.> & (.D.> =
the carrier of L;
theorem :: FILTER_2:42
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 10
p "/\" q in I iff p in I or q in I;
end;
theorem :: FILTER_2:43
I is prime iff I.: is prime;
definition
let L,D1,D2;
func D1 "\/" D2 -> Subset of L equals
:: FILTER_2:def 11
{ p"\/"q : p in D1 & q in D2 };
end;
registration
let L,D1,D2;
cluster D1 "\/" D2 -> non empty;
end;
theorem :: FILTER_2:44
D1 "\/" D2 = D1.: "/\" D2.: & D1.: "\/" D2.: = D1 "/\" D2 & D19
"\/" D29 = .:D19 "/\" .:D29 & .:D19 "\/" .:D29 = D19 "/\" D29;
theorem :: FILTER_2:45
p in D1 & q in D2 implies p"\/"q in D1 "\/" D2 & q"\/"p in D1 "\/" D2;
theorem :: FILTER_2:46
x in D1 "\/" D2 implies ex p,q st x = p"\/"q & p in D1 & q in D2;
theorem :: FILTER_2:47
D1 "\/" D2 = D2 "\/" D1;
registration
let L be D_Lattice;
let I1,I2 be Ideal of L;
cluster I1 "\/" I2 -> initial join-closed;
end;
theorem :: FILTER_2:48
(.D1 \/ D2.> = (.(.D1.> \/ D2.> & (.D1 \/ D2.> = (.D1 \/ (.D2.>.>;
theorem :: FILTER_2:49
(.I \/ J.> = { r : ex p,q st r [= p"\/"q & p in I & q in J };
theorem :: FILTER_2:50
I c= I "\/" J & J c= I "\/" J;
theorem :: FILTER_2:51
(.I \/ J.> = (.I "\/" J.>;
reserve B for B_Lattice,
IB,JB for Ideal of B,
a,b for Element of B;
theorem :: FILTER_2:52
L is C_Lattice iff L.: is C_Lattice;
theorem :: FILTER_2:53
L is B_Lattice iff L.: is B_Lattice;
registration
let B be B_Lattice;
cluster B.: -> Boolean Lattice-like;
end;
reserve a9 for Element of (B qua Lattice).:;
theorem :: FILTER_2:54
a.:` = a` & ( .:a9)` = a9`;
theorem :: FILTER_2:55
(.IB \/ JB.> = IB "\/" JB;
theorem :: FILTER_2:56
IB is max-ideal iff IB <> the carrier of B & for a holds a in IB or a` in
IB;
theorem :: FILTER_2:57
IB <> (.B.> & IB is prime iff IB is max-ideal;
theorem :: FILTER_2:58
IB is max-ideal implies for a holds a in IB iff not a` in IB;
theorem :: FILTER_2:59
a <> b implies ex IB st IB is max-ideal & (a in IB & not b in IB or
not a in IB & b in IB);
reserve P for non empty ClosedSubset of L,
o1,o2 for BinOp of P;
theorem :: FILTER_2:60
(the L_join of L)||P is BinOp of P & (the L_meet of L)||P is BinOp of P;
theorem :: FILTER_2:61
o1 = (the L_join of L)||P & o2 = (the L_meet of L)||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 12
{r: p [= r & r [=
q};
end;
theorem :: FILTER_2:62
p [= q implies (r in [#p,q#] iff p [= r & r [= q);
theorem :: FILTER_2:63
p [= q implies p in [#p,q#] & q in [#p,q#];
theorem :: FILTER_2:64
[#p,p#] = {p};
theorem :: FILTER_2:65
L is upper-bounded implies <.p.) = [#p,Top L#];
theorem :: FILTER_2:66
L is lower-bounded implies (.p.> = [#Bottom L,p#];
theorem :: FILTER_2:67
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
notation
let L;
synonym Sublattice of L for SubLattice of L;
end;
definition
let L;
redefine mode Sublattice of L means
:: FILTER_2:def 13
ex P,o1,o2 st o1 = (the L_join
of L)||P & o2 = (the L_meet of L)||P & the LattStr of it = LattStr (#P, o1, o2
#);
end;
theorem :: FILTER_2:68
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 14
ex o1,o2 st o1 = (the
L_join of L)||P & o2 = (the L_meet of L)||P & it = LattStr (#P, o1, o2#);
end;
registration
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:69
latt F = latt (L,F);
theorem :: FILTER_2:70
latt (L,P) = (latt (L.:,P.:)).:;
theorem :: FILTER_2:71
latt (L,(.L.>) = the LattStr of L & latt (L,<.L.)) = the LattStr of L;
theorem :: FILTER_2:72
the carrier of latt (L,P) = P & the L_join of latt (L,P) = (the
L_join of L)||P & the L_meet of latt (L,P) = (the L_meet of L)||P;
theorem :: FILTER_2:73
for p,q for p9,q9 being Element of latt (L,P) st p = p9 & q = q9
holds p"\/"q = p9"\/"q9 & p"/\"q = p9"/\"q9;
theorem :: FILTER_2:74
for p,q for p9,q9 being Element of latt (L,P) st p = p9 & q = q9
holds p [= q iff p9 [= q9;
theorem :: FILTER_2:75
L is lower-bounded implies latt (L,I) is lower-bounded;
theorem :: FILTER_2:76
L is modular implies latt (L,P) is modular;
theorem :: FILTER_2:77
L is distributive implies latt (L,P) is distributive;
theorem :: FILTER_2:78
L is implicative & p [= q implies latt (L,[#p,q#]) is implicative;
registration
let L,p;
cluster latt (L,(.p.>) -> upper-bounded;
end;
theorem :: FILTER_2:79
Top latt (L,(.p.>) = p;
theorem :: FILTER_2:80
L is lower-bounded implies latt (L,(.p.>) is lower-bounded &
Bottom latt (L,(.p.>) = Bottom L;
theorem :: FILTER_2:81
L is lower-bounded implies latt (L,(.p.>) is bounded;
theorem :: FILTER_2:82
p [= q implies latt (L,[#p,q#]) is bounded & Top latt (L,[#p,q#]
) = q & Bottom latt (L,[#p,q#]) = p;
theorem :: FILTER_2:83
L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice;
theorem :: FILTER_2:84
L is C_Lattice & L is modular & p [= q implies latt (L,[#p,q#]) is C_Lattice;
theorem :: FILTER_2:85
L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice;
theorem :: FILTER_2:86
for S being non empty Subset of L holds
S is Ideal of L iff for p,q being Element of L holds
p in S & q in S iff p "\/" q in S;