def Hex.GraphIso.Sparse.Aut.stabilizer {n k : ℕ} (G : Colored n k) (base : List (Fin n)) : Subgroup (Perm n)

The full native automorphism group fixing the actual individualized base. This is a semantic subgroup, with no additional graph search.

Equations

• Hex.GraphIso.Sparse.Aut.stabilizer G base = { carrier := {p : Hex.Perm n | Hex.GraphIso.Sparse.IsIso G G p ∧ Hex.GraphIso.Perm.Fixes base p}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Hex.GraphIso.Sparse.Aut.mem_stabilizer {n k : ℕ} (G : Colored n k) (base : List (Fin n)) (p : Perm n) : p ∈ stabilizer G base ↔ IsIso G G p ∧ Perm.Fixes base p

theorem Hex.GraphIso.Sparse.Aut.stabilizer_nil {n k : ℕ} (G : Colored n k) : stabilizer G [] = group G

theorem Hex.GraphIso.Sparse.Aut.mem_stabilizer_orbit {n k : ℕ} (G : Colored n k) (base : List (Fin n)) (u v : Fin n) : v ∈ MulAction.orbit (↥(stabilizer G base)) u ↔ Aut.Orbit G.toDense base u v

def Hex.GraphIso.Sparse.Aut.stabilizerEquiv {n k : ℕ} (G : Colored n k) (base : List (Fin n)) (v : Fin n) : ↥(MulAction.stabilizer (↥(stabilizer G base)) v) ≃ ↥(stabilizer G (v :: base))

Adding the next first-path vertex to the base gives the ordinary point stabilizer of the preceding full stabilizer.

Equations

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

theorem Hex.GraphIso.Sparse.Aut.stabilizer_orbit_card {n k : ℕ} (G : Colored n k) (base : List (Fin n)) (v : Fin n) [DecidablePred (Aut.Orbit G.toDense base v)] : List.countP (fun (w : Fin n) => decide (Aut.Orbit G.toDense base v w)) (List.finRange n) = Nat.card ↑(MulAction.orbit (↥(stabilizer G base)) v)

The finite-vertex count used in the native index theorem is the cardinality of the corresponding full stabilizer orbit.

theorem Hex.GraphIso.Sparse.Aut.stabilizer_card {n k : ℕ} (G : Colored n k) (base : List (Fin n)) (v : Fin n) [DecidablePred (Aut.Orbit G.toDense base v)] : Nat.card ↥(stabilizer G base) = Nat.card ↥(stabilizer G (v :: base)) * List.countP (fun (w : Fin n) => decide (Aut.Orbit G.toDense base v w)) (List.finRange n)

Orbit–stabilizer for precisely the individualized base and guide whose index the sparse executable multiplies into its accumulator.