The GI degree, collected

The degree is defined on DescriptiveComplexity.GraphIso, the undirected problem the literature names GI. Its members therefore reach it through the digraph-to-graph gadget of DescriptiveComplexity.Problems.GraphIso.Hardness, which is why the completeness theorems of the problems stated over the directed vocabulary are collected here rather than beside their reductions.

Complete for the degree: Graph Isomorphism itself (DescriptiveComplexity.graphIso_GI_complete), Digraph Isomorphism (DescriptiveComplexity.digraphIso_GI_complete) and DAG Isomorphism (DescriptiveComplexity.dagIso_GI_complete).

theorem DescriptiveComplexity.dagIso_mem_GI : GI.Mem DagIso

DAG Isomorphism belongs to the GI degree: forget the topological orders, then turn the digraph into a simple graph.

theorem DescriptiveComplexity.dagIso_GI_hard : GI.Hard DagIso

DAG Isomorphism is hard for the GI degree: Digraph Isomorphism, which is, reduces to it.

theorem DescriptiveComplexity.dagIso_GI_complete : GI.Complete DagIso

DAG Isomorphism is GI-complete: it reduces to Digraph Isomorphism by forgetting the carried topological orders, and Digraph Isomorphism reduces to it by subdividing every arc twice.