↑ Top

Equation preservation for setoid algebras

This is the Setoid.Varieties.Preservation module of the Agda Universal Algebra Library where we show that the classes \af H \ab{𝒦}, \af S \ab{𝒦}, \af P \ab{𝒦}, and \af V \ab{𝒦} all satisfy the same identities.

{-# OPTIONS --without-K --exact-split --safe #-}

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.Varieties.Preservation {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library -------------------------------
open import Agda.Primitive         using ()       renaming ( Set to Type )
open import Data.Product           using ( _,_ )
                                   renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Data.Unit.Polymorphic  using ( ⊀ )
open import Function               using ( _∘_ )  renaming ( Func to _⟢_ )
open import Level                  using ( Level ; _βŠ”_ )
open import Relation.Binary        using ( Setoid )
open import Relation.Unary         using ( Pred ; _βŠ†_ ; _∈_ )

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from the Agda Universal Algebra Library -------------------------------
open  import Overture using ( ∣_∣ ; βˆ₯_βˆ₯ )
open  import Setoid.Functions
      using ( IsSurjective ; SurjInv ; SurjInvIsInverseΚ³ )

open  import Base.Terms {𝑆 = 𝑆} using ( Term )

open  import Setoid.Algebras {𝑆 = 𝑆}
      using ( Algebra ; ov ; π•Œ[_] ; Lift-Alg ; β¨… )

open  import Setoid.Homomorphisms {𝑆 = 𝑆}
      using ( ≅⨅⁺-refl ; β‰…-refl ; IdHomImage ; β‰…-sym )

open  import Setoid.Terms {𝑆 = 𝑆}
      using ( module Environment; comm-hom-term )

open  import Setoid.Subalgebras {𝑆 = 𝑆}
      using ( _≀_ ; _≀c_ ; β¨…-≀ ; β‰…-trans-≀ ; ≀-reflexive )

open  import Setoid.Varieties.Closure {𝑆 = 𝑆}
      using ( H ; S ; P ; S-expa ; H-expa ; V ; P-expa ; V-expa ;Level-closure )

open  import Setoid.Varieties.Properties {𝑆 = 𝑆}
      using ( ⊧-H-invar ; ⊧-S-invar ; ⊧-P-invar ; ⊧-I-invar )

open  import Setoid.Varieties.SoundAndComplete {𝑆 = 𝑆}
      using ( _⊧_ ; _⊨_ ; _⊫_ ; Eq ; _β‰ˆΜ‡_ ; lhs ; rhs ; _⊒_β–Ή_β‰ˆ_ ; Th)

open _⟢_      using ( cong ) renaming ( f to _⟨$⟩_ )
open Algebra  using ( Domain )

Closure properties

The types defined above represent operators with useful closure properties. We now prove a handful of such properties that we need later.

The next lemma would be too obvious to care about were it not for the fact that we’ll need it later, so it too must be formalized.

module _  {Ξ± ρᡃ β„“ : Level}{𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
 private
  a = Ξ± βŠ” ρᡃ
  oaβ„“ = ov (a βŠ” β„“)

 SβŠ†SP : βˆ€{ΞΉ} β†’ S β„“ 𝒦 βŠ† S {Ξ² = Ξ±}{ρᡃ} (a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦)
 SβŠ†SP {ΞΉ} (𝑨 , (kA , B≀A )) = 𝑨 , (pA , B≀A)
  where
  pA : 𝑨 ∈ P β„“ ΞΉ 𝒦
  pA = ⊀ , (Ξ» _ β†’ 𝑨) , (Ξ» _ β†’ kA) , ≅⨅⁺-refl

PS(𝒦) βŠ† SP(𝒦)

More class inclusions

We conclude this subsection with three more inclusion relations that will have bit parts to play later (e.g., in the formal proof of Birkhoff’s Theorem).

 PβŠ†SP : βˆ€{ΞΉ} β†’ P β„“ ΞΉ 𝒦 βŠ† S (a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦)
 PβŠ†SP {ΞΉ} x = S-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ} x


 PβŠ†HSP : βˆ€{ΞΉ} β†’  P {Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦
                 βŠ† H (a βŠ” β„“ βŠ” ΞΉ) (S {Ξ² = Ξ±}{ρᡃ}(a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦))
 PβŠ†HSP {ΞΉ} x = H-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ}  (S-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ} x)

 PβŠ†V : βˆ€{ΞΉ} β†’ P β„“ ΞΉ 𝒦 βŠ† V β„“ ΞΉ 𝒦
 PβŠ†V = PβŠ†HSP

 SPβŠ†V : βˆ€{ΞΉ} β†’ S{Ξ² = Ξ±}{ρᡇ = ρᡃ} (a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦) βŠ† V β„“ ΞΉ 𝒦
 SPβŠ†V {ΞΉ} x = H-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ} x

Finally, we are in a position to prove that a product of subalgebras of algebras in a class 𝒦 is a subalgebra of a product of algebras in 𝒦.

 PSβŠ†SP : P (a βŠ” β„“) oaβ„“ (S{Ξ² = Ξ±}{ρᡃ} β„“ 𝒦) βŠ† S oaβ„“ (P β„“ oaβ„“ 𝒦)
 PSβŠ†SP {𝑩} (I , ( π’œ , sA , Bβ‰…β¨…A )) = Goal
  where
  ℬ : I β†’ Algebra Ξ± ρᡃ
  ℬ i = ∣ sA i ∣
  kB : (i : I) β†’ ℬ i ∈ 𝒦
  kB i =  fst βˆ₯ sA i βˆ₯
  β¨…A≀⨅B : β¨… π’œ ≀ β¨… ℬ
  β¨…A≀⨅B = β¨…-≀ Ξ» i β†’ snd βˆ₯ sA i βˆ₯
  Goal : 𝑩 ∈ S{Ξ² = oaβ„“}{oaβ„“}oaβ„“ (P {Ξ² = oaβ„“}{oaβ„“} β„“ oaβ„“ 𝒦)
  Goal = β¨… ℬ , (I , (ℬ , (kB , β‰…-refl))) , (β‰…-trans-≀ Bβ‰…β¨…A β¨…A≀⨅B)

H preserves identities

First we prove that the closure operator H is compatible with identities that hold in the given class.

module _   {Ξ± ρᡃ β„“ Ο‡ : Level}
           {𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)}
           {X : Type Ο‡}
           {p q : Term X}
           where

 H-id1 : 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ H {Ξ² = Ξ±}{ρᡃ}β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 H-id1 Οƒ 𝑩 (𝑨 , kA , BimgA) = ⊧-H-invar{p = p}{q} (Οƒ 𝑨 kA) BimgA

The converse of the foregoing result is almost too obvious to bother with. Nonetheless, we formalize it for completeness.

 H-id2 : H β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 H-id2 Hpq 𝑨 kA = Hpq 𝑨 (𝑨 , (kA , IdHomImage))

S preserves identities

 S-id1 : 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ (S {Ξ² = Ξ±}{ρᡃ} β„“ 𝒦) ⊫ (p β‰ˆΜ‡ q)
 S-id1 Οƒ 𝑩 (𝑨 , kA , B≀A) = ⊧-S-invar{p = p}{q} (Οƒ 𝑨 kA) B≀A

 S-id2 : S β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 S-id2 Spq 𝑨 kA = Spq 𝑨 (𝑨 , (kA , ≀-reflexive))

P preserves identities

 P-id1 : βˆ€{ΞΉ} β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 P-id1 Οƒ 𝑨 (I , π’œ , kA , Aβ‰…β¨…A) = ⊧-I-invar 𝑨 p q IH (β‰…-sym Aβ‰…β¨…A)
  where
  ih : βˆ€ i β†’ π’œ i ⊧ (p β‰ˆΜ‡ q)
  ih i = Οƒ (π’œ i) (kA i)
  IH : β¨… π’œ ⊧ (p β‰ˆΜ‡ q)
  IH = ⊧-P-invar {p = p}{q} π’œ ih

 P-id2 : βˆ€{ΞΉ} β†’ P β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 P-id2{ΞΉ} PKpq 𝑨 kA = PKpq 𝑨 (P-expa {β„“ = β„“}{ΞΉ} kA)

V preserves identities

Finally, we prove the analogous preservation lemmas for the closure operator V.

module _  {Ξ± ρᡃ β„“ ΞΉ Ο‡ : Level}
          {𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)}
          {X : Type Ο‡}
          {p q : Term X} where

 private aβ„“ΞΉ = Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ

 V-id1 : 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ V β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 V-id1 Οƒ 𝑩 (𝑨 , (β¨…A , pβ¨…A , A≀⨅A) , BimgA) =
  H-id1{β„“ = aβ„“ΞΉ}{𝒦 = S aβ„“ΞΉ (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦)}{p = p}{q} spK⊧pq 𝑩 (𝑨 , (spA , BimgA))
   where
   spA : 𝑨 ∈ S aβ„“ΞΉ (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦)
   spA = β¨…A , (pβ¨…A , A≀⨅A)
   spK⊧pq : S aβ„“ΞΉ (P β„“ ΞΉ 𝒦) ⊫ (p β‰ˆΜ‡ q)
   spK⊧pq = S-id1{β„“ = aβ„“ΞΉ}{p = p}{q} (P-id1{β„“ = β„“} {𝒦 = 𝒦}{p = p}{q} Οƒ)

 V-id2 : V β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 V-id2 Vpq 𝑨 kA = Vpq 𝑨 (V-expa β„“ ΞΉ kA)

 Lift-id1 : βˆ€{Ξ² ρᡇ} β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ Level-closure{Ξ±}{ρᡃ}{Ξ²}{ρᡇ} β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 Lift-id1 pKq 𝑨 (𝑩 , kB , Bβ‰…A) ρ = Goal
  where
  open Environment 𝑨
  open Setoid (Domain 𝑨) using (_β‰ˆ_)
  Goal : ⟦ p ⟧ ⟨$⟩ ρ β‰ˆ ⟦ q ⟧ ⟨$⟩ ρ
  Goal = ⊧-I-invar 𝑨 p q (pKq 𝑩 kB) Bβ‰…A ρ

Class identities

From V-id1 it follows that if 𝒦 is a class of structures, then the set of identities modeled by all structures in 𝒦 is equivalent to the set of identities modeled by all structures in V 𝒦. In other terms, Th (V 𝒦) is precisely the set of identities modeled by 𝒦. We formalize this observation as follows.

 classIds-βŠ†-VIds : 𝒦 ⊫ (p β‰ˆΜ‡ q)  β†’ (p , q) ∈ Th (V β„“ ΞΉ 𝒦)
 classIds-βŠ†-VIds pKq 𝑨 = V-id1 pKq 𝑨

 VIds-βŠ†-classIds : (p , q) ∈ Th (V β„“ ΞΉ 𝒦) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 VIds-βŠ†-classIds Thpq 𝑨 kA = V-id2 Thpq 𝑨 kA

← Setoid.Varieties.Properties Setoid.Varieties.FreeAlgebras β†’