This is the Setoid.Varieties.Preservation module of the Agda Universal Algebra Library where we show that the classes \af H \ab{π¦}, \af S \ab{π¦}, \af P \ab{π¦}, and \af V \ab{π¦} all satisfy the same identities.
{-# OPTIONS --without-K --exact-split --safe #-} open import Base.Algebras.Basic using ( π ; π₯ ; Signature ) module Setoid.Varieties.Preservation {π : Signature π π₯} where -- Imports from Agda and the Agda Standard Library ----------------------------------------------- open import Agda.Primitive using ( Level ; _β_ ; lsuc ) renaming ( Set to Type ) open import Data.Product using ( _,_ ) renaming ( projβ to fst ; projβ to snd ) open import Data.Unit.Polymorphic using ( β€ ) open import Function using ( _β_ ) open import Function.Bundles using () renaming ( Func to _βΆ_ ) 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 Base.Overture.Preliminaries using ( β£_β£ ; β₯_β₯ ) open import Base.Terms.Basic {π = π} using ( Term ) open import Setoid.Overture.Surjective using ( IsSurjective ; SurjInv ) using ( SurjInvIsInverseΚ³ ) open import Setoid.Algebras.Basic {π = π} using ( Algebra ; ov ; π[_] ; Lift-Alg ) open import Setoid.Algebras.Products {π = π} using ( β¨ ) open import Setoid.Homomorphisms.Basic {π = π} using ( hom ) open import Setoid.Homomorphisms.Isomorphisms {π = π} using ( β β¨ βΊ-refl ; β -refl ; β -sym ) using ( _β _ ; β -trans ; Lift-β ) open import Setoid.Homomorphisms.HomomorphicImages {π = π} using ( IdHomImage ) open import Setoid.Terms.Basic {π = π} using ( module Environment) open import Setoid.Terms.Operations {π = π} using ( comm-hom-term ) open import Setoid.Subalgebras.Subalgebras {π = π} using ( _β€_ ; _β€c_ ) open import Setoid.Subalgebras.Properties {π = π} using ( β¨ -β€ ; β -trans-β€ ; β€-reflexive ) open import Setoid.Varieties.Closure {π = π} using ( H ; S ; P ; V ; S-expa ; H-expa ) using ( P-expa ; V-expa ; Level-closure ) open import Setoid.Varieties.Properties {π = π} using ( β§-H-invar ; β§-S-invar ) using ( β§-P-invar ; β§-I-invar ) open import Setoid.Varieties.SoundAndComplete {π = π} using ( _β§_ ; _β¨_ ; _β«_ ; Eq ; _βΜ_ ) using ( lhs ; rhs ; _β’_βΉ_β_ ; Th) open _βΆ_ using ( cong ) renaming ( f to _β¨$β©_ ) open Algebra using ( Domain )
The types defined above represent operators with useful closure properties. We now prove a handful of such properties that we need later.
The next lemma would be too obvious to care about were it not for the fact that weβll need it later, so it too must be formalized.
module _ {Ξ± Οα΅ β : Level}{π¦ : Pred(Algebra Ξ± Οα΅) (Ξ± β Οα΅ β ov β)} where private a = Ξ± β Οα΅ oaβ = ov (a β β) SβSP : β{ΞΉ} β S β π¦ β S {Ξ² = Ξ±}{Οα΅} (a β β β ΞΉ) (P {Ξ² = Ξ±}{Οα΅} β ΞΉ π¦) SβSP {ΞΉ} (π¨ , (kA , Bβ€A )) = π¨ , (pA , Bβ€A) where pA : π¨ β P β ΞΉ π¦ pA = β€ , (Ξ» _ β π¨) , (Ξ» _ β kA) , β β¨ βΊ-refl
We conclude this subsection with three more inclusion relations that will have bit parts to play later (e.g., in the formal proof of Birkhoffβs Theorem).
PβSP : β{ΞΉ} β P β ΞΉ π¦ β S (a β β β ΞΉ) (P {Ξ² = Ξ±}{Οα΅}β ΞΉ π¦) PβSP {ΞΉ} x = S-expa{β = a β β β ΞΉ} x PβHSP : β{ΞΉ} β P {Ξ² = Ξ±}{Οα΅} β ΞΉ π¦ β H (a β β β ΞΉ) (S {Ξ² = Ξ±}{Οα΅}(a β β β ΞΉ) (P {Ξ² = Ξ±}{Οα΅}β ΞΉ π¦)) PβHSP {ΞΉ} x = H-expa{β = a β β β ΞΉ} (S-expa{β = a β β β ΞΉ} x) PβV : β{ΞΉ} β P β ΞΉ π¦ β V β ΞΉ π¦ PβV = PβHSP SPβV : β{ΞΉ} β S{Ξ² = Ξ±}{Οα΅ = Οα΅} (a β β β ΞΉ) (P {Ξ² = Ξ±}{Οα΅} β ΞΉ π¦) β V β ΞΉ π¦ SPβV {ΞΉ} x = H-expa{β = a β β β ΞΉ} x
Finally, we are in a position to prove that a product of subalgebras of algebras in a class π¦ is a subalgebra of a product of algebras in π¦.
PSβSP : P (a β β) oaβ (S{Ξ² = Ξ±}{Οα΅} β π¦) β S oaβ (P β oaβ π¦) PSβSP {π©} (I , ( π , sA , Bβ β¨ A )) = Goal where β¬ : I β Algebra Ξ± Οα΅ β¬ i = β£ sA i β£ kB : (i : I) β β¬ i β π¦ kB i = fst β₯ sA i β₯ β¨ Aβ€β¨ B : β¨ π β€ β¨ β¬ β¨ Aβ€β¨ B = β¨ -β€ Ξ» i β snd β₯ sA i β₯ Goal : π© β S{Ξ² = oaβ}{oaβ}oaβ (P {Ξ² = oaβ}{oaβ} β oaβ π¦) Goal = β¨ β¬ , (I , (β¬ , (kB , β -refl))) , (β -trans-β€ Bβ β¨ A β¨ Aβ€β¨ B)
First we prove that the closure operator H is compatible with identities that hold in the given class.
module _ {Ξ± Οα΅ β Ο : Level} {π¦ : Pred(Algebra Ξ± Οα΅) (Ξ± β Οα΅ β ov β)} {X : Type Ο} {p q : Term X} where H-id1 : π¦ β« (p βΜ q) β H {Ξ² = Ξ±}{Οα΅}β π¦ β« (p βΜ q) H-id1 Ο π© (π¨ , kA , BimgA) = β§-H-invar{p = p}{q} (Ο π¨ kA) BimgA
The converse of the foregoing result is almost too obvious to bother with. Nonetheless, we formalize it for completeness.
H-id2 : H β π¦ β« (p βΜ q) β π¦ β« (p βΜ q) H-id2 Hpq π¨ kA = Hpq π¨ (π¨ , (kA , IdHomImage))
S-id1 : π¦ β« (p βΜ q) β (S {Ξ² = Ξ±}{Οα΅} β π¦) β« (p βΜ q) S-id1 Ο π© (π¨ , kA , Bβ€A) = β§-S-invar{p = p}{q} (Ο π¨ kA) Bβ€A S-id2 : S β π¦ β« (p βΜ q) β π¦ β« (p βΜ q) S-id2 Spq π¨ kA = Spq π¨ (π¨ , (kA , β€-reflexive))
P-id1 : β{ΞΉ} β π¦ β« (p βΜ q) β P {Ξ² = Ξ±}{Οα΅}β ΞΉ π¦ β« (p βΜ q) P-id1 Ο π¨ (I , π , kA , Aβ β¨ A) = β§-I-invar π¨ p q IH (β -sym Aβ β¨ A) where ih : β i β π i β§ (p βΜ q) ih i = Ο (π i) (kA i) IH : β¨ π β§ (p βΜ q) IH = β§-P-invar {p = p}{q} π ih P-id2 : β{ΞΉ} β P β ΞΉ π¦ β« (p βΜ q) β π¦ β« (p βΜ q) P-id2{ΞΉ} PKpq π¨ kA = PKpq π¨ (P-expa {β = β}{ΞΉ} kA)
Finally, we prove the analogous preservation lemmas for the closure operator V
.
module _ {Ξ± Οα΅ β ΞΉ Ο : Level} {π¦ : Pred(Algebra Ξ± Οα΅) (Ξ± β Οα΅ β ov β)} {X : Type Ο} {p q : Term X} where private aβΞΉ = Ξ± β Οα΅ β β β ΞΉ V-id1 : π¦ β« (p βΜ q) β V β ΞΉ π¦ β« (p βΜ q) V-id1 Ο π© (π¨ , (β¨ A , pβ¨ A , Aβ€β¨ A) , BimgA) = H-id1{β = aβΞΉ}{π¦ = S aβΞΉ (P {Ξ² = Ξ±}{Οα΅}β ΞΉ π¦)}{p = p}{q} spKβ§pq π© (π¨ , (spA , BimgA)) where spA : π¨ β S aβΞΉ (P {Ξ² = Ξ±}{Οα΅}β ΞΉ π¦) spA = β¨ A , (pβ¨ A , Aβ€β¨ A) spKβ§pq : S aβΞΉ (P β ΞΉ π¦) β« (p βΜ q) spKβ§pq = S-id1{β = aβΞΉ}{p = p}{q} (P-id1{β = β} {π¦ = π¦}{p = p}{q} Ο) V-id2 : V β ΞΉ π¦ β« (p βΜ q) β π¦ β« (p βΜ q) V-id2 Vpq π¨ kA = Vpq π¨ (V-expa β ΞΉ kA) Lift-id1 : β{Ξ² Οα΅} β π¦ β« (p βΜ q) β Level-closure{Ξ±}{Οα΅}{Ξ²}{Οα΅} β π¦ β« (p βΜ q) Lift-id1 pKq π¨ (π© , kB , Bβ A) Ο = Goal where open Environment π¨ open Setoid (Domain π¨) using (_β_) Goal : β¦ p β§ β¨$β© Ο β β¦ q β§ β¨$β© Ο Goal = β§-I-invar π¨ p q (pKq π© kB) Bβ A Ο
From V-id1
it follows that if π¦ is a class of structures, then the set of identities modeled by all structures in π¦
is equivalent to the set of identities modeled by all structures in V π¦
. In other terms, Th (V π¦)
is precisely the set of identities modeled by π¦
. We formalize this observation as follows.
classIds-β-VIds : π¦ β« (p βΜ q) β (p , q) β Th (V β ΞΉ π¦) classIds-β-VIds pKq π¨ = V-id1 pKq π¨ VIds-β-classIds : (p , q) β Th (V β ΞΉ π¦) β π¦ β« (p βΜ q) VIds-β-classIds Thpq π¨ kA = V-id2 Thpq π¨ kA
β Setoid.Varieties.Properties Setoid.Varieties.FreeAlgebras β