theorem Hex.GraphIso.Nauty.Renaming.surjective {n : Nat} (σ : Renaming n) (v : Fin n) : ∃ (i : Fin n), σ.toFun ↑i = ↑v

Restricting an injective, range-preserving renaming to the finite vertex range gives a surjection of that range.

def Hex.GraphIso.Nauty.Renaming.toPerm {n : Nat} (σ : Renaming n) : Perm n

The finite permutation underlying a vertex renaming. This conversion is used in proofs connecting shared stabilizers to native graph adjacency.

Equations

• σ.toPerm = Hex.Perm.ofFn (fun (i : Fin n) => ⟨σ.toFun ↑i, ⋯⟩) ⋯ ⋯

@[simp]

theorem Hex.GraphIso.Nauty.Renaming.get_toPerm {n : Nat} (σ : Renaming n) (v : Fin n) : ↑(σ.toPerm.get v) = σ.toFun ↑v

theorem Hex.GraphIso.Nauty.Renaming.map_toPerm {n : Nat} (σ : Renaming n) (lab : Array Nat) (h : ∀ (i : Nat), i < lab.size → lab[i]! < n) : Array.map (renamingOf σ.toPerm).toFun lab = Array.map σ.toFun lab

On valid label entries, the standard extension of the finite permutation is exactly the original renaming.