Two marked copies of a vocabulary, and the isomorphism problem they carry

Every problem of the GI degree has the same shape: one universe holding two marked structures over the same vocabulary, and the question whether they are isomorphic. DescriptiveComplexity.Problems.DigraphIso and DescriptiveComplexity.Problems.DagIso each hand-roll that shape (FirstOrder.Language.twoGraphs, FirstOrder.Language.twoDags), which is fine for one problem and wasteful for a family.

FirstOrder.Language.twoCopies L₁ builds it once: two unary marks, and two copies of every relation symbol of L₁. A structure over it carries an L₁-structure on each marked set (DescriptiveComplexity.patSideStructure, DescriptiveComplexity.hostSideStructure), and DescriptiveComplexity.TwoCopiesIso is the decision problem asking whether those two L₁-structures are isomorphic.

The reason to have it is the gadget layer this file is written for: a construction on single L₁-structures can be doubled – run relativized to each mark – only if the target vocabulary is known to be two copies of something, since the defining formulas have to be given symbol by symbol. Problems added to the degree from here on should be stated over twoCopies; the two existing hand-rolled vocabularies stay as they are, their results being already proved.

inductive FirstOrder.Language.twoCopiesRel (L₁ : Language) : ℕ → Type

Relation symbols of the two-copy vocabulary: a mark for each side, and two copies of every relation symbol of the base vocabulary.

• patMark {L₁ : Language} : L₁.twoCopiesRel 1

  patMark a: a belongs to the pattern side.

• hostMark {L₁ : Language} : L₁.twoCopiesRel 1

  hostMark a: a belongs to the host side.

• pat {L₁ : Language} {n : ℕ} (r : L₁.Relations n) : L₁.twoCopiesRel n

  The pattern copy of a relation symbol of the base vocabulary.

• host {L₁ : Language} {n : ℕ} (r : L₁.Relations n) : L₁.twoCopiesRel n

  The host copy of a relation symbol of the base vocabulary.

def FirstOrder.Language.twoCopies (L₁ : Language) : Language

Two marked copies of a relational vocabulary, sharing one universe.

Equations

• L₁.twoCopies = { Functions := fun (x : ℕ) => Empty, Relations := L₁.twoCopiesRel }

instance FirstOrder.Language.twoCopies_isRelational (L₁ : Language) : L₁.twoCopies.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.tcPatMark (L₁ : Language) : L₁.twoCopies.Relations 1

The pattern mark.

Equations

• L₁.tcPatMark = FirstOrder.Language.twoCopiesRel.patMark

@[reducible, inline]

abbrev FirstOrder.Language.tcHostMark (L₁ : Language) : L₁.twoCopies.Relations 1

The host mark.

Equations

• L₁.tcHostMark = FirstOrder.Language.twoCopiesRel.hostMark

@[reducible, inline]

abbrev FirstOrder.Language.tcPat {L₁ : Language} {n : ℕ} (r : L₁.Relations n) : L₁.twoCopies.Relations n

The pattern copy of a base relation symbol.

Equations

• FirstOrder.Language.tcPat r = FirstOrder.Language.twoCopiesRel.pat r

@[reducible, inline]

abbrev FirstOrder.Language.tcHost {L₁ : Language} {n : ℕ} (r : L₁.Relations n) : L₁.twoCopies.Relations n

The host copy of a base relation symbol.

Equations

• FirstOrder.Language.tcHost r = FirstOrder.Language.twoCopiesRel.host r

def DescriptiveComplexity.TCPatMark {L₁ : FirstOrder.Language} {A : Type} [L₁.twoCopies.Structure A] (a : A) : Prop

Belonging to the pattern side.

Equations

• DescriptiveComplexity.TCPatMark a = FirstOrder.Language.Structure.RelMap L₁.tcPatMark ![a]

def DescriptiveComplexity.TCHostMark {L₁ : FirstOrder.Language} {A : Type} [L₁.twoCopies.Structure A] (a : A) : Prop

Belonging to the host side.

Equations

• DescriptiveComplexity.TCHostMark a = FirstOrder.Language.Structure.RelMap L₁.tcHostMark ![a]

@[instance_reducible]

instance DescriptiveComplexity.patSideStructure {L₁ : FirstOrder.Language} [L₁.IsRelational] {A : Type} [L₁.twoCopies.Structure A] : L₁.Structure { x : A // TCPatMark x }

The pattern side, as a structure over the base vocabulary.

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.hostSideStructure {L₁ : FirstOrder.Language} [L₁.IsRelational] {A : Type} [L₁.twoCopies.Structure A] : L₁.Structure { x : A // TCHostMark x }

The host side, as a structure over the base vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.TCSideEquiv {L₁ : FirstOrder.Language} [L₁.IsRelational] (A : Type) [L₁.twoCopies.Structure A] : Type

An isomorphism of the two sides, over the base vocabulary.

Equations

• DescriptiveComplexity.TCSideEquiv A = L₁.Equiv { x : A // DescriptiveComplexity.TCPatMark x } { y : A // DescriptiveComplexity.TCHostMark y }

Isomorphism-invariance

def DescriptiveComplexity.patSideMap {L₁ : FirstOrder.Language} {A B : Type} [L₁.twoCopies.Structure A] [L₁.twoCopies.Structure B] (e : L₁.twoCopies.Equiv A B) (x : { x : A // TCPatMark x }) : { y : B // TCPatMark y }

An isomorphism of the ambient structures restricts to the pattern sides.

Equations

• DescriptiveComplexity.patSideMap e x = ⟨e ↑x, ⋯⟩

def DescriptiveComplexity.hostSideMap {L₁ : FirstOrder.Language} {A B : Type} [L₁.twoCopies.Structure A] [L₁.twoCopies.Structure B] (e : L₁.twoCopies.Equiv A B) (x : { x : A // TCHostMark x }) : { y : B // TCHostMark y }

An isomorphism of the ambient structures restricts to the host sides.

Equations

• DescriptiveComplexity.hostSideMap e x = ⟨e ↑x, ⋯⟩

def DescriptiveComplexity.patSideEquiv {L₁ : FirstOrder.Language} [L₁.IsRelational] {A B : Type} [L₁.twoCopies.Structure A] [L₁.twoCopies.Structure B] (e : L₁.twoCopies.Equiv A B) : L₁.Equiv { x : A // TCPatMark x } { y : B // TCPatMark y }

The restriction of an ambient isomorphism to the pattern sides is itself an isomorphism over the base vocabulary.

Equations

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

def DescriptiveComplexity.hostSideEquiv {L₁ : FirstOrder.Language} [L₁.IsRelational] {A B : Type} [L₁.twoCopies.Structure A] [L₁.twoCopies.Structure B] (e : L₁.twoCopies.Equiv A B) : L₁.Equiv { x : A // TCHostMark x } { y : B // TCHostMark y }

The restriction of an ambient isomorphism to the host sides.

Equations

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

theorem DescriptiveComplexity.nonempty_tcSideEquiv_congr {L₁ : FirstOrder.Language} [L₁.IsRelational] {A B : Type} [L₁.twoCopies.Structure A] [L₁.twoCopies.Structure B] (e : L₁.twoCopies.Equiv A B) : Nonempty (TCSideEquiv A) ↔ Nonempty (TCSideEquiv B)

Isomorphic sides transport along an isomorphism of the ambient structures.

def DescriptiveComplexity.TwoCopiesIso (L₁ : FirstOrder.Language) [L₁.IsRelational] : DecisionProblem L₁.twoCopies

The isomorphism problem of a vocabulary: are the two marked L₁-structures of the instance isomorphic? Every entry of the GI degree added from here on is an instance of this shape.

Equations

• DescriptiveComplexity.TwoCopiesIso L₁ = { Holds := fun (A : Type) (_inst : L₁.twoCopies.Structure A) => Finite A ∧ Nonempty (DescriptiveComplexity.TCSideEquiv A), iso_invariant := ⋯ }