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

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