↑ Top


Properties of the models relation

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

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

open import Algebras.Basic using ( π“ž ; π“₯ ; Signature )

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

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

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

Algebraic invariance of ⊧

The binary relation ⊧ would be practically useless if it were not an algebraic invariant (i.e., 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                      β‰‘βŸ¨ wd Ο‡ Ξ² (𝑩 ⟦ p ⟧) x (∣ f ∣ ∘ ∣ g ∣ ∘ x) (Ξ» i β†’ ( f∼g (x i))⁻¹) ⟩
  (𝑩 ⟦ p ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘ x)  β‰‘βŸ¨ (comm-hom-term (wd π“₯ Ξ²) 𝑩 f p (∣ g ∣ ∘ x))⁻¹ ⟩
  ∣ f ∣ ((𝑨 ⟦ p ⟧) (∣ g ∣ ∘ x))    β‰‘βŸ¨ cong ∣ f ∣ (Apq (∣ g ∣ ∘ x))  ⟩
  ∣ f ∣ ((𝑨 ⟦ q ⟧) (∣ g ∣ ∘ x))    β‰‘βŸ¨ comm-hom-term (wd π“₯ Ξ²) 𝑩 f q (∣ g ∣ ∘ x) ⟩
  (𝑩 ⟦ q ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘  x) β‰‘βŸ¨ wd Ο‡ Ξ² (𝑩 ⟦ q ⟧) (∣ f ∣ ∘ ∣ g ∣ ∘ x) x (Ξ» i β†’ ( f∼g (x i))) ⟩
  (𝑩 ⟦ q ⟧) x                      ∎

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 _ (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) --  (β‰…-sym Lift-β‰…)

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               β‰‘βŸ¨ cong ∣ Ο† ∣(term-agreement(wd π“₯ (ov Ο‡)) p)⟩
                       ∣ Ο† ∣((𝑻 X ⟦ p ⟧) β„Š)  β‰‘βŸ¨ comm-hom-term (wd π“₯ Ξ±) 𝑨 Ο† p β„Š ⟩
                       (𝑨 ⟦ p ⟧) (∣ Ο† ∣ ∘ β„Š) β‰‘βŸ¨ Ξ² (∣ Ο† ∣ ∘ β„Š ) ⟩
                       (𝑨 ⟦ q ⟧) (∣ Ο† ∣ ∘ β„Š) β‰‘βŸ¨ (comm-hom-term (wd π“₯ Ξ±)  𝑨 Ο† q β„Š )⁻¹ ⟩
                       ∣ Ο† ∣ ((𝑻 X ⟦ q ⟧) β„Š) β‰‘βŸ¨(cong ∣ Ο† ∣ (term-agreement (wd π“₯ (ov Ο‡)) q))⁻¹ ⟩
                       ∣ Ο† ∣ q               ∎

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 ∣ ∘ β„Š)     ∎


← Varieties.Closure Varieties.Preservation β†’