<abstract xmlns="http://www.w3.org/1999/xhtml">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.</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.

Prime Filters and Ideals in Distributive Lattices

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

Formalized Mathematics

{"article-title":"Prime Filters and Ideals in Distributive Lattices"}

The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar...

Prime Filters and Ideals in Distributive Lattices

Data publikacji: 01 paź 2013

Zakres stron: 213 - 221

DOI: https://doi.org/10.2478/forma-2013-0023

Słowa kluczowe
prime filters, prime ideals, distributive lattices

This content is open access.

Prime Filters and Ideals in Distributive Lattices

Data publikacji: 01 paź 2013

Zakres stron: 213 - 221

DOI: https://doi.org/10.2478/forma-2013-0023

Słowa kluczoweprime filters, prime ideals, distributive lattices

This content is open access.

Słowa kluczowe
prime filters, prime ideals, distributive lattices