Homomorphisms of interpretations

A homomorphism between two interpretations of the same signature is a map of carriers that commutes with every operation. This file defines identity and composition and proves their laws.

The main use of homomorphisms in this library is that evaluation of lines, programs, and circuits commutes with them (Line.map_eval, Program.map_eval, Program.map_trace, and Circuit.map_eval).

structure Cslib.Circuits.Homomorphism {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} (i₁ : Interpretation σ U₁) (i₂ : Interpretation σ U₂) : Type (max u₁ u₂)

A map that preserves every operation in a pair of interpretations.

• map : U₁ → U₂

  The underlying map.

• homomorphic (op : σ.Op) (input : Fin (σ.Arity op) → U₁) : self.map (i₁ op input) = i₂ op (self.map ∘ input)

  The map commutes with every operation in the signature.

theorem Cslib.Circuits.Homomorphism.ext {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} {source : Interpretation σ U₁} {target : Interpretation σ U₂} {left right : Homomorphism source target} (map_eq : left.map = right.map) : left = right

theorem Cslib.Circuits.Homomorphism.ext_iff {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} {source : Interpretation σ U₁} {target : Interpretation σ U₂} {left right : Homomorphism source target} : left = right ↔ left.map = right.map

def Cslib.Circuits.Homomorphism.id {σ : Signature} {U : Type u} (interpretation : Interpretation σ U) : Homomorphism interpretation interpretation

The identity map is a homomorphism.

Equations

• Cslib.Circuits.Homomorphism.id interpretation = { map := id, homomorphic := ⋯ }

def Cslib.Circuits.Homomorphism.comp {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} {U₃ : Type u₃} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {i₃ : Interpretation σ U₃} (outer : Homomorphism i₂ i₃) (inner : Homomorphism i₁ i₂) : Homomorphism i₁ i₃

Compose homomorphisms in the direction of their underlying maps.

Equations

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

@[simp]

theorem Cslib.Circuits.Homomorphism.id_map {σ : Signature} {U : Type u} (interpretation : Interpretation σ U) : (id interpretation).map = _root_.id

@[simp]

theorem Cslib.Circuits.Homomorphism.comp_map {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} {U₃ : Type u₃} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {i₃ : Interpretation σ U₃} (outer : Homomorphism i₂ i₃) (inner : Homomorphism i₁ i₂) : (outer.comp inner).map = outer.map ∘ inner.map

@[simp]

theorem Cslib.Circuits.Homomorphism.id_comp {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} {source : Interpretation σ U₁} {target : Interpretation σ U₂} (homomorphism : Homomorphism source target) : (id target).comp homomorphism = homomorphism

@[simp]

theorem Cslib.Circuits.Homomorphism.comp_id {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} {source : Interpretation σ U₁} {target : Interpretation σ U₂} (homomorphism : Homomorphism source target) : homomorphism.comp (id source) = homomorphism

theorem Cslib.Circuits.Homomorphism.comp_assoc {σ : Signature} {U₁ : Type u₁} {U₂ : Type u₂} {U₃ : Type u₃} {U₄ : Type u₄} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {i₃ : Interpretation σ U₃} {i₄ : Interpretation σ U₄} (outer : Homomorphism i₃ i₄) (middle : Homomorphism i₂ i₃) (inner : Homomorphism i₁ i₂) : (outer.comp middle).comp inner = outer.comp (middle.comp inner)