Skip to content

Setoid.Varieties.Properties

Properties of the models relation for setoid algebras

We prove some closure and invariance properties of the relation ⊧. In particular, we prove the following facts (which are needed, for example, in the proof the Birkhoff HSP Theorem).

  • Algebraic invariance. ⊧ is an algebraic invariant (stable under isomorphism).

  • Subalgebraic invariance. Identities modeled by a class of algebras are also modeled by all subalgebras of algebras in the class.

  • Product invariance. Identities modeled by a class of algebras are also modeled by all products of algebras in the class.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Varieties.Properties where

-- Imports from Agda and the Agda Standard Library -------------------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; proj₁ ; projβ‚‚ )
open import Function         using ( _∘_ ; Func ; _$_ )
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  ( π“ž ; π“₯ ; Signature ; 𝑆 )
open  import Overture.Terms                     using  ( Term ; β„Š )
open  import Setoid.Algebras                    using  ( Algebra ; Lift-AlgΛ‘ ; ov
                                                       ; π•Œ[_] ; 𝔻[_] ; β¨… )
open  import Setoid.Functions                   using  ( InvIsInverseΚ³ ; SurjInv )
open  import Setoid.Homomorphisms               using  ( hom ; _β‰…_ ; mkiso ; Lift-β‰…Λ‘
                                                       ; β‰…-sym ; _IsHomImageOf_ )
open  import Setoid.Subalgebras                 using  ( _≀_ ; SubalgebrasOfClass )
open  import Setoid.Terms                       using  ( 𝑻 ; module Environment
                                                       ; comm-hom-term ; interp-prod
                                                       ; term-agreement )
open  import Setoid.Varieties.SoundAndComplete  using  ( _⊧_ ; _⊫_ ; ⊫-proof ; _β‰ˆΜ‡_
                                                       ; _⊒_β–Ή_β‰ˆ_ )

private variable Ξ± ρᡃ Ξ² ρᡇ Ο‡ β„“ : Level

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

Algebraic invariance of ⊧

The binary relation ⊧ would be practically useless if it were not an algebraic invariant (i.e., invariant under isomorphism).

module _ {X : Type Ο‡}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}(𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ)(p q : Term {𝑆 = 𝑆} X) where
  open Environment 𝑨      using () renaming ( ⟦_⟧   to ⟦_βŸ§β‚ )
  open Environment 𝑩      using () renaming ( ⟦_⟧   to ⟦_βŸ§β‚‚ )
  open Setoid (Domain 𝑩)  using ( _β‰ˆ_ ; sym ; trans )
  open SetoidReasoning (Domain 𝑩)

  ⊧-I-invar : 𝑨 ⊧ (p β‰ˆΜ‡ q)  β†’  𝑨 β‰… 𝑩  β†’  𝑩 ⊧ (p β‰ˆΜ‡ q)
  ⊧-I-invar Apq (mkiso fh gh f∼g g∼f) ρ = trans i $ trans ii $ trans iii $ trans iv v
    where
    -- TODO: refactor this proof using new relational reasoning syntax/style
    f = _⟨$⟩_ (proj₁ fh) ; g = _⟨$⟩_ (proj₁ gh)

    i : ⟦ p βŸ§β‚‚ ⟨$⟩ ρ β‰ˆ ⟦ p βŸ§β‚‚ ⟨$⟩ (f ∘ (g ∘ ρ))
    i = sym $ cong ⟦ p βŸ§β‚‚ (f∼g ∘ ρ)

    ii : ⟦ p βŸ§β‚‚ ⟨$⟩ (f ∘ (g ∘ ρ)) β‰ˆ f (⟦ p βŸ§β‚ ⟨$⟩ (g ∘ ρ))
    ii = sym $ comm-hom-term fh p (g ∘ ρ)

    iii : f (⟦ p βŸ§β‚ ⟨$⟩ (g ∘ ρ)) β‰ˆ f (⟦ q βŸ§β‚ ⟨$⟩ (g ∘ ρ))
    iii = cong (proj₁ fh) $ Apq (g ∘ ρ)

    iv : f (⟦ q βŸ§β‚ ⟨$⟩ (g ∘ ρ)) β‰ˆ ⟦ q βŸ§β‚‚ ⟨$⟩ (f ∘ (g ∘ ρ))
    iv = comm-hom-term fh q (g ∘ ρ)

    v : ⟦ q βŸ§β‚‚ ⟨$⟩ (f ∘ (g ∘ ρ)) β‰ˆ ⟦ q βŸ§β‚‚ ⟨$⟩ ρ
    v = cong ⟦ q βŸ§β‚‚ (f∼g ∘ ρ)

As the proof makes clear, we show 𝑩 ⊧ p β‰ˆ q by showing that 𝑩 ⟦ p ⟧ ≑ 𝑩 ⟦ q ⟧ holds extensionally, that is, βˆ€ x, 𝑩 ⟦ p ⟧ x ≑ 𝑩 ⟦q ⟧ x.

Lift-invariance of ⊧

The ⊧ relation is also invariant under the algebraic lift and lower operations.

module _ {X : Type Ο‡}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ} where

  ⊧-Lift-invar : (p q : Term {𝑆 = 𝑆} X) β†’ 𝑨 ⊧ (p β‰ˆΜ‡ q) β†’ Lift-AlgΛ‘ 𝑨 Ξ² ⊧ (p β‰ˆΜ‡ q)
  ⊧-Lift-invar p q Apq = ⊧-I-invar (Lift-AlgΛ‘ 𝑨 _) p q Apq Lift-β‰…Λ‘

  ⊧-lower-invar : (p q : Term {𝑆 = 𝑆} X) β†’ Lift-AlgΛ‘ 𝑨 Ξ² ⊧ (p β‰ˆΜ‡ q)  β†’  𝑨 ⊧ (p β‰ˆΜ‡ q)
  ⊧-lower-invar p q lApq = ⊧-I-invar 𝑨 p q lApq (β‰…-sym Lift-β‰…Λ‘)

Homomorphic invariance of ⊧

Identities modeled by an algebra 𝑨 are also modeled by every homomorphic image of 𝑨, which fact can be formalized as follows.

module _ {X : Type Ο‡}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}{𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ}{p q : Term {𝑆 = 𝑆} X} where

  ⊧-H-invar : 𝑨 ⊧ (p β‰ˆΜ‡ q) β†’ 𝑩 IsHomImageOf 𝑨 β†’ 𝑩 ⊧ (p β‰ˆΜ‡ q)
  ⊧-H-invar Apq (Ο†h , Ο†E) ρ =
   begin
        ⟦ p ⟧   ⟨$⟩               ρ    β‰ˆΛ˜βŸ¨  cong ⟦ p ⟧(Ξ» _ β†’ InvIsInverseΚ³ Ο†E)  ⟩
        ⟦ p ⟧   ⟨$⟩ (Ο† ∘  φ⁻¹  ∘  ρ)   β‰ˆΛ˜βŸ¨  comm-hom-term Ο†h p (φ⁻¹ ∘ ρ)        ⟩
    Ο†(  ⟦ p ⟧ᴬ  ⟨$⟩ (     φ⁻¹  ∘  ρ))  β‰ˆβŸ¨   cong (proj₁ Ο†h) (Apq (φ⁻¹ ∘ ρ))         ⟩
    Ο†(  ⟦ q ⟧ᴬ  ⟨$⟩ (     φ⁻¹  ∘  ρ))  β‰ˆβŸ¨   comm-hom-term Ο†h q (φ⁻¹ ∘ ρ)        ⟩
        ⟦ q ⟧   ⟨$⟩ (Ο† ∘  φ⁻¹  ∘  ρ)   β‰ˆβŸ¨   cong ⟦ q ⟧(Ξ» _ β†’ InvIsInverseΚ³ Ο†E)  ⟩
        ⟦ q ⟧   ⟨$⟩               ρ    ∎
    where
    φ⁻¹ : π•Œ[ 𝑩 ] β†’ π•Œ[ 𝑨 ]
    φ⁻¹ = SurjInv (proj₁ Ο†h) Ο†E
    Ο† = (_⟨$⟩_ (proj₁ Ο†h))
    open Environment 𝑨  using () renaming ( ⟦_⟧ to ⟦_⟧ᴬ)
    open Environment 𝑩  using ( ⟦_⟧ )
    open SetoidReasoning 𝔻[ 𝑩 ]

Subalgebraic invariance of ⊧

Identities modeled by an algebra 𝑨 are also modeled by every subalgebra of 𝑨, which fact can be formalized as follows.

module _ {X : Type Ο‡}{p q : Term {𝑆 = 𝑆} X}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}{𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ} where
  open Environment 𝑨      using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
  open Environment 𝑩      using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
  open Setoid (Domain 𝑨)  using ( _β‰ˆ_ )
  open Setoid (Domain 𝑩)  using () renaming ( _β‰ˆ_ to _β‰ˆβ‚‚_ )
  open SetoidReasoning (Domain 𝑨)

  ⊧-S-invar : 𝑨 ⊧ (p β‰ˆΜ‡ q) β†’  𝑩 ≀ 𝑨  β†’  𝑩 ⊧ (p β‰ˆΜ‡ q)
  ⊧-S-invar Apq B≀A b = goal
    where
    hh : hom 𝑩 𝑨
    hh = (proj₁ B≀A)
    h = _⟨$⟩_ (proj₁ hh)
    ΞΎ : βˆ€ b β†’ h (⟦ p βŸ§β‚‚ ⟨$⟩ b) β‰ˆ h (⟦ q βŸ§β‚‚ ⟨$⟩ b)
    ΞΎ b = begin
           h (⟦ p βŸ§β‚‚ ⟨$⟩ b)    β‰ˆβŸ¨ comm-hom-term hh p b ⟩
           ⟦ p βŸ§β‚ ⟨$⟩ (h ∘ b)  β‰ˆβŸ¨ Apq (h ∘ b) ⟩
           ⟦ q βŸ§β‚ ⟨$⟩ (h ∘ b)  β‰ˆΛ˜βŸ¨ comm-hom-term hh q b ⟩
           h (⟦ q βŸ§β‚‚ ⟨$⟩ b)    ∎

    goal : ⟦ p βŸ§β‚‚ ⟨$⟩ b β‰ˆβ‚‚ ⟦ q βŸ§β‚‚ ⟨$⟩ b
    goal = (projβ‚‚ B≀A) (ΞΎ b)

Next, identities modeled by a class of algebras is also modeled by all subalgebras of the class. In other terms, every term equation (p β‰ˆΜ‡ q) that is satisfied by all 𝑨 ∈ 𝒦 is also satisfied by every subalgebra of a member of 𝒦.

module _ {X : Type Ο‡}{p q : Term {𝑆 = 𝑆} X} where

  ⊧-S-class-invar :  {𝒦 : Pred (Algebra {𝑆 = 𝑆} Ξ± ρᡃ) β„“}
   β†’                 (𝒦 ⊫ (p β‰ˆΜ‡ q)) β†’ ((𝑩 , _) : SubalgebrasOfClass 𝒦 {Ξ²}{ρᡇ})
   β†’                 𝑩 ⊧ (p β‰ˆΜ‡ q)
  ⊧-S-class-invar Kpq (𝑩 , 𝑨 , kA , B≀A) = ⊧-S-invar{p = p}{q} (Kpq .⊫-proof 𝑨 kA) B≀A

Product invariance of ⊧

An identity satisfied by all algebras in an indexed collection is also satisfied by the product of algebras in that collection.

module _ {X : Type Ο‡}{p q : Term {𝑆 = 𝑆} X}{I : Type β„“}(π’œ : I β†’ Algebra {𝑆 = 𝑆} Ξ± ρᡃ) where

  ⊧-P-invar : (βˆ€ i β†’ π’œ i ⊧ (p β‰ˆΜ‡ q)) β†’ β¨… π’œ ⊧ (p β‰ˆΜ‡ q)
  ⊧-P-invar π’œpq a = goal
    where
    open Algebra (β¨… π’œ)      using () renaming ( Domain to β¨…A )
    open Environment (β¨… π’œ)  using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
    open Environment        using ( ⟦_⟧ )
    open Setoid β¨…A          using ( _β‰ˆ_ )
    open SetoidReasoning β¨…A

    ΞΎ : (Ξ» i β†’ (⟦ π’œ i ⟧ p) ⟨$⟩ (Ξ» x β†’ (a x) i)) β‰ˆ (Ξ» i β†’ (⟦ π’œ i ⟧ q) ⟨$⟩ (Ξ» x β†’ (a x) i))
    ΞΎ = Ξ» i β†’ π’œpq i (Ξ» x β†’ (a x) i)
    goal : ⟦ p βŸ§β‚ ⟨$⟩ a β‰ˆ ⟦ q βŸ§β‚ ⟨$⟩ a
    goal = begin
            ⟦ p βŸ§β‚ ⟨$⟩ a                             β‰ˆβŸ¨ interp-prod π’œ p a ⟩
            (Ξ» i β†’ (⟦ π’œ i ⟧ p) ⟨$⟩ (Ξ» x β†’ (a x) i))  β‰ˆβŸ¨ ΞΎ ⟩
            (Ξ» i β†’ (⟦ π’œ i ⟧ q) ⟨$⟩ (Ξ» x β†’ (a x) i))  β‰ˆΛ˜βŸ¨ interp-prod π’œ q a ⟩
            ⟦ q βŸ§β‚ ⟨$⟩ a                             ∎

An identity satisfied by all algebras in a class is also satisfied by the product of algebras in the class.

  ⊧-P-class-invar :  (𝒦 : Pred (Algebra {𝑆 = 𝑆} Ξ± ρᡃ)(ov {𝑆 = 𝑆} Ξ±))
   β†’                 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ (βˆ€ i β†’ π’œ i ∈ 𝒦) β†’ β¨… π’œ ⊧ (p β‰ˆΜ‡ q)

  ⊧-P-class-invar 𝒦 Οƒ Kπ’œ = ⊧-P-invar (Ξ» i ρ β†’ Οƒ .⊫-proof (π’œ i) (Kπ’œ i) ρ)

Another fact that will turn out to be useful is that a product of a collection of algebras models (p β‰ˆΜ‡ q) if the lift of each algebra in the collection models (p β‰ˆΜ‡ q).

  ⊧-P-lift-invar : (βˆ€ i β†’ Lift-AlgΛ‘ (π’œ i) Ξ² ⊧ (p β‰ˆΜ‡ q))  β†’  β¨… π’œ ⊧ (p β‰ˆΜ‡ q)
  ⊧-P-lift-invar α = ⊧-P-invar Aipq
    where
    Aipq : βˆ€ i β†’ (π’œ i) ⊧ (p β‰ˆΜ‡ q)
    Aipq i = ⊧-lower-invar{𝑨 = (π’œ i)} p q (Ξ± i)

Modeled identities and homomorphism kernels

If an algebra 𝑨 models an identity (p β‰ˆΜ‡ q), then the pair (p , q) belongs to the kernel of every homomorphism Ο† : hom (𝑻 X) 𝑨 from the term algebra to 𝑨; that is, every homomorphism from 𝑻 X to 𝑨 maps p and q to the same element of 𝑨.

module _ {𝑆 : Signature π“ž π“₯}{X : Type Ο‡}{p q : Term {𝑆 = 𝑆} X}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}(Ο†h : hom (𝑻 X) 𝑨) where
  open Setoid (Domain 𝑨) using ( _β‰ˆ_ )
  private Ο† = _⟨$⟩_ (proj₁ Ο†h)

  ⊧-H-ker : 𝑨 ⊧ (p β‰ˆΜ‡ q) β†’ Ο† p β‰ˆ Ο† q
  ⊧-H-ker β =
   begin
    Ο† p                 β‰ˆβŸ¨ cong (proj₁ Ο†h) (term-agreement p)⟩
    Ο† (⟦ p ⟧ ⟨$⟩ β„Š)     β‰ˆβŸ¨ comm-hom-term Ο†h p β„Š ⟩
    ⟦ p βŸ§β‚‚ ⟨$⟩ (Ο† ∘ β„Š)  β‰ˆβŸ¨ Ξ² (Ο† ∘ β„Š) ⟩
    ⟦ q βŸ§β‚‚ ⟨$⟩ (Ο† ∘ β„Š)  β‰ˆΛ˜βŸ¨ comm-hom-term Ο†h q β„Š ⟩
    Ο† (⟦ q ⟧ ⟨$⟩ β„Š)     β‰ˆΛ˜βŸ¨ cong (proj₁ Ο†h) (term-agreement q)⟩
    Ο† q                 ∎

    where
    open SetoidReasoning (Domain 𝑨)
    open Environment 𝑨      using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
    open Environment (𝑻 X)  using ( ⟦_⟧ )