Prime Filters and Ideals in Distributive Lattices

Adam Grabowski

Formalized Mathematics (2013)

  • Volume: 21, Issue: 3, page 213-221
  • ISSN: 1426-2630

Abstract

top
The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding [9] proven some results; we tried however to follow [21], [12], and [13]. All three were devoted to the Stone representation theorem [18] for Boolean or Heyting lattices. The main aim of the present article was to bridge this gap between general distributive lattices and Boolean algebras, having in mind that the more general approach will eventually replace the common proof of aforementioned articles.1 Because in Boolean algebras the notions of ultrafilters, prime filters and maximal filters coincide, we decided to construct some concrete examples of ultrafilters in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem not as BPI (Boolean Prime Ideal), but in the more general setting. In the final section we present Nachbin theorems [15],[1] expressed both in terms of maximal and prime filters and as the unordered spectra of a lattice [11], [10]. This shows that if the notion of maximal and prime filters coincide in the lattice, it is Boolean.

How to cite

top

Adam Grabowski. "Prime Filters and Ideals in Distributive Lattices." Formalized Mathematics 21.3 (2013): 213-221. <http://eudml.org/doc/266572>.

@article{AdamGrabowski2013,
abstract = {The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding [9] proven some results; we tried however to follow [21], [12], and [13]. All three were devoted to the Stone representation theorem [18] for Boolean or Heyting lattices. The main aim of the present article was to bridge this gap between general distributive lattices and Boolean algebras, having in mind that the more general approach will eventually replace the common proof of aforementioned articles.1 Because in Boolean algebras the notions of ultrafilters, prime filters and maximal filters coincide, we decided to construct some concrete examples of ultrafilters in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem not as BPI (Boolean Prime Ideal), but in the more general setting. In the final section we present Nachbin theorems [15],[1] expressed both in terms of maximal and prime filters and as the unordered spectra of a lattice [11], [10]. This shows that if the notion of maximal and prime filters coincide in the lattice, it is Boolean.},
author = {Adam Grabowski},
journal = {Formalized Mathematics},
keywords = {prime filters; prime ideals; distributive lattices},
language = {eng},
number = {3},
pages = {213-221},
title = {Prime Filters and Ideals in Distributive Lattices},
url = {http://eudml.org/doc/266572},
volume = {21},
year = {2013},
}

TY - JOUR
AU - Adam Grabowski
TI - Prime Filters and Ideals in Distributive Lattices
JO - Formalized Mathematics
PY - 2013
VL - 21
IS - 3
SP - 213
EP - 221
AB - The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding [9] proven some results; we tried however to follow [21], [12], and [13]. All three were devoted to the Stone representation theorem [18] for Boolean or Heyting lattices. The main aim of the present article was to bridge this gap between general distributive lattices and Boolean algebras, having in mind that the more general approach will eventually replace the common proof of aforementioned articles.1 Because in Boolean algebras the notions of ultrafilters, prime filters and maximal filters coincide, we decided to construct some concrete examples of ultrafilters in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem not as BPI (Boolean Prime Ideal), but in the more general setting. In the final section we present Nachbin theorems [15],[1] expressed both in terms of maximal and prime filters and as the unordered spectra of a lattice [11], [10]. This shows that if the notion of maximal and prime filters coincide in the lattice, it is Boolean.
LA - eng
KW - prime filters; prime ideals; distributive lattices
UR - http://eudml.org/doc/266572
ER -

References

top
  1. [1] Raymond Balbes and Philip Dwinger. Distributive Lattices. University of Missouri Press, 1975. 
  2. [2] Grzegorz Bancerek. Filters - part I. Formalized Mathematics, 1(5):813-819, 1990. 
  3. [3] Grzegorz Bancerek. Ideals. Formalized Mathematics, 5(2):149-156, 1996. 
  4. [4] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719-725, 1991. 
  5. [5] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  6. [6] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  7. [7] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  8. [8] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  9. [9] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980. Zbl0452.06001
  10. [10] George Grätzer. General Lattice Theory. Academic Press, New York, 1978. Zbl0436.06001
  11. [11] George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011. Zbl1233.06001
  12. [12] Jolanta Kamienska. Representation theorem for Heyting lattices. Formalized Mathematics, 4(1):41-45, 1993. 
  13. [13] Jolanta Kamienska and Jarosław Stanisław Walijewski. Homomorphisms of lattices, finite join and finite meet. Formalized Mathematics, 4(1):35-40, 1993. 
  14. [14] Agnieszka Julia Marasik. Boolean properties of lattices. Formalized Mathematics, 5(1): 31-35, 1996. 
  15. [15] Leopoldo Nachbin. Une propriété characteristique des algebres booleiennes. Portugaliae Mathematica, 6:115-118, 1947. Zbl0034.16603
  16. [16] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  17. [17] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990. 
  18. [18] Marshall H. Stone. The theory of representations of Boolean algebras. Transactions of the American Mathematical Society, 40:37-111, 1936. Zbl0014.34002
  19. [19] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9-11, 1990. 
  20. [20] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  21. [21] Jarosław Stanisław Walijewski. Representation theorem for Boolean algebras. Formalized Mathematics, 4(1):45-50, 1993. 
  22. [22] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  23. [23] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  24. [24] Stanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.