The CW structures on Milnor's countable join and classifying space

The realization of a simplicial complex is a CW complex whose n-cells are its faces with n + 1 vertices, once a linear order on the vertices fixes the characteristic maps. The vertices ⟨i, h⟩ of a face of the countable join universalGSpace G have pairwise distinct indices i, so any order on the vertices that compares different indices as ℕ does orders every face by index. We fix one such order, universalGSpaceVertexOrder G, lexicographic for an arbitrary well-order on G. The characteristic maps of the resulting CW structure on universalGSpace G only compare vertices of a common face, so they enumerate each simplex by increasing index, whatever the order on G.

Translation by g : G relabels the vertices of a face, ⟨i, h⟩ ↦ ⟨i, g * h⟩, without changing their indices. So it preserves the order on each face, and carries the characteristic map of each cell exactly onto the characteristic map of the translated cell, not merely up to orientation. This is an action of G on the n-cells, and it is free: if g ≠ 1, translation by g changes the label of every vertex. Hence G permutes the open cells, closed cells and cell frontiers of universalGSpace G, carrying an open cell onto itself only for g = 1. This is also the input for describing the cellular chains of universalGSpace G as free modules over the group ring.

The CW structure descends along the quotient covering map classifyingSpaceProj G (IsQuotientCoveringMap.cwComplexQuotient), so the classifying space classifyingSpace G is a Hausdorff CW complex whose n-cells are the G-orbits of the n-simplices of the countable join. Since translation carries characteristic maps exactly onto characteristic maps and does not move points of the classifying space, the characteristic map of an orbit is the characteristic map of any of its simplices followed by the orbit map; it does not depend on the chosen representative.

Main definitions

• TauCeti.universalGSpaceVertexOrder: a linear order on the vertices of the countable join extending the order of the indices.
• TauCeti.instCWComplexUniversalGSpace: the CW structure on universalGSpace G whose cells are the simplices of the countable join, each enumerated by increasing index.
• TauCeti.instMulActionRealizationCellUniversalGSpace: the action of G on the simplices of the countable join.
• TauCeti.instMulActionCellUniversalGSpace: the corresponding action on the cells of the CW structure.
• TauCeti.instCWComplexClassifyingSpace: the CW structure on classifyingSpace G.
• TauCeti.classifyingSpaceCellEquiv: its n-cells are the G-orbits of n-simplices of the countable join.

Main results

• TauCeti.universalGSpaceVertexOrder_lt_iff: on a face, the vertex order is the order of the indices.
• TauCeti.face_smul_universalGSpace: translation commutes with taking faces of simplices.
• TauCeti.smul_characteristicMap_universalGSpace and TauCeti.smul_map_universalGSpace: translation carries characteristic maps to characteristic maps.
• TauCeti.smul_openCell_universalGSpace, TauCeti.smul_closedCell_universalGSpace and TauCeti.smul_cellFrontier_universalGSpace: translation permutes the open cells, closed cells and cell frontiers.
• TauCeti.instIsCancelSMulCellUniversalGSpace and TauCeti.eq_one_of_smul_openCell_universalGSpace_eq: the action on cells is free.
• TauCeti.instT2SpaceClassifyingSpace: the classifying space is Hausdorff.
• TauCeti.map_classifyingSpaceCellEquiv_symm_mk: the characteristic map of the orbit of a simplex is its characteristic map followed by the orbit map.
• TauCeti.openCell_classifyingSpaceCellEquiv_symm_mk, TauCeti.closedCell_classifyingSpaceCellEquiv_symm_mk and TauCeti.cellFrontier_classifyingSpaceCellEquiv_symm_mk: the open cells, closed cells and cell frontiers of the classifying space are the images of those of the countable join.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.
• T. tom Dieck, Transformation Groups, de Gruyter, 1987, Section II.1.
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 0.

@[instance_reducible]

noncomputable def TauCeti.universalGSpaceVertexOrder (G : Type u) : LinearOrder ((_ : ℕ) × G)

A linear order on the vertices ⟨i, h⟩ of the countable join of copies of G: vertices with different indices are compared by their indices, and vertices with the same index by an arbitrary well-order of G. Only the first clause matters for the faces of the join, whose vertices have pairwise distinct indices.

theorem TauCeti.universalGSpaceVertexOrder_lt_of_fst_lt {G : Type u} {v w : (_ : ℕ) × G} (h : v.fst < w.fst) : v < w

Vertices with smaller index come first.

theorem TauCeti.universalGSpaceVertexOrder_lt_iff {G : Type u} {σ : Finset ((_ : ℕ) × G)} (hσ : σ ∈ indexedJoin fun (x : ℕ) => G) {v w : (_ : ℕ) × G} (hv : v ∈ σ) (hw : w ∈ σ) : v < w ↔ v.fst < w.fst

On a face of the countable join, the vertex order is the order of the indices.

theorem TauCeti.strictMono_fst_vertexEmbedding_universalGSpace {G : Type u} {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : StrictMono fun (k : Fin (n + 1)) => (c.vertexEmbedding k).fst

The increasing enumeration of the vertices of a cell of the countable join enumerates them by increasing index.

@[instance_reducible]

noncomputable instance TauCeti.instCWComplexUniversalGSpace {G : Type u} : Topology.CWComplex Set.univ

The CW structure on Milnor's countable join: its n-cells are the simplices of the join with n + 1 vertices, and the characteristic map of a simplex enumerates its vertices by increasing index.

theorem TauCeti.map_toPerm_mem_indexedJoin {G : Type u} [Group G] (g : G) {σ : Finset ((_ : ℕ) × G)} (hσ : σ ∈ indexedJoin fun (x : ℕ) => G) : Finset.map (Equiv.toEmbedding (MulAction.toPerm g)) σ ∈ indexedJoin fun (x : ℕ) => G

The translate of a face of the countable join by g is a face.

@[instance_reducible]

instance TauCeti.instSMulRealizationCellUniversalGSpace {G : Type u} [Group G] {n : ℕ} : SMul G ((indexedJoin fun (x : ℕ) => G).RealizationCell n)

A group acts on the simplices of Milnor's countable join of copies of itself by translating the labels of their vertices.

theorem TauCeti.smul_realizationCell_face {G : Type u} [Group G] {n : ℕ} (g : G) (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : ↑↑(g • c) = Finset.map (Equiv.toEmbedding (MulAction.toPerm g)) ↑↑c

The face of a translated simplex is the translated face.

@[simp]

theorem TauCeti.mem_smul_realizationCell_face_iff {G : Type u} [Group G] {n : ℕ} (g : G) (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (v : (_ : ℕ) × G) : v ∈ ↑↑(g • c) ↔ g⁻¹ • v ∈ ↑↑c

A vertex lies in the face of a translated simplex exactly when its translate back lies in the face of the original simplex.

@[instance_reducible]

instance TauCeti.instMulActionRealizationCellUniversalGSpace {G : Type u} [Group G] {n : ℕ} : MulAction G ((indexedJoin fun (x : ℕ) => G).RealizationCell n)

The translation of simplices is an action of the group.

instance TauCeti.instIsCancelSMulRealizationCellUniversalGSpace {G : Type u} [Group G] {n : ℕ} : IsCancelSMul G ((indexedJoin fun (x : ℕ) => G).RealizationCell n)

The action of a group on the simplices of the countable join is free: a simplex fixed by g has a vertex v, and g • v is a vertex of the same simplex over the same index as v, so g • v = v and g = 1.

theorem TauCeti.smul_characteristicMap_universalGSpace {G : Type u} [Group G] {n : ℕ} (g : G) (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (x : Fin n → ℝ) : g • ↑c.characteristicMap x = ↑(g • c).characteristicMap x

Translation carries characteristic maps to characteristic maps. For a simplex c of the countable join, translating its characteristic map by g gives the characteristic map of g • c, on the whole domain.

@[simp]

theorem TauCeti.vertexEmbedding_smul_universalGSpace {G : Type u} [Group G] {n : ℕ} (g : G) (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (j : Fin (n + 1)) : (g • c).vertexEmbedding j = g • c.vertexEmbedding j

Translation preserves the index-ordered enumeration of each simplex of the countable join.

@[simp]

theorem TauCeti.face_smul_universalGSpace {G : Type u} [Group G] {n : ℕ} (g : G) (c : (indexedJoin fun (x : ℕ) => G).RealizationCell (n + 1)) (j : Fin (n + 2)) : (g • c).face j = g • c.face j

Translation commutes with deleting a vertex: the j-th face of a translated simplex of the countable join is the translate of its j-th face.

@[instance_reducible]

noncomputable instance TauCeti.instMulActionCellUniversalGSpace {G : Type u} [Group G] {n : ℕ} : MulAction G (Topology.RelCWComplex.cell Set.univ n)

The action of a group on the cells of the CW structure on the countable join, through the identification of the cells with the simplices of the join.

@[simp]

theorem TauCeti.realizationCellEquiv_smul {G : Type u} [Group G] {n : ℕ} (g : G) (i : Topology.RelCWComplex.cell Set.univ n) : ((indexedJoin fun (x : ℕ) => G).realizationCellEquiv n) (g • i) = g • ((indexedJoin fun (x : ℕ) => G).realizationCellEquiv n) i

The identification of the cells of the countable join with its simplices is equivariant.

@[simp]

theorem TauCeti.realizationCellEquiv_symm_smul {G : Type u} [Group G] {n : ℕ} (g : G) (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : ((indexedJoin fun (x : ℕ) => G).realizationCellEquiv n).symm (g • c) = g • ((indexedJoin fun (x : ℕ) => G).realizationCellEquiv n).symm c

The inverse identification of the simplices of the countable join with its cells is equivariant.

theorem TauCeti.smul_map_universalGSpace {G : Type u} [Group G] {n : ℕ} (g : G) (i : Topology.RelCWComplex.cell Set.univ n) (x : Fin n → ℝ) : g • ↑(Topology.RelCWComplex.map n i) x = ↑(Topology.RelCWComplex.map n (g • i)) x

Translation carries characteristic maps to characteristic maps: translating the characteristic map of a cell of the countable join by g gives the characteristic map of the translated cell.

theorem TauCeti.smul_openCell_universalGSpace {G : Type u} [Group G] {n : ℕ} (g : G) (i : Topology.RelCWComplex.cell Set.univ n) : g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n (g • i)

Translation carries each open cell of the countable join onto the open cell of the translated cell.

theorem TauCeti.smul_closedCell_universalGSpace {G : Type u} [Group G] {n : ℕ} (g : G) (i : Topology.RelCWComplex.cell Set.univ n) : g • Topology.RelCWComplex.closedCell n i = Topology.RelCWComplex.closedCell n (g • i)

Translation carries each closed cell of the countable join onto the closed cell of the translated cell.

theorem TauCeti.smul_cellFrontier_universalGSpace {G : Type u} [Group G] {n : ℕ} (g : G) (i : Topology.RelCWComplex.cell Set.univ n) : g • Topology.RelCWComplex.cellFrontier n i = Topology.RelCWComplex.cellFrontier n (g • i)

Translation carries each cell frontier of the countable join onto the cell frontier of the translated cell.

instance TauCeti.instIsCancelSMulCellUniversalGSpace {G : Type u} [Group G] {n : ℕ} : IsCancelSMul G (Topology.RelCWComplex.cell Set.univ n)

The action of a group on the cells of the countable join is free.

theorem TauCeti.eq_one_of_smul_openCell_universalGSpace_eq {G : Type u} [Group G] {n : ℕ} {g : G} {i : Topology.RelCWComplex.cell Set.univ n} (h : g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i) : g = 1

The action on the cells of the countable join is free: translation by g carries an open cell onto itself only when g = 1.

@[instance_reducible]

noncomputable instance TauCeti.instCWComplexClassifyingSpace {G : Type u} [Group G] : Topology.CWComplex Set.univ

Milnor's classifying space is a CW complex. Its n-cells are the G-orbits of the n-simplices of the countable join (TauCeti.classifyingSpaceCellEquiv), and the characteristic map of an orbit is the characteristic map of any of its simplices followed by the orbit map (TauCeti.map_classifyingSpaceCellEquiv_symm_mk).

instance TauCeti.instT2SpaceClassifyingSpace {G : Type u} [Group G] : T2Space (classifyingSpace G)

Milnor's classifying space is Hausdorff, as the orbit space of a free cellular action on a Hausdorff CW complex.

noncomputable def TauCeti.classifyingSpaceCellEquiv (G : Type u) [Group G] (n : ℕ) : Topology.RelCWComplex.cell Set.univ n ≃ MulAction.orbitRel.Quotient G ((indexedJoin fun (x : ℕ) => G).RealizationCell n)

The cells of the classifying space are the orbits of simplices. The n-cells of classifyingSpace G correspond to the G-orbits of the simplices of the countable join with n + 1 vertices.

@[simp]

theorem TauCeti.map_classifyingSpaceCellEquiv_symm_mk {G : Type u} [Group G] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (x : Fin n → ℝ) : ↑(Topology.RelCWComplex.map n ((classifyingSpaceCellEquiv G n).symm (Quotient.mk'' c))) x = classifyingSpaceProj G (↑c.characteristicMap x)

The characteristic maps of the classifying space. The characteristic map of the orbit of a simplex c of the countable join is the characteristic map of c followed by the orbit map, whichever simplex of the orbit is chosen.

@[simp]

theorem TauCeti.openCell_classifyingSpaceCellEquiv_symm_mk {G : Type u} [Group G] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : Topology.RelCWComplex.openCell n ((classifyingSpaceCellEquiv G n).symm (Quotient.mk'' c)) = classifyingSpaceProj G '' {x : universalGSpace G | (↑x).support = ↑↑c}

The open cell of the orbit of a simplex of the countable join is the image of the points whose support is that simplex.

@[simp]

theorem TauCeti.closedCell_classifyingSpaceCellEquiv_symm_mk {G : Type u} [Group G] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : Topology.RelCWComplex.closedCell n ((classifyingSpaceCellEquiv G n).symm (Quotient.mk'' c)) = classifyingSpaceProj G '' {x : universalGSpace G | (↑x).support ⊆ ↑↑c}

The closed cell of the orbit of a simplex of the countable join is the image of the closed simplex.

@[simp]

theorem TauCeti.cellFrontier_classifyingSpaceCellEquiv_symm_mk {G : Type u} [Group G] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : Topology.RelCWComplex.cellFrontier n ((classifyingSpaceCellEquiv G n).symm (Quotient.mk'' c)) = classifyingSpaceProj G '' {x : universalGSpace G | (↑x).support ⊂ ↑↑c}

The cell frontier of the orbit of a simplex of the countable join is the image of the points supported on its proper faces.