:: Prime Filters and Ideals in Distributive Lattices
:: by Adam Grabowski
::
:: Received October 7, 2013
:: Copyright (c) 2013-2016 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_1, FUNCT_2, FINSET_1,
FINSUB_1, STRUCT_0, LATTICES, PRE_TOPC, CARD_1, RELSET_1, TOPS_1,
LATTICE2, FILTER_2, LATTICE3, LATTICE4;
requirements BOOLE, SUBSET;
begin :: Preliminaries
definition let IT be set;
attr IT is unordered means
:: LATTICEA:def 1
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;
end;
theorem :: LATTICEA:1
for L being non trivial bounded Lattice holds
Top L <> Bottom L;
theorem :: LATTICEA:2
for L being Lattice,
I being Ideal of L holds
I is prime iff
I` is Filter of L or I` = {};
theorem :: LATTICEA:3
for L being Lattice,
F being Filter of L holds
F is prime iff
F` is Ideal of L or F` = {};
definition let L be Lattice;
func PFilters L -> Subset-Family of L equals
:: LATTICEA:def 2
{ F where F is Filter of L : F is prime };
end;
registration let L be Lattice;
cluster (.L.> -> prime;
end;
theorem :: LATTICEA:4
for L being distributive Lattice holds
F_primeSet L c< PFilters L;
begin :: Examples of Filters in Nontrivial Boolean Lattices
theorem :: LATTICEA:5
the carrier of BooleLatt {{}} = {{},{{}}};
theorem :: LATTICEA:6
for L being Lattice,
A being Subset of L
st L = BooleLatt {{}} holds
A = {} or A = {{}} or A = {{},{{}}} or A = {{{}}};
theorem :: LATTICEA:7
for L being Lattice,
A being Filter of L
st L = BooleLatt {{}} holds
A = {} or A = {{},{{}}} or A = {{{}}};
theorem :: LATTICEA:8
for L being Lattice,
A being Filter of L
st L = BooleLatt {{}} holds
A = {Top L} or A = <.L.);
theorem :: LATTICEA:9
for L being non trivial Boolean Lattice,
A being Filter of L
st L = BooleLatt {{}} & A = {Top L} holds
A is prime;
theorem :: LATTICEA:10
for L being Lattice,
A being Filter of L
st L = BooleLatt {{}} & A is being_ultrafilter holds
A = {Top L};
begin :: On Prime and Maximal Filters and Ideals
theorem :: LATTICEA:11
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;
definition let L be Lattice;
let F be Filter of L;
attr F is maximal means
:: LATTICEA:def 3
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;
end;
registration let L be Lattice;
cluster maximal -> being_ultrafilter for Filter of L;
cluster being_ultrafilter -> maximal for Filter of L;
end;
definition let L be Lattice;
let I be Ideal of L;
attr I is maximal means
:: LATTICEA:def 4
I is proper &
for J being Ideal of L st J is proper & I c= J holds I = J;
end;
theorem :: LATTICEA:12
for L being Lattice, I being Ideal of L holds
I is max-ideal iff I is maximal;
registration let L be Lattice;
cluster maximal -> max-ideal for Ideal of L;
cluster max-ideal -> maximal for Ideal of L;
end;
registration let L be Lattice;
cluster maximal -> proper for Ideal of L;
end;
theorem :: LATTICEA:13
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;
theorem :: LATTICEA:14
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;
theorem :: LATTICEA:15
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;
theorem :: LATTICEA:16
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;
theorem :: LATTICEA:17
for L being distributive Lattice,
F being Filter of L st
F is maximal holds F is prime;
registration let L be distributive Lattice;
cluster maximal -> prime for Filter of L;
end;
theorem :: LATTICEA:18
for L being distributive Lattice,
F being Ideal of L st
F is maximal holds F is prime;
registration let L be distributive Lattice;
cluster maximal -> prime for Ideal of L;
end;
begin :: Prime Ideal Theorem for Distributive Lattices
::$N Prime ideal theorem for distributive lattices
theorem :: LATTICEA:19 :: 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;
theorem :: LATTICEA:20
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;
theorem :: LATTICEA:21
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);
theorem :: LATTICEA:22
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;
theorem :: LATTICEA:23
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 };
begin :: The Stone Representation
definition
let L be Lattice;
func PrimeFilters L -> Function means
:: LATTICEA:def 5
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 };
end;
theorem :: LATTICEA:24
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;
theorem :: LATTICEA:25
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;
theorem :: LATTICEA:26
for L being distributive Lattice,
a, b being Element of L holds
PrimeFilters L.(a "/\" b) = PrimeFilters L.a /\ PrimeFilters L.b;
theorem :: LATTICEA:27
for L being distributive Lattice,
a, b being Element of L holds
PrimeFilters L.(a "\/" b) = PrimeFilters L.a \/ PrimeFilters L.b;
definition let L be distributive Lattice;
redefine func PrimeFilters L ->
Function of the carrier of L, bool PFilters L;
end;
definition let L be distributive Lattice;
func StoneR L -> set equals
:: LATTICEA:def 6
rng PrimeFilters L;
end;
registration let L be distributive Lattice;
cluster StoneR L -> non empty;
end;
theorem :: LATTICEA:28
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;
definition let L be upper-bounded distributive Lattice;
func StoneSpace L -> strict TopSpace means
:: LATTICEA:def 7
the carrier of it = PFilters L &
the topology of it =
{ union A where A is Subset-Family of PFilters L : A c= StoneR L };
end;
registration let L be non trivial upper-bounded distributive Lattice;
cluster StoneSpace L -> non empty;
end;
begin :: Pseudocomplements in Lattices
definition let L be Lattice;
let a be Element of L;
func PseudoComplements a -> Subset of L equals
:: LATTICEA:def 8
{ x where x is Element of L : a "/\" x = Bottom L };
func PseudoCocomplements a -> Subset of L equals
:: LATTICEA:def 9
{ x where x is Element of L : a "\/" x = Top L };
end;
registration let L be distributive bounded Lattice;
let a be Element of L;
cluster PseudoComplements a -> initial non empty join-closed;
cluster PseudoCocomplements a -> final non empty meet-closed;
end;
theorem :: LATTICEA:29
for L being Lattice,
a,b being Element of L holds
b in PseudoComplements a iff b "/\" a = Bottom L;
theorem :: LATTICEA:30
for L being Lattice,
a,b being Element of L holds
b in PseudoCocomplements a iff b "\/" a = Top L;
theorem :: LATTICEA:31
for L being bounded Lattice,
a being Element of L holds
Bottom L in PseudoComplements a;
theorem :: LATTICEA:32
for L being bounded Lattice,
a being Element of L holds
Top L in PseudoCocomplements a;
begin :: Nachbin Theorems
definition let L be Lattice;
func Spectrum L -> Subset-Family of L equals
:: LATTICEA:def 10
{ I where I is Ideal of L : I is prime proper };
end;
::$N Nachbin's theorem for bounded distributive lattices
theorem :: LATTICEA:33
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;
registration let L be non trivial distributive bounded Lattice;
cluster Spectrum L -> non empty;
end;
::$N Nachbin theorem for spectra of distributive lattices
theorem :: LATTICEA:34
for L being distributive bounded Lattice holds
L is Boolean iff Spectrum L is unordered;
registration let L be Boolean Lattice;
cluster Spectrum L -> unordered;
end;