Dependencies

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.

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\).

For subsets \(K,L\subseteq X\), define the transporter

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.

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.

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.

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\).

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.

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.

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.

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.

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.

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 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.

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.

For a subgroup \(H\leq \Gamma \), let

with the subspace topology. The Lean definition uses Mathlib’s existing MulAction.fixedPoints.

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.

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.

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.

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.

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 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.

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\).

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.

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.

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\).

Any two finite-isotropy equivariant CW spaces satisfying the fixed-point criterion are equivariantly homotopy equivalent.

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.

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.

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.

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\).

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.

Let \(\Gamma \) be a countable discrete group. Every equivariant CW space whose orbit cells have finite stabilizers has a proper \(\Gamma \)-action.

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.

Continuous equivariant maps have identity and associative composition, with both identity laws. Equality of maps is determined pointwise.

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.

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.

The fixed-point criterion is preserved by equivariant homotopy equivalence.

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\).

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.

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 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\).

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\).

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.

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.

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.

Every finite subgroup \(H\) has an explicitly constructed fixed vertex at each natural-number label: use the identity coset in the \(H\)-tagged summand.

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 \).

The actual fixed-point space of every finite subgroup is contractible, and that of every infinite subgroup is empty.

The weak labeled realization has a genuine finite-isotropy equivariant CW structure, with its dimension filtration as the actual skeletal sequence.

Every discrete group acts continuously and properly on the weak realization.

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.

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\).

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.

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.

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.

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.

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.

For any family of finite subgroups \((H_i)_{i\in J}\), the disjoint union

has a zero-dimensional equivariant CW structure.

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.

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.

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.

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.

Every point stabilizer \(\Gamma _x\) in a proper discrete-group action is finite. This implication does not require local compactness of \(X\).

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.

For a proper discrete-group action, any subgroup fixing a point is finite. Consequently \(X^H=\varnothing \) whenever \(H\) is infinite.

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.

A proper action has Hausdorff orbit space \(X/\Gamma \). If \(X\) is locally compact, then \(X/\Gamma \) is locally compact as well.

Restricting a proper discrete-group action to any subgroup preserves properness.

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.

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.