theorem Hex.GraphIso.Mathlib.Colored.Iso.ext {V : Type u} [Fintype V] {k : ℕ} {G : Colored V k} {f g : G.Iso G} (h : ∀ (v : V), f.graphIso v = g.graphIso v) : f = g

theorem Hex.GraphIso.Mathlib.Colored.Iso.ext_iff {V : Type u} [Fintype V] {k : ℕ} {G : Colored V k} {f g : G.Iso G} : f = g ↔ ∀ (v : V), f.graphIso v = g.graphIso v

@[instance_reducible]

instance Hex.GraphIso.Mathlib.instGroupIso {V : Type u} [Fintype V] {k : ℕ} {G : Colored V k} : Group (G.Iso G)

Equations

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

@[simp]

theorem Hex.GraphIso.Mathlib.Colored.Iso.one_apply {V : Type u} [Fintype V] {k : ℕ} {G : Colored V k} (v : V) : (graphIso 1) v = v

@[simp]

theorem Hex.GraphIso.Mathlib.Colored.Iso.mul_apply {V : Type u} [Fintype V] {k : ℕ} {G : Colored V k} (f g : G.Iso G) (v : V) : (f * g).graphIso v = f.graphIso (g.graphIso v)

@[simp]

theorem Hex.GraphIso.Mathlib.Colored.Iso.inv_apply {V : Type u} [Fintype V] {k : ℕ} {G : Colored V k} (f : G.Iso G) (v : V) : f⁻¹.graphIso v = f.graphIso.symm v

@[instance_reducible]

instance Hex.GraphIso.Mathlib.instMulActionIso {V : Type u} [Fintype V] {k : ℕ} {G : Colored V k} : MulAction (G.Iso G) V

Equations

• Hex.GraphIso.Mathlib.instMulActionIso = { smul := fun (f : G.Iso G) => ⇑f.graphIso, mul_smul := ⋯, one_smul := ⋯ }

def Hex.GraphIso.Mathlib.autEquiv {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : G.Iso G ≃* ↥(Aut.group (encode e G))

Encoding is an isomorphism of full automorphism groups.

Equations

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

theorem Hex.GraphIso.Mathlib.autos_complete {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (f : G.Iso G) : f ∈ Subgroup.closure {g : G.Iso G | g ∈ autos e G}

Every colour-preserving automorphism belongs to the subgroup generated by the decoded list.

theorem Hex.GraphIso.Mathlib.autos_sameOrbit {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (v w : V) : (Aut.orbits (encode e G))[↑(e v)]! = (Aut.orbits (encode e G))[↑(e w)]! ↔ ∃ (f : G.Iso G), f.graphIso v = w

The reported partition is exactly the full automorphism orbit relation.

noncomputable def Hex.GraphIso.Mathlib.autOrbitEquiv {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : MulAction.orbitRel.Quotient (G.Iso G) V ≃ MulAction.orbitRel.Quotient (↥(Aut.group (encode e G))) (Fin n)

Encoding preserves the full automorphism orbit quotient.

Equations

• Hex.GraphIso.Mathlib.autOrbitEquiv e G = Quotient.congr e ⋯

theorem Hex.GraphIso.Mathlib.autNumOrbits_card {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : autNumOrbits e G = Nat.card (MulAction.orbitRel.Quotient (G.Iso G) V)

The reported orbit count equals the cardinality of the Mathlib-facing full automorphism orbit quotient.

theorem Hex.GraphIso.Mathlib.autOrder_card {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : autOrder e G = Nat.card (G.Iso G)

The reported order equals the cardinality of the Mathlib-facing colour-preserving automorphism group.