The free action on Milnor's countable join

A group G acts on the vertices ⟨i, h⟩ of the countable join of copies of G by left multiplication of the label, g • ⟨i, h⟩ = ⟨i, g * h⟩. This relabelling is a simplicial automorphism of the join, so it extends affinely over each simplex to an action of G on universalGSpace G by homeomorphisms. In barycentric coordinates, (g • x) ⟨i, h⟩ = x ⟨i, g⁻¹ * h⟩.

The action is free, and it has the local disjointness asked of the domain of a quotient covering map. The open star of a vertex v, the set of points whose v-coordinate is positive, is carried by g onto the open star of ⟨v.1, g * v.2⟩. If g ≠ 1 these are open stars of two distinct vertices over the same index, and they are disjoint because the carrier of a point of a join contains at most one vertex over each index.

Main definitions

• TauCeti.instMulActionUniversalGSpace: the action of G on universalGSpace G.

Main results

• TauCeti.universalGSpace_smul_apply: the action on barycentric coordinates.
• TauCeti.instContinuousConstSMulUniversalGSpace: each translation is continuous.
• TauCeti.smul_mem_openStarRealization_universalGSpace_iff: translation permutes open stars.
• TauCeti.eq_one_of_image_smul_openStarRealization_inter_nonempty: the translates of an open star by distinct group elements are disjoint.
• TauCeti.instIsCancelSMulUniversalGSpace: the action is free.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.

@[instance_reducible]

noncomputable instance TauCeti.instSMulUniversalGSpace {G : Type u} [Group G] : SMul G (universalGSpace G)

A group acts on Milnor's countable join of copies of itself through the simplicial automorphisms ⟨i, h⟩ ↦ ⟨i, g * h⟩, extended affinely over each simplex.

theorem TauCeti.universalGSpace_smul_val {G : Type u} [Group G] (g : G) (x : universalGSpace G) : ↑(g • x) = Finsupp.mapDomain (fun (v : (_ : ℕ) × G) => ⟨v.fst, g * v.snd⟩) ↑x

Translation pushes barycentric coordinates forward along left multiplication of labels.

@[simp]

theorem TauCeti.universalGSpace_smul_apply {G : Type u} [Group G] (g : G) (x : universalGSpace G) (v : (_ : ℕ) × G) : ↑(g • x) v = ↑x ⟨v.fst, g⁻¹ * v.snd⟩

The barycentric coordinate of a translate at a vertex is the coordinate of the original point at the vertex obtained by translating the label back.

@[instance_reducible]

noncomputable instance TauCeti.instMulActionUniversalGSpace {G : Type u} [Group G] : MulAction G (universalGSpace G)

The action of a group on Milnor's countable join of copies of itself by relabelling vertices.

@[simp]

theorem TauCeti.universalGSpace_smul_vertex {G : Type u} [Group G] (g : G) (v : (_ : ℕ) × G) : g • (indexedJoin fun (x : ℕ) => G).vertex v = (indexedJoin fun (x : ℕ) => G).vertex ⟨v.fst, g * v.snd⟩

Translation sends a vertex of the countable join to the vertex with translated label.

theorem TauCeti.smul_universalGSpaceBasepoint {G : Type u} [Group G] (g : G) : g • universalGSpaceBasepoint G = (indexedJoin fun (x : ℕ) => G).vertex ⟨0, g⟩

Translating the base point of the countable join gives the vertex over index zero labelled by the translating element.

instance TauCeti.instContinuousConstSMulUniversalGSpace {G : Type u} [Group G] : ContinuousConstSMul G (universalGSpace G)

Each translation of Milnor's countable join is continuous.

theorem TauCeti.smul_mem_openStarRealization_universalGSpace_iff {G : Type u} [Group G] (g : G) (x : universalGSpace G) (v : (_ : ℕ) × G) : g • x ∈ (indexedJoin fun (x : ℕ) => G).openStarRealization v ↔ x ∈ (indexedJoin fun (x : ℕ) => G).openStarRealization ⟨v.fst, g⁻¹ * v.snd⟩

A translate lies in the open star of a vertex exactly when the original point lies in the open star of the vertex with translated-back label.

theorem TauCeti.eq_one_of_image_smul_openStarRealization_inter_nonempty {G : Type u} [Group G] (g : G) (v : (_ : ℕ) × G) (h : ((fun (x : (indexedJoin fun (x : ℕ) => G).Realization) => g • x) '' (indexedJoin fun (x : ℕ) => G).openStarRealization v ∩ (indexedJoin fun (x : ℕ) => G).openStarRealization v).Nonempty) : g = 1

The translates of the open star of a vertex by distinct group elements are disjoint: a point of the countable join cannot have positive coordinates at two distinct vertices over the same index.

instance TauCeti.instIsCancelSMulUniversalGSpace {G : Type u} [Group G] : IsCancelSMul G (universalGSpace G)

The action of a group on Milnor's countable join of copies of itself is free.

@[simp]

theorem MonoidHom.universalGSpaceMap_smul {G : Type u_1} {H : Type u_2} [Group G] [Group H] (φ : G →* H) (g : G) (x : TauCeti.universalGSpace G) : φ.universalGSpaceMap (g • x) = φ g • φ.universalGSpaceMap x

The map of Milnor total spaces induced by a homomorphism is equivariant for that homomorphism.