def Hex.GraphIso.Sparse.Aut.group {n k : ℕ} (G : Colored n k) : Subgroup (Perm n)

The full native colour-preserving automorphism subgroup. The dense interpretation here is a proof bridge and performs no graph search.

Equations

• Hex.GraphIso.Sparse.Aut.group G = Hex.GraphIso.Aut.group G.toDense

@[simp]

theorem Hex.GraphIso.Sparse.Aut.mem_group {n k : ℕ} (G : Colored n k) (p : Perm n) : p ∈ group G ↔ IsIso G G p

theorem Hex.GraphIso.Sparse.Aut.closure_eq_group {n k : ℕ} (G : Colored n k) : Subgroup.closure {p : Perm n | p ∈ gens G} = group G

The generators emitted by one sparse traversal generate the full automorphism subgroup, including for the empty graph.

theorem Hex.GraphIso.Sparse.Aut.mem_orbit {n k : ℕ} (G : Colored n k) (u v : Fin n) : v ∈ MulAction.orbit (↥(group G)) u ↔ SameOrbit G u v

noncomputable def Hex.GraphIso.Sparse.Aut.orbitEquiv {n k : ℕ} (G : Colored n k) : MulAction.orbitRel.Quotient (↥(group G)) (Fin n) ≃ { v : Fin n // (orbits G)[↑v]! = ↑v }

The actual least representatives identify the full automorphism orbit quotient with the vertices counted by the native orbit counter.

Equations

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

theorem Hex.GraphIso.Sparse.Aut.numOrbits_card {n k : ℕ} (G : Colored n k) : numOrbits G = Nat.card (MulAction.orbitRel.Quotient (↥(group G)) (Fin n))

The orbit count stored by the executed sparse traversal is exactly the cardinality of the full automorphism orbit quotient.