Simultaneous changes of signature and carrier

A simulation combines a circuit translation with a map between universes. It subsumes both ordinary homomorphisms and same-carrier realizations.

@[reducible, inline]

abbrev Algebraic.Simulation {σ : Signature} {τ : Signature} {U : Type u_3} {V : Type u_4} (translation : Translation σ τ) (source : Interpretation σ U) (target : Interpretation τ V) : Type (max u_3 u_4)

A simulation is precisely a homomorphism from the source interpretation to the target interpretation pulled back through the circuit translation.

Equations

• Algebraic.Simulation translation source target = Cslib.Circuits.Homomorphism source (translation.pull target)

def Algebraic.Simulation.id {σ : Signature} {U : Type u_2} (interpretation : Interpretation σ U) : Simulation (Translation.id σ) interpretation interpretation

Identity simulation on an interpreted signature.

Equations

• Algebraic.Simulation.id interpretation = { map := id, homomorphic := ⋯ }

def Algebraic.Simulation.comp {σ : Signature} {τ : Signature} {υ : Signature} {U : Type u_4} {V : Type u_5} {W : Type u_6} {innerTranslation : Translation σ τ} {outerTranslation : Translation τ υ} {source : Interpretation σ U} {middle : Interpretation τ V} {target : Interpretation υ W} (outer : Simulation outerTranslation middle target) (inner : Simulation innerTranslation source middle) : Simulation (outerTranslation.comp innerTranslation) source target

Compose simultaneous changes of signature and carrier.

Equations

• outer.comp inner = { map := outer.map ∘ inner.map, homomorphic := ⋯ }

def Algebraic.Simulation.ofPreserves {σ : Signature} {τ : Signature} {U : Type u_3} {V : Type u_4} {translation : Translation σ τ} {source : Interpretation σ U} {target : Interpretation τ V} (map : U → V) (preserves : ∀ (op : σ.Op) (input : Fin (σ.Arity op) → U), map (source op input) = (translation.operation op).eval target (map ∘ input) 0) : Simulation translation source target

Construct a simulation using the operation-circuit form of its preservation law.

Equations

• Algebraic.Simulation.ofPreserves map preserves = { map := map, homomorphic := preserves }

theorem Algebraic.Simulation.preserves {σ : Signature} {τ : Signature} {U : Type u_3} {V : Type u_4} {translation : Translation σ τ} {source : Interpretation σ U} {target : Interpretation τ V} (simulation : Simulation translation source target) (op : σ.Op) (input : Fin (σ.Arity op) → U) : simulation.map (source op input) = (translation.operation op).eval target (simulation.map ∘ input) 0

The homomorphism law of a simulation, exposed in operation-circuit form.

theorem Algebraic.Simulation.map_compile_eval {σ : Signature} {τ : Signature} {U : Type u_3} {V : Type u_4} {n m : ℕ} {translation : Translation σ τ} {source : Interpretation σ U} {target : Interpretation τ V} (simulation : Simulation translation source target) (circuit : Circuit σ n m) (input : Fin n → U) : simulation.map ∘ circuit.eval source input = (translation.compile circuit).eval target (simulation.map ∘ input)

Evaluation commutes with simultaneous signature compilation and carrier mapping.

def Cslib.Circuits.Homomorphism.toSimulation {σ : Signature} {U : Type u_2} {V : Type u_3} {source : Interpretation σ U} {target : Interpretation σ V} (homomorphism : Homomorphism source target) : Algebraic.Simulation (Algebraic.Translation.id σ) source target

Every ordinary homomorphism is a simulation through the identity translation.

Equations

• homomorphism.toSimulation = { map := homomorphism.map, homomorphic := ⋯ }

def Algebraic.Realization.toSimulation {σ : Signature} {U : Type u_2} {τ : Signature} {source : Interpretation σ U} {target : Interpretation τ U} (realization : Realization σ τ source target) : Simulation realization.toTranslation source target

Every same-carrier realization is a simulation with the identity carrier map.

Equations

• realization.toSimulation = { map := id, homomorphic := ⋯ }