Morphisms of second-order blocks

An arity-preserving map of relation variables induces a morphism of the blocks' vocabularies (DescriptiveComplexity.SOBlock.homLHom), and a sentence over a base vocabulary expanded by the source block transports to one over the base expanded by the target block (DescriptiveComplexity.SOBlock.realize_homSentence): realization against an assignment of the target block is realization against its pullback along the map (DescriptiveComplexity.SOBlock.homAssign).

This is the bookkeeping that reads a formula written for one block inside a larger block containing a copy of it. Its first consumer is the FO(≤, IFP) → FO(LFP) translation (DescriptiveComplexity.FixedPointInflationaryLFP), whose output sentence mentions the original relation variables while the translated program computes them as one group of a larger block; the invariant-structure simulations of DescriptiveComplexity.Invariant.Simulation want it for the same reason.

def DescriptiveComplexity.SOBlock.homLHom {B B' : SOBlock} (f : B.ι → B'.ι) (hf : ∀ (i : B.ι), B'.arity (f i) = B.arity i) : B.lang →ᴸ B'.lang

The vocabulary morphism induced by an arity-preserving map of relation variables.

Equations

• DescriptiveComplexity.SOBlock.homLHom f hf = { onFunction := fun {x : ℕ} (g : B.lang.Functions x) => isEmptyElim g, onRelation := fun {x : ℕ} (r : B.lang.Relations x) => ⟨f ↑r, ⋯⟩ }

def DescriptiveComplexity.SOBlock.homAssign {B B' : SOBlock} (f : B.ι → B'.ι) (hf : ∀ (i : B.ι), B'.arity (f i) = B.arity i) {A : Type} (σ : B'.Assignment A) : B.Assignment A

The pullback of an assignment of the target block along the map: each source variable reads its image.

Equations

• DescriptiveComplexity.SOBlock.homAssign f hf σ i x = σ (f i) fun (j : Fin (B'.arity (f i))) => x (Fin.cast ⋯ j)

theorem DescriptiveComplexity.SOBlock.homLHom_isExpansionOn {B B' : SOBlock} (f : B.ι → B'.ι) (hf : ∀ (i : B.ι), B'.arity (f i) = B.arity i) {A : Type} (σ : B'.Assignment A) : (homLHom f hf).IsExpansionOn A

The vocabulary morphism is an expansion between the two induced structures.

theorem DescriptiveComplexity.SOBlock.realize_homFormula {B B' : SOBlock} (f : B.ι → B'.ι) (hf : ∀ (i : B.ι), B'.arity (f i) = B.arity i) {L : FirstOrder.Language} {A : Type} [L.Structure A] {α : Type} (σ : B'.Assignment A) (φ : (L.sum B.lang).Formula α) (v : α → A) : (((FirstOrder.Language.LHom.id L).sumMap (homLHom f hf)).onFormula φ).Realize v ↔ φ.Realize v

Transport of a formula along a block morphism: realization over the target block's assignment is realization of the original formula over the pulled-back assignment.

theorem DescriptiveComplexity.SOBlock.realize_homSentence {B B' : SOBlock} (f : B.ι → B'.ι) (hf : ∀ (i : B.ι), B'.arity (f i) = B.arity i) {L : FirstOrder.Language} {A : Type} [L.Structure A] (σ : B'.Assignment A) (φ : (L.sum B.lang).Sentence) : A ⊨ ((FirstOrder.Language.LHom.id L).sumMap (homLHom f hf)).onSentence φ ↔ A ⊨ φ

Transport of a sentence along a block morphism: realization over the target block's assignment is realization of the original sentence over the pulled-back assignment.