42 Def 24: Quotient Graph Trivialization
A graph with group action consists of a finite graph \(X\) (given as a 1-dimensional cell complex, i.e., a CellComplex) equipped with a free right action of a finite group \(H\) on both vertices \(X_0\) and edges \(X_1\), compatible with the boundary map, and satisfying a quotient condition.
Formally, it is a structure \(\mathtt{GraphWithGroupAction}(H)\) for a group \(H\) with \(|H| {\lt} \infty \), comprising:
A cell complex \(\mathtt{graph} : \mathtt{CellComplex}\) (the underlying graph).
A right \(H\)-action \(\mathtt{vertexAction}\) on the vertices \(X.\mathtt{graph}.\mathtt{cells}(0)\), modeled as a left MulAction via \(h \cdot v = v \cdot h^{-1}\).
A right \(H\)-action \(\mathtt{edgeAction}\) on the edges \(X.\mathtt{graph}.\mathtt{cells}(1)\).
Freeness of the vertex action: for all \(h \in H\) and \(v \in X_0\), if \(h \cdot v = v\) then \(h = 1\).
Freeness of the edge action: for all \(h \in H\) and \(e \in X_1\), if \(h \cdot e = e\) then \(h = 1\).
Boundary equivariance: for all \(e \in X_1\), \(h \in H\), and \(\tau \in X_0\),
\[ \tau \in \partial (h \cdot e) \iff h^{-1} \cdot \tau \in \partial e. \]Quotient condition: for all \(e \in X_1\), \(v \in X_0\), and \(h \in H\), if \(v \in \partial e\) and \(h \cdot v \in \partial e\), then \(h = 1\). (No edge connects a vertex to a nontrivially translated copy of itself.)
Let \(X : \mathtt{GraphWithGroupAction}(H)\). The quotient vertices of \(X\) by \(H\) are the orbits of the \(H\)-action on \(X_0\):
Let \(X : \mathtt{GraphWithGroupAction}(H)\). The quotient edges of \(X\) by \(H\) are the orbits of the \(H\)-action on \(X_1\):
The vertex quotient map \(\pi _0 : X_0 \to (X/H)_0\) sends a vertex \(v\) to its \(H\)-orbit:
The edge quotient map \(\pi _1 : X_1 \to (X/H)_1\) sends an edge \(e\) to its \(H\)-orbit:
Let \(X : \mathtt{GraphWithGroupAction}(H)\), \(e \in X_1\), \(h \in H\), and \(\tau \in X_0\). If \(\tau \in \partial e\), then \(h \cdot \tau \in \partial (h \cdot e)\).
We must show \(h \cdot \tau \in \partial (h \cdot e)\). By boundary equivariance, \(h \cdot \tau \in \partial (h \cdot e)\) if and only if \(h^{-1} \cdot (h \cdot \tau ) \in \partial e\). Since \(h^{-1} \cdot (h \cdot \tau ) = \tau \) and \(\tau \in \partial e\) by hypothesis, the result follows by simplification.
The quotient boundary map on the quotient graph assigns to each edge orbit \(E \in (X/H)_1\) a finite set of vertex orbits:
where \(e\) is any representative of \(E\). This is well-defined: if \(e_1, e_2\) represent the same orbit, so \(\exists \, g \in H,\; g \cdot e_2 = e_1\), then for any \(\tau \in \partial e_1\), we have \(g^{-1} \cdot \tau \in \partial e_2\) by boundary equivariance, and \(\pi _0(g^{-1} \cdot \tau ) = \pi _0(\tau )\) since they are in the same \(H\)-orbit; and vice versa.
Let \(X : \mathtt{GraphWithGroupAction}(H)\), and suppose every edge has at least one boundary vertex: \(\forall \, e \in X_1,\; \partial e \neq \emptyset \). Then for every edge orbit \(E \in (X/H)_1\), the quotient boundary \(\partial _{X/H}(E)\) is nonempty.
By induction on \(E\) using a representative \(e\). By the unfolding of \(\mathtt{quotientBdry}\), we have \(\partial _{X/H}([e]) = \{ \pi _0(\tau ) \mid \tau \in \partial e\} \). Since \(\partial e\) is nonempty by hypothesis, choose \(\tau \in \partial e\). Then \(\pi _0(\tau ) \in \partial _{X/H}([e])\), so the set is nonempty.
A trivialization of the vertex quotient map \(\pi _0 : X_0 \to (X/H)_0\) is a section, i.e., a function
such that for every vertex orbit \(V \in (X/H)_0\), the representative \(R(V)\) lies in \(V\):
The set \(\{ R(V) \mid V \in (X/H)_0\} \subseteq X_0\) contains exactly one representative from each \(H\)-orbit of vertices.
For any \(X : \mathtt{GraphWithGroupAction}(H)\), a trivialization exists: \(\mathtt{Nonempty}(X.\mathtt{Trivialization})\).
We first observe that for every vertex orbit \(V \in (X/H)_0\), there exists a vertex \(v \in X_0\) with \(\pi _0(v) = V\): this follows by induction on \(V\) using a representative. Specifically, if \(V = [v]\) for some \(v \in X_0\), then \(\pi _0(v) = [v] = V\) by reflexivity.
Having shown existence for each orbit, we apply the axiom of choice to obtain a selection function \(V \mapsto \varepsilon (V)\) where \(\varepsilon (V)\) is a chosen representative with \(\pi _0(\varepsilon (V)) = V\). This selection defines a trivialization \(R = \langle \varepsilon , \text{(the proof of representativeness)} \rangle \), so \(X.\mathtt{Trivialization}\) is nonempty.
For any \(X : \mathtt{GraphWithGroupAction}(H)\), \(\mathtt{Nonempty}(X.\mathtt{Trivialization})\). This follows immediately from trivialization_exists.
This is an immediate consequence of \(X.\mathtt{trivialization\_ exists}\).
Given a trivialization \(R\) of \(X\) and a vertex \(v \in X_0\), the vertex group element \(g_v \in H\) is the unique group element such that
Since \(\pi _0(R(\pi _0(v))) = \pi _0(v)\), the vertices \(R(\pi _0(v))\) and \(v\) lie in the same \(H\)-orbit, so such a \(g_v\) exists (chosen via the axiom of choice).
For any trivialization \(R\) and vertex \(v \in X_0\):
where \(g_v = \mathtt{vertexGroupElement}(R, v)\).
This follows directly from the definition of \(\mathtt{vertexGroupElement}\) as the chosen witness of the existential statement, whose proof gives \(g_v \cdot R(\pi _0(v)) = v\).
Given a trivialization \(R\), an edge \(e \in X_1\), and two boundary vertices \(\tau _1, \tau _2 \in \partial e\) lying in distinct vertex orbits (\(\pi _0(\tau _1) \neq \pi _0(\tau _2)\)), the connection of \(e\) relative to \(\tau _1\) and \(\tau _2\) is the group element
where \(g_{\tau _i} = \mathtt{vertexGroupElement}(R, \tau _i)\) is the unique element satisfying \(g_{\tau _i} \cdot R(\pi _0(\tau _i)) = \tau _i\).
Let \(R\) be a trivialization, \(e \in X_1\), \(g \in H\), and \(\tau _1, \tau _2 \in \partial e\) with \(\pi _0(\tau _1) \neq \pi _0(\tau _2)\). Then the connection is invariant under the \(H\)-action:
We unfold \(\mathtt{connectionOnEdge}\) on both sides. It suffices to show that for any \(v \in X_0\),
Let \(h = \mathtt{vertexGroupElement}(R, v)\), so \(h \cdot R(\pi _0(v)) = v\).
First, note \(\pi _0(g \cdot v) = \pi _0(v)\), since \(g \cdot v\) and \(v\) are in the same \(H\)-orbit (with \(\pi _0\) sending each element to its orbit, which is a sound quotient relation via \(\exists g, g \cdot v' = v\)). Hence \(R(\pi _0(g \cdot v)) = R(\pi _0(v))\).
Let \(h' = \mathtt{vertexGroupElement}(R, g \cdot v)\), so \(h' \cdot R(\pi _0(v)) = g \cdot v\). Also \((g \cdot h) \cdot R(\pi _0(v)) = g \cdot (h \cdot R(\pi _0(v))) = g \cdot v\). Thus
By freeness of the vertex action applied to \((h')^{-1} \cdot (g \cdot h) \in H\) acting on \(R(\pi _0(v))\), we get \((h')^{-1} \cdot (g \cdot h) = 1\), i.e., \(h' = g \cdot h\).
Substituting back, \(\phi _R(g \cdot e; g \cdot \tau _1, g \cdot \tau _2) = (g \cdot g_{\tau _1})^{-1} \cdot (g \cdot g_{\tau _2}) = g_{\tau _1}^{-1} \cdot g^{-1} \cdot g \cdot g_{\tau _2} = g_{\tau _1}^{-1} \cdot g_{\tau _2} = \phi _R(e; \tau _1, \tau _2)\), using commutativity of the inverse and simplification by linear arithmetic.
Given a trivialization \(R\) of \(X\), the induced connection is a map
defined as follows. For an edge orbit \(E \in (X/H)_1\), let \(e = \mathtt{out}(E)\) be a chosen representative edge with boundary \(\partial e\). If there exist \(\tau _1, \tau _2 \in \partial e\) with \(\pi _0(\tau _1) \neq \pi _0(\tau _2)\), we set
where \(\tau _1, \tau _2\) are chosen witnesses and \(g_{\tau _i} = \mathtt{vertexGroupElement}(R,\tau _i)\). Otherwise (all boundary vertices are in the same orbit, or the boundary is small), we set \(\phi _R(E) := 1\).
By the orbit compatibility lemma, this is independent of the choice of representative edge.
Let \(R\) be a trivialization of \(X\), let \(e \in X_1\), and let \(\tau _1, \tau _2 \in \partial e\) with \(\pi _0(\tau _1) \neq \pi _0(\tau _2)\). Then there exists an edge \(e' \in X_1\) such that:
\(\pi _1(e') = \pi _1(e)\) (i.e., \(e'\) is in the same orbit as \(e\)),
\(R(\pi _0(\tau _1)) \in \partial e'\),
\(\phi _R(e;\tau _1,\tau _2) \cdot R(\pi _0(\tau _2)) \in \partial e'\).
Let \(g_1 = \mathtt{vertexGroupElement}(R, \tau _1)\), so that \(g_1 \cdot R(\pi _0(\tau _1)) = \tau _1\). Set \(e' := g_1^{-1} \cdot e\).
(1) Same orbit: We have \(\pi _1(e') = \pi _1(g_1^{-1} \cdot e) = \pi _1(e)\), since \(e'\) and \(e\) are related by \(g_1^{-1} \in H\), giving a sound quotient relation (i.e., \(\exists \, h,\, h \cdot e = e'\) with \(h = g_1^{-1}\)).
(2) First boundary vertex: We must show \(R(\pi _0(\tau _1)) \in \partial (g_1^{-1} \cdot e)\). By boundary equivariance, \(R(\pi _0(\tau _1)) \in \partial (g_1^{-1} \cdot e)\) iff \((g_1^{-1})^{-1} \cdot R(\pi _0(\tau _1)) = g_1 \cdot R(\pi _0(\tau _1)) \in \partial e\). Since \(g_1 \cdot R(\pi _0(\tau _1)) = \tau _1\) by the specification of \(\mathtt{vertexGroupElement}\), and \(\tau _1 \in \partial e\) by hypothesis, this holds.
(3) Second boundary vertex: We must show \(\phi _R(e;\tau _1,\tau _2) \cdot R(\pi _0(\tau _2)) \in \partial (g_1^{-1} \cdot e)\). Unfolding \(\mathtt{connectionOnEdge}\), we have \(\phi _R(e;\tau _1,\tau _2) = g_1^{-1} \cdot g_2\) where \(g_2 = \mathtt{vertexGroupElement}(R,\tau _2)\). By boundary equivariance, \((g_1^{-1} \cdot g_2) \cdot R(\pi _0(\tau _2)) \in \partial (g_1^{-1} \cdot e)\) iff \(g_1 \cdot (g_1^{-1} \cdot g_2) \cdot R(\pi _0(\tau _2)) = g_2 \cdot R(\pi _0(\tau _2)) = \tau _2 \in \partial e\), which holds by hypothesis. Rewriting using \(g_1 \cdot g_1^{-1} \cdot \tau _2 = \tau _2\) completes the argument.
If \(X_0\) is nonempty, then \((X/H)_0\) is nonempty.
Since \(X_0\) is nonempty, choose an arbitrary vertex \(v \in X_0\) by \(\mathtt{Classical.arbitrary}\). Then \([v] \in X_0/H\) witnesses that \((X/H)_0\) is nonempty.
If \(X_1\) is nonempty, then \((X/H)_1\) is nonempty.
Since \(X_1\) is nonempty, choose an arbitrary edge \(e \in X_1\) by \(\mathtt{Classical.arbitrary}\). Then \([e] \in X_1/H\) witnesses that \((X/H)_1\) is nonempty.