structure Hex.GraphIso.Sparse.Colored (n k : Nat) : Type

A sparse graph with the same ordered, surjective colouring as dense graphs.

• graph : SparseGraph n
• coloring : Coloring n k

def Hex.GraphIso.Sparse.instDecidableEqColored.decEq {n✝ k✝ : Nat} (x✝ x✝¹ : Colored n✝ k✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Sparse.instDecidableEqColored {n✝ k✝ : Nat} : DecidableEq (Colored n✝ k✝)

Equations

• Hex.GraphIso.Sparse.instDecidableEqColored = Hex.GraphIso.Sparse.instDecidableEqColored.decEq

def Hex.GraphIso.Sparse.Colored.toDense {n k : Nat} (G : Colored n k) : GraphIso.Colored n k

Explicitly materialize a dense coloured graph.

Equations

• G.toDense = { graph := G.graph.toDense, coloring := G.coloring }

def Hex.GraphIso.Sparse.Colored.relabel {n k : Nat} (G : Colored n k) (l : Label n) : Colored n k

Equations

• G.relabel l = { graph := G.graph.relabel l.perm, coloring := { cells := Hex.Vector.ofFn' fun (i : Fin n) => G.coloring.cells[l.get i], onto := ⋯ } }

@[simp]

theorem Hex.GraphIso.Sparse.Colored.toDense_relabel {n k : Nat} (G : Colored n k) (l : Label n) : (G.relabel l).toDense = G.toDense.relabel l

theorem Hex.GraphIso.Sparse.Colored.toDense_injective {n k : Nat} : Function.Injective toDense

@[simp]

theorem Hex.GraphIso.Sparse.Colored.relabel_id {n k : Nat} (G : Colored n k) : G.relabel (Label.id n) = G

theorem Hex.GraphIso.Sparse.Colored.relabel_relabel {n k : Nat} (G : Colored n k) (l m : Label n) : (G.relabel l).relabel m = G.relabel (l.comp m)

structure Hex.GraphIso.Sparse.CanonResult (n k : Nat) : Type

• form : Colored n k
• label : Label n

@[instance_reducible]

instance Hex.GraphIso.Sparse.instDecidableEqCanonResult {n✝ k✝ : Nat} : DecidableEq (CanonResult n✝ k✝)

Equations

• Hex.GraphIso.Sparse.instDecidableEqCanonResult = Hex.GraphIso.Sparse.instDecidableEqCanonResult.decEq

def Hex.GraphIso.Sparse.instDecidableEqCanonResult.decEq {n✝ k✝ : Nat} (x✝ x✝¹ : CanonResult n✝ k✝) : Decidable (x✝ = x✝¹)

Equations

• Hex.GraphIso.Sparse.instDecidableEqCanonResult.decEq { form := a, label := a_1 } { form := b, label := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯