State of the formalization of continuous lattices

by Grzegorz Bancerek, Piotr Rudnicki, and Pauline N. Kawamoto

The aim is to formalize in Mizar the theory from A Compendium of Continuous Lattices (CCL)
by G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, Springer-Verlag, 1980.

The theory already formalized in Mizar was done by 16 authors:

Author	CCL	MML	Author	CCL	MML
Grzegorz Bancerek	19	91	Agnieszka J. Marasik	1	4
Czeslaw Bylinski	3	36	Robert Milewski	8	25
Noboru Endou	2	16	Adam Naumowicz	3	11
Adam Grabowski	4	22	Piotr Rudnicki	3	43
Ewa Gradzka	1	2	Yuji Sakai	1	3
Jaroslaw Gryko	3	6	Bartlomiej M. Skorulski	2	4
Artur Kornilowicz	11	45	Andrzej Trybulec	3	86
Beata Madras	1	7	Mariusz Zynel	2	5

It is included in 58 articles. Articles are stored in the Mizar Mathematical Library (MML). The formalization means the formalization of concepts and proofs mechanically checked for logical correctness.

The Mizar formalization of the theory of continuous lattices was supported by

Office of Navy Research Grant N00014-95-1-1336 and N00014-97-1-0777 (USA),
Komitet Badan Naukowych (State Committee for Scientific Research, Poland) Grant 8 T11C01812,
NATO Grant CRG 951368,
NSERC OGP 9207,
Japan Sociaty for the Promotion of Science.

The problem stated on QED Workshop II (Warsaw 1995) was:

Can we do formalization of advanced mathematics like that included in regular mathematical monographs in the current proof-checking systems?

Especially, in our case, we may ask:

Can we do such formalization in Mizar?

Why is the question so important? -- Former formalizations dealt with small and separated mathematical theories chosen often to be easy to formalize. There were, at least two exceptions: Jutting's formalization of Landau's Grundlagen in AUTOMATH and mizaring of Grzegorczyk's Arithmetic in Mizar 2. Both those systems did not required, let me call it, continuous formalization. That means that one may use statements which were not proved, e.g. mathlore. In recent Mizar any articles accepted to the Mizar Mathematical Library has to be a continuation of the Library.

In the MML there was (and still is) a quite big number of articles formalizing beginning of some theory and the theory has no continuation. However, those articles were, mainly, devoted to form the base for more advanced theories. The challenge consists in the fact that against such formalizations the mizaring of the monograph requires much bigger machinery of interrelated concepts and facts, and, then, needs more careful decisions on the way of formalization which may influence later.

Other question was if the MML was enough big to do such formalization.

Why the theory of continuous lattices? -- It seems to be a good compromise on, so called, well-definedness of mathematical field and advancement of it. It is relatively recent and combines different fields of mathematics (algebra, topology, categories).

Report

A Compendium of Continuous Lattices

Table of contents

Chapter 0. A Primer of Complete Lattices

1. Generalities and notation
pages	items	articles	authors	remarks
1--3	1.1--1.5	WAYBEL_0	G. Bancerek
4	1.6	LATTICE3	G. Bancerek
4	1.7	RELSET_1	E. Woronowicz
4--5	1.8--1.10	WAYBEL_0	G. Bancerek
5--7	1.11--1.16			exercises
2. Complete lattices
8--14	2.1--2.8	LATTICE3	G. Bancerek
3. Galois connection
18--23	3.1--3.12	WAYBEL_1	Cz. Bylinski
23--24	3.13--3.14	WAYBEL10	G. Bancerek
24--25	3.15--3.20	WAYBEL_1	Cz. Bylinski
4. Meet-continuous lattices
30--31	4.1--4.3	WAYBEL_2	A. Kornilowicz
32	4.4	WAYBEL_9	A. Kornilowicz

Chapter I. Lattice Theory of Continuous Lattices

1. The ``way-below'' relation
pages	items	articles	authors
38--42	1.1--1.8	WAYBEL_3	G. Bancerek
43--47	1.9--1.19	WAYBEL_4	A. Grabowski
51	1.23	WAYBEL_4	A. Grabowski
52	1.27	WAYBEL_4	A. Grabowski
2. The equational characterization
57--60	2.1--2.6	WAYBEL_5	M. Zynel
60	2.7	WAYBEL_5 WAYBEL20	M. Zynel P. Rudnicki
60	2.8	WAYBEL20	P. Rudnicki
61	2.9	WAYBEL10	G. Bancerek
61	2.10	WAYBEL15	R. Milewski
60--62	2.11--2.13	WAYBEL20	P. Rudnicki
63	2.14	WAYBEL15	R. Milewski
63	2.15	WAYBEL20	P. Rudnicki
3. Irreducible elements
69--72	3.1--3.15	WAYBEL_6	B. Madras
73--77	3.16--3.27	WAYBEL_7	G. Bancerek
82--84	3.43	WAYBEL12	A. Kornilowicz
4. Algebraic lattices
85--87	4.1--4.9	WAYBEL_8	R. Milewski
87	4.10	WAYBEL13	R. Milewski
87	4.11	WAYBEL_8	R. Milewski
88--89	4.12--4.15	WAYBEL13	R. Milewski
89--90	4.16	WAYBEL15	R. Milewski
90--91	4.17	WAYBEL22	P. Rudnicki
91--92	4.18	WAYBEL15	R. Milewski
92--93	4.19--4.24	WAYBEL16	R. Milewski

Chapter II. Topology of Continuous Lattices: The Scott Topology

1. The Scott topology
pages	items	articles	authors
98--105	1.1--1.10	WAYBEL11	A. Trybulec
105--108	1.11--1.15	WAYBEL14	Cz. Bylinski, P. Rudnicki
108--109	1.16--1.17	WAYBEL32	E. Gradzka
2. Scott-continuous functions
112--113	2.1--2.2	WAYBEL17	A. Grabowski
115--116	2.5--2.8	WAYBEL27	G. Bancerek, A. Naumowicz
116--117	2.9	WAYBEL24	A. Grabowski
115--117	2.5--2.10	WAYBEL27	G. Bancerek, A. Naumowicz
118	2.11	WAYBEL11	(not finished)
3. Injective spaces
121--123	3.1--3.4	WAYBEL18	J. Gryko
123--126	3.5--3.12	WAYBEL25	A. Kornilowicz, J. Gryko
4. Function Spaces
128--130	4.1--4.9	WAYBEL26	G. Bancerek
130--133	4.10--4.11	WAYBEL29	G. Bancerek, A. Naumowicz
133--137	4.12--4.19		not done

Chapter III. Topology of Continuous Lattices: The Lawson Topology

1. The Lawson topology
pages	items	articles	authors
142--145	1.1--1.6	WAYBEL19	G. Bancerek
145--146	1.7--1.8	WAYBEL21	G. Bancerek
146--146	1.9--1.10	WAYBEL19	G. Bancerek
146--147	1.11	WAYBEL21	G. Bancerek
2. Meet-continuous lattices revisited
153--156	2.1--2.13	WAYBEL30	A. Kornilowicz
156	2.16	WAYBEL30	A. Kornilowicz
3. Lim-inf convergence
158--159	3.1--3.3	WAYBEL28	B. Skorulski
159	3.4--3.6	WAYBEL33	G. Bancerek, N. Endou
160--163	3.7--3.13		not done
4. Bases and weights
168--169	4.1--4.4	WAYBEL23	R. Milewski
170--171	4.5--4.7	WAYBEL31	R. Milewski
171--175	4.8--4.17		not done

Chapter IV. Morphisms and Functors

1. Duality theory
pages	items	articles	authors	remarks
179--183	1.1--1.12	WAYBEL34	G. Bancerek
183--189	1.13--1.28			not done
189--192	1.29--1.45			exercises
2. Morphisms into chains
194--202	2.1--2.20			not done
202--205	2.21--2.30			exercises
3. Projective limits and functors which preserve them
206--222	3.1--3.25			not done
222--223	3.26--3.28			exercises
4. Fixed point construction for functors
224--233	4.1--4.15			not done
233--235	4.16--4.23			exercises

Index

List of concepts

Mizar articles

WAYBEL_0:: Directed Sets, Nets, Ideals, Filters, and Maps by Grzegorz Bancerek.; CCL: Chapter 0, section 1, pages: 2 - 5, items: 1.1 - 1.5, 1.8 - 1.10.
WAYBEL_1:: Galois Connections by Czeslaw Bylinski.; CCL: Chapter 0, section 3, pages: 18 - 25, items: 3.1 - 3.12, 3.15 - 3.20.
WAYBEL_2:: Meet -- Continuous Lattices by Artur Kornilowicz.; CCL: Chapter 0, section 4, pages: 30 and 31, items: 4.1 - 4.3.
WAYBEL_3:: The ``Way-Below'' Relation by Grzegorz Bancerek.; CCL: Chapter I, section 1, pages: 38 - 42, items: 1.1 - 1.8.
WAYBEL_4:: Auxiliary and Approximating Relations by Adam Grabowski.; CCL: Chapter I, section 1, pages: 43 - 47, items: 1.9 - 1.19, 1.23, 1.27.
WAYBEL_5:: The Equational Characterization of Continuous Lattices by Mariusz Zynel.; CCL: Chapter I, section 2, pages: 57 - 60, items: 2.1 - 2.7.
WAYBEL_6:: Irreducible and Prime Elements by Beata Madras.; CCL: Chapter I, section 3, pages: 69 - 72, items: 3.1 - 3.15.
WAYBEL_7:: Prime Ideals and Filters by Grzegorz Bancerek.; CCL: Chapter I, section 3, pages: 73 - 77, items: 3.16 - 3.27.
WAYBEL_8:: Algebraic Lattices by Robert Milewski.; CCL: Chapter I, section 4, pages: 85 - 87, items: 4.1 - 4.9, 4.11.
WAYBEL_9:: On the Topological Properties of Meet-Continuous Lattices by Artur Kornilowicz.; CCL: Chapter 0, section 4, page: 32, item: 4.4.
WAYBEL10:: Closure Operators and Subalgebras by Grzegorz Bancerek.; CCL: Chapter 0, section 3, pages: 23 and 24, items: 3.13, 3.14.
WAYBEL11:: Scott Topology by Andrzej Trybulec.; CCL: Chapter II, section 1, pages: 98 - 105, items: 1.1 - 1.10.
WAYBEL12:: On the Baire Category Theorem by Artur Kornilowicz.; CCL: Chapter I, section 3, pages: 82 - 84, item: 3.43.
WAYBEL13:: Algebraic and Arithmetic Lattices by Robert Milewski.; CCL: Chapter I, section 4, pages: 87 - 89, items: 4.10 - 4.15.
WAYBEL14:: The Scott topology, Part II by Czeslaw Bylinski and Piotr Rudnicki.; CCL: Chapter II, section 1, pages: 105 - 108, items: 1.11 - 1.15.
WAYBEL15:: More on the Algebraic and Arithmetic Lattices by Robert Milewski.; CCL: Chapter I, sections 2 and 4, pages: 61, 63, 89 - 92, items: 2.10, 2.14. 4.16, 4.18
WAYBEL16:: Completely-Irreducible Elements by Robert Milewski.; CCL: Chapter I, section 4, pages: 92 - 93, items: 4.19 - 4.24.
WAYBEL17:: Scott-Continuous Functions by Adam Grabowski.; CCL: Chapter II, section 2, pages: 112 - 113, item 2.1.
WAYBEL18:: Injective Spaces by Jaroslaw Gryko.; CCL: Chapter II, section 3, pages: 121 - 122, items: 3.1 - 3.4.
WAYBEL19:: The Lawson Topology by Grzegorz Bancerek.; CCL: Chapter III, section 1, pages: 142 - 146, items: 1.1 - 1.7, 1.9, 1.10.
WAYBEL20:: Kernel Projections and Quotient Lattices by Piotr Rudnicki.; CCL: Chapter I, section 2, pages: 60 - 63, items: 2.7, 2.8, 2.11 - 2.14.
WAYBEL21:: Lawson Topology in Continuous Lattices by Grzegorz Bancerek.; CCL: Chapter III, section 1, pages: 145 - 147, items: 1.7, 1.8, 1.11.
WAYBEL22:: Representation theorem for free continuous lattices by Piotr Rudnicki.; CCL: Chapter I, section 4, pages: 90, 91, item 4.17.
WAYBEL23:: Bases of continuous lattices by Robert Milewski.; CCL: Chapter II, section 2, pages: 116 - 117, item: 2.9.
WAYBEL24,: Scott-Continuous Functions. Part II by Adam Grabowski.; CCL: Chapter III, section 4, pages: 168 - 169, items: 4.1 - 4.4.
WAYBEL25,: Injective Spaces. Part II by Artur Kornilowicz and Jaroslaw Gryko.; CCL: Chapter II, section 3, pages: 123 - 126, items: 3.5 - 3.12.
WAYBEL26,: Continuous Lattices of Maps between T$_0$ Spaces by Grzegorz Bancerek.; CCL: Chapter II, section 4, pages: 128 - 130, items: 4.1 - 4.9.
WAYBEL27,: Function Spaces in the Category of Directed Suprema Preserving Maps by Grzegorz Bancerek and Adam Naumowicz.; CCL: Chapter II, section 2, pages: 115 - 117, items: 2.5 - 2.10.
WAYBEL28,: Lim-Inf Convergence by Bartlomiej Skorulski.; CCL: Chapter III, section 3, pages: 158 - 159, items: 3.1 - 3.3.
WAYBEL29,: The Characterization of the Continuity of Topologies by Grzegorz Bancerek and Adam Naumowicz.
WAYBEL30,: Meet Continuous Lattices Revisited by Artur Kornilowicz.; CCL: Chapter III, section 2, pages: 153 - 156, items: 2.1 - 2.13, 2.16.
WAYBEL31,: Weights of Continuous Lattices by Robert Milewski.; CCL: Chapter III, section 4, pages: 170 - 171, items: 4.5 - 4.7.
WAYBEL32,: On the Order-consistent Topology of Complete and Uncomplete Lattices by Ewa Gradzka.; CCL: Chapter II, section 1, pages: 108 - 109, items: 1.16 - 1.17.
WAYBEL33,: Compactness of Lim-inf Topology by Grzegorz Bancerek and Noboru Endou.; CCL: Chapter III, section 3, page: 159, items: 3.4 - 3.6.
WAYBEL34,: Duality Based on Galois Connection. Part I by Grzegorz Bancerek.
WAYBEL35,: Morphisms Into Chains. Part I by Artur Kornilowicz.

YELLOW_0:: Bounds in Posets and Relational Substructures by Grzegorz Bancerek.
YELLOW_1:: Boolean Posets, Posets under Inclusion and Products of Relational Structures by Adam Grabowski and Robert Milewski.
YELLOW_2:: Properties of Relational Structures, Posets, Lattices and Maps by Mariusz Zynel and Czeslaw Bylinski.
YELLOW_3:: Cartesian Products of Relations and Relational Structures by Artur Kornilowicz.
YELLOW_4:: Definitions and Properties of the Join and Meet of Subsets by Artur Kornilowicz.
YELLOW_5:: Miscellaneous Facts about Relation Structure by Agnieszka Julia Marasik.
YELLOW_6:: Moore-Smith Convergence by Andrzej Trybulec.
YELLOW_7:: Duality in Relation Structures by Grzegorz Bancerek.
YELLOW_8:: Baire Spaces, Sober Spaces by Andrzej Trybulec.
YELLOW_9:: Bases and Refinements of Topologies by Grzegorz Bancerek.
YELLOW10,: The Properties of Product of Relational Structures by Artur Kornilowicz.
YELLOW11:: On the Characterization of Modular and Distributive Lattices by Adam Naumowicz.
YELLOW12:: On the Characterization of Hausdorff Spaces by Artur Kornilowicz.
YELLOW13:: Introduction to meet-continuous topological lattices by Artur Kornilowicz.
YELLOW14,: Jaroslaw Gryko and Artur Kornilowicz.; Some Properties of Isomorphism between Relational Structures. On the Product of Topological Spaces.
YELLOW15,: Robert Milewski.; Components and Basis of Topological Spaces.
YELLOW16,: Grzegorz Bancerek.; Retracts and Inheritance.
YELLOW17,: Bartlomiej Skorulski.; The Tichonov Theorem.
YELLOW18,: Grzegorz Bancerek.; Concrete Categories.
YELLOW19,: Grzegorz Bancerek, Noboru Endou, and Yuji Sakai.; On the Characterizations of Compactness.
YELLOW20,: Grzegorz Bancerek.; Miscellaneous Facts about Functors.
YELLOW21,: Grzegorz Bancerek.; Categorial Background for Duality Theory.
YELLOW_0,: Grzegorz Bancerek.

Works under progress

August 2, 2002, e-mail: bancerek@mizar.org