Documentation

Cslib.Computability.Circuit.Homomorphism

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).

source
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.

Instances For
    source
    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
    source
    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
    source
    def Cslib.Circuits.Homomorphism.id {σ : Signature} {U : Type u} (interpretation : Interpretation σ U) :
    Homomorphism interpretation interpretation

    The identity map is a homomorphism.

    Instances For
      source
      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.

      Instances For
        source
        @[simp]
        theorem Cslib.Circuits.Homomorphism.id_map {σ : Signature} {U : Type u} (interpretation : Interpretation σ U) :
        (id interpretation).map = _root_.id
        source
        @[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
        source
        @[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
        source
        @[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
        source
        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)