The two marked sides of an isomorphism problem, as structures

Every problem of the GI degree says “the two marked sides of the instance are isomorphic”, and every reduction between two such problems runs one gadget on the pattern side and the same gadget on the host side. The reductions built so far (DescriptiveComplexity.Problems.DagIso) pay for that shape twice: each characterization lemma is stated once for the pattern side and once, verbatim, for the host side.

This file is the first half of the cure. It reads a marked binary relation inside a structure as a FirstOrder.Language.graph-structure in its own right (DescriptiveComplexity.sideStructure), and shows that the semantic condition these problems use – DescriptiveComplexity.RelIsoOn, a bijection of the two marked sets preserving the relation in both directions – is exactly an isomorphism of those two structures (DescriptiveComplexity.relIsoOn_iff_nonempty_sideEquiv).

The point is what it makes statable: a gadget can then be given on single graphs, where the pattern/host distinction does not exist, and its correctness asked for in the form “F G ≅ F H implies G ≅ H” – one statement instead of two mirrored families. The forward implication is free, an interpretation being functorial (DescriptiveComplexity.FOInterpretation.mapLEquiv).

Nothing here is specific to a vocabulary: the side is given by a unary predicate and a binary one, so the same lemmas serve FirstOrder.Language.twoGraphs (patV/patE) and FirstOrder.Language.twoDags (patV/patArc), whose extra relations the isomorphism ignores.

A marked relation as a graph

@[instance_reducible]

def DescriptiveComplexity.sideStructure {A : Type} (V : A → Prop) (E : A → A → Prop) : FirstOrder.Language.graph.Structure { x : A // V x }

The marked part of a binary relation, as a structure over the language of graphs: the universe is the marked set, and adjacency is the relation.

Equations

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

@[simp]

theorem DescriptiveComplexity.sideStructure_adj {A : Type} (V : A → Prop) (E : A → A → Prop) (x y : { x : A // V x }) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] ↔ E ↑x ↑y

@[reducible, inline]

abbrev DescriptiveComplexity.SideEquiv {A : Type} (PV HV : A → Prop) (PE HE : A → A → Prop) : Type

An isomorphism of the two sides, as structures over the language of graphs.

Equations

• DescriptiveComplexity.SideEquiv PV HV PE HE = FirstOrder.Language.graph.Equiv { x : A // PV x } { y : A // HV y }

The generic property

def DescriptiveComplexity.RelIsoOn {A : Type} (PV HV : A → Prop) (PE HE : A → A → Prop) : Prop

Some map is a bijection of the PV-vertices onto the HV-vertices carrying PE-edges to HE-edges and back: an isomorphism of the two marked graphs. Compare DescriptiveComplexity.SubgraphIsoOn, which asks only for an injection and only for the forward implication.

Equations

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

theorem DescriptiveComplexity.RelIsoOn.of_equiv {A B : Type} (u : B ≃ A) {PVB HVB : B → Prop} {PEB HEB : B → B → Prop} {PVA HVA : A → Prop} {PEA HEA : A → A → Prop} (hPV : ∀ (b : B), PVB b ↔ PVA (u b)) (hHV : ∀ (b : B), HVB b ↔ HVA (u b)) (hPE : ∀ (b b' : B), PEB b b' ↔ PEA (u b) (u b')) (hHE : ∀ (b b' : B), HEB b b' ↔ HEA (u b) (u b')) (h : RelIsoOn PVB HVB PEB HEB) : RelIsoOn PVA HVA PEA HEA

RelIsoOn transports along an equivalence commuting with the four predicates.

theorem DescriptiveComplexity.RelIsoOn.equiv_iff {A B : Type} (u : B ≃ A) {PVB HVB : B → Prop} {PEB HEB : B → B → Prop} {PVA HVA : A → Prop} {PEA HEA : A → A → Prop} (hPV : ∀ (b : B), PVB b ↔ PVA (u b)) (hHV : ∀ (b : B), HVB b ↔ HVA (u b)) (hPE : ∀ (b b' : B), PEB b b' ↔ PEA (u b) (u b')) (hHE : ∀ (b b' : B), HEB b b' ↔ HEA (u b) (u b')) : RelIsoOn PVB HVB PEB HEB ↔ RelIsoOn PVA HVA PEA HEA

RelIsoOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.relIsoOn_iff_equiv {A : Type} (PV HV : A → Prop) (PE HE : A → A → Prop) : RelIsoOn PV HV PE HE ↔ ∃ (e : { x : A // PV x } ≃ { y : A // HV y }), ∀ (x y : { x : A // PV x }), PE ↑x ↑y ↔ HE ↑(e x) ↑(e y)

The property is isomorphism of the two marked graphs: a map of the universe as in DescriptiveComplexity.RelIsoOn is the same thing as an equivalence of the marked subsets carrying one adjacency relation to the other.

The two sides as structures

theorem DescriptiveComplexity.relIsoOn_iff_nonempty_sideEquiv {A : Type} (PV HV : A → Prop) (PE HE : A → A → Prop) : RelIsoOn PV HV PE HE ↔ Nonempty (SideEquiv PV HV PE HE)

The condition is an isomorphism of the two sides, as structures over the language of graphs. This is the form a gadget's correctness is stated against: on single graphs, where no pattern/host distinction exists.