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.
@article{bwmeta1.element.doi-10_2478_forma-2013-0023,
author = {Adam Grabowski},
title = {Prime Filters and Ideals in Distributive Lattices},
journal = {Formalized Mathematics},
volume = {21},
year = {2013},
pages = {213-221},
zbl = {1298.06003},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_forma-2013-0023}
}
Adam Grabowski. Prime Filters and Ideals in Distributive Lattices. Formalized Mathematics, Tome 21 (2013) pp. 213-221. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_forma-2013-0023/
[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. | Zbl 0452.06001
[10] George Grätzer. General Lattice Theory. Academic Press, New York, 1978. | Zbl 0436.06001
[11] George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011. | Zbl 1233.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. | Zbl 0034.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. | Zbl 0014.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.