Independent copies of a second-order block

An exponential expansion (DescriptiveComplexity.ExpExpansion) defines an n-ary relation on its universe – the assignments of a block B – by a first-order sentence that must read n assignments at once. The vocabulary it is written over is therefore n independent copies of B.lang, packaged here as a single block DescriptiveComplexity.SOBlock.replicate:

• its relation variables are pairs (k, i) of a copy index and a variable of B, with the arity of i;
• DescriptiveComplexity.SOBlock.replicateAssign assembles one assignment per copy into an assignment of the replicated block – exactly, since the index type is a plain product;
• DescriptiveComplexity.SOBlock.replicateSym names the symbol of copy k, read back by DescriptiveComplexity.SOBlock.relMap_replicateSym.

This is a product presentation of a quantifier prefix, as opposed to the iterated-merge presentation of DescriptiveComplexity.repMerged (DescriptiveComplexity.SecondOrderReplicate), which is built by recursion on k and whose index type is a nest of sums. The product presentation is what this development needs, for one reason: replication commutes with the pullback of a block through an interpretation definitionally (DescriptiveComplexity.SOBlock.homAssign_replicatePullHom), because both sides re-associate the same Σ-type over a product. Pulling an expansion back through an interpretation is exactly that re-association, so the commutation is the lemma DescriptiveComplexity.Exponential.Pull rests on, and is proved by rfl.

The replicated block

def DescriptiveComplexity.SOBlock.replicate (B : SOBlock) (n : ℕ) : SOBlock

n independent copies of a block: one relation variable per pair of a copy index and a relation variable of B, keeping its arity.

Equations

• B.replicate n = { ι := Fin n × B.ι, ιFinite := ⋯, arity := fun (p : Fin n × B.ι) => B.arity p.2 }

@[simp]

theorem DescriptiveComplexity.SOBlock.replicate_arity (B : SOBlock) (n : ℕ) (p : Fin n × B.ι) : (B.replicate n).arity p = B.arity p.2

def DescriptiveComplexity.SOBlock.replicateAssign (B : SOBlock) {A : Type} {n : ℕ} (ρs : Fin n → B.Assignment A) : (B.replicate n).Assignment A

The assignment of the replicated block determined by one assignment per copy. The index type being a plain product, this is currying and nothing more.

Equations

• B.replicateAssign ρs p = ρs p.1 p.2

def DescriptiveComplexity.SOBlock.replicateSym (B : SOBlock) {n m : ℕ} (k : Fin n) (r : B.lang.Relations m) : (B.replicate n).lang.Relations m

The relation symbol of the k-th copy corresponding to a symbol of the block's own vocabulary.

Equations

• B.replicateSym k r = ⟨(k, ↑r), ⋯⟩

theorem DescriptiveComplexity.SOBlock.relMap_replicateSym (B : SOBlock) {A : Type} {n m : ℕ} (k : Fin n) (r : B.lang.Relations m) (ρs : Fin n → B.Assignment A) (v : Fin m → A) : FirstOrder.Language.Structure.RelMap (B.replicateSym k r) v ↔ FirstOrder.Language.Structure.RelMap r v

Reading back the relation variable of a copy.

Replication commutes with the pullback through an interpretation

DescriptiveComplexity.SOBlock.pull turns an a-ary variable on the interpreted universe Tag × A^d into one (a · d)-ary variable on A per tuple of tags. Applied to the replicated block it produces variables indexed by Σ (k, i), Fin (B.arity i) → Tag; replicating the pulled block produces variables indexed by Fin n × Σ i, Fin (B.arity i) → Tag. These are the same data re-associated, with equal arities, so the induced block morphism is an arity-preserving bijection and the transported assignments agree by rfl.

def DescriptiveComplexity.SOBlock.replicatePullHom (B : SOBlock) (T : Type) [Finite T] (d n : ℕ) : (pull T d (B.replicate n)).ι → ((pull T d B).replicate n).ι

The re-association of indices identifying the pullback of a replicated block with the replication of the pulled block.

Equations

• B.replicatePullHom T d n p = (p.fst.1, ⟨p.fst.2, p.snd⟩)

theorem DescriptiveComplexity.SOBlock.replicatePullHom_arity (B : SOBlock) (T : Type) [Finite T] (d n : ℕ) (i : (pull T d (B.replicate n)).ι) : ((pull T d B).replicate n).arity (B.replicatePullHom T d n i) = (pull T d (B.replicate n)).arity i

def DescriptiveComplexity.SOBlock.replicatePullLHom (B : SOBlock) (T : Type) [Finite T] (d n : ℕ) : (pull T d (B.replicate n)).lang →ᴸ ((pull T d B).replicate n).lang

The vocabulary morphism reading a sentence over the pullback of the replicated block inside the replication of the pulled block.

Equations

• B.replicatePullLHom T d n = DescriptiveComplexity.SOBlock.homLHom (B.replicatePullHom T d n) ⋯

theorem DescriptiveComplexity.SOBlock.homAssign_replicatePullHom (B : SOBlock) (T : Type) [Finite T] (d n : ℕ) {A : Type} (ρs : Fin n → B.Assignment (T × (Fin d → A))) : homAssign (B.replicatePullHom T d n) ⋯ ((pull T d B).replicateAssign fun (k : Fin n) => B.pullAssign (ρs k)) = (B.replicate n).pullAssign (B.replicateAssign ρs)

The commutation DescriptiveComplexity.Exponential.Pull rests on: replicating the pulled assignments and transporting back along the re-association gives the pullback of the replicated assignment. Both sides read ρs k i at the same decoded arguments, so this is definitional.