Circles as Eilenberg--Mac Lane spaces

A real additive circle of nonzero period is a K(ℤ, 1): it is path-connected, its fundamental group is infinite cyclic, and all its higher homotopy groups vanish.

These results package the existing circle calculations into the Eilenberg--Mac Lane API. The fundamental-group witness is AddCircle.fundamentalGroupMulEquiv, and higher homotopy vanishing is supplied by AddCircle.subsingleton_homotopyGroup.

This realizes TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13, "K(G, 1) spaces", for circles.

Main declarations

• AddCircle.isAspherical: every real additive circle is aspherical.
• AddCircle.isEilenbergMacLaneSpaceOne: a nondegenerate real circle is a K(ℤ, 1).

theorem AddCircle.isAspherical (p : ℝ) (x : AddCircle p) : TauCeti.IsAspherical (AddCircle p) x

Every real additive circle is aspherical. The nonzero-period hypothesis is needed only for the later identification of its fundamental group with ℤ.

theorem AddCircle.isEilenbergMacLaneSpaceOne (p : ℝ) (hp : p ≠ 0) (x : AddCircle p) : TauCeti.IsEilenbergMacLaneSpaceOne (Multiplicative ℤ) (AddCircle p) x

A real additive circle with nonzero period is an Eilenberg--Mac Lane space of type K(ℤ, 1), with ℤ written multiplicatively to match the fundamental group.