Maps of simplices in Milnor's countable join

A homomorphism sends a simplex of the countable join to a simplex of the same dimension, even when the homomorphism is not injective: distinct vertices of a simplex have distinct indices, which the map preserves. The increasing-index orientation is preserved as well. Consequently the map commutes with deleting vertices and with forgetting indices to obtain the tuple indexing a standard-resolution generator.

The characteristic-map formula identifies this cell map with the existing continuous map MonoidHom.universalGSpaceMap. These formulas supply the combinatorial input to naturality of the comparison between join chains and the standard resolution. The relabelling map is also the realization of MonoidHom.universalGSpaceSimplicialMap, so its restriction MonoidHom.universalGSpaceCellularMap to the universal subsets used by cellular chains is cellular, as proved by MonoidHom.isCellular_universalGSpaceCellularMap.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.
• K. S. Brown, Cohomology of Groups, Springer, 1982, Chapter I.

def MonoidHom.universalGSpaceSimplicialMap {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) : (TauCeti.indexedJoin fun (x : ℕ) => G).SimplicialMap (TauCeti.indexedJoin fun (x : ℕ) => H).toPreAbstractSimplicialComplex

Relabelling vertices as a simplicial map for the increasing-index vertex orders. This uses the decidable equality of those orders, so it can be passed directly to the ordered-cell and cellular-chain comparison APIs.

@[simp]

theorem MonoidHom.universalGSpaceSimplicialMap_apply {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) (v : (_ : ℕ) × G) : φ.universalGSpaceSimplicialMap v = ⟨v.fst, φ v.snd⟩

The simplicial map applies the homomorphism to the label and preserves the index.

theorem MonoidHom.universalGSpaceSimplicialMap_strictMonoOn {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : StrictMonoOn ⇑φ.universalGSpaceSimplicialMap ↑↑↑c

Relabelling is strictly increasing on each simplex for the increasing-index orders, even if the homomorphism is not injective.

noncomputable def MonoidHom.universalGSpaceCellMap {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : (TauCeti.indexedJoin fun (x : ℕ) => H).RealizationCell n

Apply a homomorphism to the labels of a simplex, preserving its indices and dimension.

theorem MonoidHom.universalGSpaceCellMap_def {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : φ.universalGSpaceCellMap c = c.map φ.universalGSpaceSimplicialMap ⋯

The cell map is induced by the ordered simplicial map.

@[simp]

theorem MonoidHom.universalGSpaceCellMap_val {G : Type u} {H : Type v} [MulOne G] [MulOne H] [DecidableEq ((_ : ℕ) × H)] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : ↑↑(φ.universalGSpaceCellMap c) = Finset.image (fun (v : (_ : ℕ) × G) => ⟨v.fst, φ v.snd⟩) ↑↑c

The underlying face is the image under relabelling vertices.

@[simp]

theorem MonoidHom.universalGSpaceCellMap_vertexEmbedding {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) (j : Fin (n + 1)) : (φ.universalGSpaceCellMap c).vertexEmbedding j = ⟨(c.vertexEmbedding j).fst, φ (c.vertexEmbedding j).snd⟩

Relabelling preserves the increasing-index vertex enumeration.

@[simp]

theorem MonoidHom.universalGSpaceCellLabels_universalGSpaceCellMap {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : TauCeti.universalGSpaceCellLabels (φ.universalGSpaceCellMap c) = ⇑φ ∘ TauCeti.universalGSpaceCellLabels c

The tuple of labels of an image simplex is the image of its tuple of labels.

@[simp]

theorem MonoidHom.universalGSpaceCellMap_face {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell (n + 1)) (j : Fin (n + 2)) : φ.universalGSpaceCellMap (c.face j) = (φ.universalGSpaceCellMap c).face j

Relabelling commutes with deleting the vertex at a specified position.

@[simp]

theorem MonoidHom.universalGSpaceCellMap_id {G : Type u} [MulOne G] {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : (id G).universalGSpaceCellMap c = c

Identity homomorphisms fix simplices.

@[simp]

theorem MonoidHom.universalGSpaceCellMap_comp {G : Type u} {H : Type v} {K : Type w} [MulOne G] [MulOne H] [MulOne K] (ψ : H →* K) (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : (ψ.comp φ).universalGSpaceCellMap c = ψ.universalGSpaceCellMap (φ.universalGSpaceCellMap c)

Relabelling simplices respects composition of homomorphisms.

@[simp]

theorem MonoidHom.universalGSpaceCellMap_smul {G : Type u} {H : Type v} [Group G] [Group H] (φ : G →* H) {n : ℕ} (g : G) (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) : φ.universalGSpaceCellMap (g • c) = φ g • φ.universalGSpaceCellMap c

Relabelling intertwines translation by a group element with translation by its image.

@[reducible, inline]

noncomputable abbrev MonoidHom.universalGSpaceCellMulActionHom {G : Type u} {H : Type v} [Group G] [Group H] (φ : G →* H) (n : ℕ) : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n →ₑ[⇑φ] (TauCeti.indexedJoin fun (x : ℕ) => H).RealizationCell n

Relabelling simplices as a map equivariant along the group homomorphism.

@[simp]

theorem MonoidHom.universalGSpaceCellMulActionHom_id {G : Type u} [Group G] (n : ℕ) : (id G).universalGSpaceCellMulActionHom n = MulActionHom.id G

The identity homomorphism gives the identity equivariant map on simplices.

@[simp]

theorem MonoidHom.universalGSpaceCellMulActionHom_comp {G : Type u} {H : Type v} {K : Type w} [Group G] [Group H] [Group K] (ψ : H →* K) (φ : G →* H) (n : ℕ) : (ψ.comp φ).universalGSpaceCellMulActionHom n = (ψ.universalGSpaceCellMulActionHom n).comp (φ.universalGSpaceCellMulActionHom n)

Equivariant relabelling of simplices respects composition.

@[simp]

theorem MonoidHom.universalGSpaceSimplicialMap_realizationMap {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) : φ.universalGSpaceSimplicialMap.realizationMap = φ.universalGSpaceMap

The ordered simplicial map realizes to the usual continuous map of Milnor joins.

theorem MonoidHom.universalGSpaceMap_characteristicMap {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) {n : ℕ} (c : (TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) (x : Fin n → ℝ) : φ.universalGSpaceMap (↑c.characteristicMap x) = ↑(φ.universalGSpaceCellMap c).characteristicMap x

The continuous total-space map carries each characteristic map to the characteristic map of the relabelled simplex, with the same disk coordinates.

noncomputable def MonoidHom.universalGSpaceCellularMap {G H : Type u} [MulOne G] [MulOne H] (φ : G →* H) : ↧↑Set.univ ⟶ ↧↑Set.univ

The map of Milnor joins on the universal subsets used by cellular chains.

@[simp]

theorem MonoidHom.universalGSpaceCellularMap_apply {G H : Type u} [MulOne G] [MulOne H] (φ : G →* H) (x : ↑Set.univ) : ↑((CategoryTheory.ConcreteCategory.hom φ.universalGSpaceCellularMap) x) = φ.universalGSpaceMap ↑x

The universal-subset map agrees with the continuous map on underlying points.

theorem MonoidHom.universalGSpaceSimplicialMap_restrictPreimage {G H : Type u} [MulOne G] [MulOne H] (φ : G →* H) : TopCat.ofHom (φ.universalGSpaceSimplicialMap.realizationMap.restrictPreimage Set.univ) = φ.universalGSpaceCellularMap

Restricting the realized simplicial map to the universal subset gives the cellular map.

theorem MonoidHom.isCellular_universalGSpaceCellularMap {G H : Type u} [MulOne G] [MulOne H] (φ : G →* H) : TauCeti.IsCellular Set.univ Set.univ φ.universalGSpaceCellularMap

The continuous map on Milnor joins preserves the simplicial CW filtrations. The map is restricted to the universal subsets used by cellular chains.