Maps of signatures

A map of signatures φ : σ.Hom τ sends each operation of σ to an operation of τ of the same arity. It is a map of the operation symbols, unlike cslib's Homomorphism, which maps the carriers of two interpretations of one signature. Signature.Hom.Preserves asks that φ keep the meaning of every operation. Circuits and formulas are translated along such maps in Cslib.Circuits.Circuit.mapOp; word-RAM programs in Cslib.WordRAM.Program.mapOp.

Main definitions

• Cslib.Circuits.Signature.Hom: an arity-preserving map of operations, with Hom.id and Hom.comp.
• Cslib.Circuits.Signature.Hom.Preserves: a map of operations keeps their meaning.

Main results

• Cslib.Circuits.Signature.Hom.comp_assoc, Cslib.Circuits.Signature.Hom.id_comp, Cslib.Circuits.Signature.Hom.comp_id: maps of signatures form a category.
• Cslib.Circuits.Signature.Hom.Preserves.comp: meaning-preserving maps compose.

structure Cslib.Circuits.Signature.Hom (σ : Signature) (τ : Signature) : Type (max u_1 u_2)

A map of signatures: an arity-preserving map of operations.

• toFun : σ.Op → τ.Op

  The image of each operation.

• arity_eq (op : σ.Op) : τ.Arity (self.toFun op) = σ.Arity op

  Operations keep their arity.

@[instance_reducible]

instance Cslib.Circuits.Signature.Hom.instFunLikeOp {σ : Signature} {τ : Signature} : FunLike (σ.Hom τ) σ.Op τ.Op

Maps of signatures are applied like functions.

@[simp]

theorem Cslib.Circuits.Signature.Hom.toFun_eq_coe {σ : Signature} {τ : Signature} (φ : σ.Hom τ) : φ.toFun = ⇑φ

theorem Cslib.Circuits.Signature.Hom.ext {σ : Signature} {τ : Signature} {φ ψ : σ.Hom τ} (h : ∀ (op : σ.Op), φ op = ψ op) : φ = ψ

Two maps of signatures agreeing on every operation are equal.

theorem Cslib.Circuits.Signature.Hom.ext_iff {σ : Signature} {τ : Signature} {φ ψ : σ.Hom τ} : φ = ψ ↔ ∀ (op : σ.Op), φ op = ψ op

def Cslib.Circuits.Signature.Hom.id (σ : Signature) : σ.Hom σ

The identity map of a signature.

def Cslib.Circuits.Signature.Hom.comp {σ : Signature} {τ : Signature} {υ : Signature} (ψ : τ.Hom υ) (φ : σ.Hom τ) : σ.Hom υ

The composition of maps of signatures.

@[simp]

theorem Cslib.Circuits.Signature.Hom.id_apply {σ : Signature} (op : σ.Op) : (Hom.id σ) op = op

@[simp]

theorem Cslib.Circuits.Signature.Hom.comp_apply {σ : Signature} {τ : Signature} {υ : Signature} (ψ : τ.Hom υ) (φ : σ.Hom τ) (op : σ.Op) : (ψ.comp φ) op = ψ (φ op)

@[simp]

theorem Cslib.Circuits.Signature.Hom.id_comp {σ : Signature} {τ : Signature} (φ : σ.Hom τ) : (Hom.id τ).comp φ = φ

@[simp]

theorem Cslib.Circuits.Signature.Hom.comp_id {σ : Signature} {τ : Signature} (φ : σ.Hom τ) : φ.comp (Hom.id σ) = φ

theorem Cslib.Circuits.Signature.Hom.comp_assoc {σ : Signature} {τ : Signature} {υ : Signature} {ω : Signature} (χ : υ.Hom ω) (ψ : τ.Hom υ) (φ : σ.Hom τ) : (χ.comp ψ).comp φ = χ.comp (ψ.comp φ)

Composition of maps of signatures is associative.

class Cslib.Circuits.Signature.Hom.Preserves {σ : Signature} {τ : Signature} {U : Type u_1} (φ : σ.Hom τ) (I : Interpretation σ U) (J : Interpretation τ U) : Prop

φ keeps the meaning of every operation: op means under I what φ op means under J.

• interpret_eq (op : σ.Op) (x : Fin (σ.Arity op) → U) : (J (φ op) fun (a : Fin (τ.Arity (φ op))) => x (Fin.cast ⋯ a)) = I op x

  The operation φ op means under J what op means under I.

instance Cslib.Circuits.Signature.Hom.preserves_id {σ : Signature} {U : Type u_1} (I : Interpretation σ U) : (Hom.id σ).Preserves I I

theorem Cslib.Circuits.Signature.Hom.Preserves.comp {σ : Signature} {τ : Signature} {υ : Signature} {U : Type u_1} {I : Interpretation σ U} {J : Interpretation τ U} {K : Interpretation υ U} {ψ : τ.Hom υ} {φ : σ.Hom τ} (hψ : ψ.Preserves J K) (hφ : φ.Preserves I J) : (ψ.comp φ).Preserves I K

A composition of meaning-preserving maps preserves meaning.