Definition 24: Quotient Graph Trivialization

Let X be a finite graph (1-dimensional cell complex, Def_7) equipped with a free right H-action on vertices and edges, compatible with the boundary map. The quotient graph X/H inherits a cell complex structure. A trivialization is a section R ⊆ X₀ of the quotient map on vertices (one representative per orbit). Given R, the induced connection φ_R : (X/H)₁ → H assigns to each edge orbit the unique group element relating the chosen vertex representatives.

Main Definitions

• GraphWithGroupAction: a graph with free right H-action compatible with boundary
• GraphWithGroupAction.quotientGraph: the quotient graph X/H
• GraphWithGroupAction.Trivialization: a section of the vertex quotient map
• GraphWithGroupAction.inducedConnection: the connection φ_R : (X/H)₁ → H

Main Results

• quotientGraph_cells_zero: (X/H)₀ = X₀/H (orbits of vertices)
• quotientGraph_cells_one: (X/H)₁ = X₁/H (orbits of edges)
• trivialization_nonempty: a trivialization exists (by the of choice)
• inducedConnection_spec: the connection satisfies the defining property

Graph with Group Action

structure GraphWithGroupAction (H : Type u) [Group H] [Fintype H] : Type (max 1 u)

A finite graph (1-dimensional cell complex) X with a free right action of a finite group H on vertices and edges, compatible with the boundary map, and satisfying the quotient condition (no edge connects v to vh for h ≠ 1).

We model the right action as H acting on the left via h ↦ (· * h⁻¹), i.e., MulAction H (X.cells 0) where h • v = v * h⁻¹ in right-action notation.

• graph : CellComplex

  The underlying graph as a cell complex (only degrees 0 and 1 are nontrivial).

• vertexAction : MulAction H (self.graph.cells 0)

  Right H-action on vertices X₀.

• edgeAction : MulAction H (self.graph.cells 1)

  Right H-action on edges X₁.

• vertexFree (h : H) (v : self.graph.cells 0) : h • v = v → h = 1

  The action on vertices is free.

• edgeFree (h : H) (e : self.graph.cells 1) : h • e = e → h = 1

  The action on edges is free.

• bdry_equivariant (e : self.graph.cells 1) (h : H) (τ : self.graph.cells 0) : τ ∈ self.graph.bdry (h • e) ↔ h⁻¹ • τ ∈ self.graph.bdry e

  Compatibility: ∂(h • e) = h • ∂(e), i.e., the boundary of a translated edge equals the translation of the boundary. Concretely, τ ∈ ∂(h • e) ↔ h⁻¹ • τ ∈ ∂e.

• quotientCondition (e : self.graph.cells 1) (v : self.graph.cells 0) (h : H) : v ∈ self.graph.bdry e → h • v ∈ self.graph.bdry e → h = 1

  Quotient condition: no edge connects v to h • v for h ≠ 1. Equivalently, if e has both v and h • v in its boundary, then h = 1.

instance GraphWithGroupAction.instMulActionCellsGraphOfNatInt {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : MulAction H (X.graph.cells 0)

Equations

• X.instMulActionCellsGraphOfNatInt = X.vertexAction

instance GraphWithGroupAction.instMulActionCellsGraphOfNatInt_1 {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : MulAction H (X.graph.cells 1)

Equations

• X.instMulActionCellsGraphOfNatInt_1 = X.edgeAction

Quotient Graph

def GraphWithGroupAction.quotientVertices {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : Type

The quotient type of vertices: (X/H)₀ = X₀ / H.

Equations

• X.quotientVertices = MulAction.orbitRel.Quotient H (X.graph.cells 0)

def GraphWithGroupAction.quotientEdges {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : Type

The quotient type of edges: (X/H)₁ = X₁ / H.

Equations

• X.quotientEdges = MulAction.orbitRel.Quotient H (X.graph.cells 1)

instance GraphWithGroupAction.instFintypeQuotientVertices {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : Fintype X.quotientVertices

Equations

• X.instFintypeQuotientVertices = Quotient.fintype (MulAction.orbitRel H (X.graph.cells 0))

instance GraphWithGroupAction.instFintypeQuotientEdges {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : Fintype X.quotientEdges

Equations

• X.instFintypeQuotientEdges = Quotient.fintype (MulAction.orbitRel H (X.graph.cells 1))

instance GraphWithGroupAction.instDecidableEqQuotientVertices {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : DecidableEq X.quotientVertices

Equations

• X.instDecidableEqQuotientVertices = Quotient.decidableEq

instance GraphWithGroupAction.instDecidableEqQuotientEdges {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : DecidableEq X.quotientEdges

Equations

• X.instDecidableEqQuotientEdges = Quotient.decidableEq

def GraphWithGroupAction.vertexQuot {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) (v : X.graph.cells 0) : X.quotientVertices

The quotient map on vertices: π₀ : X₀ → (X/H)₀.

Equations

• X.vertexQuot v = Quotient.mk'' v

def GraphWithGroupAction.edgeQuot {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) (e : X.graph.cells 1) : X.quotientEdges

The quotient map on edges: π₁ : X₁ → (X/H)₁.

Equations

• X.edgeQuot e = Quotient.mk'' e

theorem GraphWithGroupAction.bdry_orbit_compat {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (e : X.graph.cells 1) (h : H) (τ : X.graph.cells 0) (hτ : τ ∈ X.graph.bdry e) : h • τ ∈ X.graph.bdry (h • e)

The boundary map on the quotient graph is well-defined: if τ ∈ ∂e, then h • τ ∈ ∂(h • e) by equivariance.

def GraphWithGroupAction.quotientBdry {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (E : X.quotientEdges) : Finset X.quotientVertices

The boundary of an edge in the quotient: the set of vertex orbits that appear as boundaries of any representative edge.

Equations

• X.quotientBdry E = Quotient.liftOn E (fun (e : X.graph.cells 1) => Finset.image X.vertexQuot (X.graph.bdry e)) ⋯

theorem GraphWithGroupAction.quotientBdry_nonempty {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (E : X.quotientEdges) (hbdry : ∀ (e : X.graph.cells 1), (X.graph.bdry e).Nonempty) : (X.quotientBdry E).Nonempty

Witness: the quotient boundary of an edge orbit is nonempty, provided every edge has at least one boundary vertex (which holds for any graph).

Trivialization (Section of the quotient map)

structure GraphWithGroupAction.Trivialization {H : Type u} [Group H] [Fintype H] (X : GraphWithGroupAction H) : Type

A trivialization of the quotient map π : X → X/H is a section R ⊆ X₀ containing exactly one representative from each vertex orbit.

• repr : X.quotientVertices → X.graph.cells 0

  The representative function: for each vertex orbit, pick a representative.

• repr_mem (V : X.quotientVertices) : X.vertexQuot (self.repr V) = V

  Each representative lies in its orbit.

theorem GraphWithGroupAction.trivialization_exists {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) : Nonempty X.Trivialization

A trivialization always exists (by the of choice).

theorem GraphWithGroupAction.trivialization_nonempty {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) : Nonempty X.Trivialization

Witness: a trivialization is nonempty.

Induced Connection

def GraphWithGroupAction.vertexGroupElement {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (R : X.Trivialization) (v : X.graph.cells 0) : H

Given an edge e ∈ X₁ and a vertex v ∈ ∂e, the unique group element h such that v = h • repr(π(v)), i.e., the element relating v to its orbit representative.

Equations

• X.vertexGroupElement R v = ⋯.choose

theorem GraphWithGroupAction.vertexGroupElement_spec {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (R : X.Trivialization) (v : X.graph.cells 0) : X.vertexGroupElement R v • R.repr (X.vertexQuot v) = v

def GraphWithGroupAction.connectionOnEdge {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (R : X.Trivialization) (e : X.graph.cells 1) (τ₁ τ₂ : X.graph.cells 0) (hτ₁ : τ₁ ∈ X.graph.bdry e) (hτ₂ : τ₂ ∈ X.graph.bdry e) (hne : X.vertexQuot τ₁ ≠ X.vertexQuot τ₂) : H

For an edge e with boundary vertices τ₁, τ₂, the induced connection assigns the group element h such that the edge connects repr(π(τ₁)) to h • repr(π(τ₂)).

More precisely, if τ₁ ∈ ∂e and τ₂ ∈ ∂e with τ₁ = g₁ • repr(π(τ₁)) and τ₂ = g₂ • repr(π(τ₂)), then φ_R(π(e)) relates the two representatives via g₁⁻¹ • g₂. By the quotient condition, this is independent of the choice of representative edge in the orbit.

For simplicity, we define the connection as a function on edges of X (not the quotient), and prove it is constant on orbits.

Equations

• X.connectionOnEdge R e τ₁ τ₂ hτ₁ hτ₂ hne = (X.vertexGroupElement R τ₁)⁻¹ * X.vertexGroupElement R τ₂

theorem GraphWithGroupAction.connectionOnEdge_orbit_compat {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (R : X.Trivialization) (e : X.graph.cells 1) (g : H) (τ₁ τ₂ : X.graph.cells 0) (hτ₁ : τ₁ ∈ X.graph.bdry e) (hτ₂ : τ₂ ∈ X.graph.bdry e) (hne : X.vertexQuot τ₁ ≠ X.vertexQuot τ₂) (hgτ₁ : g • τ₁ ∈ X.graph.bdry (g • e)) (hgτ₂ : g • τ₂ ∈ X.graph.bdry (g • e)) (hne' : X.vertexQuot (g • τ₁) ≠ X.vertexQuot (g • τ₂)) : X.connectionOnEdge R (g • e) (g • τ₁) (g • τ₂) hgτ₁ hgτ₂ hne' = X.connectionOnEdge R e τ₁ τ₂ hτ₁ hτ₂ hne

The connection is well-defined on orbits: translating the edge by g does not change the connection value.

def GraphWithGroupAction.inducedConnection {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (R : X.Trivialization) (E : X.quotientEdges) : H

The induced connection as a map from quotient edges. For each edge orbit E, we pick a representative e, pick boundary vertices τ₁, τ₂, and compute connectionOnEdge. When the edge has both boundary vertices in the same orbit (which cannot happen by the quotient condition for edges connecting distinct orbits), we return 1.

Equations

• One or more equations did not get rendered due to their size.

theorem GraphWithGroupAction.inducedConnection_spec {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (R : X.Trivialization) (e : X.graph.cells 1) (τ₁ τ₂ : X.graph.cells 0) (hτ₁ : τ₁ ∈ X.graph.bdry e) (hτ₂ : τ₂ ∈ X.graph.bdry e) (hne : X.vertexQuot τ₁ ≠ X.vertexQuot τ₂) : ∃ (e' : X.graph.cells 1), X.edgeQuot e' = X.edgeQuot e ∧ R.repr (X.vertexQuot τ₁) ∈ X.graph.bdry e' ∧ X.connectionOnEdge R e τ₁ τ₂ hτ₁ hτ₂ hne • R.repr (X.vertexQuot τ₂) ∈ X.graph.bdry e'

The induced connection satisfies the defining property: for an edge e with boundary vertices τ₁ and τ₂ in distinct orbits, φ_R(π(e)) relates the representatives. Specifically, the edge g₁⁻¹ • e (where g₁ = vertexGroupElement R τ₁) connects repr(π(τ₁)) to φ_R(π(e)) • repr(π(τ₂)).

Witness lemmas

theorem GraphWithGroupAction.quotientVertices_nonempty {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) [Nonempty (X.graph.cells 0)] : Nonempty X.quotientVertices

Witness: the quotient vertices type is nonempty when the graph has vertices.

theorem GraphWithGroupAction.quotientEdges_nonempty {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) [Nonempty (X.graph.cells 1)] : Nonempty X.quotientEdges

Witness: the quotient edges type is nonempty when the graph has edges.