Artículo
Formalization of a normalization theorem in simplicial topology
Autor/es | Lambán Pardo, Laureano
Martín Mateos, Francisco Jesús Rubio, Julio Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2012 |
Fecha de depósito | 2019-05-13 |
Publicado en |
|
Resumen | 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, ... 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. |
Identificador del proyecto | MTM2009-13842
ForMath n. 243847 |
Cita | Lambán Pardo, L., Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2012). Formalization of a normalization theorem in simplicial topology. Annals of Mathematics and Artificial Intelligence, 64 (1), 1-37. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Formalization of a normalization ... | 750.8Kb | [PDF] | Ver/ | |