:: Prime Filters and Ideals in Distributive Lattices :: by Adam Grabowski :: :: Received October 7, 2013 :: Copyright (c) 2013-2021 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; 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;