4 Proper actions and the universal proper space
This chapter begins with the verified topology of proper discrete-group actions and their subgroup fixed-point spaces. Continuous equivariant maps, homotopies, and their fixed-point restrictions are also verified. The results below add homogeneous orbits, proper orbit cells, the fixed-point criterion, a finite-group point model, conditional uniqueness, and directed cocompact pieces for a given space. Equivariant CW attachment, closed skeletal inclusions, Hausdorffness, and properness for countable discrete groups are verified. The cellular mapping property is also verified for targets satisfying the fixed-point criterion. A countable proper zero-skeleton containing a fixed vertex for every finite subgroup is now constructed. For finite groups, a genuine locally compact second-countable universal proper CW model is verified. The concrete weak labeled join is now constructed, and its properness and full subgroup fixed-point criterion are verified for arbitrary discrete groups. Its genuine CW attachment witnesses are also verified. For every countable discrete group, the staircase prism realization is equivariantly homeomorphic to a locally compact second-countable telescope, giving a genuine universal proper CW model with all required properties on the same space.
4.1 Proper actions and compact transporters
For a topological group \(\Gamma \) acting on a topological space \(X\), the action is proper when
is a proper map. This is exactly Mathlib’s ProperSMul predicate; it includes continuity of the action. In the applications below \(\Gamma \) is discrete. Finite stabilizers alone do not replace properness.
For subsets \(K,L\subseteq X\), define the transporter
For a proper action of a discrete group, \(T(K,L)\) is finite whenever \(K,L\) are compact. If \(X\) is locally compact Hausdorff and the action is continuous, the converse holds. Under these hypotheses properness is also equivalent to compactness of \(\alpha ^{-1}(C)\) for every compact \(C\subseteq X\times X\).
The first projection maps the compact set \(\alpha ^{-1}(L\times K)\) onto \(T(K,L)\). Compact subsets of a discrete space are finite. Conversely, for compact \(C\subseteq X\times X\), its coordinate projections are compact. The inverse image of \(C\) is a closed subset of the product of a finite transporter and the second coordinate projection. The pinned Mathlib proper-map and compact-transporter criteria formalize these implications on locally compact Hausdorff spaces.
Every point stabilizer \(\Gamma _x\) in a proper discrete-group action is finite. This implication does not require local compactness of \(X\).
The stabilizer is \(T(\{ x\} ,\{ x\} )\), and singletons are compact.
A proper action has Hausdorff orbit space \(X/\Gamma \). If \(X\) is locally compact, then \(X/\Gamma \) is locally compact as well.
Use Mathlib’s Hausdorff quotient theorem for proper actions. The orbit projection is an open quotient map for a continuous group action, and local compactness descends through an open quotient map.
Restricting a proper discrete-group action to any subgroup preserves properness.
Every subgroup of a discrete group is closed. Apply the proper-action restriction theorem for a closed embedding of groups.
Every continuous action of a finite discrete group on a locally compact Hausdorff space is proper. Left translation of a topological group on itself is proper. If a discrete group acts properly on a nonempty compact space, the group is finite.
For a finite group every transporter is finite. For left translation, \((g,x)\mapsto (gx,x)\) is a homeomorphism with inverse \((y,x)\mapsto (yx^{-1},x)\). For the last assertion, \(T(X,X)=\Gamma \) is finite by compactness and nonemptiness.
4.2 Subgroup fixed-point spaces
For a subgroup \(H\leq \Gamma \), let
with the subspace topology. The Lean definition uses Mathlib’s existing MulAction.fixedPoints.
A point \(x\) lies in \(X^H\) exactly when \(H\leq \Gamma _x\). If \(H\leq K\), then \(X^K\subseteq X^H\), and \(X^{\{ 1\} }=X\).
Unfold the fixed-point and stabilizer conditions and use subgroup inclusion.
For an action by continuous translations on a Hausdorff space, \(X^H\) is closed for every subgroup \(H\). If \(X\) is locally compact, so is \(X^H\).
The fixed-point set is the intersection, over \(h\in H\), of the closed equalizers of \(x\mapsto hx\) and \(x\mapsto x\). Closed subspaces of locally compact spaces are locally compact.
For a proper discrete-group action, any subgroup fixing a point is finite. Consequently \(X^H=\varnothing \) whenever \(H\) is infinite.
If \(x\in X^H\), then \(H\) is a subgroup of the finite group \(\Gamma _x\).
Properness does not imply contractibility of fixed-point spaces for finite subgroups. That is additional structure required of a universal proper model.
4.3 Equivariant maps and homotopies
For topological spaces \(X,Y\) with \(\Gamma \)-actions, a continuous equivariant map \(f:X\to Y\) is a continuous map satisfying \(f(gx)=gf(x)\). The underlying equivariant function uses Mathlib’s MulActionHom. The constructions in this section do not require properness, a discrete group topology, local compactness, or Hausdorffness.
Continuous equivariant maps have identity and associative composition, with both identity laws. Equality of maps is determined pointwise.
Use the identity and composition of continuous maps. Equivariance is preserved because \(g(f(ax))=g(af(x))=ag(f(x))\). The laws follow pointwise.
For every subgroup \(H\leq \Gamma \), an equivariant map \(f:X\to Y\) restricts to a continuous map \(f^H:X^H\to Y^H\). Restriction preserves identity and composition. The subgroup need not be normal.
For \(h\in H\) and \(x\in X^H\), one has \(hf(x)=f(hx)=f(x)\). Continuity follows from the subspace topology; the laws follow pointwise.
An equivariant homotopy from \(f_0\) to \(f_1\) is a jointly continuous map \(F:[0,1]\times X\to Y\) with \(F(0,x)=f_0(x)\), \(F(1,x)=f_1(x)\), and \(F(t,gx)=gF(t,x)\). The interval has trivial action. Write \(f_0\simeq _\Gamma f_1\) when such a homotopy exists. The Lean definition specializes Mathlib’s ContinuousMap.HomotopyWith.
Equivariant homotopy is reflexive, symmetric, transitive, and compatible with composition. Every time slice of an equivariant homotopy is a continuous equivariant map, with the specified maps at times zero and one.
Use constant homotopies, time reversal, and concatenation on the two half intervals. Composition is \((G\circ F)(t,x)=G(t,F(t,x))\). Joint continuity follows from Mathlib’s homotopy operations; equivariance holds at each time. Restriction to a time slice is continuous.
An equivariant homotopy \(F:f_0\simeq _\Gamma f_1\) restricts to an ordinary continuous homotopy \(F^H:f_0^H\simeq f_1^H\) for every subgroup \(H\). Restriction preserves constant homotopies, reversal, concatenation with the chosen half-interval parametrization, and composition of homotopies.
At each time equivariance ensures \(F(t,X^H)\subseteq Y^H\). The map into \(Y^H\) is jointly continuous by the subspace topology, and the endpoint identities hold as equalities of subtype elements. The operation laws follow from their formulas, splitting the two time intervals for concatenation.
An equivariant homotopy equivalence between \(X\) and \(Y\) consists of continuous equivariant maps \(f:X\to Y\) and \(g:Y\to X\) with \(gf\simeq _\Gamma \operatorname {id}_X\) and \(fg\simeq _\Gamma \operatorname {id}_Y\).
Equivariant homotopy equivalences have identity, reversal, and composition. Every equivariant homotopy equivalence \(X\simeq _\Gamma Y\) induces an ordinary homotopy equivalence \(X^H\simeq Y^H\) for every subgroup \(H\).
Compose the equivariant maps and their inverse homotopies to obtain the three operations. Restrict both maps and both inverse homotopies to the fixed-point spaces, using the proved identity and composition laws.
4.4 Homogeneous orbits and orbit cells
For a discrete group \(\Gamma \), any subgroup \(H\), and any \(\Gamma \)-space \(X\), evaluation at \(H\in \Gamma /H\) is a bijection
for continuous equivariant maps. Its inverse sends \(x\) to \(gH\mapsto gx\). The bijection is natural under continuous equivariant maps in \(X\). No normality or finiteness hypothesis on \(H\) is required.
The fixed-point condition makes the orbit map independent of the coset representative. The orbit is discrete, so the descended map is continuous. Equivariance determines a map by its value at the identity coset.
The left action on \(\Gamma /H\) is proper if and only if \(H\) is finite. When \(H\) is finite, the projection \(\Gamma \to \Gamma /H\) is a proper map.
Fibers of the coset projection are finite translates of \(H\). A continuous map between discrete spaces is closed, so this projection is proper. The proper-orbit-map criterion gives properness of the action. Conversely, \(H\) fixes the identity coset and hence must be finite.
For a subgroup \(H\) and a space \(D\), the orbit cell is \(\Gamma /H\times D\) with action \(g(q,d)=(gq,d)\) and the product topology. Projection onto \(\Gamma /H\) is continuous and equivariant. Taking \(D\) to be a disk gives the cell shape for the intended CW construction; cell attachment is a separate target below.
A continuous equivariant map from a locally compact Hausdorff \(\Gamma \)-space to a proper \(\Gamma \)-space implies properness of the source. In particular, \(\Gamma /H\times D\) is proper if \(H\) is finite and \(D\) is locally compact Hausdorff.
The transporter of two compact subsets of the source is contained in the transporter of their compact images. Apply the finite-transporter criterion, and then apply the result to the orbit-cell projection.
4.5 The fixed-point criterion and uniqueness
For subgroups \(H,K\leq \Gamma \) and a topological parameter space \(D\) with trivial action, there is a natural homeomorphism \(((\Gamma /H)\times D)^K\cong (\Gamma /H)^K\times D\). The fixed cell is nonempty exactly when both factors are nonempty; an empty factor gives an empty fixed cell. Neither subgroup needs to be finite or normal.
Project a fixed pair to its fixed coset and parameter, and pair them for the inverse. Both maps are continuous in the product and subspace topologies.
The fixed-point criterion for a prospective model \(E\) requires \(E^H\) to be contractible for every finite subgroup \(H\) and empty for every infinite subgroup \(H\). This predicate alone does not supply an equivariant CW structure or a proof of the universal mapping property.
The fixed-point criterion is preserved by equivariant homotopy equivalence.
Restrict an equivariant homotopy equivalence to each subgroup’s fixed points. Contractibility is invariant under homotopy equivalence, and the inverse map transfers emptiness.
For a specified source \(X\) and target \(Y\), the homotopy-terminal mapping condition says that a continuous equivariant map \(X\to Y\) exists and any two such maps are equivariantly homotopic.
Suppose the homotopy-terminal mapping condition holds for each of the four ordered pairs \((X,X),(X,Y),(Y,X),(Y,Y)\). Then \(X\) and \(Y\) are equivariantly homotopy equivalent, and their \(H\)-fixed-point spaces are homotopy equivalent for every subgroup \(H\). The mapping condition is preserved when its target is replaced by an equivariantly homotopy-equivalent space. These are conditional statements; they do not establish the mapping condition for a general model satisfying the fixed-point criterion.
Choose maps in both directions. Uniqueness up to homotopy for the two endomorphism spaces identifies the composites with the identity maps. For replacement of the target, compose with the equivalence and its inverse and use their equivariant homotopies.
For a finite discrete group, the trivial action on a point is proper and satisfies the fixed-point criterion. For every \(\Gamma \)-space \(X\), maps from \(X\) to this point exist and are unique, hence unique up to equivariant homotopy. This verifies the topological and mapping claims for the finite-group point model; a formal CW structure is not asserted here.
Every subgroup is finite, and each fixed-point space is a point. A finite discrete group acts properly on a locally compact Hausdorff point. The constant map is the unique equivariant map to the point.
4.6 Cocompact indexing for a given ambient space
For a continuous \(\Gamma \)-action on \(E\) and an invariant subset \(X\) with its subspace topology, \(X/\Gamma \to E/\Gamma \) is a topological embedding. Thus \(X/\Gamma \) is compact if and only if the image of \(X\) in \(E/\Gamma \) is compact. No closedness or properness is needed for this assertion.
The orbit projection is an open quotient map. Apply Mathlib’s subquotient embedding theorem to the invariant inclusion \(X\hookrightarrow E\).
For a given \(\Gamma \)-space \(E\), a closed cocompact piece is a closed invariant subset \(X\subseteq E\) whose image in \(E/\Gamma \) is compact. For continuous actions, this is equivalent to compactness of its intrinsic quotient \(X/\Gamma \). Pieces are ordered by inclusion.
The closed cocompact pieces form a nonempty directed indexing system: the empty set is a piece, and \(X\cup Y\) is a common upper bound. For continuous actions every piece has compact intrinsic quotient. If \(E\) is locally compact, every piece is locally compact.
A finite union of closed invariant sets is closed and invariant, and its image is the finite union of the compact images. Closed subspaces inherit local compactness.
For a proper \(\Gamma \)-space \(E\), every compact subset \(K\subseteq E\) is contained in a closed cocompact invariant piece, namely its saturation \(q^{-1}(q(K))\), where \(q:E\to E/\Gamma \). In particular the pieces cover \(E\).
The compact image \(q(K)\) is closed in the Hausdorff orbit space. Its preimage is closed and invariant, and its quotient image is exactly \(q(K)\). Apply this construction to singletons for the covering assertion.
4.7 Categorical equivariant cell attachments
For invariant subsets \(S\subseteq T\) of a \(\Gamma \)-space, the inclusion \(S\to T\) is continuous, equivariant and injective. These inclusions obey identity and composition laws and commute with inclusion into the ambient space. In particular, they give the inclusion maps between ordered cocompact pieces.
Use the subtype inclusion, its induced topology and its induced action. All compatibility laws follow from the unchanged ambient coordinate.
In the category of topological \(\Gamma \)-actions, use the boundary inclusions \(\Gamma /H\times \partial D^n\to \Gamma /H\times D^n\), indexed by finite subgroups \(H\), as the generating cells at stage \(n\). A relative equivariant CW structure is a sequential relative cell complex for this family: its data contain the coproducts, pushout squares, skeleta, and colimit witnesses. An equivariant CW structure starts from the initial, empty action. The categorical morphisms between actions obtained from \(\Gamma \)-spaces correspond exactly to the continuous equivariant maps defined above.
These are cellular data. Topological properness of the resulting colimit is not assumed in this definition and remains to be proved.
Every orbit boundary inclusion is injective. For finite \(H\), both \(\Gamma /H\times D^n\) and \(\Gamma /H\times \partial D^n\) are proper \(\Gamma \)-spaces, including when \(n=0\).
The inclusion preserves the coset coordinate and is the usual injective boundary inclusion in the second coordinate. The disk and its boundary are compact Hausdorff, so the previously verified orbit-cell properness theorem applies.
For a relative equivariant CW structure \(X\to Y\), two equivariant continuous maps \(Y\to Z\) are equal if they agree on \(X\) and on every characteristic cell map into \(Y\).
Apply the morphism extensionality theorem for relative cell complexes, using the pushout universal property at successor stages and the colimit universal property for the resulting cellular object.
Let \(H\) be any subgroup and let the action on the parameter spaces \(D,E\) be trivial. For a target \(\Gamma \)-space \(X\), evaluation on the identity-coset slice gives a bijection between continuous equivariant maps \(\Gamma /H\times D\to X\) and continuous maps \(D\to X^H\). For a continuous map \(i:D\to E\), a map on \(\Gamma /H\times D\) extends across \(\mathrm{id}\times i\) if and only if its fixed-point slice extends across \(i\). This is a bijection of sets of maps, not a claimed homeomorphism of mapping spaces.
The inverse sends \(u:D\to X^H\) to \((gH,d)\mapsto g\, u(d)\). Fixed-point membership makes it well-defined, and the discrete coset factor reduces continuity to continuity on each slice. Evaluation and this construction are inverse and commute with parameter restriction, giving the extension criterion. Existence of the ordinary fixed-point extensions is not asserted here.
Every continuous map \(f:\partial D^n\to Y\) into a contractible space \(Y\) extends to a continuous map \(F:D^n\to Y\), including when \(n=0\). More generally, a null-homotopic map from the unit sphere of a proper real normed vector space extends over its closed unit ball.
For a nonempty unit sphere, the radial map \((t,s)\mapsto ts\) from its cylinder onto the closed unit ball is a continuous surjection from a compact space to a Hausdorff space, hence a quotient map. A reversed null-homotopy is constant on its fibers: only the zero-radius fiber is collapsed. Descending this homotopy gives the extension. For an empty sphere use the constant map at the point supplied by the null-homotopy.
If \(X^H\) is contractible, every continuous equivariant map \(\Gamma /H\times \partial D^n\to X\) extends to \(\Gamma /H\times D^n\). In particular, a target satisfying the fixed-point criterion has this extension property for every finite subgroup \(H\).
Evaluate on the identity-coset slice, extend the resulting map into \(X^H\) over the disk, and apply the inverse orbit/fixed-point correspondence.
Let \(A\to B\) have a relative equivariant CW structure with finite cell stabilizers, and let \(X\) satisfy the fixed-point criterion. Every continuous equivariant map \(A\to X\) extends to \(B\to X\). Consequently every equivariant CW complex admits a continuous equivariant map to \(X\). No uniqueness up to equivariant homotopy is asserted here.
The map \(X\to *\) has the right lifting property against each generating orbit boundary inclusion. The corresponding left lifting property is preserved by coproducts, pushouts, and sequential compositions. Apply it to the relative CW structure. For the final assertion take \(A\) to be the initial, empty action.
Let \(Y\) be contractible, let \(f_0,f_1:D^n\to Y\) be continuous, and let \(H:[0,1]\times \partial D^n\to Y\) be a homotopy between their restrictions. There is a homotopy \(F:[0,1]\times D^n\to Y\) from \(f_0\) to \(f_1\) satisfying \(F(t,s)=H(t,s)\) on the whole boundary, including when \(n=0\). Equivalently, every family of boundary paths with prescribed disk endpoints extends to a continuous family of disk paths, with those endpoints unchanged.
Use the max norm on \(\mathbb R\times \mathbb R^n\). Its unit sphere is a quotient of the disjoint union of the two disk faces and the cylindrical side. The endpoint conditions make \(f_0,f_1,H\) agree on the fibers of this quotient. Descend them to a boundary map and apply the verified ball extension theorem. Parametrizing the resulting max-norm ball by \((t,x)\mapsto (2t-1,x)\) gives \(F\). The path-family formulation follows by currying; the unit interval is locally compact, so evaluation is jointly continuous.
Suppose \(X^H\) is contractible. A continuous equivariant family of paths on \(\Gamma /H\times \partial D^n\) extends to \(\Gamma /H\times D^n\) whenever its two endpoint maps are prescribed on the disk and agree on the boundary. Both endpoint maps and every prescribed boundary path are preserved exactly.
An \(H\)-fixed path in \(X\) is a path in \(X^H\), and this identification is continuous in both directions for the compact-open topology. Evaluate on the identity coset, apply disk path lifting in \(X^H\), and recover the equivariant family using the orbit/fixed-point correspondence.
Let \(A\) have a finite-isotropy equivariant CW structure and let \(X\) satisfy the fixed-point criterion. Continuous equivariant maps \(A\to X\) exist, and any two such maps are equivariantly homotopic.
The endpoint evaluation map \(C([0,1],X)\to X\times X\) has the right lifting property against every generating orbit boundary inclusion. The lifting property persists under coproducts, pushouts and sequential composition. For the initial inclusion into \(A\), lift the pair of endpoint maps to a continuous equivariant map \(A\to C([0,1],X)\). Joint evaluation produces the required equivariant homotopy. Existence was verified by cellular extension.
Any two finite-isotropy equivariant CW spaces satisfying the fixed-point criterion are equivariantly homotopy equivalent.
The preceding mapping theorem supplies maps in both directions and homotopies of their composites to the respective identities. Apply the verified homotopy-terminal uniqueness argument. This does not assert existence of a CW space satisfying the fixed-point criterion.
4.8 A concrete probability target
Let \(P(\Gamma )\) be the space of functions \(p:\Gamma \to \mathbb R\) such that \(p(g)\geq 0\), \(p\) is summable, and \(\sum _g p(g)=1\). Give it the subspace topology of pointwise convergence in \(\mathbb R^\Gamma \) and the action \((a\cdot p)(g)=p(a^{-1}g)\). Each translation is continuous. This definition supplies a topological action; it does not supply a CW structure or local compactness.
For finite \(H\leq \Gamma \), \(P(\Gamma )^H\) is contractible. For infinite \(H\leq \Gamma \), it is empty. Thus \(P(\Gamma )\) satisfies the fixed-point criterion.
The fixed-point space is homeomorphic to the convex set of invariant probability functions. For finite \(H\), this set contains the uniform probability function on \(H\). For infinite \(H\), a nonzero nonnegative invariant function has a positive constant value on an infinite coset, contradicting summability. The total mass condition excludes the zero function.
For countable discrete \(\Gamma \), \(P(\Gamma )\) is a proper second-countable \(\Gamma \)-space. More generally, compact subsets of \(P(\Gamma )\) have finite transporters for every discrete group.
Compactness gives a finite set carrying more than half the mass of every probability function in a given compact subset. If \(gK\cap L\ne \varnothing \) and \(S,T\) are such finite sets for \(K,L\), respectively, then \(gS\cap T\) is nonempty; hence \(g\in TS^{-1}\). The transporter is finite. For countable \(\Gamma \), the function space and its subspace are first countable and Hausdorff, so the compact-transporter criterion implies properness. Second countability follows from the countable product topology.
Let \(A\) be a Hausdorff continuous \(\Gamma \)-space, let \(X\) be a proper \(\Gamma \)-space, and let \(f:A\to X\) be continuous and equivariant. Then the action on \(A\) is proper. No properness assumption on the map \(f\) is needed.
Push an ultrafilter on \(\Gamma \times A\) forward along \((g,a)\mapsto (g,f(a))\). Properness of the action on \(X\) supplies convergence of its group coordinate. The Hausdorff ultrafilter criterion for the action on \(A\) then proves properness.
Every finite-isotropy equivariant CW complex admits a map to \(P(\Gamma )\), unique up to equivariant homotopy. For countable discrete groups the target is proper. This is a mapping theorem for CW sources; a CW structure on \(P(\Gamma )\) has not been constructed.
Apply the verified cellular mapping theorem to the explicit target and its fixed-point criterion. Its properness is given by the preceding proposition.
For countable discrete \(\Gamma \), a Hausdorff space carrying a finite-isotropy equivariant CW structure has a proper action. Hausdorffness is an explicit hypothesis here; its derivation from the categorical CW data remains a separate obligation.
Choose the map to \(P(\Gamma )\) supplied by the cellular mapping theorem and transfer properness along that equivariant map.
4.9 Closed skeletal inclusions and the colimit topology
For every subgroup \(H\leq \Gamma \) and every \(n\geq 0\), the inclusion \(\Gamma /H\times \partial D^n\longrightarrow \Gamma /H\times D^n\) is a closed embedding.
The disk boundary is compact and the disk is Hausdorff, so the boundary inclusion is a closed embedding. Take its product with the identity on \(\Gamma /H\). Finiteness of \(H\) is not required here.
Let \(A\longrightarrow X\) carry a relative equivariant CW structure, with skeletal sequence \((X_n)_{n\geq 0}\). The map \(A\longrightarrow X\), every transition \(X_m\longrightarrow X_n\) for \(m\leq n\), and every inclusion \(X_n\longrightarrow X\) are closed embeddings. In particular, no distinct points of a skeleton are identified in later stages or in the colimit.
Coproducts and pushouts preserve closed embeddings in the category of topological spaces. This proves the assertion for successive attachments, and composition gives all finite transitions. The underlying set functor preserves colimits; stability of injective maps under these cellular colimits proves injectivity of the skeletal inclusions. For a closed subset of one skeleton, its inverse image on an earlier skeleton is a continuous preimage, and on a later skeleton is a closed image. The colimit topology therefore makes its image closed in \(X\).
Every point of \(X\) comes from some finite skeletal stage. A subset of \(X\) is open, respectively closed, exactly when its inverse image in every \(X_n\) is open, respectively closed. A function \(X\longrightarrow Z\) into any topological space is continuous exactly when its restriction to every skeletal stage is continuous.
Forget the action and use the corresponding set and topological colimit universal properties.
4.10 Real-valued extension and Hausdorffness
A continuous real-valued function on the source of an orbit-cell attachment extends to its target. More generally, every continuous real-valued function on a skeleton \(X_n\) of a relative equivariant CW complex extends to the whole space \(X\). These scalar functions need not be equivariant.
Each disjoint union of orbit disks is normal, and its boundary is closed embedded. Tietze extension and the topological pushout property extend functions across an attachment. Express this extension property as a lifting property against the terminal map from the real line. Stability under transfinite composition gives extension along each skeletal inclusion into the colimit.
Every equivariant CW space built from the stated orbit cells is Hausdorff. More precisely, continuous real-valued functions separate its distinct points. This conclusion is derived from the categorical cell-attachment data; Hausdorffness is not an additional hypothesis.
Separation by real-valued functions is preserved by attachment: extend separating functions on old points, and use Urysohn’s lemma on the disk coproduct to distinguish new points from the boundary and from each other. Induction gives separation on every skeleton, starting from the empty space. Any two points of the colimit lie in a common skeletal stage. Extend a separating function on that stage to the colimit, and pull back disjoint real neighborhoods.
Let \(\Gamma \) be a countable discrete group. Every equivariant CW space whose orbit cells have finite stabilizers has a proper \(\Gamma \)-action.
Hausdorffness now follows from the cellular data. Apply the already verified properness theorem for Hausdorff equivariant CW spaces, using the map to the proper probability-space target.
4.11 Constructed zero-skeleta and finite-group CW models
For any family of finite subgroups \((H_i)_{i\in J}\), the disjoint union
has a zero-dimensional equivariant CW structure.
The boundaries of zero-disks are empty. The explicit orbit-cell coproduct is a pushout from the empty action. Extend this attachment to a sequential CW construction by taking a constant tail; each later attachment has an empty cell family. The coproduct, pushout, and colimit witnesses are constructed in Lean.
For countable discrete \(\Gamma \), take one zero-cell orbit \(\Gamma /H\) for every finite subgroup \(H\). The resulting space is countable, discrete, locally compact, second countable, and proper. Every finite subgroup has an explicitly constructed fixed vertex, and infinite subgroups have no fixed vertices.
Finite subgroups inject into the finite subsets of \(\Gamma \), so there are countably many of them. The corresponding orbit coproduct is countable. The identity coset in the \(\Gamma /H\) summand is fixed by \(H\). Properness follows from the verified CW structure. This is a starting zero-skeleton; contractibility of its fixed-point spaces is not asserted.
For finite \(\Gamma \), the single zero-cell orbit \(\Gamma /\Gamma \times D^0\) is a locally compact second-countable universal proper equivariant CW model, with contractible subgroup fixed-point spaces and the universal mapping property for equivariant CW sources.
The constructed space has a single point and a genuine orbit-cell CW structure. Every subgroup fixed-point space is a singleton. Apply the verified cellular mapping theorem. All topological and properness properties are proved for this explicit model.
4.12 Labeled orbit simplices for a join construction
For any group \(\Gamma \), let \(V=\coprod _{H\leq \Gamma ,\ H\text{ finite}}\Gamma /H\). Label its copies by \(\mathbb N\). A labeled orbit simplex is a finite subset of \(\mathbb N\times V\) whose projection to \(\mathbb N\) is injective. Translation acts on the orbit coordinate and fixes the label. Every finite subset of a simplex is again a simplex, so the family is closed under taking faces. The empty simplex is allowed. These are combinatorial data; no topology or geometric realization is asserted here.
If a group element stabilizes a labeled orbit simplex setwise, it fixes each of its vertices. Every nonempty simplex has finite stabilizer subgroup. The nonempty hypothesis is essential: the empty simplex is stabilized by all of \(\Gamma \).
Translation preserves labels, and each label occurs at most once in a simplex. Thus a translated vertex that remains in the simplex is the same vertex. The stabilizer of an orbit vertex \(aH\) is contained in the finite conjugate \(aHa^{-1}\). Fixing one vertex therefore bounds the stabilizer of a nonempty simplex by a finite set.
Every finite subgroup \(H\) has an explicitly constructed fixed vertex at each natural-number label: use the identity coset in the \(H\)-tagged summand.
Left multiplication by \(h\in H\) fixes the coset \(H\) and leaves the label unchanged.
The weak realization consists of nonnegative real vertex coordinates with sum one and finite support contained in an admissible labeled simplex. Equip it with the final topology of all finite simplex charts. A map out of this realization is continuous exactly when it is continuous on every chart; the same criterion holds after taking a product with a locally compact space. The coordinate map into the product of real lines is continuous and injective, so the weak realization is Hausdorff.
Every nonempty simplex chart is homeomorphic to a closed disk of dimension one less than its number of vertices. Its full face boundary corresponds exactly to the unit sphere, including the zero-dimensional case. Each chart is compact and closed embedded in the weak realization.
Restrict the coordinate vector to the finite vertex set to obtain the standard simplex. Identify that simplex with a compact convex body with nonempty interior, and use radial rescaling to obtain the disk pair. Vanishing barycentric coordinates describe precisely its boundary.
Every discrete group acts continuously and properly on the weak realization.
Translation permutes vertex coordinates and takes each finite chart continuously to the translated chart. A compact set admits a finite set of vertices carrying more than half the barycentric mass at every point. Intersecting translates of two such compact sets must transport one of these vertices to another. Vertex transporters are finite because vertex isotropy is finite. The resulting finite transporter bound also gives the properness of the action map directly.
The actual fixed-point space of every finite subgroup is contractible, and that of every infinite subgroup is empty.
A continuous sequence of shifts moves all join factors upward by one. On each finite chart the sequence is represented by a finite homotopy, and these homotopies agree on chart overlaps. The shifted realization has no vertex in factor zero and can therefore be coned to the subgroup’s fixed vertex in that factor. Both homotopies preserve the actual fixed-point subspace. Infinite-subgroup fixed points are excluded by properness.
The weak labeled realization has a genuine finite-isotropy equivariant CW structure, with its dimension filtration as the actual skeletal sequence.
Index the new dimension-\(n\) cells by orbits of simplices with \(n+1\) vertices. The stabilizer of each representative fixes its whole chart, so its disk pair extends to a characteristic orbit disk and attaching orbit sphere. The coproduct maps are actual categorical coproducts. Their characteristic maps identify precisely the sphere attaching locus: outside the preceding skeleton, the support recovers the orbit index, coset, and disk point. Given any attaching cocone, lift each chart into its orbit disk and glue the prescribed continuous maps using their exact boundary agreement. This proves the full pushout universal property. The empty zero stage and the proved weak-topology skeletal colimit assemble these attachments into the CW witness.
The proper weak realization, its full fixed-point criterion, and its actual categorical CW structure are now verified. The locally compact second-countable CW model is being constructed separately.
4.13 Equivariant CW complexes and a model for \(\underline E\Gamma \)
A finite-isotropy \(\Gamma \)-CW structure consists of a sequential cellular construction from the empty action, with cells \(\Gamma /H\times D^n\) for finite subgroups \(H\). The construction includes the coproduct, pushout, and colimit witnesses. Its skeleta are closed embedded subspaces, and Hausdorffness follows from the cellular data. For countable discrete \(\Gamma \), the resulting action is topologically proper.
For every discrete group \(\Gamma \), the weak labeled join constructed above is an explicit universal proper \(\Gamma \)-CW complex. It has a genuine finite-isotropy CW structure, a proper action, contractible fixed-point spaces for finite subgroups, and empty fixed-point spaces for infinite subgroups. Every finite-isotropy equivariant CW complex admits an equivariant map to this model, and any two such maps are equivariantly homotopic. Every other equivariant CW model satisfying the same fixed-point criterion is equivariantly homotopy equivalent to it.
4.14 Cocompact pieces and model choices
For a countable discrete group \(\Gamma \), choose the concrete geometric telescope \(E\) of the finite-orbit stages of the weak labeled join. This same space is a genuine finite-isotropy equivariant CW complex, is locally compact and second-countable, has a proper action, and has contractible fixed spaces for finite subgroups and empty fixed spaces for infinite subgroups. It has the universal cellular mapping property and is unique up to equivariant homotopy among genuine CW models with the fixed-point criterion. Its closed invariant subsets with compact quotient form the directed cocompact indexing system proved above, and their union is \(E\).
The CW structure is transported through the actual equivariant homeomorphism from the invariant staircase prism subcomplex. The general CW constructor applies to its invariant family closed under faces. Its attachments are actual orbit-disk pushouts and its weak topology is the actual skeletal colimit. The telescope’s local compactness and second countability are proved independently from its nested closed finite-orbit stages. Fixed-space contraction uses compact finite-stage control and a continuous height majorant; it does not assume a global height section on the weak join.