Digraph Isomorphism is the generic isomorphism problem of the graph vocabulary

DescriptiveComplexity.DigraphIso was stated over the hand-rolled FirstOrder.Language.twoGraphs before the generic FirstOrder.Language.twoCopies existed. The two vocabularies are the same up to renaming – patV/patE against the pattern mark and the pattern copy of adj – and this file proves the problems are FO-interreducible, in both directions, by the interpretation that renames the symbols.

The payoff is DescriptiveComplexity.below_digraphIso_eq_below_twoCopiesIso: the degree of DescriptiveComplexity.DigraphIso is the degree of DescriptiveComplexity.TwoCopiesIso FirstOrder.Language.graph, and hence the GI degree. A problem stated over twoCopies – as every entry added from here on is meant to be – therefore reaches the degree through DescriptiveComplexity.isoReflecting_fo_reduction and this bridge, with no further vocabulary bookkeeping.

Renaming the hand-rolled vocabulary to the generic one

def DescriptiveComplexity.DigraphBridge.toTC : FOInterpretation FirstOrder.Language.twoGraphs FirstOrder.Language.graph.twoCopies Unit 1

The interpretation renaming twoGraphs to twoCopies graph: one tag, one dimension, each symbol to its counterpart.

Equations

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

def DescriptiveComplexity.DigraphBridge.ofTC : FOInterpretation FirstOrder.Language.graph.twoCopies FirstOrder.Language.twoGraphs Unit 1

The interpretation renaming twoCopies graph back to twoGraphs.

Equations

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

The one-dimensional universe

def DescriptiveComplexity.DigraphBridge.toPt {A : Type} (v : A) : toTC.Map A

The unique copy of an element, going to the generic vocabulary.

Equations

• DescriptiveComplexity.DigraphBridge.toPt v = ((), fun (x : Fin 1) => v)

def DescriptiveComplexity.DigraphBridge.ofPt {A : Type} (v : A) : ofTC.Map A

The unique copy of an element, coming back.

Equations

• DescriptiveComplexity.DigraphBridge.ofPt v = ((), fun (x : Fin 1) => v)

def DescriptiveComplexity.DigraphBridge.toEquivMap {A : Type} : toTC.Map A ≃ A

The image universe is a copy of the original.

Equations

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

def DescriptiveComplexity.DigraphBridge.ofEquivMap {A : Type} : ofTC.Map A ≃ A

The image universe is a copy of the original, coming back.

Equations

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

What the renamings realize

theorem DescriptiveComplexity.DigraphBridge.toTC_patMark {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (p : toTC.Map A) : TCPatMark p ↔ TGPatV (p.2 0)

theorem DescriptiveComplexity.DigraphBridge.toTC_hostMark {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (p : toTC.Map A) : TCHostMark p ↔ TGHostV (p.2 0)

theorem DescriptiveComplexity.DigraphBridge.toTC_patAdj {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (p q : toTC.Map A) : FirstOrder.Language.Structure.RelMap (FirstOrder.Language.tcPat FirstOrder.Language.adj) ![p, q] ↔ TGPatE (p.2 0) (q.2 0)

theorem DescriptiveComplexity.DigraphBridge.toTC_hostAdj {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (p q : toTC.Map A) : FirstOrder.Language.Structure.RelMap (FirstOrder.Language.tcHost FirstOrder.Language.adj) ![p, q] ↔ TGHostE (p.2 0) (q.2 0)

theorem DescriptiveComplexity.DigraphBridge.ofTC_patV {A : Type} [FirstOrder.Language.graph.twoCopies.Structure A] (p : ofTC.Map A) : TGPatV p ↔ TCPatMark (p.2 0)

theorem DescriptiveComplexity.DigraphBridge.ofTC_hostV {A : Type} [FirstOrder.Language.graph.twoCopies.Structure A] (p : ofTC.Map A) : TGHostV p ↔ TCHostMark (p.2 0)

theorem DescriptiveComplexity.DigraphBridge.ofTC_patE {A : Type} [FirstOrder.Language.graph.twoCopies.Structure A] (p q : ofTC.Map A) : TGPatE p q ↔ FirstOrder.Language.Structure.RelMap (FirstOrder.Language.tcPat FirstOrder.Language.adj) ![p.2 0, q.2 0]

theorem DescriptiveComplexity.DigraphBridge.ofTC_hostE {A : Type} [FirstOrder.Language.graph.twoCopies.Structure A] (p q : ofTC.Map A) : TGHostE p q ↔ FirstOrder.Language.Structure.RelMap (FirstOrder.Language.tcHost FirstOrder.Language.adj) ![p.2 0, q.2 0]

The generic side condition, as a relation isomorphism

def DescriptiveComplexity.DigraphBridge.TCPatAdj {B : Type} [FirstOrder.Language.graph.twoCopies.Structure B] (x y : B) : Prop

The pattern relation of a twoCopies graph-structure.

Equations

• DescriptiveComplexity.DigraphBridge.TCPatAdj x y = FirstOrder.Language.Structure.RelMap (FirstOrder.Language.tcPat FirstOrder.Language.adj) ![x, y]

def DescriptiveComplexity.DigraphBridge.TCHostAdj {B : Type} [FirstOrder.Language.graph.twoCopies.Structure B] (x y : B) : Prop

The host relation of a twoCopies graph-structure.

Equations

• DescriptiveComplexity.DigraphBridge.TCHostAdj x y = FirstOrder.Language.Structure.RelMap (FirstOrder.Language.tcHost FirstOrder.Language.adj) ![x, y]

theorem DescriptiveComplexity.DigraphBridge.patSide_relMap {B : Type} [FirstOrder.Language.graph.twoCopies.Structure B] (a b : { x : B // TCPatMark x }) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![a, b] ↔ TCPatAdj ↑a ↑b

The pattern side's adjacency, read on the ambient structure.

theorem DescriptiveComplexity.DigraphBridge.hostSide_relMap {B : Type} [FirstOrder.Language.graph.twoCopies.Structure B] (a b : { x : B // TCHostMark x }) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![a, b] ↔ TCHostAdj ↑a ↑b

The host side's adjacency, read on the ambient structure.

theorem DescriptiveComplexity.DigraphBridge.nonempty_tcSideEquiv_iff_relIsoOn {B : Type} [FirstOrder.Language.graph.twoCopies.Structure B] : Nonempty (TCSideEquiv B) ↔ RelIsoOn TCPatMark TCHostMark TCPatAdj TCHostAdj

The generic isomorphism condition is the concrete one: an isomorphism of the two sides, over the graph vocabulary, is a bijection of the two marks preserving the two relations. Stated through DescriptiveComplexity.relIsoOn_iff_equiv, whose right-hand side mentions no structure, so the two presentations of a side never have to be identified as instances.

Correctness of the two renamings

theorem DescriptiveComplexity.DigraphBridge.toTC_correct (A : Type) [FirstOrder.Language.twoGraphs.Structure A] [Finite A] : DigraphIso.Holds A ↔ (TwoCopiesIso FirstOrder.Language.graph).Holds (toTC.Map A)

Going to the generic vocabulary preserves the answer.

theorem DescriptiveComplexity.DigraphBridge.ofTC_correct (A : Type) [FirstOrder.Language.graph.twoCopies.Structure A] [Finite A] : (TwoCopiesIso FirstOrder.Language.graph).Holds A ↔ DigraphIso.Holds (ofTC.Map A)

Coming back preserves the answer.

The two reductions, and the degree

def DescriptiveComplexity.digraphIso_fo_reduction_twoCopiesIso : FOReduction DigraphIso (TwoCopiesIso FirstOrder.Language.graph)

Digraph Isomorphism reduces to the generic isomorphism problem of the graph vocabulary, by renaming the symbols.

Equations

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

def DescriptiveComplexity.twoCopiesIso_fo_reduction_digraphIso : FOReduction (TwoCopiesIso FirstOrder.Language.graph) DigraphIso

And back.

Equations

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

theorem DescriptiveComplexity.below_digraphIso_eq_below_twoCopiesIso : ComplexityClass.below DigraphIso = ComplexityClass.below (TwoCopiesIso FirstOrder.Language.graph)

Digraph Isomorphism and the generic isomorphism problem of the graph vocabulary have the same degree. A problem stated over twoCopies reaches the GI degree through this equality, so DescriptiveComplexity.isoReflecting_fo_reduction – a gadget on single structures – is all a new entry needs.