:: Prime Filters and Ideals in Distributive Lattices
:: by Adam Grabowski
::
:: Received October 7, 2013
:: Copyright (c) 2013-2026 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, PRE_TOPC, SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1,
STRUCT_0, FUNCT_1, LATTICES, EQREL_1, XXREAL_2, CARD_FIL, RELAT_1, INT_2,
FILTER_0, PBOOLE, LOPCLSET, ORDINAL1, FILTER_2, CAT_1, GROUP_4, OPENLATT,
YELLOW11, LATTICEA, ISOMICHI, LATTICE3;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
ORDINAL1, PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, PRE_TOPC,
LATTICES, LATTICE2, FILTER_0, FILTER_2, SETWISEO, OPENLATT, ISOMICHI,
LATTICE3;
constructors BINOP_1, SETWISEO, PRE_TOPC, LATTICE2, FILTER_1, CLASSES1,
LATTICE4, RELSET_1, FILTER_0, FILTER_2, OPENLATT, DOMAIN_1, BOOLEALG,
ISOMICHI, LATTICE3;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_2, STRUCT_0, LATTICES,
PRE_TOPC, CARD_1, RELSET_1, FILTER_2, LATTICE3, LATTICE4;
requirements BOOLE, SUBSET;
definitions TARSKI, LATTICES;
equalities STRUCT_0, SUBSET_1, FILTER_0, FILTER_2, OPENLATT;
expansions TARSKI, LATTICES, XBOOLE_0;
theorems TARSKI, SETFAM_1, LATTICES, PRE_TOPC, SUBSET_1, LATTICE4, FILTER_0,
FUNCT_1, FUNCT_2, ZFMISC_1, LOPCLSET, RELSET_1, XBOOLE_0, XBOOLE_1,
EQREL_1, ORDINAL1, ORDERS_1, FILTER_2, BOOLEALG, LATTICE3, OPENLATT;
schemes FUNCT_1;
begin :: Preliminaries
definition let IT be set;
attr IT is unordered means
for p1,p2 being set st p1 in IT & p2 in IT & p1 <> p2 holds
p1,p2 are_c=-incomparable;
end;
registration
cluster non trivial for B_Lattice;
existence
proof
set L = {{},{{}}};
reconsider B = BooleLatt {{}} as non empty LattStr;
bool {{}} = L by ZFMISC_1:24; then
A3: the carrier of B = L by LATTICE3:def 1;
{} in L & {{}} in L by TARSKI:def 2; then
B is non trivial by A3,ZFMISC_1:def 10;
hence thesis;
end;
end;
theorem TopBot:
for L being non trivial bounded Lattice holds
Top L <> Bottom L
proof
let L be non trivial bounded Lattice;
set p = Top L;
assume
A0: Top L = Bottom L;
consider p being Element of L such that
A2: p <> Top L by SUBSET_1:50;
Bottom L [= p;
hence thesis by A2,A0;
end;
theorem
for L being Lattice,
I being Ideal of L holds
I is prime iff
I` is Filter of L or I` = {}
proof
let L be Lattice,
I be Ideal of L;
set F = I`;
thus I is prime implies I` is Filter of L or I` = {}
proof
assume I is prime; then
A1: for x,y being Element of L st x "/\" y in I holds x in I or y in I
by FILTER_2:def 10;
A2: F is meet-closed
proof
let x,y be Element of L;
assume x in F & y in F;
then (not x in I) & not y in I by XBOOLE_0:def 5;
hence thesis by A1,SUBSET_1:29;
end;
F is final
proof
let x,y be Element of L;
assume that
A5: x [= y and
A4: x in F;
y in I implies x in I by A5,LATTICES:def 22;
hence thesis by A4,XBOOLE_0:def 5;
end;
hence thesis by A2;
end;
assume
A6: I` is Filter of L or I` = {};
for x, y being Element of L holds
x "/\" y in I iff x in I or y in I
proof
let x,y be Element of L;
hereby
assume x "/\" y in I; then
T1: not x "/\" y in F by XBOOLE_0:def 5;
per cases by A6;
suppose F is Filter of L; then
not x in F or not y in F by T1,FILTER_0:9;
hence x in I or y in I by XBOOLE_0:def 5;
end;
suppose
T2: F = {};
I = F`;
hence x in I or y in I by T2;
end;
end;
assume x in I or y in I; then
T4: not x in F or not y in F by XBOOLE_0:def 5;
per cases by A6;
suppose F is Filter of L; then
not x "/\" y in F by FILTER_0:8,T4;
hence x "/\" y in I by XBOOLE_0:def 5;
end;
suppose
T2: F = {};
I = F`;
hence x "/\" y in I by T2;
end;
end;
hence thesis by FILTER_2:def 10;
end;
theorem
for L being Lattice,
F being Filter of L holds
F is prime iff
F` is Ideal of L or F` = {}
proof
let L be Lattice,
I be Filter of L;
set F = I`;
thus I is prime implies F is Ideal of L or F = {}
proof
assume I is prime; then
A1: for x,y being Element of L st x "\/" y in I holds x in I or y in I
by FILTER_0:def 5;
A2: F is join-closed
proof
let x,y be Element of L;
assume x in F & y in F;
then (not x in I) & not y in I by XBOOLE_0:def 5;
hence thesis by A1,SUBSET_1:29;
end;
F is initial
proof
let x,y be Element of L;
assume that
A5: x [= y and
A4: y in F;
x in I implies y in I by A5,LATTICES:def 23;
hence thesis by A4,XBOOLE_0:def 5;
end;
hence thesis by A2;
end;
assume
A6: I` is Ideal of L or I` = {};
for x, y being Element of L holds
x "\/" y in I iff x in I or y in I
proof
let x,y be Element of L;
hereby
assume x "\/" y in I; then
T1: not x "\/" y in F by XBOOLE_0:def 5;
per cases by A6;
suppose F is Ideal of L; then
not x in F or not y in F by T1,FILTER_2:21;
hence x in I or y in I by XBOOLE_0:def 5;
end;
suppose
T2: F = {};
I = F`;
hence x in I or y in I by T2;
end;
end;
assume x in I or y in I; then
T4: not x in F or not y in F by XBOOLE_0:def 5;
per cases by A6;
suppose F is Ideal of L; then
not x "\/" y in F by FILTER_2:86,T4;
hence x "\/" y in I by XBOOLE_0:def 5;
end;
suppose
T2: F = {};
I = F`;
hence x "\/" y in I by T2;
end;
end;
hence thesis by FILTER_0:def 5;
end;
definition let L be Lattice;
func PFilters L -> Subset-Family of L equals
{ F where F is Filter of L : F is prime };
coherence
proof
set US = { F where F is Filter of L : F is prime };
US c= bool the carrier of L
proof
let x be object;
assume x in US;
then ex UF being Filter of L st UF = x & UF is prime;
hence thesis;
end;
hence thesis;
end;
end;
IIsPrime:
for L being Lattice holds
(.L.> is prime
proof
let L be Lattice;
set F = (.L.>;
for p, q being Element of L holds
p "/\" q in F iff p in F or q in F;
hence thesis by FILTER_2:def 10;
end;
registration let L be Lattice;
cluster (.L.> -> prime;
coherence by IIsPrime;
end;
theorem PrimFil:
for L being distributive Lattice holds
F_primeSet L c< PFilters L
proof
let L be distributive Lattice;
A1: F_primeSet L c= PFilters L
proof
let x be object;
assume x in F_primeSet L; then
consider F being Filter of L such that
A2: x = F & F <> the carrier of L & F is prime;
thus thesis by A2;
end;
not <.L.) in F_primeSet L
proof
assume <.L.) in F_primeSet L; then
consider F being Filter of L such that
B1: F = <.L.) & F <> the carrier of L & F is prime;
thus thesis by B1;
end;
hence thesis by A1;
end;
begin :: Examples of Filters in Nontrivial Boolean Lattices
theorem lemma3:
the carrier of BooleLatt {{}} = {{},{{}}}
proof
the carrier of BooleLatt {{}} = bool {{}} by LATTICE3:def 1;
hence thesis by ZFMISC_1:24;
end;
theorem lemma1:
for L being Lattice,
A being Subset of L
st L = BooleLatt {{}} holds
A = {} or A = {{}} or A = {{},{{}}} or A = {{{}}}
proof
let L be Lattice,
A be Subset of L;
assume L = BooleLatt {{}}; then
A2: the carrier of L = bool {{}} by LATTICE3:def 1;
bool {{}} = {{}, {{}}} by ZFMISC_1:24;
hence thesis by ZFMISC_1:36,A2;
end;
theorem lemma2:
for L being Lattice,
A being Filter of L
st L = BooleLatt {{}} holds
A = {} or A = {{},{{}}} or A = {{{}}}
proof
let L be Lattice,
A be Filter of L;
assume
A0: L = BooleLatt {{}};
A <> {{}}
proof
assume
Z0: A = {{}};
reconsider b = {{}}, a = {} as Element of L by TARSKI:def 2,A0,lemma3;
z1: {{}} /\ {} = b "/\" a by A0,LATTICE3:1;
b in A & a in A iff b "/\" a in A by FILTER_0:8;
hence thesis by z1,Z0,TARSKI:def 1;
end;
hence thesis by A0,lemma1;
end;
theorem
for L being Lattice,
A being Filter of L
st L = BooleLatt {{}} holds
A = {Top L} or A = <.L.)
proof
let L be Lattice,
A be Filter of L;
assume
A0: L = BooleLatt {{}};
Top L = {{}} by A0,LATTICE3:4; then
reconsider B = {{{}}} as Filter of L by FILTER_0:12,A0;
per cases by lemma2,A0;
suppose
A = {};
hence thesis;
end;
suppose A = {{},{{}}};
hence thesis by lemma3,A0;
end;
suppose A = {{{}}};
hence thesis by A0,LATTICE3:4;
end;
end;
theorem
for L being non trivial Boolean Lattice,
A being Filter of L
st L = BooleLatt {{}} & A = {Top L} holds
A is prime
proof
let L be non trivial Boolean Lattice,
A be Filter of L;
assume
A1: L = BooleLatt {{}} & A = {Top L};
for H being Filter of L st
A c= H & H <> the carrier of L holds A = H
proof
let H be Filter of L;
assume A c= H & H <> the carrier of L; then
H = {} or H = {{{}}} by lemma3,A1,lemma2;
hence thesis by A1,LATTICE3:4;
end; then
A is being_ultrafilter by A1,FILTER_0:def 3;
hence thesis by FILTER_0:45;
end;
theorem
for L being Lattice,
A being Filter of L
st L = BooleLatt {{}} & A is being_ultrafilter holds
A = {Top L}
proof
let L be Lattice,
A be Filter of L;
assume
A0: L = BooleLatt {{}};
assume
Z1: A is being_ultrafilter;
A1: Top L = {{}} by A0,LATTICE3:4; then
reconsider B = {{{}}} as Filter of L by FILTER_0:12,A0;
Z2: not {} in A
proof
assume {} in A; then
Bottom L in A by A0,LATTICE3:3;
hence contradiction by Z1,LOPCLSET:29,A0;
end;
A <> {{},{{}}} by Z2,TARSKI:def 2;
hence thesis by A1,lemma2,A0;
end;
begin :: On Prime and Maximal Filters and Ideals
theorem Th16:
for L being Lattice,
a being Element of L holds
{ F where F is Filter of L : F is prime & a in F } c= PFilters L
proof
let L be Lattice,
a be Element of L;
let x be object;
assume x in { F where F is Filter of L : F is prime & a in F };
then ex UF being Filter of L st UF = x & UF is prime & a in UF;
hence thesis;
end;
definition let L be Lattice;
let F be Filter of L;
attr F is maximal means
F is proper &
for G being Filter of L st G is proper & F c= G holds
F = G;
end;
registration let L be Lattice;
cluster maximal -> proper for Filter of L;
coherence;
end;
registration let L be Lattice;
cluster maximal -> being_ultrafilter for Filter of L;
coherence
proof
let F be Filter of L;
assume
a0: F is maximal;
for H being Filter of L st
F c= H & H <> the carrier of L holds F = H
proof
let H be Filter of L;
assume
A2: F c= H & H <> the carrier of L; then
H is proper by SUBSET_1:def 6;
hence thesis by a0,A2;
end;
hence thesis by a0,SUBSET_1:def 6,FILTER_0:def 3;
end;
cluster being_ultrafilter -> maximal for Filter of L;
coherence
proof
let F be Filter of L;
assume
a0: F is being_ultrafilter; then
A0: F <> the carrier of L & for H being Filter of L st
F c= H & H <> the carrier of L holds F = H by FILTER_0:def 3;
for G being Filter of L st G is proper & F c= G holds F = G
proof
let G be Filter of L;
assume
A2: G is proper & F c= G; then
G <> the carrier of L by SUBSET_1:def 6;
hence thesis by a0,A2,FILTER_0:def 3;
end;
hence thesis by A0,SUBSET_1:def 6;
end;
end;
definition let L be Lattice;
let I be Ideal of L;
attr I is maximal means
I is proper &
for J being Ideal of L st J is proper & I c= J holds I = J;
end;
theorem LemM:
for L being Lattice, I being Ideal of L holds
I is max-ideal iff I is maximal
proof
let L be Lattice, I be Ideal of L;
hereby
assume
A0: I is max-ideal; then
a2: I <> the carrier of L by FILTER_2:def 8;
for G being Ideal of L st G is proper & I c= G holds I = G
proof
let G be Ideal of L;
assume
B1: G is proper & I c= G; then
G <> the carrier of L by SUBSET_1:def 6;
hence thesis by FILTER_2:def 8,A0,B1;
end;
hence I is maximal by a2,SUBSET_1:def 6;
end;
assume
A0: I is maximal;
for J being Ideal of L st I c= J & J <> the carrier of L holds I = J
proof
let J be Ideal of L;
assume
B1: I c= J & J <> the carrier of L; then
J is proper by SUBSET_1:def 6;
hence thesis by A0,B1;
end;
hence thesis by A0,FILTER_2:def 8,SUBSET_1:def 6;
end;
registration let L be Lattice;
cluster maximal -> max-ideal for Ideal of L;
coherence by LemM;
cluster max-ideal -> maximal for Ideal of L;
coherence by LemM;
end;
registration let L be Lattice;
cluster maximal -> proper for Ideal of L;
coherence;
end;
theorem Lem1:
for L being Lattice,
F being Filter of L st F is not prime holds
ex a, b being Element of L st
a "\/" b in F & not a in F & not b in F
proof
let L be Lattice,
F be Filter of L;
assume F is not prime; then
consider a, b being Element of L such that
Z1: not (a "\/" b in F iff a in F or b in F) by FILTER_0:def 5;
now assume not a "\/" b in F & (a in F or b in F); then
per cases;
suppose not a "\/" b in F & a in F;
hence contradiction by FILTER_0:10;
end;
suppose not a "\/" b in F & b in F;
hence contradiction by FILTER_0:10;
end;
end;
hence thesis by Z1;
end;
theorem Lem2:
for L being Lattice,
F being Ideal of L st F is not prime holds
ex a, b being Element of L st
a "/\" b in F & not a in F & not b in F
proof
let L be Lattice,
F be Ideal of L;
assume F is not prime; then
consider a, b being Element of L such that
Z1: not (a "/\" b in F iff a in F or b in F) by FILTER_2:def 10;
now assume not a "/\" b in F & (a in F or b in F); then
per cases;
suppose not a "/\" b in F & a in F;
hence contradiction by FILTER_2:22;
end;
suppose not a "/\" b in F & b in F;
hence contradiction by FILTER_2:22;
end;
end;
hence thesis by Z1;
end;
theorem HelpMaxPrime:
for L be Lattice,
F be Filter of L,
a be Element of L,
G be set st
G = { x where x is Element of L : ex u being Element of L st
u in F & a "/\" u [= x } & a in G holds
G is Filter of L
proof
let L be Lattice;
let F be Filter of L;
let a be Element of L;
let G be set;
assume
A1: G = { x where x is Element of L : ex u being Element of L st
u in F & a "/\" u [= x } & a in G;
G c= the carrier of L
proof
let y be object;
assume y in G; then
consider x being Element of L such that
S2: y = x & ex u being Element of L st u in F & a "/\" u [= x by A1;
thus thesis by S2;
end; then
reconsider G1 = G as Subset of L;
set u = the Element of F;
ZD: G1 is meet-closed
proof
let p,q be Element of L;
assume
P0: p in G1 & q in G1; then
consider xx being Element of L such that
P1: xx = p & ex u being Element of L st u in F & a "/\" u [= xx by A1;
consider u1 being Element of L such that
P3: u1 in F & a "/\" u1 [= p by P1;
consider yy being Element of L such that
P2: yy = q & ex u being Element of L st u in F & a "/\" u [= yy
by P0,A1;
consider u2 being Element of L such that
P4: u2 in F & a "/\" u2 [= q by P2;
P6: (a "/\" u1) "/\" (a "/\" u2) [= p "/\" q by P3,P4,FILTER_0:5;
P7: u1 "/\" u2 in F by P3,P4,FILTER_0:8;
(a "/\" u1) "/\" (a "/\" u2) = a "/\" u1 "/\" a "/\" u2
by LATTICES:def 7
.= (a "/\" a) "/\" u1 "/\" u2 by LATTICES:def 7
.= a "/\" (u1 "/\" u2) by LATTICES:def 7;
hence thesis by P7,P6,A1;
end;
G1 is final
proof
let p, q be Element of L;
assume
Y0: p [= q & p in G1; then
consider s being Element of L such that
Y1: s = p & ex u being Element of L st
u in F & a "/\" u [= s by A1;
consider u being Element of L such that
Y2: u in F & a "/\" u [= s by Y1;
a "/\" u [= q by Y2,Y0,Y1,LATTICES:7;
hence thesis by Y2,A1;
end;
hence thesis by A1,ZD;
end;
theorem HelpMaxPrime2:
for L be Lattice,
F be Ideal of L,
a be Element of L,
G be set st
G = { x where x is Element of L : ex u being Element of L st
u in F & x [= a "\/" u } & a in G holds
G is Ideal of L
proof
let L be Lattice;
let F be Ideal of L;
let a be Element of L;
let G be set;
assume
A1: G = { x where x is Element of L : ex u being Element of L st
u in F & x [= a "\/" u } & a in G;
G c= the carrier of L
proof
let y be object;
assume y in G; then
consider x being Element of L such that
S2: y = x & ex u being Element of L st u in F & x [= a "\/" u by A1;
thus thesis by S2;
end; then
reconsider G as Subset of L;
set u = the Element of F;
ZD: G is join-closed
proof
let p,q be Element of L;
assume
P0: p in G & q in G; then
consider xx being Element of L such that
P1: xx = p & ex u being Element of L st u in F & xx [= a "\/" u by A1;
consider u1 being Element of L such that
P3: u1 in F & p [= a "\/" u1 by P1;
consider yy being Element of L such that
P2: yy = q & ex u being Element of L st u in F & yy [= a "\/" u by P0,A1;
consider u2 being Element of L such that
P4: u2 in F & q [= a "\/" u2 by P2;
P6: p "\/" q [= (a "\/" u1) "\/" (a "\/" u2) by P3,P4,FILTER_0:4;
P7: u1 "\/" u2 in F by P3,P4,FILTER_2:86;
(a "\/" u1) "\/" (a "\/" u2) = a "\/" u1 "\/" a "\/" u2
by LATTICES:def 5
.= (a "\/" a) "\/" u1 "\/" u2 by LATTICES:def 5
.= a "\/" (u1 "\/" u2) by LATTICES:def 5;
hence thesis by P7,P6,A1;
end;
G is initial
proof
let p, q be Element of L;
assume
Y0: p [= q & q in G; then
consider s being Element of L such that
Y1: s = q & ex u being Element of L st
u in F & s [= a "\/" u by A1;
consider u being Element of L such that
Y2: u in F & s [= a "\/" u by Y1;
p [= a "\/" u by Y2,Y0,Y1,LATTICES:7;
hence thesis by Y2,A1;
end;
hence thesis by ZD,A1;
end;
theorem MaxPrime:
for L being distributive Lattice,
F being Filter of L st
F is maximal holds F is prime
proof
let L be distributive Lattice,
F be Filter of L;
assume
a5: F is maximal;
assume F is not prime; then
consider a, b being Element of L such that
S1: a "\/" b in F & not a in F & not b in F by Lem1;
set G = { x where x is Element of L : ex u being Element of L st
u in F & a "/\" u [= x };
set u = the Element of F;
a "/\" u [= a by LATTICES:6; then
ZE: a in G; then
reconsider G as Filter of L by HelpMaxPrime;
HH: not b in G
proof
assume b in G; then
consider x being Element of L such that
J1: x = b & ex m being Element of L st
m in F & a "/\" m [= x;
consider c being Element of L such that
J2: c in F & a "/\" c [= b by J1;
c "\/" b in F by J2,FILTER_0:10; then
(a "\/" b) "/\" (c "\/" b) in F by FILTER_0:8,S1; then
(a "/\" c) "\/" b in F by LATTICES:11;
hence thesis by S1,J2;
end;
H1: F c= G
proof
let v be object;
assume
H2: v in F; then
reconsider vv = v as Element of L;
a "/\" vv [= vv by LATTICES:6;
hence thesis by H2;
end;
G <> the carrier of L by HH; then
G is proper by SUBSET_1:def 6;
hence thesis by H1,a5,ZE,S1;
end;
registration let L be distributive Lattice;
cluster maximal -> prime for Filter of L;
coherence by MaxPrime;
end;
theorem MaxIPrime:
for L being distributive Lattice,
F being Ideal of L st
F is maximal holds F is prime
proof
let L be distributive Lattice,
F be Ideal of L;
assume
a5: F is maximal;
assume F is not prime; then
consider a, b being Element of L such that
S1: a "/\" b in F & not a in F & not b in F by Lem2;
set G = { x where x is Element of L : ex u being Element of L st
u in F & x [= a "\/" u };
G c= the carrier of L
proof
let y be object; assume y in G; then
consider x being Element of L such that
S2: y = x & ex u being Element of L st u in F & x [= a "\/" u;
thus thesis by S2;
end; then
reconsider G as Subset of L;
set u = the Element of F;
a [= a "\/" u by LATTICES:5; then
ze: a in G;
reconsider G as Ideal of L by HelpMaxPrime2,ze;
HH: not b in G
proof
assume b in G; then
consider x being Element of L such that
J1: x = b & ex m being Element of L st
m in F & x [= a "\/" m;
consider c being Element of L such that
J2: c in F & b [= a "\/" c by J1;
c "/\" b in F by J2,FILTER_2:22; then
(a "/\" b) "\/" (c "/\" b) in F by FILTER_2:21,S1; then
(a "\/" c) "/\" b in F by LATTICES:def 11;
hence thesis by S1,J2,LATTICES:4;
end;
H1: F c= G
proof
let v be object;
assume
H2: v in F; then
reconsider vv = v as Element of L;
vv [= a "\/" vv by LATTICES:5;
hence thesis by H2;
end;
G <> the carrier of L by HH; then
G is proper by SUBSET_1:def 6;
hence thesis by H1,a5,S1,ze;
end;
registration let L be distributive Lattice;
cluster maximal -> prime for Ideal of L;
coherence by MaxIPrime;
end;
begin :: Prime Ideal Theorem for Distributive Lattices
::$N Prime ideal theorem for distributive lattices
theorem Th15: :: Theorem 15, p. 64, Gratzer
for L being distributive Lattice,
I being Ideal of L,
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
proof
let L be distributive Lattice,
I be Ideal of L,
F be Filter of L;
assume
A1: I misses F;
set X = { i where i is Ideal of L : I c= i & i misses F };
z1: I in X by A1;
for Z being set st Z <> {} & Z c= X & Z is c=-linear holds union Z in X
proof
let Z be set;
assume
s1: Z <> {} & Z c= X & Z is c=-linear;
BB: for x being object st x in Z holds x is Ideal of L
proof
let x be object;
assume x in Z; then
x in X by s1; then
consider i being Ideal of L such that
SO: i = x & I c= i & i misses F;
thus thesis by SO;
end;
set M = union Z;
consider f being object such that
K1: f in Z by s1,XBOOLE_0:def 1;
reconsider f as set by TARSKI:1;
UU: M c= the carrier of L
proof
let x be object;
assume x in M; then
consider g being set such that
U1: x in g & g in Z by TARSKI:def 4;
g is Ideal of L by U1, BB;
hence thesis by U1;
end;
f in X by K1,s1; then
consider j being Ideal of L such that
SF: f = j & I c= j & j misses F;
f c= M by K1,ZFMISC_1:74; then
reconsider M as non empty Subset of L by SF,UU;
H0: now let a, b be Element of L;
assume
S1: a in M & b in M; then
consider W being set such that
S2: a in W & W in Z by TARSKI:def 4;
consider V being set such that
S3: b in V & V in Z by S1,TARSKI:def 4;
H1: V is Ideal of L by S3,BB;
h1: W is Ideal of L by S2,BB;
W, V are_c=-comparable by s1,S2,S3,ORDINAL1:def 8; then
per cases;
suppose W c= V; then
H2: a "\/" b in V by FILTER_2:21,H1,S2,S3;
V c= M by ZFMISC_1:74,S3;
thus then a "\/" b in M by H2;
end;
suppose V c= W; then
H2: a "\/" b in W by FILTER_2:21,h1,S2,S3;
W c= M by ZFMISC_1:74,S2;
thus then a "\/" b in M by H2;
end;
end;
for p,q being Element of L st p in M & q [= p holds q in M
proof
let p, q be Element of L;
assume
J0: p in M & q [= p; then
consider W being set such that
J1: p in W & W in Z by TARSKI:def 4;
W is Ideal of L by J1,BB; then
q in W by FILTER_2:21,J0,J1;
hence q in M by TARSKI:def 4,J1;
end; then
F2: M is Ideal of L by H0,FILTER_2:21;
F1: I c= M
proof
let t be object;
assume
J1: t in I;
consider J being object such that
SS: J in Z by s1,XBOOLE_0:def 1;
J in X by SS,s1; then
consider j being Ideal of L such that
SF: j = J & I c= j & j misses F;
thus thesis by SS,TARSKI:def 4,J1,SF;
end;
M misses F
proof
assume M meets F; then
consider x being object such that
F4: x in M & x in F by XBOOLE_0:3;
reconsider x as set by TARSKI:1;
consider y being set such that
F5: x in y & y in Z by TARSKI:def 4,F4;
y in X by F5,s1; then
consider i being Ideal of L such that
F6: i = y & I c= i & i misses F;
thus thesis by F6,XBOOLE_0:3,F4,F5;
end;
hence thesis by F1,F2;
end;
then consider Y being set such that
J0: Y in X & for Z being set st Z in X & Z <> Y holds
not Y c= Z by ORDERS_1:67,z1;
consider i being Ideal of L such that
KK: Y = i & I c= i & i misses F by J0;
take i;
i is prime
proof
assume i is not prime; then
consider a, b being Element of L such that
G3: a "/\" b in i & not a in i & not b in i by Lem2;
set Ia = i "\/" (.a.>;
i c= Ia by FILTER_2:50; then
J1: I c= Ia by KK;
Ia meets F
proof
assume Ia misses F; then
Ia in X by J1; then
UI: Ia = i by FILTER_2:50,J0,KK;
(.a.> c= Ia by FILTER_2:50;
hence thesis by G3,UI,FILTER_2:28;
end; then
consider p1 being object such that
HH: p1 in Ia & p1 in F by XBOOLE_0:3;
reconsider p1 as Element of L by HH;
consider p,q being Element of L such that
h1: p1 = p "\/" q & p in i & q in (.a.> by HH;
p "\/" q [= p "\/" a by FILTER_0:1,FILTER_2:28,h1; then
p "\/" a in F by FILTER_0:9,HH,h1; then
consider p being Element of L such that
G1: p in i & p "\/" a in F by h1;
set Ib = i "\/" (.b.>;
i c= Ib by FILTER_2:50; then
J1: I c= Ib by KK;
Ib meets F
proof
assume Ib misses F; then
Ib in X by J1; then
UI: Ib = i by FILTER_2:50,J0,KK;
(.b.> c= Ib by FILTER_2:50;
hence thesis by G3,UI,FILTER_2:28;
end; then
consider p1 being object such that
HH: p1 in Ib & p1 in F by XBOOLE_0:3;
reconsider p1 as Element of L by HH;
consider P,Q being Element of L such that
h1: p1 = P "\/" Q & P in i & Q in (.b.> by HH;
P "\/" Q [= P "\/" b by FILTER_0:1,FILTER_2:28,h1; then
P "\/" b in F by FILTER_0:9,HH,h1; then
consider q being Element of L such that
G2: q in i & q "\/" b in F by h1;
set y = (p "\/" a) "/\" (q "\/" b);
Z1: y in F by G1,G2,FILTER_0:8;
ZZ: y = ((p "\/" a) "/\" q) "\/" ((p "\/" a) "/\" b) by LATTICES:def 11
.= ((p "/\" q) "\/" (a "/\" q)) "\/" ((p "\/" a) "/\" b)
by LATTICES:def 11
.= ((p "/\" q) "\/" (a "/\" q)) "\/" ((p "/\" b) "\/" (a "/\" b))
by LATTICES:def 11
.= ((p "/\" q) "\/" (a "/\" q)) "\/" (p "/\" b) "\/" (a "/\" b)
by LATTICES:def 5
.= (p "/\" q) "\/" (p "/\" b) "\/" (a "/\" q) "\/" (a "/\" b)
by LATTICES:def 5;
set x = (p "/\" q) "\/" (p "/\" b) "\/" (a "/\" q) "\/" (a "/\" b);
G4: p "/\" q in i by G2,FILTER_2:22;
G5: p "/\" b in i by G1,FILTER_2:22;
G6: a "/\" q in i by G2,FILTER_2:22;
(p "/\" q) "\/" (p "/\" b) in i by G4,G5,FILTER_2:21; then
(p "/\" q) "\/" (p "/\" b) "\/" (a "/\" q) in i by G6,FILTER_2:21;
then x in i by FILTER_2:21,G3;
hence thesis by KK,XBOOLE_0:3,Z1,ZZ;
end;
hence thesis by KK;
end;
theorem Cor16:
for L being distributive Lattice,
I being Ideal of L,
a being Element of L st not a in I
ex P being Ideal of L st P is prime & I c= P & not a in P
proof
let L be distributive Lattice,
I be Ideal of L,
a be Element of L;
assume
A0: not a in I;
set F = <.a.);
A2: a in F;
I misses F
proof
assume I meets F; then
consider x being object such that
A1: x in I & x in F by XBOOLE_0:3;
reconsider x as Element of L by A1;
a [= x by A1,FILTER_0:15;
hence thesis by A0,FILTER_2:21,A1;
end; then
consider P being Ideal of L such that
T1: P is prime & I c= P & P misses F by Th15;
not a in P by A2,T1,XBOOLE_0:3;
hence thesis by T1;
end;
theorem
for L being distributive Lattice,
a, b being Element of L st a <> b holds
ex P being Ideal of L st P is prime &
(a in P & not b in P) or (not a in P & b in P)
proof
let L be distributive Lattice,
a, b be Element of L;
assume
AA: a <> b;
ZZ: (.a.> misses <.b.) or <.a.) misses (.b.>
proof
assume
A0: (.a.> meets <.b.) &
<.a.) meets (.b.>; then
consider x being object such that
A1: x in (.a.> & x in <.b.) by XBOOLE_0:3;
consider y being object such that
A2: y in (.b.> & y in <.a.) by A0,XBOOLE_0:3;
reconsider x,y as Element of L by A1,A2;
A3: x [= a by A1,FILTER_2:28;
b [= x by A1,FILTER_0:15; then
A5: b [= a by A3,LATTICES:7;
A4: y [= b by A2,FILTER_2:28;
a [= y by A2,FILTER_0:15; then
a [= b by A4,LATTICES:7;
hence thesis by AA,A5,LATTICES:8;
end;
set I = (.a.>, F = <.b.);
set I1 = (.b.>, F1 = <.a.);
per cases by ZZ;
suppose I misses F; then
consider P being Ideal of L such that
B1: P is prime & I c= P & P misses F by Th15;
B2: a in P by B1,FILTER_2:28;
b in F; then
not b in P by B1,XBOOLE_0:3;
hence thesis by B1,B2;
end;
suppose I1 misses F1; then
consider P being Ideal of L such that
B1: P is prime & I1 c= P & P misses F1 by Th15;
B2: b in P by B1,FILTER_2:28;
a in F1; then
not a in P by B1,XBOOLE_0:3;
hence thesis by B2;
end;
end;
theorem
for L being distributive Lattice,
a, b being Element of L st not a [= b holds
ex P being Ideal of L st P is prime & not a in P & b in P
proof
let L be distributive Lattice,
a, b be Element of L;
assume
AA: not a [= b;
ZZ: <.a.) misses (.b.>
proof
assume <.a.) meets (.b.>; then
consider y being object such that
A2: y in (.b.> & y in <.a.) by XBOOLE_0:3;
reconsider y as Element of L by A2;
A4: y [= b by A2,FILTER_2:28;
a [= y by A2,FILTER_0:15;
hence thesis by AA,A4,LATTICES:7;
end;
set I1 = (.b.>, F1 = <.a.);
consider P being Ideal of L such that
B1: P is prime & I1 c= P & P misses F1 by Th15,ZZ;
B2: b in P by B1,FILTER_2:28;
a in F1; then
not a in P by B1,XBOOLE_0:3;
hence thesis by B1,B2;
end;
theorem
for L being distributive Lattice,
I being Ideal of L holds
I = meet { P where P is Ideal of L : P is prime & I c= P }
proof
let L be distributive Lattice,
I be Ideal of L;
X1: [#]L is prime
proof
set II = [#]L;
for p, q being Element of L holds
p "/\" q in II iff p in II or q in II;
hence thesis by FILTER_2:def 10;
end;
set P = [#]L;
set X = { P where P is Ideal of L : P is prime & I c= P };
set I1 = meet X;
k1: P in X by X1;
set x = the Element of X;
meet X c= the carrier of L by k1,SETFAM_1:def 1; then
reconsider I2 = I1 as Subset of L;
assume I1 <> I; then
per cases;
suppose not I1 c= I; then
consider a being object such that
A1: a in I1 & not a in I;
a in I2 by A1; then
reconsider a as Element of L;
consider P being Ideal of L such that
A2: P is prime & I c= P & not a in P by Cor16,A1;
P in X by A2; then
I1 c= P by SETFAM_1:3;
hence thesis by A1,A2;
end;
suppose not I c= I1; then
consider a being object such that
A1: a in I & not a in I1;
consider Y being set such that
X4: Y in X & not a in Y by SETFAM_1:def 1,A1,k1;
consider P1 being Ideal of L such that
X5: Y = P1 & P1 is prime & I c= P1 by X4;
thus thesis by A1,X4,X5;
end;
end;
begin :: The Stone Representation
definition
let L be Lattice;
func PrimeFilters L -> Function means :Def6:
dom it = the carrier of L &
for a being Element of L holds
it.a = { F where F is Filter of L : F is prime & a in F };
existence
proof
deffunc U(object) = { F where F is Filter of L : F is prime & $1 in F};
consider f being Function such that
A1: dom f = the carrier of L and
A2: for x being object st x in the carrier of L
holds f.x = U(x) from FUNCT_1:sch 3;
take f;
thus thesis by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function;
assume that
A3: dom f1 = the carrier of L &
for a being Element of L
holds f1.a = { F where F is Filter of L : F is prime & a in F } and
A4: dom f2 = the carrier of L &
for a being Element of L
holds f2.a = { F where F is Filter of L : F is prime & a in F };
now
let x be object;
assume x in the carrier of L;
then reconsider a = x as Element of L;
thus f1.x = {F where F is Filter of L : F is prime & a in F } by A3
.= f2.x by A4;
end;
hence thesis by A3,A4,FUNCT_1:2;
end;
end;
theorem Th17:
for L being Lattice,
a being Element of L,
x being set holds
x in PrimeFilters L.a iff ex F being Filter of L st
F = x & F is prime & a in F
proof
let L be Lattice,
a be Element of L, x be set;
thus x in PrimeFilters L.a implies ex F being Filter of L st
F = x & F is prime & a in F
proof
assume x in PrimeFilters L.a;
then x in { F1 where F1 is Filter of L : F1 is prime & a in F1 }
by Def6;
then consider F being Filter of L such that
A2: F = x and
A3: F is prime and
A4: a in F;
take F;
thus thesis by A2,A3,A4;
end;
assume ex F being Filter of L st F = x & F is prime & a in F;
then x in { F where F is Filter of L : F is prime & a in F };
hence thesis by Def6;
end;
theorem
for L being Lattice,
a being Element of L,
F being Filter of L holds
F in PrimeFilters L.a iff F is prime & a in F
proof
let L be Lattice,
a be Element of L,
F be Filter of L;
hereby
assume F in PrimeFilters L.a;
then ex F0 being Filter of L st
F0 = F & F0 is prime & a in F0 by Th17;
hence F is prime & a in F;
end;
thus thesis by Th17;
end;
theorem
for L being distributive Lattice,
a, b being Element of L holds
PrimeFilters L.(a "/\" b) = PrimeFilters L.a /\ PrimeFilters L.b
proof
let L be distributive Lattice,
a, b be Element of L;
A1: PrimeFilters L.(a "/\" b) c= PrimeFilters L.a /\ PrimeFilters L.b
proof
let x be object;
set c = a "/\" b;
assume x in PrimeFilters L.c;
then consider F0 being Filter of L such that
A2: x = F0 and
A3: F0 is prime and
A4: c in F0 by Th17;
A5: a in F0 by A4,FILTER_0:8;
A6: b in F0 by A4,FILTER_0:8;
A7: F0 in PrimeFilters L.a by A3,A5,Th17;
F0 in PrimeFilters L.b by A3,A6,Th17;
hence thesis by A2,A7,XBOOLE_0:def 4;
end;
PrimeFilters L.a /\ PrimeFilters L.b c= PrimeFilters L.(a "/\" b)
proof
let x be object;
assume
A8: x in PrimeFilters L.a /\ PrimeFilters L.b; then
A9: x in PrimeFilters L.a by XBOOLE_0:def 4;
A10: x in PrimeFilters L.b by A8,XBOOLE_0:def 4;
A11: ex F0 being Filter of L st x = F0 & F0 is prime & a in F0 by A9,Th17;
ex F0 being Filter of L st x = F0 & F0 is prime & b in F0 by A10,Th17;
then consider F0 being Filter of L such that
A12: x = F0 and
A13: F0 is prime and
A14: a in F0 and
A15: b in F0 by A11;
a "/\" b in F0 by A14,A15,FILTER_0:8;
hence thesis by A12,A13,Th17;
end;
hence thesis by A1;
end;
theorem
for L being distributive Lattice,
a, b being Element of L holds
PrimeFilters L.(a "\/" b) = PrimeFilters L.a \/ PrimeFilters L.b
proof
let L be distributive Lattice,
a, b be Element of L;
A1: PrimeFilters L.(a "\/" b) c= PrimeFilters L.a \/ PrimeFilters L.b
proof
let x be object;
set c = a "\/" b;
assume x in PrimeFilters L.c;
then consider F0 being Filter of L such that
A2: x = F0 and
A3: F0 is prime and
A4: c in F0 by Th17;
a in F0 or b in F0 by A3,A4,FILTER_0:def 5;
then F0 in PrimeFilters L.a or F0 in PrimeFilters L.b by A3,Th17;
hence thesis by A2,XBOOLE_0:def 3;
end;
PrimeFilters L.a \/ PrimeFilters L.b c= PrimeFilters L.(a "\/" b)
proof
let x be object;
assume x in PrimeFilters L.a \/ PrimeFilters L.b;
then x in PrimeFilters L.a or x in PrimeFilters L.b by XBOOLE_0:def 3;
then ( ex F0 being Filter of L st x = F0 & F0 is prime & a in F0 ) or
ex F0 being Filter of L st x = F0 & F0 is prime & b in F0 by Th17;
then consider F0 being Filter of L such that
A5: x = F0 and
A6: F0 is prime and
A7: a in F0 or b in F0;
a "\/" b in F0 by A6,A7,FILTER_0:def 5;
hence thesis by A5,A6,Th17;
end;
hence thesis by A1;
end;
definition let L be distributive Lattice;
redefine func PrimeFilters L -> :: redefines PrimeFilters (LATTICEA, definition)
Function of the carrier of L, bool PFilters L;
coherence
proof
reconsider f = PrimeFilters L as Function;
A1: dom f = the carrier of L by Def6;
rng f c= bool PFilters L
proof
let y be object;
reconsider yy = y as set by TARSKI:1;
assume y in rng f;
then consider x being object such that
A2: x in dom f and
A3: y = f.x by FUNCT_1:def 3;
y = { F where F is Filter of L : F is prime & x in F }
by A1,A2,A3,Def6;
then yy c= PFilters L by A1,A2,Th16;
hence thesis;
end;
then reconsider f as Function of the carrier of L, bool PFilters L
by A1,FUNCT_2:def 1,RELSET_1:4;
for a being Element of L holds
f.a = { F where F is Filter of L : F is prime & a in F } by Def6;
hence thesis;
end;
end;
definition let L be distributive Lattice;
func StoneR L -> set equals
rng PrimeFilters L;
coherence;
end;
registration let L be distributive Lattice;
cluster StoneR L -> non empty;
coherence;
end;
theorem Th23:
for L being distributive Lattice,
x being set holds
x in StoneR L iff ex a being Element of L st (PrimeFilters L).a = x
proof
let L be distributive Lattice,
x be set;
thus x in StoneR L implies ex a being Element of L st
(PrimeFilters L).a = x
proof
assume x in StoneR L;
then consider y being object such that
A2: y in dom PrimeFilters L and
A3: x = PrimeFilters L.y by FUNCT_1:def 3;
reconsider a = y as Element of L by A2;
take a;
thus thesis by A3;
end;
given a being Element of L such that
A4: x = PrimeFilters L.a;
a in the carrier of L;
then a in dom PrimeFilters L by Def6;
hence thesis by A4,FUNCT_1:def 3;
end;
definition let L be upper-bounded distributive Lattice;
func StoneSpace L -> strict TopSpace means :StoneDef:
the carrier of it = PFilters L &
the topology of it =
{ union A where A is Subset-Family of PFilters L : A c= StoneR L };
existence
proof
set US = PFilters L;
set STP = { union A where A is Subset-Family of PFilters L :
A c= StoneR L };
STP c= bool US
proof
let x be object;
assume x in STP;
then ex B being Subset-Family of PFilters L st
x = union B & B c= StoneR L;
hence thesis;
end;
then reconsider STP = {union A where A is Subset-Family of PFilters L :
A c= StoneR L } as Subset-Family of US;
TopStruct(# US,STP#) is strict TopSpace
proof
set TS = TopStruct(# US,STP#);
A1: the carrier of TS in the topology of TS
proof
set B = { F where F is Filter of L : F is prime & Top L in F };
B c= PFilters L
proof
let x be object;
assume x in B;
then ex F being Filter of L st F = x & F is prime & Top L in F;
hence thesis;
end; then
A2: bool B c= bool PFilters L by ZFMISC_1:67;
{B} c= bool B by ZFMISC_1:68;
then reconsider SB = {B} as
Subset-Family of PFilters L by A2,XBOOLE_1:1;
reconsider SB as Subset-Family of PFilters L;
PFilters L c= B
proof
let x be object;
assume x in PFilters L;
then consider F being Filter of L such that
A4: F = x and
A5: F is prime;
Top L in F by FILTER_0:11;
hence thesis by A4,A5;
end; then
A6: PFilters L = union SB by ZFMISC_1:25;
(PrimeFilters L).Top L = { F where F is Filter of L
: F is prime & Top L in F } by Def6;
then SB c= StoneR L by ZFMISC_1:31,Th23;
hence thesis by A6;
end;
A7: for a being Subset-Family of TS
st a c= the topology of TS holds union a in the topology of TS
proof
let a be Subset-Family of TS;
assume
A8: a c= the topology of TS;
set B = { A where A is Subset of StoneR L : union A in a };
B c= bool StoneR L
proof
let x be object;
assume x in B;
then ex C being Subset of StoneR L st C = x & union C in a;
then reconsider C = x as Subset of StoneR L;
C c= StoneR L;
hence thesis;
end;
then reconsider BS = B as Subset-Family of StoneR L;
A9: union union BS = union
{ union A where A is Subset of StoneR L : A in BS } by EQREL_1:54;
A10: a c= { union A where A is Subset of StoneR L : A in BS }
proof
let x be object;
assume
A11: x in a;
then x in STP by A8;
then consider C being Subset-Family of PFilters L such that
A12: x = union C and
A13: C c= StoneR L;
C in BS by A11,A12,A13;
hence thesis by A12;
end;
{ union A where A is Subset of StoneR L : A in BS } c= a
proof
let x be object;
assume x in {union A where A is Subset of StoneR L : A in BS };
then consider C being Subset of StoneR L such that
A14: union C = x and
A15: C in BS;
ex D being Subset of StoneR L st D = C & union D in a by A15;
hence thesis by A14;
end;
then
A16: a = { union A where A is Subset of StoneR L : A in BS } by A10;
union BS is Subset-Family of PFilters L by XBOOLE_1:1;
hence thesis by A9,A16;
end;
for p,q being Subset of TS st
p in the topology of TS & q in the topology of TS
holds p /\ q in the topology of TS
proof
let p,q be Subset of TS;
assume that
A17: p in the topology of TS and
A18: q in the topology of TS;
consider P being Subset-Family of PFilters L such that
A19: union P = p and
A20: P c= StoneR L by A17;
consider Q being Subset-Family of PFilters L such that
A21: union Q = q and
A22: Q c= StoneR L by A18;
A23: union P /\ union Q = union INTERSECTION(P,Q) by SETFAM_1:28;
INTERSECTION(P,Q) c= bool PFilters L
proof
let x be object;
assume x in INTERSECTION(P,Q);
then consider X,Y being set such that
A24: X in P and
A25: Y in Q and
A26: x = X /\ Y by SETFAM_1:def 5;
A27: X /\ Y c= X \/ Y by XBOOLE_1:29;
X \/ Y c= PFilters L by A24,A25,XBOOLE_1:8;
then X /\ Y c= PFilters L by A27;
hence thesis by A26;
end;
then reconsider C= INTERSECTION(P,Q) as Subset-Family of PFilters L;
reconsider C as Subset-Family of PFilters L;
C c= StoneR L
proof
let x be object;
assume x in C;
then consider X,Y being set such that
A28: X in P and
A29: Y in Q and
A30: x = X /\ Y by SETFAM_1:def 5;
consider a being Element of L such that
A31: X = (PrimeFilters L).a by A20,A28,Th23;
consider b being Element of L such that
A32: Y = (PrimeFilters L).b by A22,A29,Th23;
A33: X = { F where F is Filter of L : F is prime & a in F }
by A31,Def6;
A34: Y = { F where F is Filter of L : F is prime & b in F }
by A32,Def6;
A35: X /\ Y = { F where F is Filter of L : F is prime & a "/\" b in F }
proof
A36: X /\ Y c= { F where F is Filter of L :
F is prime & a "/\" b in F }
proof
let x be object;
assume
A37: x in X /\ Y; then
A38: x in X by XBOOLE_0:def 4;
A39: x in Y by A37,XBOOLE_0:def 4;
consider F1 being Filter of L such that
A40: x = F1 and
A41: F1 is prime and
A42: a in F1 by A33,A38;
ex F2 being Filter of L st x = F2 & F2 is prime & b in F2
by A34,A39;
then a "/\" b in F1 by A40,A42,FILTER_0:8;
hence thesis by A40,A41;
end;
{ F where F is Filter of L :
F is prime & a "/\" b in F } c= X /\ Y
proof
let x be object;
assume x in { F where F is Filter of L :
F is prime & a "/\" b in F };
then consider F0 being Filter of L such that
A43: x = F0 and
A44: F0 is prime and
A45: a "/\" b in F0;
a in F0 by A45,FILTER_0:8;
then consider F being Filter of L such that
A46: F = F0 and
A47: F is prime and
A48: a in F by A44;
A49: F in X by A33,A47,A48;
b in F0 by A45,FILTER_0:8;
then consider F1 being Filter of L such that
A50: F1 = F0 and
A51: F1 is prime and
A52: b in F1 by A44;
F1 in Y by A34,A51,A52;
hence thesis by A43,A46,A49,A50,XBOOLE_0:def 4;
end;
hence thesis by A36;
end;
(PrimeFilters L).(a "/\" b) = { F where F is Filter of L
: F is prime & (a "/\" b) in F } by Def6;
hence thesis by A30,A35,Th23;
end;
hence thesis by A19,A21,A23;
end;
hence thesis by A1,A7,PRE_TOPC:def 1;
end;
then reconsider TS = TopStruct (# US,STP #) as strict TopSpace;
take TS;
thus thesis;
end;
uniqueness;
end;
registration let L be non trivial upper-bounded distributive Lattice;
cluster StoneSpace L -> non empty;
coherence
proof
consider a,b being Element of L such that
A0: a in [#]L & b in [#]L & a <> b by SUBSET_1:45;
consider F being Filter of L such that
A1: F in F_primeSet L by OPENLATT:21,A0;
F_primeSet L c< PFilters L by PrimFil;
hence thesis by StoneDef,A1;
end;
end;
begin :: Pseudocomplements in Lattices
definition let L be Lattice;
let a be Element of L;
func PseudoComplements a -> Subset of L equals
{ x where x is Element of L : a "/\" x = Bottom L };
coherence
proof
set I = { x where x is Element of L : a "/\" x = Bottom L };
I c= the carrier of L
proof
let g be object;
assume g in I; then
consider x1 being Element of L such that
C1: x1 = g & a "/\" x1 = Bottom L;
thus thesis by C1;
end;
hence thesis;
end;
func PseudoCocomplements a -> Subset of L equals
{ x where x is Element of L : a "\/" x = Top L };
coherence
proof
set I = { x where x is Element of L : a "\/" x = Top L };
I c= the carrier of L
proof
let g be object;
assume g in I; then
consider x1 being Element of L such that
C1: x1 = g & a "\/" x1 = Top L;
thus thesis by C1;
end;
hence thesis;
end;
end;
LemDistr:
for L being distributive Lattice,
a, x1, x2 being Element of L holds
a "\/" (x1 "/\" x2) = (a "\/" x1) "/\" (a "\/" x2)
proof
let L be distributive Lattice,
a, x1, x2 be Element of L;
for a,b,c being Element of L holds
a "/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c) by LATTICES:def 11;
hence thesis by LATTICES:3;
end;
registration let L be distributive bounded Lattice;
let a be Element of L;
cluster PseudoComplements a -> initial non empty join-closed;
coherence
proof
set I0 = PseudoComplements a;
CC: for p,q being Element of L st p [= q & q in I0 holds p in I0
proof
let p,q be Element of L;
assume
C0: p [= q & q in I0; then
consider x1 being Element of L such that
C1: x1 = q & a "/\" x1 = Bottom L;
C2: Bottom L [= a "/\" p;
a "/\" p [= a "/\" q by C0,LATTICES:9; then
a "/\" p = Bottom L by C2,LATTICES:8,C1;
hence thesis;
end;
C2: for p,q being Element of L st p in I0 & q in I0 holds p "\/" q in I0
proof
let p, q be Element of L;
assume
d0: p in I0 & q in I0; then
consider x1 being Element of L such that
d1: x1 = p & a "/\" x1 = Bottom L;
consider x2 being Element of L such that
d2: x2 = q & a "/\" x2 = Bottom L by d0;
a "/\" (x1 "\/" x2) = (a "/\" x1) "\/" (a "/\" x2) by LATTICES:def 11
.= Bottom L by d1,d2;
hence thesis by d1,d2;
end;
a "/\" Bottom L = Bottom L; then
Bottom L in I0;
hence thesis by CC,C2;
end;
cluster PseudoCocomplements a -> final non empty meet-closed;
coherence
proof
set I0 = PseudoCocomplements a;
CC: for p,q being Element of L st p [= q & p in I0 holds q in I0
proof
let p,q be Element of L;
assume
C0: p [= q & p in I0; then
consider x1 being Element of L such that
C1: x1 = p & a "\/" x1 = Top L;
a "\/" p [= a "\/" q by C0,FILTER_0:1;
hence thesis by C1;
end;
C2: for p,q being Element of L st p in I0 & q in I0 holds p "/\" q in I0
proof
let p, q be Element of L;
assume
d0: p in I0 & q in I0; then
consider x1 being Element of L such that
d1: x1 = p & a "\/" x1 = Top L;
consider x2 being Element of L such that
d2: x2 = q & a "\/" x2 = Top L by d0;
a "\/" (x1 "/\" x2) = (a "\/" x1) "/\" (a "\/" x2) by LemDistr
.= Top L by d1,d2;
hence thesis by d1,d2;
end;
a "\/" Top L = Top L; then
Top L in I0;
hence thesis by CC,C2;
end;
end;
theorem
for L being Lattice,
a,b being Element of L holds
b in PseudoComplements a iff b "/\" a = Bottom L
proof
let L be Lattice,
a,b be Element of L;
hereby assume
b in PseudoComplements a; then
consider x being Element of L such that
A1: b = x & a "/\" x = Bottom L;
thus b "/\" a = Bottom L by A1;
end;
assume b "/\" a = Bottom L;
hence thesis;
end;
theorem
for L being Lattice,
a,b being Element of L holds
b in PseudoCocomplements a iff b "\/" a = Top L
proof
let L be Lattice,
a,b be Element of L;
hereby assume
b in PseudoCocomplements a; then
consider x being Element of L such that
A1: b = x & a "\/" x = Top L;
thus b "\/" a = Top L by A1;
end;
assume b "\/" a = Top L;
hence thesis;
end;
theorem
for L being bounded Lattice,
a being Element of L holds
Bottom L in PseudoComplements a
proof
let L be bounded Lattice,
a be Element of L;
a "/\" Bottom L = Bottom L;
hence thesis;
end;
theorem
for L being bounded Lattice,
a being Element of L holds
Top L in PseudoCocomplements a
proof
let L be bounded Lattice,
a be Element of L;
a "\/" Top L = Top L;
hence thesis;
end;
begin :: Nachbin Theorems
definition let L be Lattice;
func Spectrum L -> Subset-Family of L equals
{ I where I is Ideal of L : I is prime proper };
coherence
proof
set US = { F where F is Ideal of L : F is prime proper };
US c= bool the carrier of L
proof
let x be object;
assume x in US;
then ex UF being Ideal of L st UF = x & UF is prime proper;
hence thesis;
end;
hence thesis;
end;
end;
::$N Nachbin's theorem for bounded distributive lattices
theorem
for L being distributive bounded Lattice holds
L is Boolean iff
for I being Ideal of L st I is proper prime holds I is maximal
proof
let L be distributive bounded Lattice;
thus L is Boolean implies
for I being Ideal of L st I is proper prime holds I is maximal
proof
assume
YY: L is Boolean;
let I be Ideal of L;
assume
Y0: I is proper prime;
for G being Ideal of L st G is proper & I c= G holds I = G
proof
let G be Ideal of L;
assume
y1: G is proper & I c= G; then
y3: G <> the carrier of L by SUBSET_1:def 6; then
I <> (.L.> by y1; then
I is max-ideal by Y0,FILTER_2:57,YY;
hence thesis by FILTER_2:def 8,y1,y3;
end;
hence I is maximal by Y0;
end;
assume
A1: for I being Ideal of L st I is proper prime holds I is maximal;
assume L is not Boolean; then
L is not complemented; then
consider a being Element of L such that
A2: not ex b being Element of L st b is_a_complement_of a;
set I0 = PseudoComplements a;
reconsider I0 as Ideal of L;
a "/\" Bottom L = Bottom L; then
C2: Bottom L in I0;
set I1 = { x where x is Element of L :
ex y being Element of L st y in I0 & x [= a "\/" y };
I1 c= the carrier of L
proof
let g be object;
assume g in I1; then
consider x1 being Element of L such that
C1: x1 = g & ex y being Element of L st y in I0 & x1 [= a "\/" y;
thus thesis by C1;
end; then
reconsider I1 as Subset of L;
for p,q being Element of L st p [= q & q in I1 holds p in I1
proof
let p,q be Element of L;
assume
C0: p [= q & q in I1; then
consider x1 being Element of L such that
C1: x1 = q & ex y being Element of L st y in I0 & x1 [= a "\/" y;
consider y being Element of L such that
CC: y in I0 & x1 [= a "\/" y by C1;
p [= a "\/" y by C1,C0,LATTICES:7,CC;
hence thesis by CC;
end; then
C1: I1 is initial;
for p,q being Element of L st p in I1 & q in I1 holds p "\/" q in I1
proof
let p, q be Element of L;
assume
d0: p in I1 & q in I1; then
consider x1 being Element of L such that
d1: x1 = p & ex y being Element of L st y in I0 & x1 [= a "\/" y;
consider y1 being Element of L such that
e1: y1 in I0 & x1 [= a "\/" y1 by d1;
consider x2 being Element of L such that
d2: x2 = q & ex y being Element of L st y in I0 & x2 [= a "\/" y by d0;
consider y2 being Element of L such that
e2: y2 in I0 & x2 [= a "\/" y2 by d2;
HH: y1 "\/" y2 in I0 by LATTICES:def 25,e1,e2;
FF: (a "\/" y1) "\/" (a "\/" y2) =
((a "\/" y1) "\/" a) "\/" y2 by LATTICES:def 5
.= ((a "\/" a) "\/" y1) "\/" y2 by LATTICES:def 5
.= a "\/" (y1 "\/" y2) by LATTICES:def 5;
x1 "\/" x2 [= (a "\/" y1) "\/" (a "\/" y2) by FILTER_0:4,e1,e2;
hence thesis by HH,d1,d2,FF;
end; then
CC: I1 is join-closed;
a [= a "\/" Bottom L; then
ZZ: a in I1 by C2; then
reconsider I1 as Ideal of L by C1,CC;
q1: I0 c= I1
proof
let t be object;
assume
C0: t in I0; then
consider x1 being Element of L such that
C1: x1 = t & a "/\" x1 = Bottom L;
x1 [= a "\/" x1 by LATTICES:5;
hence thesis by C1,C0;
end;
J1: not Top L in I1
proof
assume Top L in I1; then
consider x1 being Element of L such that
D1: x1 = Top L &
ex y being Element of L st y in I0 & x1 [= a "\/" y;
consider y being Element of L such that
D2: y in I0 & Top L [= a "\/" y by D1;
consider x2 being Element of L such that
C1: x2 = y & a "/\" x2 = Bottom L by D2;
y is_a_complement_of a by C1,D2;
hence thesis by A2;
end;
set FF = <.Top L.);
FF = [# Top L,Top L #] by FILTER_2:65; then
J2: FF = { Top L } by FILTER_2:64; then
FF misses I1 by J1,ZFMISC_1:50; then
consider J0 being Ideal of L such that
B1: J0 is prime & I1 c= J0 & J0 misses FF by Th15;
S4: J0 <> the carrier of L by B1,ZFMISC_1:48,J2;
set T = the carrier of L;
reconsider D = T \ J0 as non empty Subset of L by S4,XBOOLE_1:37;
for p,q being Element of L st p [= q & p in D holds q in D
proof
let p,q be Element of L;
assume
k0: p [= q & p in D; then
p in T & not p in J0 by XBOOLE_0:def 5; then
not q in J0 by k0,FILTER_2:21;
hence thesis by XBOOLE_0:def 5;
end; then
j1: D is final;
for p,q being Element of L st p in D & q in D holds p "/\" q in D
proof
let p,q be Element of L;
assume p in D & q in D; then
p in T & not p in J0 & q in T & not q in J0 by XBOOLE_0:def 5; then
not p "/\" q in J0 by FILTER_2:def 10,B1;
hence thesis by XBOOLE_0:def 5;
end; then
zc: D is meet-closed;
reconsider F = <.<.a.) \/ D .) as Filter of L;
a in <.a.); then
H1: a in <.a.) \/ D by XBOOLE_0:def 3;
h2: D \/ <.a.) c= F by FILTER_0:def 4;
G1: not T c= J0 by B1,ZFMISC_1:48,J2; then
G2: T \ J0 <> {} by XBOOLE_1:37;
D c= D \/ <.a.) by XBOOLE_1:7; then
mm: D c= F by h2;
F misses I0
proof
assume F meets I0; then
consider h being object such that
H1: h in F & h in I0 by XBOOLE_0:3;
consider x1 being Element of L such that
C1: x1 = h & a "/\" x1 = Bottom L by H1;
consider b being object such that
n1: b in T \ J0 by XBOOLE_0:def 1,G2;
reconsider b as Element of L by n1;
consider bb being Element of L such that
m2: bb in D & a "/\" bb [= x1 by LATTICE4:3,zc,C1,H1,j1;
W1: bb "/\" a [= x1 & not bb in J0 by m2,XBOOLE_0:def 5;
bb "/\" a [= a by LATTICES:6; then
bb "/\" a = Bottom L by C1,BOOLEALG:9,m2,FILTER_0:7; then
bb in I0;
hence thesis by W1,B1,q1;
end; then
consider J1 being Ideal of L such that
B2: J1 is prime & I0 c= J1 & J1 misses F by Th15;
J1 <> the carrier of L by H1,h2,B2,XBOOLE_0:3; then
S1: J1 is proper by SUBSET_1:def 6;
S2: J0 is proper by G1,SUBSET_1:def 6;
S3: J1 <> J0 by B1,ZZ,h2,H1,XBOOLE_0:3,B2;
J1 c= J0
proof
let t be object;
assume
f3: t in J1; then
not t in D by mm,B2,XBOOLE_0:3;
hence thesis by f3,XBOOLE_0:def 5;
end; then
J1 is not maximal by S2,S3;
hence thesis by B2,A1,S1;
end;
registration let L be non trivial distributive bounded Lattice;
cluster Spectrum L -> non empty;
coherence
proof
set p = Bottom L;
Bottom L <> Top L by TopBot; then
consider I being Ideal of L such that
A0: p in I & I is max-ideal by FILTER_2:35;
a2: I <> the carrier of L by FILTER_2:def 8,A0;
for G being Ideal of L st G is proper & I c= G holds I = G
proof
let G be Ideal of L;
assume
B1: G is proper & I c= G; then
G <> the carrier of L by SUBSET_1:def 6;
hence thesis by FILTER_2:def 8,A0,B1;
end; then
I is maximal by a2,SUBSET_1:def 6; then
I in Spectrum L;
hence thesis;
end;
end;
::$N Nachbin theorem for spectra of distributive lattices
theorem NachSpec:
for L being distributive bounded Lattice holds
L is Boolean iff Spectrum L is unordered
proof
let L be distributive bounded Lattice;
thus L is Boolean implies Spectrum L is unordered
proof
assume L is Boolean; then
reconsider LL = L as Boolean Lattice;
assume not Spectrum L is unordered;
then consider P, Q being set such that
F1: P in Spectrum L & Q in Spectrum L & P <> Q &
P, Q are_c=-comparable;
consider P1 being Ideal of L such that
B1: P1 = P & P1 is prime proper by F1;
consider Q1 being Ideal of LL such that
b1: Q1 = Q & Q1 is prime proper by F1;
A2: now assume
f1: P c= Q; then
P c< Q by F1; then
Q \ P <> {} by XBOOLE_1:105; then
consider a being object such that
A4: a in Q \ P by XBOOLE_0:def 1;
A5: a in Q1 & not a in P1 by b1,B1,A4,XBOOLE_0:def 5; then
reconsider a as Element of LL;
Q1 <> (.LL.> by b1,SUBSET_1:def 6; then
Q1 is max-ideal by FILTER_2:57,b1; then
B2: not a` in P by f1,b1,A4,FILTER_2:58;
a "/\" a` = Bottom LL by LATTICES:20; then
a "/\" a` in P by FILTER_2:24,B1;
hence contradiction by B1,A5,B2,FILTER_2:def 10;
end;
now assume
f1: Q c= P; then
Q c< P by F1; then
P \ Q <> {} by XBOOLE_1:105; then
consider a being object such that
A4: a in P \ Q by XBOOLE_0:def 1;
A5: a in P1 & not a in Q1 by B1,b1,A4,XBOOLE_0:def 5; then
reconsider a as Element of LL;
P1 <> (.LL.> by B1,SUBSET_1:def 6; then
P1 is max-ideal by FILTER_2:57,B1; then
B2: not a` in Q by f1,B1,A4,FILTER_2:58;
a "/\" a` = Bottom LL by LATTICES:20; then
a "/\" a` in Q1 by FILTER_2:24;
hence contradiction by A5,B2,FILTER_2:def 10,b1;
end;
hence thesis by A2,F1;
end;
assume
d1: Spectrum L is unordered;
assume not L is Boolean; then
L is not complemented; then
consider a being Element of L such that
C2: not ex b being Element of L st b is_a_complement_of a;
set D = PseudoCocomplements a;
reconsider D as Filter of L;
set D1 = <.D \/ <.a.).);
II: D1 = { r where r is Element of L :
ex d,q being Element of L st d "/\" q [= r & d in D & q in <.a.) }
by FILTER_0:35;
AB: D1 c= { x where x is Element of L : ex d being Element of L st d in D &
a "/\" d [= x }
proof
let t be object;
assume t in D1; then
consider r being Element of L such that
I1: r = t &
ex d,q being Element of L st d "/\" q [= r & d in D & q in <.a.) by II;
consider d,q being Element of L such that
I2: d "/\" q [= r & d in D & q in <.a.) by I1;
a [= q by I2,FILTER_0:15; then
d "/\" a [= d "/\" q by FILTER_0:5; then
d "/\" a [= r by I2,LATTICES:7;
hence thesis by I1,I2;
end;
{ x where x is Element of L : ex d being Element of L st d in D &
a "/\" d [= x } c= D1
proof
let t be object;
assume t in { x where x is Element of L :
ex d being Element of L st d in D & a "/\" d [= x }; then
consider x1 being Element of L such that
a1: x1 = t & ex d being Element of L st d in D & a "/\" d [= x1;
consider d being Element of L such that
a2: d in D & a "/\" d [= x1 by a1;
set q = a;
d "/\" q [= x1 & q in <.a.) by a2;
hence thesis by a1,II;
end; then
Z0: D1 = { x where x is Element of L : ex d being Element of L st d in D &
a "/\" d [= x } by AB;
a "/\" (the Element of D) [= a by LATTICES:6; then
HH: a in D1 by Z0;
reconsider D1 as Filter of L;
HJ: not Bottom L in D1
proof
assume Bottom L in D1; then
consider y being Element of L such that
Z1: y = Bottom L &
ex d being Element of L st d in D & a "/\" d [= y by Z0;
consider d being Element of L such that
Z2: d in D & d "/\" a [= y by Z1;
z4: Bottom L [= d "/\" a;
consider x being Element of L such that
Z3: d = x & a "\/" x = Top L by Z2;
d is_a_complement_of a by z4,Z3,Z1,Z2,LATTICES:8;
hence thesis by C2;
end;
reconsider I0 = { Bottom L } as Ideal of L by FILTER_2:25;
consider P being Ideal of L such that
W0: P is prime & I0 c= P & P misses D1 by Th15,ZFMISC_1:50,HJ;
P <> the carrier of L by W0,XBOOLE_0:3,HH; then
w0: P is proper by SUBSET_1:def 6;
set Pa = (.P \/ (.a.>.>;
reconsider Pa as Ideal of L;
ZZ: a in (.a.>;
ZL: P c= P \/ (.a.> by XBOOLE_1:7;
ZK: (.a.> c= P \/ (.a.> by XBOOLE_1:7;
ZM: P \/ (.a.> c= Pa by FILTER_2:def 9;
kk: D c= D \/ <.a.) by XBOOLE_1:7;
D \/ <.a.) c= D1 by FILTER_0:def 4; then
hh: D c= D1 by kk;
zx: not a in P by HH,W0,XBOOLE_0:3;
not Top L in Pa
proof
assume
f2: Top L in Pa;
(.P \/ (.a.>.> = { r where r is Element of L :
ex p,q being Element of L st r [= p"\/"q & p in P & q in (.a.> }
by FILTER_2:49; then
consider r being Element of L such that
F3: r = Top L &
ex p,q being Element of L st r [= p"\/"q & p in P & q in (.a.>
by f2;
consider p,q being Element of L such that
F4: Top L [= p "\/" q & p in P & q in (.a.> by F3;
F5: Top L [= p "\/" a by FILTER_0:1,F4,FILTER_2:28;
p in { x where x is Element of L : a "\/" x = Top L } by F5;
hence thesis by hh,XBOOLE_0:3,F4,W0;
end; then
consider QQ being Ideal of L such that
W1: QQ is prime & Pa c= QQ & not Top L in QQ by Cor16;
QQ <> the carrier of L by W1; then
w1: QQ is proper by SUBSET_1:def 6;
W2: P in Spectrum L & QQ in Spectrum L by W0,W1,w1,w0;
W3: P <> QQ by zx,W1,ZM,ZZ,ZK;
P c= QQ by W1,ZL,ZM; then
P, QQ are_c=-comparable;
hence thesis by d1,W2,W3;
end;
registration let L be Boolean Lattice;
cluster Spectrum L -> unordered;
coherence by NachSpec;
end;