Pulling an exponential expansion back through an interpretation

An interpretation followed by an expansion is an expansion. Given an ordered first-order interpretation I of L' in L and an exponential expansion X of L'-structures, the composite A ↦ X.Map (I.Map A) is again an exponential expansion of L-structures, DescriptiveComplexity.ExpExpansion.pullOrdered. This is what makes DescriptiveComplexity.ExpDefinable closed under (ordered) first-order reductions, hence DescriptiveComplexity.ComplexityClass.exp a genuine complexity class; and, read the other way round, it is the formal content of the side condition the succinctness literature attaches to its upgrade theorem – that the reduction must act on the description rather than on the described instance.

Three existing pieces do the work, and no new mathematics is needed.

• The order of the interpreted universe is definable (DescriptiveComplexity.FOInterpretation.ordExtend): an expansion's sentences see the order of the structure they expand, so pulling them back through I requires I to define that order. It does, lexicographically, and DescriptiveComplexity.FOInterpretation.ordExtendLEquiv says the extended interpretation produces exactly the interpreted structure with the lexicographic order.
• A block pulls back through an interpretation (DescriptiveComplexity.SOBlock.pull, DescriptiveComplexity.FOInterpretation.extendSO): an a-ary relation variable on Tag × A^d becomes one (a·d)-ary relation variable on A per tuple of tags, and assignments correspond bijectively (DescriptiveComplexity.SOBlock.pullAssignEquiv).
• Replication commutes with that pullback (DescriptiveComplexity.SOBlock.homAssign_replicatePullHom), definitionally, which is why the defining sentences of the composite are the pulled ones read through a renaming of relation variables and nothing more.

The chain of transports is the one DescriptiveComplexity.SecondOrderTransitiveClosurePull runs for an DescriptiveComplexity.SOTCSpec, stated here over an arbitrary block so that one lemma – DescriptiveComplexity.ExpExpansion.realize_extendSO_pullSentence – serves both the domain sentence (one copy of the block) and every defining sentence (as many copies as the symbol has arguments).

Realizing a pulled block-expanded sentence

theorem DescriptiveComplexity.ExpExpansion.realize_extendSO_pullSentence {L L' : FirstOrder.Language} [L'.IsRelational] {T : Type} [Finite T] [LinearOrder T] {d : ℕ} (I : FOInterpretation (L.sum FirstOrder.Language.order) L' T d) (A : Type) [L.Structure A] [LinearOrder A] (Bk : SOBlock) (φ : ((L'.sum FirstOrder.Language.order).sum Bk.lang).Sentence) (ρ : Bk.Assignment (I.Map A)) : A ⊨ (I.ordExtendSO Bk).pullSentence φ ↔ I.Map A ⊨ φ

The transport lemma. A sentence over the ordered vocabulary of L' expanded by a block, read in the interpreted universe with the block interpreted by ρ, says in A exactly what its pullback says with the pulled block interpreted by the pulled assignment.

The three steps are the three ingredients of the module docstring: pull the sentence through the block-extended interpretation, identify the interpreted structure of the block extension with the block expansion of the interpreted structure, and identify the order the extended interpretation defines with the lexicographic order of DescriptiveComplexity.FOInterpretation.mapLinearOrder.

The pulled expansion

noncomputable def DescriptiveComplexity.ExpExpansion.pullOrdered {L L' : FirstOrder.Language} [L'.IsRelational] {T : Type} [Finite T] [LinearOrder T] {d : ℕ} (X : ExpExpansion L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' T d) [Nonempty T] : ExpExpansion L

An interpretation followed by an expansion is an expansion: the tags and the expanded vocabulary are unchanged, the block is pulled back, and every sentence is pulled back through the order-extended, block-extended interpretation – the defining sentences also being read through the renaming of relation variables that identifies the pullback of a replicated block with the replication of the pulled block.

Equations

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

The universes and the relations match

The pulled expansion has the same expanded vocabulary as the original, by definition; but DescriptiveComplexity.ExpExpansion.pullOrdered is not reducible, so the expanded structure has to be named rather than found by instance search. DescriptiveComplexity.ExpExpansion.pullOrderedStructure is that name, and it is the very term a goal about X.pullOrdered I elaborates to.

@[instance_reducible]

noncomputable def DescriptiveComplexity.ExpExpansion.pullOrderedStructure {L L' : FirstOrder.Language} [L'.IsRelational] {T : Type} [Finite T] [LinearOrder T] {d : ℕ} (X : ExpExpansion L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' T d) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty T] : X.E.Structure ((X.pullOrdered I).Map A)

The expanded structure of the pulled expansion, at the vocabulary of the original expansion – the two vocabularies being equal by definition.

Equations

• X.pullOrderedStructure I A = (X.pullOrdered I).mapStructure A

theorem DescriptiveComplexity.ExpExpansion.domHolds_pullOrdered {L L' : FirstOrder.Language} [L'.IsRelational] {T : Type} [Finite T] [LinearOrder T] {d : ℕ} (X : ExpExpansion L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' T d) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty T] (t : X.Tag) (ρ : X.B.Assignment (I.Map A)) : DomHolds (t, X.B.pullAssign ρ) ↔ DomHolds (t, ρ)

The domain condition of the pulled expansion, at the assignment pulled from the interpreted universe, is the domain condition of the original expansion.

theorem DescriptiveComplexity.ExpExpansion.domHolds_pullOrdered_merge {L L' : FirstOrder.Language} [L'.IsRelational] {T : Type} [Finite T] [LinearOrder T] {d : ℕ} (X : ExpExpansion L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' T d) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty T] (t : X.Tag) (σ : (SOBlock.pull T d X.B).Assignment A) : DomHolds (t, σ) ↔ DomHolds (t, X.B.mergeAssign σ)

The domain condition of the pulled expansion, read at a base assignment: the same condition on the assignment it merges to. This is DescriptiveComplexity.ExpExpansion.domHolds_pullOrdered in the direction the inverse of the universe bijection consumes it, stated at a variable assignment so that the round-trip rewrite happens away from any subtype coercion.

theorem DescriptiveComplexity.ExpExpansion.relMap_pullOrdered {L L' : FirstOrder.Language} [L'.IsRelational] {T : Type} [Finite T] [LinearOrder T] {d : ℕ} (X : ExpExpansion L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' T d) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty T] {n : ℕ} (r : X.E.Relations n) (ys : Fin n → X.Map (I.Map A)) (h : ∀ (i : Fin n), DomHolds ((↑(ys i)).1, X.B.pullAssign (↑(ys i)).2)) : (FirstOrder.Language.Structure.RelMap r fun (i : Fin n) => pt (↑(ys i)).1 (X.B.pullAssign (↑(ys i)).2) ⋯) ↔ FirstOrder.Language.Structure.RelMap r ys

The relations match: the defining sentence of the pulled expansion, at the pulled assignments, says what the original defining sentence says of the points of the expansion of the interpreted structure.

noncomputable def DescriptiveComplexity.ExpExpansion.pullOrderedLEquiv {L L' : FirstOrder.Language} [L'.IsRelational] {T : Type} [Finite T] [LinearOrder T] {d : ℕ} (X : ExpExpansion L') (I : FOInterpretation (L.sum FirstOrder.Language.order) L' T d) (A : Type) [L.Structure A] [LinearOrder A] [Nonempty T] : X.E.Equiv (X.Map (I.Map A)) ((X.pullOrdered I).Map A)

The expanded universes are isomorphic: the expansion of the interpreted structure is the pulled expansion of the base structure.

The bijection is DescriptiveComplexity.SOBlock.pullAssign on assignments, with DescriptiveComplexity.SOBlock.mergeAssign as its inverse; the tags are carried unchanged.

Equations

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