↑ Top

Properties of the models relation

We prove some closure and invariance properties of the relation ⊧. In particular, we prove the following facts (which we use later in our proof of Birkhoff’s HSP Theorem).


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

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

module Base.Varieties.Properties {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library -------------------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Data.Product    using ( _,_ ; Ξ£-syntax ; _Γ—_ )
                            renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Function        using ( _∘_ )
open import Level           using ( Level ; _βŠ”_ )
open import Relation.Unary  using ( Pred ; _∈_ ; _βŠ†_ ; β‹‚ )
open import Axiom.Extensionality.Propositional
                            using () renaming ( Extensionality to funext )
open import Relation.Binary.PropositionalEquality
                            using ( _≑_ ; refl ; module ≑-Reasoning ; cong )

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture                     using ( ∣_∣ ; βˆ₯_βˆ₯ ; _⁻¹ )
open import Base.Functions               using ( IsInjective ; ∘-injective )
open import Base.Equality                using ( SwellDef ; DFunExt )
open import Base.Algebras       {𝑆 = 𝑆}  using ( Algebra ; Lift-Alg ; ov ; β¨… )
open import Base.Homomorphisms  {𝑆 = 𝑆}  using ( hom ; ∘-hom ; _β‰…_ ; mkiso )
                                         using ( Lift-β‰… ; β‰…-sym ; β‰…-trans )
open import Base.Terms          {𝑆 = 𝑆}  using ( Term ; 𝑻 ; lift-hom ; _⟦_⟧ )
                                         using ( comm-hom-term ; interp-prod )
                                         using ( term-agreement )
open import Base.Subalgebras    {𝑆 = 𝑆}  using ( _≀_ ; SubalgebraOfClass )
                                         using ( iso→injective )
open import Base.Varieties.EquationalLogic
                                {𝑆 = 𝑆}  using ( _⊧_β‰ˆ_ ; _⊫_β‰ˆ_ )

Algebraic invariance of ⊧

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


open Term
open ≑-Reasoning
open _β‰…_

module _  (wd : SwellDef){Ξ± Ξ² Ο‡ : Level}{X : Type Ο‡}{𝑨 : Algebra Ξ±}
          (𝑩 : Algebra Ξ²)(p q : Term X) where

 ⊧-I-invar : 𝑨 ⊧ p β‰ˆ q  β†’  𝑨 β‰… 𝑩  β†’  𝑩 ⊧ p β‰ˆ q

 ⊧-I-invar Apq (mkiso f g f∼g g∼f) x =
  (𝑩 ⟦ p ⟧) x                       β‰‘βŸ¨ i p ⟩
  (𝑩 ⟦ p ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘ x)   β‰‘βŸ¨ (ii p) ⁻¹ ⟩
  ∣ f ∣ ((𝑨 ⟦ p ⟧) (∣ g ∣ ∘ x))     β‰‘βŸ¨ cong ∣ f ∣ (Apq (∣ g ∣ ∘ x))  ⟩
  ∣ f ∣ ((𝑨 ⟦ q ⟧) (∣ g ∣ ∘ x))     β‰‘βŸ¨ ii q ⟩
  (𝑩 ⟦ q ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘  x)  β‰‘βŸ¨ (i q)⁻¹ ⟩
  (𝑩 ⟦ q ⟧) x                       ∎
  where
  i : βˆ€ t β†’ (𝑩 ⟦ t ⟧) x ≑ (𝑩 ⟦ t ⟧) Ξ» x₁ β†’ ∣ f ∣ (∣ g ∣ (x x₁))
  i t = wd Ο‡ Ξ² (𝑩 ⟦ t ⟧) x (∣ f ∣ ∘ ∣ g ∣ ∘ x) Ξ» i β†’ ( f∼g (x i))⁻¹

  ii :  βˆ€ t
   β†’    ∣ f ∣((𝑨 ⟦ t ⟧) Ξ» x₁ β†’ ∣ g ∣(x x₁)) ≑ (𝑩 ⟦ t ⟧) Ξ» x₁ β†’ ∣ f ∣(∣ g ∣(x x₁))
  ii t = comm-hom-term (wd π“₯ Ξ²) 𝑩 f t (∣ g ∣ ∘ x)

In the above proof we showed 𝑩 ⊧ 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 _ (wd : SwellDef){Ξ± Ξ² Ο‡ : Level}{X : Type Ο‡}{𝑨 : Algebra Ξ±} where

 ⊧-Lift-invar : (p q : Term X) β†’ 𝑨 ⊧ p β‰ˆ q β†’ Lift-Alg 𝑨 Ξ² ⊧ p β‰ˆ q
 ⊧-Lift-invar p q Apq = ⊧-I-invar wd (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 wd 𝑨 p q lApq (β‰…-sym Lift-β‰…)

Subalgebraic invariance of ⊧

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


module _ (wd : SwellDef){Ο‡ : Level}{𝓀 𝓦 : Level}{X : Type Ο‡} where

 ⊧-S-invar : {𝑨 : Algebra 𝓀}(𝑩 : Algebra 𝓦){p q : Term X}
  β†’          𝑨 ⊧ p β‰ˆ q  β†’  𝑩 ≀ 𝑨  β†’  𝑩 ⊧ p β‰ˆ q
 ⊧-S-invar {𝑨} 𝑩 {p}{q} Apq B≀A b = (βˆ₯ B≀A βˆ₯) (ΞΎ b)
  where
  h : hom 𝑩 𝑨
  h = ∣ B≀A ∣

  ΞΎ : βˆ€ b β†’ ∣ h ∣ ((𝑩 ⟦ p ⟧) b) ≑ ∣ h ∣ ((𝑩 ⟦ q ⟧) b)
  ΞΎ b =  ∣ h ∣((𝑩 ⟦ p ⟧) b)    β‰‘βŸ¨ comm-hom-term (wd π“₯ 𝓀) 𝑨 h p b ⟩
         (𝑨 ⟦ p ⟧)(∣ h ∣ ∘ b)  β‰‘βŸ¨ Apq (∣ h ∣ ∘ b) ⟩
         (𝑨 ⟦ q ⟧)(∣ h ∣ ∘ b)  β‰‘βŸ¨ (comm-hom-term (wd π“₯ 𝓀) 𝑨 h q b)⁻¹ ⟩
         ∣ h ∣((𝑩 ⟦ q ⟧) 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 𝒦.


 ⊧-S-class-invar :  {𝒦 : Pred (Algebra 𝓀)(ov 𝓀)}(p q : Term X)
  β†’                 𝒦 ⊫ p β‰ˆ q β†’ (𝑩 : SubalgebraOfClass 𝒦) β†’ ∣ 𝑩 ∣ ⊧ p β‰ˆ q

 ⊧-S-class-invar p q Kpq (𝑩 , 𝑨 , SA , (ka , Bβ‰…SA)) =
  ⊧-S-invar 𝑩 {p}{q}((Kpq ka)) (h , hinj)
   where
   h : hom 𝑩 𝑨
   h = ∘-hom 𝑩 𝑨 (to Bβ‰…SA) ∣ snd SA ∣
   hinj : IsInjective ∣ h ∣
   hinj = ∘-injective (isoβ†’injective Bβ‰…SA) βˆ₯ snd SA βˆ₯

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 _  (fe : DFunExt)(wd : SwellDef)
          {Ξ± Ξ² Ο‡ : Level}{I : Type Ξ²}
          (π’œ : I β†’ Algebra Ξ±){X : Type Ο‡} where

 ⊧-P-invar : (p q : Term X) β†’ (βˆ€ i β†’ π’œ i ⊧ p β‰ˆ q) β†’ β¨… π’œ ⊧ p β‰ˆ q
 ⊧-P-invar p q π’œpq a = goal
  where
  -- This is where function extensionality is used.
  ΞΎ : (Ξ» i β†’ (π’œ i ⟦ p ⟧) (Ξ» x β†’ (a x) i)) ≑ (Ξ» i β†’ (π’œ i ⟦ q ⟧)  (Ξ» x β†’ (a x) i))
  ΞΎ = fe Ξ² Ξ± Ξ» i β†’ π’œpq i (Ξ» x β†’ (a x) i)

  goal : (β¨… π’œ ⟦ p ⟧) a  ≑  (β¨… π’œ ⟦ q ⟧) a
  goal =  (β¨… π’œ ⟦ p ⟧) a                      β‰‘βŸ¨ interp-prod (wd π“₯ (Ξ± βŠ” Ξ²)) p π’œ a ⟩
          (Ξ» i β†’ (π’œ i ⟦ p ⟧)(Ξ» x β†’ (a x)i))  β‰‘βŸ¨ ΞΎ ⟩
          (Ξ» i β†’ (π’œ i ⟦ q ⟧)(Ξ» x β†’ (a x)i))  β‰‘βŸ¨ (interp-prod (wd π“₯ (Ξ± βŠ” Ξ²)) 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 : Term X}
  β†’                 𝒦 ⊫ p β‰ˆ q β†’ (βˆ€ i β†’ π’œ i ∈ 𝒦) β†’ β¨… π’œ ⊧ p β‰ˆ q

 ⊧-P-class-invar 𝒦 {p}{q}Οƒ Kπ’œ = ⊧-P-invar p q Ξ» 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 : (p q : Term X) β†’ (βˆ€ i β†’ Lift-Alg (π’œ i) Ξ² ⊧ p β‰ˆ q)  β†’  β¨… π’œ ⊧ p β‰ˆ q
 ⊧-P-lift-invar p q α = ⊧-P-invar p q Aipq
  where
  Aipq : βˆ€ i β†’ (π’œ i) ⊧ p β‰ˆ q
  Aipq i = ⊧-lower-invar wd p q (α i)

Homomorphic invariance of ⊧

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 _ (wd : SwellDef){Ξ± Ο‡ : Level}{X : Type Ο‡}{𝑨 : Algebra Ξ±} where

 ⊧-H-invar : {p q : Term X}(Ο† : hom (𝑻 X) 𝑨) β†’ 𝑨 ⊧ p β‰ˆ q  β†’  ∣ Ο† ∣ p ≑ ∣ Ο† ∣ q

 ⊧-H-invar {p}{q}Ο† Ξ² =  ∣ Ο† ∣ p                β‰‘βŸ¨ i p ⟩
                        ∣ Ο† ∣((𝑻 X ⟦ p ⟧) β„Š)   β‰‘βŸ¨ ii p ⟩
                        (𝑨 ⟦ p ⟧) (∣ Ο† ∣ ∘ β„Š)  β‰‘βŸ¨ Ξ² (∣ Ο† ∣ ∘ β„Š ) ⟩
                        (𝑨 ⟦ q ⟧) (∣ Ο† ∣ ∘ β„Š)  β‰‘βŸ¨ (ii q)⁻¹ ⟩
                        ∣ Ο† ∣ ((𝑻 X ⟦ q ⟧) β„Š)  β‰‘βŸ¨ (i q)⁻¹ ⟩
                        ∣ Ο† ∣ q                ∎

  where
  i : βˆ€ t β†’ ∣ Ο† ∣ t ≑ ∣ Ο† ∣ ((𝑻 X ⟦ t ⟧) β„Š)
  i t = cong ∣ Ο† ∣(term-agreement(wd π“₯ (ov Ο‡)) t)
  ii : βˆ€ t β†’ ∣ Ο† ∣ ((𝑻 X ⟦ t ⟧) β„Š) ≑ (𝑨 ⟦ t ⟧) (Ξ» x β†’ ∣ Ο† ∣ (β„Š x))
  ii t = comm-hom-term (wd π“₯ Ξ±) 𝑨 Ο† t β„Š

More generally, an identity is satisfied by all algebras in a class if and only if that identity is invariant under all homomorphisms from the term algebra 𝑻 X into algebras of the class. More precisely, if 𝒦 is a class of 𝑆-algebras and 𝑝, π‘ž terms in the language of 𝑆, then,

  𝒦 ⊧ p β‰ˆ q  ⇔  βˆ€ 𝑨 ∈ 𝒦,  βˆ€ Ο† : hom (𝑻 X) 𝑨,  Ο† ∘ (𝑻 X)⟦ p ⟧ = Ο† ∘ (𝑻 X)⟦ q ⟧.


module _ (wd : SwellDef){Ξ± Ο‡ : Level}{X : Type Ο‡}{𝒦 : Pred (Algebra Ξ±)(ov Ξ±)}  where

 -- β‡’ (the "only if" direction)
 ⊧-H-class-invar :  {p q : Term X}
  β†’                 𝒦 ⊫ p β‰ˆ q β†’ βˆ€ 𝑨 Ο† β†’ 𝑨 ∈ 𝒦 β†’ βˆ€ a
  β†’                 ∣ Ο† ∣ ((𝑻 X ⟦ p ⟧) a) ≑ ∣ Ο† ∣ ((𝑻 X ⟦ q ⟧) a)

 ⊧-H-class-invar {p = p}{q} Οƒ 𝑨 Ο† ka a = ΞΎ
  where
   ΞΎ : ∣ Ο† ∣ ((𝑻 X ⟦ p ⟧) a) ≑ ∣ Ο† ∣ ((𝑻 X ⟦ q ⟧) a)
   ΞΎ =  ∣ Ο† ∣ ((𝑻 X ⟦ p ⟧) a)  β‰‘βŸ¨ comm-hom-term (wd π“₯ Ξ±) 𝑨 Ο† p a ⟩
        (𝑨 ⟦ p ⟧)(∣ Ο† ∣ ∘ a)   β‰‘βŸ¨ (Οƒ ka) (∣ Ο† ∣ ∘ a) ⟩
        (𝑨 ⟦ q ⟧)(∣ Ο† ∣ ∘ a)   β‰‘βŸ¨ (comm-hom-term (wd π“₯ Ξ±) 𝑨 Ο† q a)⁻¹ ⟩
        ∣ Ο† ∣ ((𝑻 X ⟦ q ⟧) a)  ∎

 -- ⇐ (the "if" direction)
 ⊧-H-class-coinvar :  {p q : Term X}
  β†’                   (βˆ€ 𝑨 Ο† β†’ 𝑨 ∈ 𝒦 β†’ βˆ€ a β†’ ∣ Ο† ∣ ((𝑻 X ⟦ p ⟧) a) ≑ ∣ Ο† ∣ ((𝑻 X ⟦ q ⟧) a))
  β†’                   𝒦 ⊫ p β‰ˆ q

 ⊧-H-class-coinvar {p}{q} Ξ² {𝑨} ka = goal
  where
  Ο† : (a : X β†’ ∣ 𝑨 ∣) β†’ hom (𝑻 X) 𝑨
  Ο† a = lift-hom 𝑨 a

  goal : 𝑨 ⊧ p β‰ˆ q
  goal a =  (𝑨 ⟦ p ⟧)(∣ Ο† a ∣ ∘ β„Š)     β‰‘βŸ¨(comm-hom-term (wd π“₯ Ξ±) 𝑨 (Ο† a) p β„Š)⁻¹ ⟩
            (∣ Ο† a ∣ ∘ (𝑻 X ⟦ p ⟧)) β„Š  β‰‘βŸ¨ Ξ² 𝑨 (Ο† a) ka β„Š ⟩
            (∣ Ο† a ∣ ∘ (𝑻 X ⟦ q ⟧)) β„Š  β‰‘βŸ¨ (comm-hom-term (wd π“₯ Ξ±) 𝑨 (Ο† a) q β„Š) ⟩
            (𝑨 ⟦ q ⟧)(∣ Ο† a ∣ ∘ β„Š)     ∎

← Base.Varieties.Closure Base.Varieties.Preservation β†’