An implementation of effective homotopy of fibrations. (September 2019) - Romero, Ana; Rubio, Julio; Sergeraert, Francis
Abstract: 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.