Formalization of a normalization theorem in simplicial topology |
| |
Authors: | Laureano Lambán Francisco-Jesús Martín–Mateos Julio Rubio José-Luis Ruiz–Reina |
| |
Affiliation: | 1. Department of Mathematics and Computation, University of La Rioja, Edificio Vives, Luis de Ulloa s/n. 26004, Logro?o, Spain 2. Computational Logic Group, Department of Computer Science and Artificial Intelligence, University of Seville, Avda. Reina Mercedes, s/n. 41012, Sevilla, Spain
|
| |
Abstract: | In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology stating that there exists a homotopy equivalence between the chain complex of a simplicial set, and a smaller chain complex for the same simplicial set, called the normalized chain complex. Even if the Normalization Theorem is usually stated as a higher-order result (with a Category Theory flavor) we manage to give a first-order proof of it. To this aim it is instrumental the introduction of an algebraic data structure called simplicial polynomial. As a demonstration of the validity of our techniques we developed a formal proof in the ACL2 theorem prover. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|