# Prime Filters and Ideals in Distributive Lattices

Formalized Mathematics (2013)

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

## Access Full Article

top## Abstract

top## How to cite

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

## Citations in EuDML Documents

top## NotesEmbed ?

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