Definition 25: Invariant Labeling

Let X be a finite s-regular graph with a free right H-action (Def_24), and let Λ = {Λ_v}_{v ∈ X₀} be a labeling as in Def_15, assigning to each vertex v a bijection from the edges incident to v to [s] = Fin s.

The labeling Λ is H-invariant if Λ_{h • v}(h • e) = Λ_v(e) for all v ∈ X₀, e ∈ δv, and h ∈ H.

An H-invariant labeling descends to a well-defined labeling on the quotient graph X/H: for each vertex orbit [v] and edge orbit [e] incident to [v], define Λ̄_{[v]}([e]) = Λ_v(e).

Main Definitions

• CellLabeling: a labeling in the cell complex setting (bijection from incident edges to Fin s)
• IsInvariantLabeling: the H-invariance condition on a labeling
• quotientIncidentEdges: the incident edges in the quotient graph
• quotientLabeling: the descended labeling on X/H

Main Results

• isInvariantLabeling_nonempty: witness that the invariance premises are satisfiable
• quotientLabeling_well_defined: the quotient labeling is independent of representatives

Incident Edges in the Cell Complex

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

The set of edges incident to vertex v in the cell complex: δv = {e ∈ X₁ | v ∈ ∂e}.

Equations

• X.cellIncidentEdges v = {e : X.graph.cells 1 | v ∈ X.graph.bdry e}

theorem GraphWithGroupAction.mem_cellIncidentEdges {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (v : X.graph.cells 0) (e : X.graph.cells 1) : e ∈ X.cellIncidentEdges v ↔ v ∈ X.graph.bdry e

theorem GraphWithGroupAction.cellIncidentEdges_nonempty {H : Type u} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) (v : X.graph.cells 0) (e : X.graph.cells 1) (he : v ∈ X.graph.bdry e) : (X.cellIncidentEdges v).Nonempty

Witness: cellIncidentEdges v is non-empty whenever there is an edge incident to v.

Cell Complex Labeling

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

A labeling in the cell complex setting: for each vertex v, a bijection from the edges incident to v to Fin s. This is the cell complex analogue of Labeling (Def_15).

Equations

• X.CellLabeling s = ((v : X.graph.cells 0) → ↥(X.cellIncidentEdges v) ≃ Fin s)

H-Invariant Labeling

theorem GraphWithGroupAction.smul_incident_of_incident {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} (v : X.graph.cells 0) (e : X.graph.cells 1) (h : H) (he : e ∈ X.cellIncidentEdges v) : h • e ∈ X.cellIncidentEdges (h • v)

The H-action preserves incidence: if e is incident to v, then h • e is incident to h • v.

def GraphWithGroupAction.smulIncidentEdge {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} (v : X.graph.cells 0) (h : H) (e : ↥(X.cellIncidentEdges v)) : ↥(X.cellIncidentEdges (h • v))

Transport an element of cellIncidentEdges v to cellIncidentEdges (h • v) via the H-action.

Equations

• GraphWithGroupAction.smulIncidentEdge v h e = ⟨h • ↑e, ⋯⟩

def GraphWithGroupAction.IsInvariantLabeling {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} {s : ℕ} (Λ : X.CellLabeling s) : Prop

The labeling Λ is H-invariant if Λ_{h • v}(h • e) = Λ_v(e) for all v ∈ X₀, e ∈ δv, and h ∈ H. Using the left-action convention from Def_24 (where h • v models the right action v · h⁻¹).

Equations

• GraphWithGroupAction.IsInvariantLabeling Λ = ∀ (v : X.graph.cells 0) (h : H) (e : ↥(X.cellIncidentEdges v)), (Λ (h • v)) (GraphWithGroupAction.smulIncidentEdge v h e) = (Λ v) e

Witness: invariance premises are satisfiable

theorem GraphWithGroupAction.isInvariantLabeling_trivial_satisfiable : ∃ (H : Type) (x : Group H) (x_1 : Fintype H) (x_2 : DecidableEq H) (X : GraphWithGroupAction H) (s : ℕ) (Λ : X.CellLabeling s), IsInvariantLabeling Λ

Witness: the invariance condition is satisfiable for the trivial group H = Unit. Any labeling on a graph with trivial group action is invariant.

Quotient Labeling

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

The incident edges in the quotient graph: edge orbits [e] such that some representative edge has a boundary vertex in the orbit of v.

Equations

• GraphWithGroupAction.quotientIncidentEdges V = {E : X.quotientEdges | ∃ (e : X.graph.cells 1), X.edgeQuot e = E ∧ ∃ (v : X.graph.cells 0), X.vertexQuot v = V ∧ v ∈ X.graph.bdry e}

theorem GraphWithGroupAction.mem_quotientIncidentEdges {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} (V : X.quotientVertices) (E : X.quotientEdges) : E ∈ quotientIncidentEdges V ↔ ∃ (e : X.graph.cells 1), X.edgeQuot e = E ∧ ∃ (v : X.graph.cells 0), X.vertexQuot v = V ∧ v ∈ X.graph.bdry e

theorem GraphWithGroupAction.quotientIncident_of_incident {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} (v : X.graph.cells 0) (e : X.graph.cells 1) (he : e ∈ X.cellIncidentEdges v) : X.edgeQuot e ∈ quotientIncidentEdges (X.vertexQuot v)

Given a vertex v and an incident edge e ∈ δv, the quotient edge orbit [e] is incident to the quotient vertex orbit [v].

theorem GraphWithGroupAction.quotientIncidentEdges_nonempty {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} (v : X.graph.cells 0) (e : X.graph.cells 1) (he : v ∈ X.graph.bdry e) : (quotientIncidentEdges (X.vertexQuot v)).Nonempty

Witness: quotientIncidentEdges V is non-empty whenever there is an edge incident to a vertex in the orbit V.

def GraphWithGroupAction.quotientLabeling {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} {s : ℕ} (Λ : X.CellLabeling s) (hΛ : IsInvariantLabeling Λ) (V : X.quotientVertices) : ↥(quotientIncidentEdges V) ≃ Fin s

The quotient labeling on X/H, descended from an H-invariant labeling Λ. For a vertex orbit [v] and an incident edge orbit [e], we define Λ̄_{[v]}([e]) = Λ_v(e) using any representatives v ∈ [v] and e ∈ [e] with e ∈ δv. The H-invariance ensures this is well-defined.

Equations

• GraphWithGroupAction.quotientLabeling Λ hΛ V = Equiv.ofBijective (⇑(Λ ⋯.choose) ∘ fun (E : ↥(GraphWithGroupAction.quotientIncidentEdges V)) => ⋯.choose) ⋯

theorem GraphWithGroupAction.quotientLabeling_well_defined {H : Type u} [Group H] [Fintype H] [DecidableEq H] {X : GraphWithGroupAction H} {s : ℕ} (Λ : X.CellLabeling s) (hΛ : IsInvariantLabeling Λ) (v : X.graph.cells 0) (e : X.graph.cells 1) (he : v ∈ X.graph.bdry e) (h : H) (he' : h • v ∈ X.graph.bdry (h • e)) : (Λ (h • v)) ⟨h • e, ⋯⟩ = (Λ v) ⟨e, ⋯⟩

The quotient labeling is well-defined: using different representatives yields the same result. This follows from H-invariance.