Doubling a gadget: one construction, run on each side

A reduction between two problems of the GI degree applies one construction to the pattern side of its input and the same construction to the host side. This file makes that a theorem about a single gadget: given an interpretation F of L₁ in L₀ – a construction taking one L₀-structure to one L₁-structure – it builds DescriptiveComplexity.FOInterpretation.double, mapping FirstOrder.Language.twoCopies L₀-instances to FirstOrder.Language.twoCopies L₁-instances by running F on each marked side, and identifies the sides of the result: the pattern side of F.double applied to A is F applied to the pattern side of A (DescriptiveComplexity.patSideDoubleEquiv).

Each side's defining formulas are those of F with every atom renamed to its copy for that side (DescriptiveComplexity.patLHom) and every quantifier restricted to that side's mark (DescriptiveComplexity.relativizeTo). The correctness of the two operations is proved together, by one induction (DescriptiveComplexity.realize_patRelativize): separately, the rename would have to cross a language reduct and the restriction a Substructure coercion, and the two identifications would then have to be composed with the subtype the side structures are actually stated on.

Renaming a base symbol to its copy

def DescriptiveComplexity.patLHom (L₀ : FirstOrder.Language) [L₀.IsRelational] : L₀ →ᴸ L₀.twoCopies

The base vocabulary, mapped onto its pattern copy.

Equations

• DescriptiveComplexity.patLHom L₀ = { onFunction := fun {x : ℕ} (f : L₀.Functions x) => isEmptyElim f, onRelation := fun {x : ℕ} (r : L₀.Relations x) => FirstOrder.Language.tcPat r }

def DescriptiveComplexity.hostLHom (L₀ : FirstOrder.Language) [L₀.IsRelational] : L₀ →ᴸ L₀.twoCopies

The base vocabulary, mapped onto its host copy.

Equations

• DescriptiveComplexity.hostLHom L₀ = { onFunction := fun {x : ℕ} (f : L₀.Functions x) => isEmptyElim f, onRelation := fun {x : ℕ} (r : L₀.Relations x) => FirstOrder.Language.tcHost r }

Reading a renamed, relativized formula on a side

theorem DescriptiveComplexity.realize_patRelativize {L₀ : FirstOrder.Language} [L₀.IsRelational] {A : Type} [L₀.twoCopies.Structure A] {α : Type} {n : ℕ} (φ : L₀.BoundedFormula α n) (v : α → { x : A // TCPatMark x }) (xs : Fin n → { x : A // TCPatMark x }) : ((relativizeTo L₀.tcPatMark ((patLHom L₀).onBoundedFormula φ)).Realize (fun (a : α) => ↑(v a)) fun (i : Fin n) => ↑(xs i)) ↔ φ.Realize v xs

The pattern side reads what the gadget wrote: a formula of the base vocabulary, renamed to the pattern copy and relativized to the pattern mark, holds in the ambient structure at arguments taken from the pattern side exactly when the original formula holds on that side.

theorem DescriptiveComplexity.realize_hostRelativize {L₀ : FirstOrder.Language} [L₀.IsRelational] {A : Type} [L₀.twoCopies.Structure A] {α : Type} {n : ℕ} (φ : L₀.BoundedFormula α n) (v : α → { x : A // TCHostMark x }) (xs : Fin n → { x : A // TCHostMark x }) : ((relativizeTo L₀.tcHostMark ((hostLHom L₀).onBoundedFormula φ)).Realize (fun (a : α) => ↑(v a)) fun (i : Fin n) => ↑(xs i)) ↔ φ.Realize v xs

The host side reads what the gadget wrote: a formula of the base vocabulary, renamed to the host copy and relativized to the host mark, holds in the ambient structure at arguments taken from the host side exactly when the original formula holds on that side.

The doubled interpretation

noncomputable def DescriptiveComplexity.FOInterpretation.double {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) : FOInterpretation L₀.twoCopies L₁.twoCopies Tag d

A gadget, run on both sides. The pattern copy of a relation symbol is defined by the gadget's own formula, its atoms renamed to the pattern copies and its quantifiers restricted to the pattern mark; the host copy likewise. A point belongs to a side exactly when all d of its coordinates do.

Equations

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

theorem DescriptiveComplexity.tcPatMark_double {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) {A : Type} [L₀.twoCopies.Structure A] (p : F.double.Map A) : TCPatMark p ↔ ∀ (j : Fin d), TCPatMark (p.2 j)

A point of the doubled construction is on the pattern side exactly when all its coordinates are.

theorem DescriptiveComplexity.tcHostMark_double {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) {A : Type} [L₀.twoCopies.Structure A] (p : F.double.Map A) : TCHostMark p ↔ ∀ (j : Fin d), TCHostMark (p.2 j)

The same, on the host side.

The sides of the doubled construction

noncomputable def DescriptiveComplexity.patSideDoubleEquiv {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] [L₁.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) {A : Type} [L₀.twoCopies.Structure A] : L₁.Equiv { p : F.double.Map A // TCPatMark p } (F.Map { x : A // TCPatMark x })

The pattern side of the doubled gadget is the gadget on the pattern side. This is what makes a reduction between isomorphism problems a statement about a construction on single structures: the two sides of the constructed instance are F applied to the two sides of the input, so an isomorphism of the former is one of the latter's images.

Equations

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

noncomputable def DescriptiveComplexity.hostSideDoubleEquiv {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] [L₁.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) {A : Type} [L₀.twoCopies.Structure A] : L₁.Equiv { p : F.double.Map A // TCHostMark p } (F.Map { x : A // TCHostMark x })

The same identification on the host side.

Equations

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

What a gadget has to satisfy

theorem DescriptiveComplexity.nonempty_double_sides_iff {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] [L₁.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) {A : Type} [L₀.twoCopies.Structure A] : Nonempty (TCSideEquiv (F.double.Map A)) ↔ Nonempty (L₁.Equiv (F.Map { x : A // TCPatMark x }) (F.Map { x : A // TCHostMark x }))

The two sides of the doubled construction are isomorphic exactly when the gadget's values on the two sides of the input are.

def DescriptiveComplexity.IsoReflecting {L₀ L₁ : FirstOrder.Language} [L₁.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) : Prop

A gadget reflects isomorphism when isomorphic values come from isomorphic arguments. The converse holds for free, an interpretation being functorial (DescriptiveComplexity.FOInterpretation.mapLEquiv), so this is the whole content a client has to supply – and it speaks about single structures, with no pattern/host distinction anywhere.

Equations

• DescriptiveComplexity.IsoReflecting F = ∀ (G H : Type) [inst : L₀.Structure G] [inst_1 : L₀.Structure H] [Finite G] [Finite H], Nonempty (L₁.Equiv (F.Map G) (F.Map H)) → Nonempty (L₀.Equiv G H)

theorem DescriptiveComplexity.twoCopiesIso_double_iff {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] [L₁.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) {A : Type} [L₀.twoCopies.Structure A] [Finite Tag] (hrefl : IsoReflecting F) (hA : Finite A) : (TwoCopiesIso L₀).Holds A ↔ (TwoCopiesIso L₁).Holds (F.double.Map A)

Correctness of a doubled gadget: the two sides of the input are isomorphic exactly when the two sides of its image are.

noncomputable def DescriptiveComplexity.isoReflecting_fo_reduction {L₀ L₁ : FirstOrder.Language} [L₀.IsRelational] [L₁.IsRelational] {Tag : Type} {d : ℕ} (F : FOInterpretation L₀ L₁ Tag d) [Finite Tag] [Nonempty Tag] (hrefl : IsoReflecting F) : FOReduction (TwoCopiesIso L₀) (TwoCopiesIso L₁)

A gadget that reflects isomorphism is a reduction: run it on both sides. Order-free, as a reduction between isomorphism problems must be.

Equations

• DescriptiveComplexity.isoReflecting_fo_reduction F hrefl = { Tag := Tag, tagFinite := inst✝¹, tagNonempty := inst✝, dim := d, toInterpretation := F.double, correct := ⋯ }