×

An implementation of effective homotopy of fibrations. (English) Zbl 1436.55022

Summary: In this paper, we present a new module for the Kenzo system which makes it possible to compute the effective homotopy of the total space of a fibration, using the well-known long exact sequence of homotopy of a fibration defined by Jean-Pierre Serre. The programs are written in Common Lisp and require the implementation of new classes and functions corresponding to the definitions of setoid group (SG) and effective setoid group (ESG). Moreover, we have included a new module for working with finitely generated abelian groups, choosing the representation of a free presentation by means of a matrix in canonical form. These tools are then used to implement the long exact homotopy sequence of a fibration. We illustrate with examples some applications of our results.

MSC:

55R05 Fiber spaces in algebraic topology
68W30 Symbolic computation and algebraic computation

Software:

Kenzo; Agda; cubicaltt
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barakat, M.; Bremer, B., Higher extension modules and the Yoneda product (2008), Preprint
[2] Bousfield, A.; Kan, D., Homotopy Limits, Completions and Localizations, Lecture Notes in Mathematics, vol. 304 (1972), Springer-Verlag · Zbl 0259.55004
[3] Bove, A.; Dybjer, P.; Norell, U., A brief overview of Agda - a functional language with dependent types, (22nd International Conference on Theorem Proving in Higher Order Logics. 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs’09. 22nd International Conference on Theorem Proving in Higher Order Logics. 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs’09, Lecture Notes in Computer Science, vol. 5674 (2009)), 73-78 · Zbl 1252.68062
[4] Brown, E., Finite computability of Postnikov complexes, Ann. Math., 65, 1, 1-20 (1957) · Zbl 0077.16804
[5] Brown, K. S., Cohomology of Groups (1982), Springer-Verlag
[6] Brunerie, G., On the homotopy groups of spheres in homotopy type theory (2016), Preprint
[7] Cohen, C.; Coquand, T.; Huber, S.; Mörtberg, A., Cubical Type Theory: a constructive interpretation of the univalence axiom (2016)
[8] Dousson, X.; Rubio, J.; Sergeraert, F.; Siret, Y., The Kenzo program (1999)
[9] Kaczynski, T.; Mischaikow, K.; Mrozek, M., Computational Homology, Applied Mathematical Sciences, vol. 157 (2004), Springer · Zbl 1039.55001
[10] Knapp, A. W., Advanced Algebra (2008), Birkhäuser
[11] Kochman, S. O., Stable Homotopy Groups of Spheres. A Computer-Assisted Approach, Lecture Notes in Mathematics, vol. 1423 (1990), Springer-Verlag · Zbl 0688.55010
[12] May, J. P., Simplicial Objects in Algebraic Topology, Van Nostrand Mathematical Studies (1967), University of Chicago Press · Zbl 0165.26004
[13] Ravenel, D. C., Complex Cobordism and Stable Homotopy Groups of Spheres (2003), AMS Chelsea
[14] Romero, A.; Rubio, J., Homotopy groups of suspended classifying spaces: an experimental approach, Math. Comput., 82, 2237-2244 (2013) · Zbl 1284.68684
[15] Romero, A.; Sergeraert, F., Effective homotopy of fibrations, Appl. Algebra Eng. Commun. Comput., 23, 85-100 (2012) · Zbl 1253.55011
[16] Romero, A.; Sergeraert, F., A combinatorial tool for computing the effective homotopy of iterated loop spaces, Discrete Comput. Geom., 53, 1, 1-15 (2015) · Zbl 1311.55001
[17] Romero, A.; Sergeraert, F., A Bousfield-Kan algorithm for computing the effective homotopy of a space, Found. Comput. Math., 17, 1335-1366 (2017) · Zbl 1386.55022
[18] Rubio, J.; Sergeraert, F., Constructive algebraic topology, Bull. Sci. Math., 126, 5, 389-412 (2002) · Zbl 1007.55019
[19] Rubio, J.; Sergeraert, F., Constructive homological algebra and applications (2006), Preprint
[20] Schön, R., Effective Algebraic Topology, Mem. Amer. Math. Soc., vol. 451 (1991) · Zbl 0731.55015
[21] Sergeraert, F., The computability problem in algebraic topology, Adv. Math., 104, 1, 1-29 (1994) · Zbl 0823.55011
[22] Sergeraert, F., Effective exact couples (2009), Preprint
[23] Serre, J., Groupes d’homotopie et classes de groupes abéliens, Ann. Math., 58, 2, 258-294 (1953) · Zbl 0052.19303
[24] Serre, J.-P., Homologie singulière des espaces fibrés. Applications, Ann. Math., 425-505 (1951) · Zbl 0045.26003
[25] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics (2013), Institute for Advanced Study · Zbl 1298.03002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.