Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: distributive lattices

Sortuj według:

Ogranicz wyniki do:

Prime Filters and Ideals in Distributive Lattices

100%

Grabowski A.

Formalized Mathematics

2013

tom 21

nr 3

213-221

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.

Ograniczanie wyników

1 Formalized Mathematics

1 Grabowski A.

1 2013

Wyniki wyszukiwania

Prime Filters and Ideals in Distributive Lattices