Tori as Eilenberg--Mac Lane spaces #
An arbitrary indexed product of real additive circles with nonzero periods is a
K(Π i, ℤ, 1).
These results derive directly from the Eilenberg--Mac Lane product API and the circle
calculation in TauCeti.AlgebraicTopology.UniversalCover.Circle.EilenbergMacLane.
This realizes TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13,
"K(G, 1) spaces", for arbitrary products of circles.
Main declarations #
AddCircle.isAspherical_pi: an indexed product of real circles is aspherical.AddCircle.isEilenbergMacLaneSpaceOne_pi: an indexed product of nondegenerate real circles is aK(Π i, ℤ, 1).
theorem
AddCircle.isAspherical_pi
{ι : Type u_1}
(p : ι → ℝ)
(x : (i : ι) → AddCircle (p i))
:
TauCeti.IsAspherical ((i : ι) → AddCircle (p i)) x
Every indexed product of real additive circles is aspherical.
theorem
AddCircle.isEilenbergMacLaneSpaceOne_pi
{ι : Type u_1}
(p : ι → ℝ)
(hp : ∀ (i : ι), p i ≠ 0)
(x : (i : ι) → AddCircle (p i))
:
TauCeti.IsEilenbergMacLaneSpaceOne (ι → Multiplicative ℤ) ((i : ι) → AddCircle (p i)) x
An indexed product of real additive circles with nonzero periods is an Eilenberg--Mac
Lane space of type K(Π i, ℤ, 1). No finiteness assumption on the index type is needed.