Stone Lattices

Adam Grabowski

Formalized Mathematics (2015)

  • Volume: 23, Issue: 4, page 387-396
  • ISSN: 1426-2630

Abstract

top
The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the paper, the notion of a pseudocomplement in a lattice is formally introduced in Mizar, and based on this we define the notion of the skeleton and the set of dense elements in a pseudocomplemented lattice, giving the meet-decomposition of arbitrary element of a lattice as the infimum of two elements: one belonging to the skeleton, and the other which is dense. The core of the paper is of course the idea of Stone identity [...] a*⊔a**=T, a * a * * = T , which is fundamental for us: Stone lattices are those lattices L, which are distributive, bounded, and satisfy Stone identity for all elements a ∈ L. Stone algebras were introduced by Grätzer and Schmidt in [18]. Of course, the pseudocomplement is unique (if exists), so in a pseudcomplemented lattice we defined a * as the Mizar functor (unary operation mapping every element to its pseudocomplement). In Section 2 we prove formally a collection of ordinary properties of pseudocomplemented lattices. All Boolean lattices are Stone, and a natural example of the lattice which is Stone, but not Boolean, is the lattice of all natural divisors of p 2 for arbitrary prime number p (Section 6). At the end we formalize the notion of the Stone lattice B [2] (of pairs of elements a, b of B such that a ⩽ b) constructed as a sublattice of B 2, where B is arbitrary Boolean algebra (and we describe skeleton and the set of dense elements in such lattices). In a natural way, we deal with Cartesian product of pseudocomplemented lattices. Our formalization was inspired by [17], and is an important step in formalizing Jouni Järvinen Lattice theory for rough sets [19], so it follows rather the latter paper. We deal essentially with Section 4.3, pages 423–426. The description of handling complemented structures in Mizar [6] can be found in [12]. The current article together with [15] establishes the formal background for algebraic structures which are important for [10], [16] by means of mechanisms of merging theories as described in [11].

How to cite

top

Adam Grabowski. "Stone Lattices." Formalized Mathematics 23.4 (2015): 387-396. <http://eudml.org/doc/276829>.

@article{AdamGrabowski2015,
abstract = {The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the paper, the notion of a pseudocomplement in a lattice is formally introduced in Mizar, and based on this we define the notion of the skeleton and the set of dense elements in a pseudocomplemented lattice, giving the meet-decomposition of arbitrary element of a lattice as the infimum of two elements: one belonging to the skeleton, and the other which is dense. The core of the paper is of course the idea of Stone identity [...] a*⊔a**=T, \[a^* \sqcup a^\{**\} = \{\rm \{T\}\},\] which is fundamental for us: Stone lattices are those lattices L, which are distributive, bounded, and satisfy Stone identity for all elements a ∈ L. Stone algebras were introduced by Grätzer and Schmidt in [18]. Of course, the pseudocomplement is unique (if exists), so in a pseudcomplemented lattice we defined a * as the Mizar functor (unary operation mapping every element to its pseudocomplement). In Section 2 we prove formally a collection of ordinary properties of pseudocomplemented lattices. All Boolean lattices are Stone, and a natural example of the lattice which is Stone, but not Boolean, is the lattice of all natural divisors of p 2 for arbitrary prime number p (Section 6). At the end we formalize the notion of the Stone lattice B [2] (of pairs of elements a, b of B such that a ⩽ b) constructed as a sublattice of B 2, where B is arbitrary Boolean algebra (and we describe skeleton and the set of dense elements in such lattices). In a natural way, we deal with Cartesian product of pseudocomplemented lattices. Our formalization was inspired by [17], and is an important step in formalizing Jouni Järvinen Lattice theory for rough sets [19], so it follows rather the latter paper. We deal essentially with Section 4.3, pages 423–426. The description of handling complemented structures in Mizar [6] can be found in [12]. The current article together with [15] establishes the formal background for algebraic structures which are important for [10], [16] by means of mechanisms of merging theories as described in [11].},
author = {Adam Grabowski},
journal = {Formalized Mathematics},
keywords = {pseudocomplemented lattices; Stone lattices; Boolean lattices; lattice of natural divisors; formalization of lattices; lattices of natural divisors},
language = {eng},
number = {4},
pages = {387-396},
title = {Stone Lattices},
url = {http://eudml.org/doc/276829},
volume = {23},
year = {2015},
}

TY - JOUR
AU - Adam Grabowski
TI - Stone Lattices
JO - Formalized Mathematics
PY - 2015
VL - 23
IS - 4
SP - 387
EP - 396
AB - The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the paper, the notion of a pseudocomplement in a lattice is formally introduced in Mizar, and based on this we define the notion of the skeleton and the set of dense elements in a pseudocomplemented lattice, giving the meet-decomposition of arbitrary element of a lattice as the infimum of two elements: one belonging to the skeleton, and the other which is dense. The core of the paper is of course the idea of Stone identity [...] a*⊔a**=T, \[a^* \sqcup a^{**} = {\rm {T}},\] which is fundamental for us: Stone lattices are those lattices L, which are distributive, bounded, and satisfy Stone identity for all elements a ∈ L. Stone algebras were introduced by Grätzer and Schmidt in [18]. Of course, the pseudocomplement is unique (if exists), so in a pseudcomplemented lattice we defined a * as the Mizar functor (unary operation mapping every element to its pseudocomplement). In Section 2 we prove formally a collection of ordinary properties of pseudocomplemented lattices. All Boolean lattices are Stone, and a natural example of the lattice which is Stone, but not Boolean, is the lattice of all natural divisors of p 2 for arbitrary prime number p (Section 6). At the end we formalize the notion of the Stone lattice B [2] (of pairs of elements a, b of B such that a ⩽ b) constructed as a sublattice of B 2, where B is arbitrary Boolean algebra (and we describe skeleton and the set of dense elements in such lattices). In a natural way, we deal with Cartesian product of pseudocomplemented lattices. Our formalization was inspired by [17], and is an important step in formalizing Jouni Järvinen Lattice theory for rough sets [19], so it follows rather the latter paper. We deal essentially with Section 4.3, pages 423–426. The description of handling complemented structures in Mizar [6] can be found in [12]. The current article together with [15] establishes the formal background for algebraic structures which are important for [10], [16] by means of mechanisms of merging theories as described in [11].
LA - eng
KW - pseudocomplemented lattices; Stone lattices; Boolean lattices; lattice of natural divisors; formalization of lattices; lattices of natural divisors
UR - http://eudml.org/doc/276829
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. 
  2. [2] Grzegorz Bancerek. Filters – part II. Quotient lattices modulo filters and direct product of two lattices. Formalized Mathematics, 2(3):433–438, 1991. 
  3. [3] Grzegorz Bancerek. Ideals. Formalized Mathematics, 5(2):149–156, 1996. 
  4. [4] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991. 
  5. [5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  6. [6] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17.[Crossref] Zbl06512423
  7. [7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  8. [8] Marek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453–459, 1991. 
  9. [9] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. 
  10. [10] Adam Grabowski. On the computer-assisted reasoning about rough sets. In B. Dunin-Kęplicz, A. Jankowski, A. Skowron, and M. Szczuka, editors, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location, volume 28 of Advances in Soft Computing, pages 215–226, Berlin, Heidelberg, 2005. Springer-Verlag. doi:10.1007/3-540-32370-8 15.[Crossref] Zbl1090.68574
  11. [11] Adam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371–385, 2014. doi:10.3233/FI-2014-1129.[Crossref][WoS] Zbl1329.68247
  12. [12] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211–221, 2015. doi:10.1007/s10817-015-9333-5.[Crossref] Zbl06585255
  13. [13] Adam Grabowski. Prime filters and ideals in distributive lattices. Formalized Mathematics, 21(3):213–221, 2013. doi:10.2478/forma-2013-0023.[Crossref] Zbl1298.06003
  14. [14] Adam Grabowski. On square-free numbers. Formalized Mathematics, 21(2):153–162, 2013. doi:10.2478/forma-2013-0017.[Crossref] Zbl1298.11008
  15. [15] Adam Grabowski. Two axiomatizations of Nelson algebras. Formalized Mathematics, 23 (2):115–125, 2015. doi:10.1515/forma-2015-0012.[Crossref] Zbl1318.06010
  16. [16] Adam Grabowski and Magdalena Jastrzębska. Rough set theory from a math-assistant perspective. In Rough Sets and Intelligent Systems Paradigms, International Conference, RSEISP 2007, Warsaw, Poland, June 28–30, 2007, Proceedings, pages 152–161, 2007. doi:10.1007/978-3-540-73451-2 17.[Crossref] 
  17. [17] George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011. Zbl1233.06001
  18. [18] George Grätzer and E.T. Schmidt. On a problem of M.H. Stone. Acta Mathematica Academiae Scientarum Hungaricae, (8):455–460, 1957. 
  19. [19] Jouni Järvinen. Lattice theory for rough sets. Transactions of Rough Sets, VI, Lecture Notes in Computer Science, 4374:400–498, 2007. Zbl1186.03069
  20. [20] Magdalena Jastrzębska and Adam Grabowski. On the properties of the Möbius function. Formalized Mathematics, 14(1):29–36, 2006. doi:10.2478/v10037-006-0005-0.[Crossref] 
  21. [21] Jolanta Kamieńska and Jarosław Stanisław Walijewski. Homomorphisms of lattices, finite join and finite meet. Formalized Mathematics, 4(1):35–40, 1993. 
  22. [22] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990. 
  23. [23] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829–832, 1990. 
  24. [24] Robert Milewski. More on the lattice of many sorted equivalence relations. Formalized Mathematics, 5(4):565–569, 1996. 
  25. [25] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990. 
  26. [26] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990. 
  27. [27] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  28. [28] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.