The copies of an order-guessing expansion, and the problem read in one of them

DescriptiveComplexity.ExpExpansion.orderFree guesses the order into the block, and its universe is therefore the disjoint union, over the linear orders of the instance, of copies of the intended one. The copies are the classes of the symbol DescriptiveComplexity.ExpExpansion.sameSym, and this file reads the inner problem inside one of them:

• DescriptiveComplexity.ExpExpansion.clsPart is the part of a structure over the order-guessing vocabulary that a set of points carves out, read over the original vocabulary – a nullary symbol being read off its unary shift;
• DescriptiveComplexity.ExpExpansion.IsCls says that a set of points is one of the copies: nonempty, and consisting of exactly the points that carry the order of any one of its members;
• DescriptiveComplexity.ExpExpansion.someCls is “some copy answers yes”, the problem that replaces the inner one, and DescriptiveComplexity.ExpExpansion.someCls_map_iff is its correctness: on the expansion of a structure carrying no order, it says that the inner problem holds of the expanded universe for some linear order of the instance. Together with order-invariance – the equivalence being asked at every linear order in DescriptiveComplexity.ExpDefinable – that is what removes the order from the statement.

The whole content is the identification of a copy: a set of points satisfying IsCls is the image of the copy map at the order its members carry (DescriptiveComplexity.ExpExpansion.eq_range_copyIn), so it is isomorphic, over the original vocabulary, to the expanded universe read at that order (DescriptiveComplexity.ExpExpansion.clsEquiv).

Reducts along a language morphism

def DescriptiveComplexity.reductEquiv {F F' : FirstOrder.Language} (φ : F →ᴸ F') {M N : Type} [F'.Structure M] [F'.Structure N] (e : F'.Equiv M N) : F.Equiv M N

An isomorphism restricts to the reducts along a language morphism.

Equations

• DescriptiveComplexity.reductEquiv φ e = { toEquiv := e.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.vec_one_eq {M : Type} (z : M) : ![z] = fun (x : Fin (Nat.succ 0)) => z

A part of the order-guessing universe, over the original vocabulary

def DescriptiveComplexity.ExpExpansion.clsPart {L : FirstOrder.Language} (X : ExpExpansion L) {N : Type} [X.orderFree.E.Structure N] (S : Set N) : Type

The part of a structure over the order-guessing vocabulary that a set of points carves out. The expansion is a parameter although the carrier does not depend on it: it is what the structure below is read over.

Equations

• X.clsPart S = { x : N // x ∈ S }

@[instance_reducible]

instance DescriptiveComplexity.ExpExpansion.clsPartStructure {L : FirstOrder.Language} (X : ExpExpansion L) {N : Type} [X.orderFree.E.Structure N] (S : Set N) : X.E.Structure (X.clsPart S)

The part, read over the original vocabulary: a symbol of arity at least one holds of a tuple of the part as it held in the whole, and a nullary symbol holds when its unary shift holds of a point of the part.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.relMap_clsPart_zero {L : FirstOrder.Language} {X : ExpExpansion L} {N : Type} [X.orderFree.E.Structure N] {S : Set N} (r : X.E.Relations 0) (xs : Fin 0 → X.clsPart S) : FirstOrder.Language.Structure.RelMap r xs ↔ ∃ x ∈ S, FirstOrder.Language.Structure.RelMap (X.nullSym r) fun (x_1 : Fin 1) => x

theorem DescriptiveComplexity.ExpExpansion.relMap_clsPart_succ {L : FirstOrder.Language} {X : ExpExpansion L} {N : Type} [X.orderFree.E.Structure N] {S : Set N} {m : ℕ} (r : X.E.Relations (m + 1)) (xs : Fin (m + 1) → X.clsPart S) : FirstOrder.Language.Structure.RelMap r xs ↔ FirstOrder.Language.Structure.RelMap (X.origSym r) fun (i : Fin (m + 1)) => ↑(xs i)

def DescriptiveComplexity.ExpExpansion.IsCls {L : FirstOrder.Language} (X : ExpExpansion L) {N : Type} [X.orderFree.E.Structure N] (S : Set N) : Prop

A set of points is a copy: it is nonempty, and it consists of exactly the points carrying the order of any one of its members.

Equations

• X.IsCls S = ((∃ (x : N), x ∈ S) ∧ ∀ x ∈ S, ∀ (y : N), y ∈ S ↔ FirstOrder.Language.Structure.RelMap X.sameSym ![x, y])

Transporting a part along an isomorphism

noncomputable def DescriptiveComplexity.ExpExpansion.clsPartEquiv {L : FirstOrder.Language} (X : ExpExpansion L) {N N' : Type} [X.orderFree.E.Structure N] [X.orderFree.E.Structure N'] (e : X.orderFree.E.Equiv N N') (S : Set N) : X.E.Equiv (X.clsPart S) (X.clsPart (⇑e '' S))

A part is carried along an isomorphism of the ambient structures, over the original vocabulary.

Equations

• X.clsPartEquiv e S = { toFun := fun (x : X.clsPart S) => ⟨e ↑x, ⋯⟩, invFun := fun (y : X.clsPart (⇑e '' S)) => ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.ExpExpansion.isCls_image {L : FirstOrder.Language} (X : ExpExpansion L) {N N' : Type} [X.orderFree.E.Structure N] [X.orderFree.E.Structure N'] (e : X.orderFree.E.Equiv N N') (S : Set N) (h : X.IsCls S) : X.IsCls (⇑e '' S)

Membership of a transported copy.

Some copy answers yes

def DescriptiveComplexity.ExpExpansion.someCls {L : FirstOrder.Language} (X : ExpExpansion L) (Q : DecisionProblem X.E) : DecisionProblem X.orderFree.E

Some copy answers yes: the problem read inside one of the copies of an order-guessing expansion.

Equations

• X.someCls Q = { Holds := fun (N : Type) (x : X.orderFree.E.Structure N) => ∃ (S : Set N), X.IsCls S ∧ Q.Holds (X.clsPart S), iso_invariant := ⋯ }

A copy is the image of the copy map

theorem DescriptiveComplexity.ExpExpansion.eq_range_copyIn {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {S : Set (X.orderFree.Map A)} (hS : X.IsCls S) {p : X.orderFree.Map A} (hp : p ∈ S) (hord : ∀ (w : Fin 2 → A), pointOrd p w ↔ loRel w) : S = Set.range copyIn

Every copy is the image of a copy map: a set of points satisfying DescriptiveComplexity.ExpExpansion.IsCls, one of whose members carries the ambient order, consists of exactly the placed points.

def DescriptiveComplexity.ExpExpansion.toCls {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {S : Set (X.orderFree.Map A)} (hS : S = Set.range copyIn) (x : X.Map A) : X.clsPart S

The placed points, as a part of the order-guessing universe.

Equations

• DescriptiveComplexity.ExpExpansion.toCls hS x = ⟨DescriptiveComplexity.ExpExpansion.copyIn x, ⋯⟩

noncomputable def DescriptiveComplexity.ExpExpansion.clsEquiv {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {S : Set (X.orderFree.Map A)} (hS : S = Set.range copyIn) [Finite A] [Nonempty A] : X.E.Equiv (X.Map A) (X.clsPart S)

A copy is the expanded universe, over the original vocabulary and at the order its points carry.

Equations

• DescriptiveComplexity.ExpExpansion.clsEquiv hS = { toEquiv := Equiv.ofBijective (DescriptiveComplexity.ExpExpansion.toCls hS) ⋯, map_fun' := ⋯, map_rel' := ⋯ }

The correctness of “some copy answers yes”

theorem DescriptiveComplexity.ExpExpansion.someCls_map_iff {L : FirstOrder.Language} {X : ExpExpansion L} {Q : DecisionProblem X.E} {A : Type} [L.Structure A] [Finite A] [Nonempty A] : (X.someCls Q).Holds (X.orderFree.Map A) ↔ ∃ (lo : LinearOrder A), Q.Holds (X.Map A)

Some copy answers yes exactly when the inner problem does, at some linear order of the instance. The expansion is read on a structure carrying no order at all; each copy is the expanded universe at the order it guesses.