theorem
Hex.GraphIso.Nauty.Generation.reverse_cells
{n : Nat}
{ctx : Ctx n}
{σ τ : Renaming n}
{level : Nat}
{U V : RefineSt n}
(hU : IterOk ctx level U)
(hsp : StPerm level V (mapSt σ U))
(hinv : ∀ (v : Nat), v < n → τ.toFun (σ.toFun v) = v)
:
Cell equivalence can be reversed through an inverse vertex renaming. Only inverses on the vertex range are needed.
theorem
Hex.GraphIso.Nauty.Generation.Uniform.transport
{n : Nat}
{ctx : Ctx n}
{σ τ : Renaming n}
{tcLevel level : Nat}
{U V : RefineSt n}
{targets : List Nat}
{key : Key n}
(h : Uniform ctx tcLevel level U targets key)
(hU : IterOk ctx level U)
(hsp : StPerm level V (mapSt σ U))
(hrows : RowsMap τ ctx.g ctx.g)
(hinv : ∀ (v : Nat), v < n → τ.toFun (σ.toFun v) = v)
:
Uniform ctx tcLevel level V targets key
Uniformity transports through the same graph and cell isomorphisms as a reference occurrence. The inverse transports arbitrary destination leaves back to the uniform source.