Email Gateway (Sep 02 2026 at 08:57): Email Gateway (Sep 02 2026 at 08:57):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: The Fundamental Group of the Circle
The Fundamental Group of the Circle
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
We formalise the classical theorem of algebraic topology that the fundamental
group of the circle is isomorphic to the additive group of the integers, . The
circle is modelled as the unit sphere in the complex plane with basepoint , and
the carrier of the fundamental group is the set of path-homotopy classes of
loops based at , with concatenation as the group operation. The group laws are
obtained from the homotopy groupoid laws of the Isabelle Analysis library. The
isomorphism with is given by the degree map, sending a homotopy class to the
winding number about the origin of any representative loop. That this is a
bijective group homomorphism follows from the winding-number classification of
loops in the punctured plane, together with a radial retraction onto the circle.
The entry is self-contained on top of the Isabelle distribution.
https://isa-afp.org/entries/Fundamental_Group_Circle.html
Enjoy!
Last updated: Sep 02 2026 at 16:10 UTC