The invariant structure Iᵏ A

The quotient of the k-tuples of a structure by ≡ᵏ (DescriptiveComplexity.InvMap) – the invariant of Dawar–Lindell–Weinstein 1995 – as a structure over the invariant vocabulary DescriptiveComplexity.invLang:

• one unary bit per coordinate equality (DescriptiveComplexity.InvRel.eqBit) and per base relation at a selection of coordinates (DescriptiveComplexity.InvRel.relBit) – the atomic type of a class;
• one binary substitution relation per pebble (DescriptiveComplexity.InvRel.sub): the classes reachable by moving that pebble – how the invariant structure quantifies over A;
• one binary rearrangement relation per coordinate selection (DescriptiveComplexity.InvRel.rearr): the class of a permuted, repeated, selected copy of a tuple – how the invariant structure reads relation variables at rearranged argument tuples.

The vocabulary does not depend on the agreement family S; the structure does, and interprets the bit of a base relation outside S as false, which keeps every interpretation well-defined on classes (DescriptiveComplexity.equivK_atomicAgreeOn_of_pairSub for the coordinate manipulations, the game move DescriptiveComplexity.EquivK.update for substitution).

The second half of the file equips Iᵏ A with a linear order: any coloring c₀ whose agreement is atomic agreement (the syntactic bit coloring of the definable refinement, in DescriptiveComplexity.Invariant.OrderDef) induces the canonical order DescriptiveComplexity.OrdK on tuples, which descends to a linear order on the classes (DescriptiveComplexity.invLinearOrder) – the order the simulated computation of the Abiteboul–Vianu argument runs on.

The invariant vocabulary

inductive DescriptiveComplexity.InvRel (L : FirstOrder.Language) (k : ℕ) : ℕ → Type

The relation symbols of the invariant vocabulary: atomic-type bits, substitution along a pebble, rearrangement along a coordinate selection.

• eqBit {L : FirstOrder.Language} {k : ℕ} (i j : Fin k) : InvRel L k 1

  The tuples of the class identify coordinates i and j.

• relBit {L : FirstOrder.Language} {k : ℕ} (R : (n : ℕ) × L.Relations n) (g : Fin R.fst → Fin k) : InvRel L k 1

  The base relation R holds on the tuples of the class at the selection g of coordinates.

• sub {L : FirstOrder.Language} {k : ℕ} (j : Fin k) : InvRel L k 2

  The second class is reached from the first by moving pebble j.

• rearr {L : FirstOrder.Language} {k : ℕ} (σ : Fin k → Fin k) : InvRel L k 2

  The second class is the rearrangement of the first along σ.

def DescriptiveComplexity.invLang (L : FirstOrder.Language) (k : ℕ) : FirstOrder.Language

The invariant vocabulary: the relational language of the invariant structure.

Equations

• DescriptiveComplexity.invLang L k = { Functions := fun (x : ℕ) => Empty, Relations := DescriptiveComplexity.InvRel L k }

instance DescriptiveComplexity.instIsRelationalInvLang (L : FirstOrder.Language) (k : ℕ) : (invLang L k).IsRelational

The quotient

def DescriptiveComplexity.invSetoid {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) (k : ℕ) (A : Type) [L.Structure A] : Setoid (Fin k → A)

k-tuples up to ≡ᵏ, as a setoid.

Equations

• DescriptiveComplexity.invSetoid S k A = { r := DescriptiveComplexity.EquivK (DescriptiveComplexity.atomicAgreeOn S A k), iseqv := ⋯ }

def DescriptiveComplexity.InvMap {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) (k : ℕ) (A : Type) [L.Structure A] : Type

The invariant structure's universe: the ≡ᵏ-classes of k-tuples over A, relative to the agreement family S.

Equations

• DescriptiveComplexity.InvMap S k A = Quotient (DescriptiveComplexity.invSetoid S k A)

def DescriptiveComplexity.InvMap.mk {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] (S : Set ((n : ℕ) × L.Relations n)) (u : Fin k → A) : InvMap S k A

The class of a k-tuple.

Equations

• DescriptiveComplexity.InvMap.mk S u = ⟦u⟧

theorem DescriptiveComplexity.InvMap.mk_eq_mk {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] {u v : Fin k → A} : mk S u = mk S v ↔ EquivK (atomicAgreeOn S A k) u v

theorem DescriptiveComplexity.InvMap.exists_rep {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] (c : InvMap S k A) : ∃ (u : Fin k → A), mk S u = c

instance DescriptiveComplexity.InvMap.instFinite {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] : Finite (InvMap S k A)

instance DescriptiveComplexity.InvMap.instNonempty {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Nonempty A] : Nonempty (InvMap S k A)

def DescriptiveComplexity.InvMap.eqBitRel {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] (i j : Fin k) : InvMap S k A → Prop

The equality bit on classes.

Equations

• DescriptiveComplexity.InvMap.eqBitRel i j = Quotient.lift (fun (u : Fin k → A) => u i = u j) ⋯

def DescriptiveComplexity.InvMap.relBitRel {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] (R : (n : ℕ) × L.Relations n) (g : Fin R.fst → Fin k) : InvMap S k A → Prop

The relation bit on classes: false outside the agreement family, the base relation at the selection inside it.

Equations

• DescriptiveComplexity.InvMap.relBitRel R g = Quotient.lift (fun (u : Fin k → A) => R ∈ S ∧ FirstOrder.Language.Structure.RelMap R.snd fun (p : Fin R.fst) => u (g p)) ⋯

def DescriptiveComplexity.InvMap.subRel {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] (j : Fin k) : InvMap S k A → InvMap S k A → Prop

The substitution relation on classes: the second class is reached from the first by a move of pebble j.

Equations

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

def DescriptiveComplexity.InvMap.rearrRel {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] (σ : Fin k → Fin k) : InvMap S k A → InvMap S k A → Prop

The rearrangement relation on classes: the second class is the rearrangement of the first along σ.

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.InvMap.structure' {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] : (invLang L k).Structure (InvMap S k A)

The invariant structure: the interpretation of the invariant vocabulary on the ≡ᵏ-classes.

Equations

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

Reading the relations at representatives

theorem DescriptiveComplexity.InvMap.relMap_eqBit {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] (i j : Fin k) (x : Fin 1 → InvMap S k A) (u : Fin k → A) (hu : x 0 = mk S u) : FirstOrder.Language.Structure.RelMap (InvRel.eqBit i j) x ↔ u i = u j

theorem DescriptiveComplexity.InvMap.relMap_relBit {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] (R : (n : ℕ) × L.Relations n) (g : Fin R.fst → Fin k) (x : Fin 1 → InvMap S k A) (u : Fin k → A) (hu : x 0 = mk S u) : FirstOrder.Language.Structure.RelMap (InvRel.relBit R g) x ↔ R ∈ S ∧ FirstOrder.Language.Structure.RelMap R.snd fun (p : Fin R.fst) => u (g p)

theorem DescriptiveComplexity.InvMap.relMap_sub {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] (j : Fin k) (x : Fin 2 → InvMap S k A) (u v : Fin k → A) (hu : x 0 = mk S u) (hv : x 1 = mk S v) : FirstOrder.Language.Structure.RelMap (InvRel.sub j) x ↔ ∃ (a : A), EquivK (atomicAgreeOn S A k) (Function.update u j a) v

theorem DescriptiveComplexity.InvMap.relMap_rearr {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] [Finite A] (σ : Fin k → Fin k) (x : Fin 2 → InvMap S k A) (u v : Fin k → A) (hu : x 0 = mk S u) (hv : x 1 = mk S v) : FirstOrder.Language.Structure.RelMap (InvRel.rearr σ) x ↔ EquivK (atomicAgreeOn S A k) (fun (p : Fin k) => u (σ p)) v

The linear order on the classes

@[instance_reducible]

noncomputable def DescriptiveComplexity.invLinearOrder {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] {β : Type u_1} [LinearOrder β] {c₀ : (Fin k → A) → β} [Finite A] (hc : colorAgree c₀ = atomicAgreeOn S A k) : LinearOrder (InvMap S k A)

Any coloring whose agreement is atomic agreement induces, through the canonical order on tuples (DescriptiveComplexity.OrdK), a linear order on the ≡ᵏ-classes (decidability by choice).

Equations

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

theorem DescriptiveComplexity.invLinearOrder_le_iff {L : FirstOrder.Language} {S : Set ((n : ℕ) × L.Relations n)} {k : ℕ} {A : Type} [L.Structure A] {β : Type u_1} [LinearOrder β] {c₀ : (Fin k → A) → β} [Finite A] (hc : colorAgree c₀ = atomicAgreeOn S A k) (u v : Fin k → A) : InvMap.mk S u ≤ InvMap.mk S v ↔ OrdK c₀ u v ∨ EquivK (atomicAgreeOn S A k) u v

The order on classes, read at representatives: strictly below in the canonical order, or equivalent.