Correctness of tagged interpretation composition

Flattening tags and coordinates is a bijection. Under that bijection, the coordinate environment for the composite agrees with the environment obtained by two successive interpretations. The pullback theorem supplies relation preservation.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.flatten_unflatten (card t₁ d₁ t₂ d₂ : ℕ) (x : Fin (t₂ * t₁ ^ d₂ * card ^ (d₂ * d₁))) : flattenElement card t₁ d₁ t₂ d₂ (unflattenElement card t₁ d₁ t₂ d₂ x) = x

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.unflatten_flatten (card t₁ d₁ t₂ d₂ : ℕ) (x : Fin (t₂ * (t₁ * card ^ d₁) ^ d₂)) : unflattenElement card t₁ d₁ t₂ d₂ (flattenElement card t₁ d₁ t₂ d₂ x) = x

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.comp_coordEnv {U : Vocabulary} {t₁ d₁ t₂ d₂ : ℕ} (A : FinStruct U) {arity : ℕ} (args : Fin arity → Fin (t₂ * t₁ ^ d₂ * A.card ^ (d₂ * d₁))) : coordEnv A (compTags fun (j : Fin arity) => ((elementEquiv A.card (t₂ * t₁ ^ d₂) (d₂ * d₁)) (args j)).1) (compCoords U arity d₁ d₂) (relationEnv args) = relationEnv (unflattenElement A.card t₁ d₁ t₂ d₂ ∘ args)

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.compIso {U V W : Vocabulary} {t₁ d₁ t₂ d₂ : ℕ} (I₂ : TaggedFOInterpretation V W t₂ d₂) (I₁ : TaggedFOInterpretation U V t₁ d₁) (A : FinStruct U) : Iso ((I₂.comp I₁).apply A) (I₂.apply (I₁.apply A))

The composite and successive interpretations agree up to their canonical presentation.

Equations

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