Prime Filters and Ideals in Distributive Lattices

• Autorzy: Adam Grabowski
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

prime filters; prime ideals; distributive lattices

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2013
• Tom: 21
• Numer: 3
• Strony: 213-221

Daty

wydano

2013-10-01

Twórcy

autor

Adam Grabowski

• Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland

Bibliografia

• [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.
• [10] George Grätzer. General Lattice Theory. Academic Press, New York, 1978.
• [11] George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011.
• [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.
• [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.
• [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.

Identyfikatory

DOI

10.2478/forma-2013-0023