Milnor's classifying space as an orbit space

For a group G, classifyingSpace G is the quotient of Milnor's countable join universalGSpace G by the free action of G that relabels vertices, with the quotient topology. The orbit map classifyingSpaceProj G is a quotient covering map for G in the sense of Mathlib's IsQuotientCoveringMap: the open star of a vertex is a neighbourhood whose translates by distinct group elements are disjoint.

This file gives the orbit space the interface a user needs without unfolding the quotient. Two points of the countable join have the same image exactly when a unique group element carries one to the other, the fibre through a point is its orbit, a continuous G-invariant map descends to the orbit space, and, since the countable join is connected, the acting group is the deck transformation group of the orbit map.

The classifying space satisfies the standing hypotheses of covering-space theory: it is path-connected and locally path-connected, being a quotient of the countable join, which is both, and it is semilocally simply connected, being covered by the simply connected countable join.

Main definitions

• TauCeti.classifyingSpace: the orbit space of the countable join.
• TauCeti.classifyingSpaceProj: the orbit map.
• TauCeti.classifyingSpaceBasepoint: the image of the base point of the countable join.
• TauCeti.classifyingSpaceLift: descent of a continuous G-invariant map.
• TauCeti.classifyingSpaceDeckMulEquiv: G ≃* deck (classifyingSpaceProj G).

Main results

• TauCeti.isQuotientCoveringMap_classifyingSpaceProj: the orbit map is a quotient covering map for G.
• TauCeti.classifyingSpaceProj_eq_iff_existsUnique: two points have the same image exactly when a unique group element carries one to the other.
• TauCeti.preimage_classifyingSpaceProj_singleton: the fibre through a point is its orbit.
• TauCeti.instPathConnectedSpaceClassifyingSpace, TauCeti.instLocallyPathConnectedSpaceClassifyingSpace and TauCeti.instSemilocallySimplyConnectedSpaceClassifyingSpace: 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.

def TauCeti.classifyingSpace (G : Type u) [Group G] : Type u

Milnor's classifying space of a group G: the orbit space of the countable join of copies of G under the free action relabelling its vertices.

@[instance_reducible]

instance TauCeti.instTopologicalSpaceClassifyingSpace (G : Type u) [Group G] : TopologicalSpace (classifyingSpace G)

The classifying space carries the quotient topology of the countable join.

noncomputable def TauCeti.classifyingSpaceProj (G : Type u) [Group G] : universalGSpace G → classifyingSpace G

The orbit map from the countable join to the classifying space.

noncomputable def TauCeti.classifyingSpaceBasepoint (G : Type u) [Group G] : classifyingSpace G

The base point of the classifying space: the orbit of the vertex over index zero labelled by the unit.

@[simp]

theorem TauCeti.classifyingSpaceProj_universalGSpaceBasepoint (G : Type u) [Group G] : classifyingSpaceProj G (universalGSpaceBasepoint G) = classifyingSpaceBasepoint G

The base point of the classifying space is the image of the base point of the countable join.

theorem TauCeti.isQuotientMap_classifyingSpaceProj (G : Type u) [Group G] : Topology.IsQuotientMap (classifyingSpaceProj G)

The orbit map is a quotient map.

theorem TauCeti.continuous_classifyingSpaceProj (G : Type u) [Group G] : Continuous (classifyingSpaceProj G)

The orbit map is continuous.

theorem TauCeti.classifyingSpaceProj_surjective (G : Type u) [Group G] : Function.Surjective (classifyingSpaceProj G)

Every point of the classifying space is the orbit of a point of the countable join.

theorem TauCeti.classifyingSpaceProj_eq_iff {G : Type u} [Group G] {x y : universalGSpace G} : classifyingSpaceProj G x = classifyingSpaceProj G y ↔ x ∈ MulAction.orbit G y

Two points of the countable join have the same image in the classifying space exactly when they lie in the same orbit.

@[simp]

theorem TauCeti.classifyingSpaceProj_smul {G : Type u} [Group G] (g : G) (x : universalGSpace G) : classifyingSpaceProj G (g • x) = classifyingSpaceProj G x

Translation does not change the image in the classifying space.

theorem TauCeti.classifyingSpaceProj_eq_iff_existsUnique {G : Type u} [Group G] {x y : universalGSpace G} : classifyingSpaceProj G x = classifyingSpaceProj G y ↔ ∃! g : G, g • y = x

Two points of the countable join have the same image in the classifying space exactly when a unique group element carries the second to the first; uniqueness is freeness of the action.

theorem TauCeti.preimage_classifyingSpaceProj_singleton {G : Type u} [Group G] (x : universalGSpace G) : classifyingSpaceProj G ⁻¹' {classifyingSpaceProj G x} = MulAction.orbit G x

The fibre of the orbit map through a point of the countable join is the orbit of that point.

theorem TauCeti.isQuotientCoveringMap_classifyingSpaceProj (G : Type u) [Group G] : IsQuotientCoveringMap (classifyingSpaceProj G) G

The orbit map of Milnor's countable join is a quotient covering map. The open star of a vertex is a neighbourhood of each of its points whose translates by distinct group elements are disjoint.

instance TauCeti.instPathConnectedSpaceClassifyingSpace {G : Type u} [Group G] : PathConnectedSpace (classifyingSpace G)

The classifying space is path-connected, as the image of the path-connected countable join.

instance TauCeti.instLocallyPathConnectedSpaceClassifyingSpace {G : Type u} [Group G] : LocallyPathConnectedSpace (classifyingSpace G)

The classifying space is locally path-connected, as a quotient of the locally path-connected countable join.

instance TauCeti.instSemilocallySimplyConnectedSpaceClassifyingSpace {G : Type u} [Group G] : SemilocallySimplyConnectedSpace (classifyingSpace G)

The classifying space is semilocally simply connected, being covered by the simply connected countable join.

noncomputable def TauCeti.classifyingSpaceLift {G : Type u} [Group G] {X : Type u_1} [TopologicalSpace X] (f : C(universalGSpace G, X)) (hf : ∀ (g : G) (x : universalGSpace G), f (g • x) = f x) : C(classifyingSpace G, X)

A continuous map out of the countable join that is invariant under the group action descends to a continuous map out of the classifying space.

@[simp]

theorem TauCeti.classifyingSpaceLift_apply {G : Type u} [Group G] {X : Type u_1} [TopologicalSpace X] (f : C(universalGSpace G, X)) (hf : ∀ (g : G) (x : universalGSpace G), f (g • x) = f x) (x : universalGSpace G) : (classifyingSpaceLift f hf) (classifyingSpaceProj G x) = f x

The descended map agrees with the original map on the image of each point.

theorem TauCeti.classifyingSpace_continuousMap_ext {G : Type u} [Group G] {X : Type u_1} [TopologicalSpace X] {φ ψ : C(classifyingSpace G, X)} (h : ∀ (x : universalGSpace G), φ (classifyingSpaceProj G x) = ψ (classifyingSpaceProj G x)) : φ = ψ

Two continuous maps out of the classifying space agree once they agree on the image of the orbit map.

noncomputable def TauCeti.classifyingSpaceDeckMulEquiv (G : Type u) [Group G] : G ≃* ↥(deck (classifyingSpaceProj G))

The acting group is the deck transformation group of the orbit map. Translation by a group element is a deck transformation, and every deck transformation arises this way because the countable join is connected.

@[simp]

theorem TauCeti.classifyingSpaceDeckMulEquiv_apply (G : Type u) [Group G] (g : G) (x : universalGSpace G) : ↑((classifyingSpaceDeckMulEquiv G) g) x = g • x

The deck transformation attached to a group element is translation by that element.

@[simp]

theorem TauCeti.classifyingSpaceDeckMulEquiv_symm_apply (G : Type u) [Group G] (φ : ↥(deck (classifyingSpaceProj G))) (x : universalGSpace G) : (classifyingSpaceDeckMulEquiv G).symm φ • x = ↑φ x

A deck transformation of the orbit map is translation by the group element it corresponds to.