43 Def 25: Invariant Labeling
Let \(X\) be a graph with a group action by \(H\). The set of edges incident to a vertex \(v \in X_0\) in the cell complex is defined as
Formally, \(\operatorname {cellIncidentEdges}(v) = \{ e \in X_1 \mid v \in X.\operatorname {graph}.\operatorname {bdry}(e) \} \).
For a vertex \(v \in X_0\) and an edge \(e \in X_1\), we have
This follows immediately by simplification using the definition of \(\operatorname {cellIncidentEdges}\).
For a vertex \(v \in X_0\) and an edge \(e \in X_1\) with \(v \in \partial e\), the set \(\delta v\) is non-empty.
The element \(e\) witnesses non-emptiness: since \(v \in \partial e\), by the membership characterization we have \(e \in \delta v\), so \(\langle e, \cdot \rangle \) provides the required element.
A cell complex labeling of degree \(s\) on \(X\) is a family \(\Lambda = \{ \Lambda _v\} _{v \in X_0}\) assigning to each vertex \(v \in X_0\) a bijection
Formally, \(\operatorname {CellLabeling}(s) = \prod _{v : X_0} (\delta v \simeq \operatorname {Fin}(s))\).
If \(e \in \delta v\) (i.e., \(e\) is incident to \(v\)), then \(h \cdot e \in \delta (h \cdot v)\) for all \(h \in H\). That is, the \(H\)-action preserves incidence.
Rewriting using the membership characterization of \(\operatorname {cellIncidentEdges}\) on both sides, it suffices to show \(h \cdot v \in \partial (h \cdot e)\). This follows directly from the boundary orbit compatibility lemma \(\operatorname {bdry_orbit_compat}\), which states that \(v \in \partial e \Rightarrow h \cdot v \in \partial (h \cdot e)\).
For a vertex \(v \in X_0\), a group element \(h \in H\), and an incident edge \(e \in \delta v\), define the transported incident edge
as the pair \(\langle h \cdot e.{\operatorname {val}},\, \operatorname {smul_incident_of_incident}(v, e.{\operatorname {val}}, h, e.{\operatorname {prop}})\rangle \).
A cell complex labeling \(\Lambda \) is \(H\)-invariant if for all vertices \(v \in X_0\), all group elements \(h \in H\), and all incident edges \(e \in \delta v\),
Formally, \(\operatorname {IsInvariantLabeling}(\Lambda )\) is the proposition
There exist a group \(H\), a graph with \(H\)-action \(X\), a degree \(s \in \mathbb {N}\), a cell labeling \(\Lambda : X.\operatorname {CellLabeling}(s)\), and a proof that \(\Lambda \) is \(H\)-invariant. In other words, the invariance premises are satisfiable.
We take \(H = \operatorname {Unit}\) (the trivial group) with \(s = 0\). We construct \(X\) as the graph with trivial action in which all cell types are \(\operatorname {PEmpty}\) (no vertices or edges), all structure maps are vacuously defined, and the vertex/edge actions are trivial. The boundary map sends every edge (of which there are none) to the empty set, and the boundary-of-boundary condition holds vacuously by simplification.
We provide the labeling \(\Lambda \) and the invariance proof vacuously: since there are no vertices (\(X_0 = \operatorname {PEmpty}\)), the universal quantifiers in both the labeling and invariance condition hold trivially via \(\operatorname {PEmpty.elim}\).
For a vertex orbit \([v] \in X/H\), the quotient incident edges are the edge orbits \([e] \in X_1/H\) such that some representative edge has a boundary vertex in the orbit of \([v]\):
For a vertex orbit \([v] \in X/H\) and an edge orbit \([e] \in X_1/H\),
This follows immediately by simplification using the definition of \(\operatorname {quotientIncidentEdges}\).
If \(e \in \delta v\) (i.e., \(e\) is incident to \(v\) in the cell complex), then the edge orbit \([e]\) is incident to the vertex orbit \([v]\) in the quotient graph:
Rewriting using the membership characterization of \(\operatorname {quotientIncidentEdges}\), we provide the witnesses: \(e\) itself as the edge representative, \(v\) as the vertex representative, the reflexivity proofs \([e] = [e]\) and \([v] = [v]\), and the boundary membership \(v \in \partial e\) extracted from \(e \in \delta v\) via the membership characterization of \(\operatorname {cellIncidentEdges}\).
For any vertex \(v \in X_0\) and edge \(e \in X_1\) with \(v \in \partial e\), the quotient incident edge set \(\delta [v]\) is non-empty.
The edge orbit \([e]\) witnesses non-emptiness: since \(v \in \partial e\), by the membership characterization of \(\operatorname {cellIncidentEdges}\) we have \(e \in \delta v\), and then by \(\operatorname {quotientIncident_of_incident}\) we obtain \([e] \in \delta [v]\).
Given an \(H\)-invariant labeling \(\Lambda \) (i.e., \(\operatorname {IsInvariantLabeling}(\Lambda )\) holds), the quotient labeling \(\bar{\Lambda }\) is a well-defined bijection
for each vertex orbit \([v] \in X/H\), defined by \(\bar{\Lambda }_{[v]}([e]) = \Lambda _v(e)\) for any representatives \(v \in [v]\) and \(e \in [e]\) with \(e \in \delta v\).
We construct the bijection as follows. Given a vertex orbit \([v]\), we choose a representative vertex \(v\) using \(\operatorname {Quotient.exists_rep}\), obtaining \(v\) and the proof \([v] = [v]\).
We define a translation map: for each quotient incident edge \([e] \in \delta [v]\), we produce an incident edge in \(\delta v\). By the membership characterization of \(\operatorname {quotientIncidentEdges}\), there exists a representative edge \(e\) with \([e'] = [e]\) and a vertex \(v'\) with \([v'] = [v]\) and \(v' \in \partial e'\). Since \([v'] = [v]\), by \(\operatorname {Quotient.exact}\) there exists \(g \in H\) with \(g \cdot v = v'\). Then \(g^{-1} \cdot e'\) is incident to \(v\): indeed \(v = g^{-1} \cdot v' \in \partial (g^{-1} \cdot e')\) by the boundary equivariance of \(X\). We thus obtain the element \(\langle g^{-1} \cdot e', \cdot \rangle \in \delta v\), and it lies in the orbit \([e]\) since \(g \cdot (g^{-1} \cdot e') = e'\) has the same quotient.
We define \(\operatorname {pickEdge}([e])\) to be this translated incident edge. We verify:
Injectivity of pickEdge: If \(\operatorname {pickEdge}([e_1]) = \operatorname {pickEdge}([e_2])\), then both have the same underlying edge, hence the same image under \(\operatorname {edgeQuot}\) (by \(\operatorname {pickEdge_spec}\)), so \([e_1] = [e_2]\) as elements of \(\delta [v]\).
Surjectivity of pickEdge: For any \(e \in \delta v\), the quotient edge \([e] \in \delta [v]\) (by \(\operatorname {quotientIncident_of_incident}\)). We have \(\operatorname {pickEdge}([e]) = \) some \(e' \in \delta v\) with \([e'] = [e]\). By \(\operatorname {Quotient.exact}\), there exists \(g\) with \(g \cdot e' = e\) (or \(g \cdot e = e'\)). Both \(e\) and \(e'\) are in \(\delta v\), so \(v \in \partial e\) and \(v \in \partial e'\). From \(g \cdot e' = e\) and equivariance, \(g^{-1} \cdot v \in \partial e'\), and by the quotient condition \(\operatorname {quotientCondition}\) (which states that if \(v\) and \(g^{-1} \cdot v\) both lie in \(\partial e'\) then \(g^{-1} = 1\)), we get \(g = 1\), hence \(e = e'\).
The composition \(\Lambda _v \circ \operatorname {pickEdge}\) is therefore a bijection \(\delta [v] \to \operatorname {Fin}(s)\): it is injective as a composition of two injections (\(\operatorname {pickEdge}\) injective and \(\Lambda _v\) injective), and surjective as a composition of two surjections (\(\operatorname {pickEdge}\) surjective and \(\Lambda _v\) surjective). We conclude by \(\operatorname {Equiv.ofBijective}\).
Let \(\Lambda \) be an \(H\)-invariant labeling. For any vertex \(v \in X_0\), edge \(e \in X_1\) with \(v \in \partial e\), and \(h \in H\) (so that \(h \cdot v \in \partial (h \cdot e)\)), the labeling value is independent of the representative:
We apply the \(H\)-invariance condition to \(v\), \(h\), and the incident edge \(\langle e, \cdot \rangle \in \delta v\), obtaining
We observe that the underlying cell of \(\operatorname {smulIncidentEdge}(v, h, \langle e, \cdot \rangle )\) is definitionally equal to \(h \cdot e\). Rewriting with the \(H\)-invariance equation and using congruence of the subtype (since the values agree), we conclude the result.