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.