Milnor's classifying space is a K(G, 1)

The orbit map classifyingSpaceProj G from Milnor's countable join to classifyingSpace G is a quotient covering map for G whose total space is simply connected with vanishing higher homotopy groups. So classifyingSpace G is an Eilenberg--Mac Lane space of type K(G, 1), for every group G, with no finiteness, countability or presentation hypothesis.

The direction of the identification of π₁

Mathlib's IsQuotientCoveringMap.fundamentalGroupEquiv identifies the fundamental group of the base of a simply connected quotient covering map with the opposite of the acting group: a loop γ goes to op g when its lift starting at the chosen point e ends at g • e. Here this is composed with the inverse of MulEquiv.inv' G : G ≃* Gᵐᵒᵖ, so classifyingSpaceFundamentalGroupMulEquiv G sends a loop at the base point to g exactly when its lift starting at the vertex ⟨0, 1⟩ ends at the vertex ⟨0, g⁻¹⟩.

Main definitions

• TauCeti.classifyingSpaceFundamentalGroupMulEquiv: the isomorphism π₁(BG) ≃* G.
• TauCeti.universalGSpaceHomeomorphUniversalCover: the pointed homeomorphism over the classifying space between the countable join and the based-path universal cover.

Main results

• TauCeti.classifyingSpaceFundamentalGroupMulEquiv_apply_eq_iff: the direction of the identification, through the monodromy of the orbit map.
• TauCeti.isEilenbergMacLaneSpaceOne_classifyingSpace: the classifying space is a K(G, 1).
• TauCeti.exists_isEilenbergMacLaneSpaceOne: every group has a K(G, 1), which moreover satisfies the standing hypotheses of covering-space theory.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 1.B.

noncomputable def TauCeti.classifyingSpaceFundamentalGroupMulEquiv (G : Type u) [Group G] : FundamentalGroup (classifyingSpace G) (classifyingSpaceBasepoint G) ≃* G

The fundamental group of the classifying space is G. A loop at the base point goes to g exactly when its lift starting at the vertex ⟨0, 1⟩ of the countable join ends at the vertex ⟨0, g⁻¹⟩; see classifyingSpaceFundamentalGroupMulEquiv_apply_eq_iff.

theorem TauCeti.classifyingSpaceFundamentalGroupMulEquiv_apply_eq_iff {G : Type u} [Group G] {γ : FundamentalGroup (classifyingSpace G) (classifyingSpaceBasepoint G)} {g : G} : (classifyingSpaceFundamentalGroupMulEquiv G) γ = g ↔ ↑(⋯.monodromy γ.asHom ⟨universalGSpaceBasepoint G, ⋯⟩) = (indexedJoin fun (x : ℕ) => G).vertex ⟨0, g⁻¹⟩

A loop at the base point of the classifying space corresponds to g exactly when its monodromy carries the vertex ⟨0, 1⟩ of the countable join to the vertex ⟨0, g⁻¹⟩.

theorem TauCeti.classifyingSpaceFundamentalGroupMulEquiv_apply_mk_eq {G : Type u} [Group G] {γ : Path (classifyingSpaceBasepoint G) (classifyingSpaceBasepoint G)} {Γ : C(↑unitInterval, universalGSpace G)} {g : G} (hΓ : classifyingSpaceProj G ∘ ⇑Γ = ⇑γ) (hΓ₀ : Γ 0 = universalGSpaceBasepoint G) (hΓ₁ : Γ 1 = (indexedJoin fun (x : ℕ) => G).vertex ⟨0, g⁻¹⟩) : (classifyingSpaceFundamentalGroupMulEquiv G) { asHom := Path.Homotopic.Quotient.mk γ } = g

A loop at the base point of the classifying space whose lift starting at the vertex ⟨0, 1⟩ of the countable join ends at the vertex ⟨0, g⁻¹⟩ corresponds to g.

theorem TauCeti.isEilenbergMacLaneSpaceOne_classifyingSpace (G : Type u) [Group G] : IsEilenbergMacLaneSpaceOne G (classifyingSpace G) (classifyingSpaceBasepoint G)

Milnor's classifying space is a K(G, 1): it is path-connected, its higher homotopy groups vanish, and its fundamental group is G.

theorem TauCeti.subsingleton_homotopyGroup_classifyingSpace (G : Type u) [Group G] (n : ℕ) (x : classifyingSpace G) : Subsingleton (HomotopyGroup.Pi (n + 2) (classifyingSpace G) x)

Every homotopy group of the classifying space in dimension at least two is trivial, at every base point.

theorem TauCeti.exists_isEilenbergMacLaneSpaceOne (G : Type u) [Group G] : ∃ (X : Type u) (x : TopologicalSpace X) (x_1 : X), LocallyPathConnectedSpace X ∧ SemilocallySimplyConnectedSpace X ∧ IsEilenbergMacLaneSpaceOne G X x_1

Every group has a K(G, 1), in its own universe, satisfying the standing hypotheses of covering-space theory: local path-connectedness and semilocal simple connectivity. No hypothesis on the group is needed.

noncomputable def TauCeti.universalGSpaceHomeomorphUniversalCover (G : Type u) [Group G] : universalGSpace G ≃ₜ UniversalCover (classifyingSpaceBasepoint G)

The countable join is the universal cover of the classifying space. The pointed homeomorphism over classifyingSpace G from the countable join, based at the vertex ⟨0, 1⟩, to the based-path universal cover, based at the class of the constant path.

@[simp]

theorem TauCeti.universalGSpaceHomeomorphUniversalCover_basepoint (G : Type u) [Group G] : (universalGSpaceHomeomorphUniversalCover G) (universalGSpaceBasepoint G) = ↑(UniversalCover.basepointLift (classifyingSpaceBasepoint G))

The comparison homeomorphism carries the base point of the countable join to the class of the constant path.

@[simp]

theorem TauCeti.proj_universalGSpaceHomeomorphUniversalCover (G : Type u) [Group G] (x : universalGSpace G) : ((universalGSpaceHomeomorphUniversalCover G) x).proj = classifyingSpaceProj G x

The comparison homeomorphism lies over the classifying space.

theorem TauCeti.eq_universalGSpaceHomeomorphUniversalCover {G : Type u} [Group G] {f : C(universalGSpace G, UniversalCover (classifyingSpaceBasepoint G))} (hf₀ : f (universalGSpaceBasepoint G) = ↑(UniversalCover.basepointLift (classifyingSpaceBasepoint G))) (hf : UniversalCover.proj ∘ ⇑f = classifyingSpaceProj G) : f = ↑(universalGSpaceHomeomorphUniversalCover G)

The comparison homeomorphism is the only continuous map from the countable join to the universal cover that lies over the classifying space and preserves the base points.