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 Overture using (π ; π₯ ; Signature) module Setoid.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 ( _,_ ) 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 ( β£_β£ ; β₯_β₯ ) open import Setoid.Functions using ( InvIsInverseΚ³ ; SurjInv ) open import Base.Terms {π = π} using ( Term ; β ) open import Setoid.Algebras {π = π} using ( Algebra ; Lift-AlgΛ‘ ; ov ; π[_] ; π»[_] ; β¨ ) open import Setoid.Homomorphisms {π = π} using ( hom ; _β _ ; mkiso ; Lift-β Λ‘ ; β -sym ; _IsHomImageOf_ ) open import Setoid.Terms {π = π} using ( π» ; module Environment ; comm-hom-term ; interp-prod ; term-agreement ) open import Setoid.Subalgebras {π = π} using ( _β€_ ; SubalgebrasOfClass ) open import Setoid.Varieties.SoundAndComplete {π = π} using ( _β§_ ; _β¨_ ; _β«_ ; Eq ; _βΜ_ ; lhs ; rhs ; _β’_βΉ_β_ ) private variable Ξ± Οα΅ Ξ² Οα΅ Ο β : Level open Func using ( cong ) renaming ( to to _β¨$β©_ ) open Algebra using ( Domain )
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 () 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 private f = _β¨$β©_ β£ fh β£ ; g = _β¨$β©_ β£ 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 β£ 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
.
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-β Λ‘)
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 β£ Οh β£ (Apq (Οβ»ΒΉ β Ο)) β© Ο( β¦ q β§α΄¬ β¨$β© ( Οβ»ΒΉ β Ο)) ββ¨ comm-hom-term Οh q (Οβ»ΒΉ β Ο) β© β¦ q β§ β¨$β© (Ο β Οβ»ΒΉ β Ο) ββ¨ cong β¦ q β§(Ξ» _ β InvIsInverseΚ³ ΟE) β© β¦ q β§ β¨$β© Ο β where Οβ»ΒΉ : π[ π© ] β π[ π¨ ] Οβ»ΒΉ = SurjInv β£ Οh β£ ΟE private Ο = (_β¨$β©_ β£ Οh β£) open Environment π¨ using () renaming ( β¦_β§ to β¦_β§α΄¬) open Environment π© using ( β¦_β§ ) open SetoidReasoning π»[ π© ]
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 = β£ Bβ€A β£ h = _β¨$β©_ β£ 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 = β₯ 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 π¨ kA) Bβ€A
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 Ο β Ο (π 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)
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 _ {X : Type Ο}{p q : Term X}{π¨ : Algebra Ξ± Οα΅}(Οh : hom (π» X) π¨) where open Setoid (Domain π¨) using ( _β_ ) private Ο = _β¨$β©_ β£ Οh β£ β§-H-ker : π¨ β§ (p βΜ q) β Ο p β Ο q β§-H-ker Ξ² = begin Ο p ββ¨ cong β£ Οh β£ (term-agreement p)β© Ο (β¦ p β§ β¨$β© β) ββ¨ comm-hom-term Οh p β β© β¦ p β§β β¨$β© (Ο β β) ββ¨ Ξ² (Ο β β) β© β¦ q β§β β¨$β© (Ο β β) βΛβ¨ comm-hom-term Οh q β β© Ο (β¦ q β§ β¨$β© β) βΛβ¨ cong β£ Οh β£ (term-agreement q)β© Ο q β where open SetoidReasoning (Domain π¨) open Environment π¨ using () renaming ( β¦_β§ to β¦_β§β ) open Environment (π» X) using ( β¦_β§ )
β Setoid.Varieties.Closure Setoid.Varieties.Preservation β