Topological Foundations for a Formal Theory of Manifolds

Abstract

Topological manifolds form an important class of topological spaces with applications throughout mathematics. However, the development of this scientic area, even at the initial stage, requires non-trivial Brouwer's theorems: the xed point theorem, the topological invariance of degree, and the topological invariance of dimension, where each of them is provided for n-dimensional case. We present a formalization, that is checked in the Mizar system, of several results in algebraic topology that is sucient to show the basic properties of manifolds with boundary of dimension n.

Keywords

• Topological manifolds
• Formalization
• Mizar

Introduction

connected component of a compact manifold is a manifold with a determined dimension and also he proved the dependence between interior and boundary points. He showed for an n-dimensional manifold that its interior is a manifold without boundary of dimension n and its boundary is a manifold without boundary of dimension n 1. Additionally, he showed that the Cartesian product of manifolds also forms a manifold whose dimension is the sum of the dimensions of its factors and also determined the interior and boundary of this product. 3

Contributions

To establish these results, K. P¡k had to develop mainly the algebraic topology in the MML. It includes theory of simplicial complexes in real linear spaces and its barycenter subdivision. The theory was necessary to provide Brouwer’s xed point theorem based on Sperner’s lemma [ 13, 16 ]. The theorem has been used in the formalization of the Jordan curve theorem in Mizar [ 5 ]. But for this purpose, the 2-dimensional case was sucient. Therefore, this statement has been provided by A. Korni“owicz, only for this case using basic arguments concerning the fundamental groups of the respective spaces [ 7 ]. Note that this approach for higher-dimensional cases requires incomparably more dicult facts about these groups. Another approach based on Sperner’s lemma requires only intuitively clear facts about the standard n-dimensional simplex and its arbitrarily small subdivision (see [ 11, 12 ]). Additionally, the simplex structure is explored in one of the approaches to prove Brouwer’s invariance of the domain theorem that is helpful to distinguish points from the internal and the boundary of a manifold (see [ 3 ]).

Obviously the realization of the selected approach required to develop several other areas of topology and algebra. The most important of these are the small inductive dimension of topological spaces [ 9, 10 ]; an ane indepedence of points and barycentric coordinates in an ane space including the theory that barycentric coordinates with respect to an ane independence set is continuous [ 14 ]; the rotation group of Euclidean topological spaces [ 15 ].

Acknowledgements References

The paper has been nanced by the resources of the Polish National Science Center granted by decision n DEC-2012/07/N/ST6/02147.

References

[1] G. Bancerek and P. Rudnicki . Information Retrieval in MML. In A . Asperti, B. Buchberger , and J.H .Davenport, editors, Proc. of Mathematical Knowledge Management 2003 , volume 2594 , page 119131. Springer, Heidelberg, 2003 .

[2] G. Bancerek , C. Bylinski , A. Grabowski , A . Korni“owicz, R. Matuszewski , A. Naumowicz , K. P¡k, and J. Urban . Mizar: State-of-the-art and Beyond . In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13 - 17 , 2015 , Proceedings , volume 9150 of Lecture Notes in Computer Science , pages 261279 . Springer, 2015 .

[3] R. Engelking . General Topology . PWN - Polish Scientic Publishers, Warsaw, 1977 .

[4] A. Grabowski and Ch. Schwarzweller. Improving Representation of Knowledge within the Mizar Library . Studies in Logic, Grammar and Rhetoric , 18 ( 31 ): 3550 , 2009 .

[5] A. Grabowski , A. Kornilowicz , and Adam Naumowicz . Mizar in a Nutshell . Journal of Formalized Reasoning , 3 ( 2 ): 153245 , 2010 .

[6] A. Grabowski and Ch. Schwarzweller. Revisions as an essential tool to maintain mathematical repositories . In Proceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference, Calculemus '07 / MKM '07 , pages 235249 , Berlin, Heidelberg, 2007 . Springer-Verlag.

[7] A. Korni “owicz and Y. Shidama . Brouwer Fixed Point Theorem for Disks on the Plane . Formalized Mathematics , 13 ( 2 ): 333336 , 2005 .

[8] K. P¡k . Topological Manifolds. Formalized Mathematics , 22 ( 2 ): 179186 , 2014 .

[9] K. P¡k. Small inductive dimension of topological spaces . Formalized Mathematics , 17 ( 3 ): 207212 , 2009 .

[10] K. P¡k. Small inductive dimension of topological spaces . Part II. Formalized Mathematics , 17 ( 3 ): 219222 , 2009 .

[11] K. P¡k. Abstract simplicial complexes . Formalized Mathematics , 18 ( 1 ): 95106 , 2010 .

[12] K. P¡k. Sperner's lemma . Formalized Mathematics , 18 ( 4 ): 189196 , 2010 .

[13] K. P¡k. Brouwer xed point theorem for simplexes . Formalized Mathematics , 19 ( 3 ): 145150 , 2011 .

[14] K. P¡k. Continuity of barycentric coordinates in Euclidean topological spaces . Formalized Mathematics , 19 ( 3 ): 139144 , 2011 .

[15] K. P¡k. The rotation group . Formalized Mathematics , 20 ( 1 ): 2329 , 2012 .

[16] K. P¡k. Brouwer invariance of domain theorem . Formalized Mathematics , 22 ( 1 ): 2128 , 2014 .

[17] M. Riccardi . The denition of topological manifolds . Formalized Mathematics , 19 ( 1 ): 4144 , 2011 .

[18] M. Riccardi . Planes and spheres as topological manifolds. Stereographic projection . Formalized Mathematics , 20 ( 1 ): 4145 , 2012 .