Agda UALib ↑

Equation preservation

This section presents the Varieties.Preservation module of the Agda Universal Algebra Library. In this module we show that identities are preserved by closure operators H, S, and P. This will establish the easy direction of Birkhoff’s HSP Theorem.


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

open import Algebras.Signatures using (Signature; π“ž; π“₯)
open import Universes  using (Universe; _Μ‡)

module Varieties.Preservation {𝑆 : Signature π“ž π“₯} {𝓀 𝓧 : Universe}{X : 𝓧 Μ‡} where

open import Varieties.Varieties {𝑆 = 𝑆}{𝓧}{X} public

𝓕 𝓕⁺ 𝓾𝔁 : Universe
𝓕 = ov 𝓀
𝓕⁺ = (ov 𝓀) ⁺    -- (this will be the level of the relatively free algebra)
𝓾𝔁 = 𝓀 βŠ” 𝓧

H preserves identities

First we prove that the closure operator H is compatible with identities that hold in the given class.


module _ {fe : DFunExt} {𝒦 : Pred (Algebra 𝓀 𝑆)(ov 𝓀)} where

 H-id1 : (p q : Term X) β†’ 𝒦 ⊧ p ≋ q β†’ H{𝓀}{𝓀} 𝒦 ⊧ p ≋ q
 H-id1 p q α (hbase x) = ⊧-Lift-invar fe p q (α x)
 H-id1 p q Ξ± (hlift{𝑨} x) = ⊧-Lift-invar fe p q (H-id1 p q Ξ± x)

 H-id1 p q Ξ± (hhimg{𝑨}{π‘ͺ} HA((𝑩 , Ο• , (Ο•hom , Ο•sur)), Bβ‰…C)) = ⊧-I-invar fe π‘ͺ p q Ξ³ Bβ‰…C
  where
  Ξ² : 𝑨 ⊧ p β‰ˆ q
  Ξ² = (H-id1 p q Ξ±) HA

  preim : βˆ€ 𝒃 x β†’ ∣ 𝑨 ∣
  preim 𝒃 x = Inv Ο• (Ο•sur (𝒃 x))

  ΞΆ : βˆ€ 𝒃 β†’ Ο• ∘ (preim 𝒃) ≑ 𝒃
  ΞΆ 𝒃 = (fe 𝓧 𝓀) Ξ» x β†’ InvIsInv Ο• (Ο•sur (𝒃 x))

  Ξ³ : 𝑩 ⟦ p ⟧  ≑ 𝑩 ⟦ q ⟧
  Ξ³ = (fe 𝓾𝔁 𝓀) Ξ» 𝒃 β†’ (𝑩 ⟦ p ⟧) 𝒃             β‰‘βŸ¨ (ap (𝑩 ⟦ p ⟧) (ΞΆ 𝒃))⁻¹ ⟩
                (𝑩 ⟦ p ⟧)(Ο• ∘(preim 𝒃)) β‰‘βŸ¨(comm-hom-term (fe π“₯ 𝓀) 𝑩(Ο• , Ο•hom) p(preim 𝒃))⁻¹ ⟩
                Ο•((𝑨 ⟦ p ⟧)(preim 𝒃))   β‰‘βŸ¨ ap Ο• (happly Ξ² (preim 𝒃)) ⟩
                Ο•((𝑨 ⟦ q ⟧)(preim 𝒃))   β‰‘βŸ¨ comm-hom-term (fe π“₯ 𝓀) 𝑩 (Ο• , Ο•hom) q (preim 𝒃) ⟩
                (𝑩 ⟦ q ⟧)(Ο• ∘(preim 𝒃)) β‰‘βŸ¨ ap (𝑩 ⟦ q ⟧) (ΞΆ 𝒃) ⟩
                (𝑩 ⟦ q ⟧) 𝒃             ∎

 H-id1 p q Ξ± (hiso{𝑨}{𝑩} x x₁) = ⊧-I-invar fe 𝑩 p q (H-id1 p q Ξ± x) x₁

The converse of the foregoing result is almost too obvious to bother with. Nonetheless, we formalize it for completeness.


 H-id2 : βˆ€ {𝓦} β†’ (p q : Term X) β†’ H{𝓀}{𝓦} 𝒦 ⊧ p ≋ q β†’ 𝒦 ⊧ p ≋ q

 H-id2 p q Hpq KA = ⊧-lower-invar fe p q (Hpq (hbase KA))

S preserves identities


 S-id1 : (p q : Term X) β†’ 𝒦 ⊧ p ≋ q β†’ S{𝓀}{𝓀} 𝒦 ⊧ p ≋ q

 S-id1 p q α (sbase x) = ⊧-Lift-invar fe p q (α x)
 S-id1 p q α (slift x) = ⊧-Lift-invar fe p q ((S-id1 p q α) x)

 S-id1 p q Ξ± (ssub{𝑨}{𝑩} sA B≀A) =
  ⊧-S-class-invar fe p q Ξ³ (𝑩 , 𝑨 , (𝑩 , B≀A) , injβ‚‚ refl , β‰…-refl)
   where --Apply S-⊧ to the class 𝒦 βˆͺ ο½› 𝑨 ｝
   Ξ² : 𝑨 ⊧ p β‰ˆ q
   Ξ² = S-id1 p q Ξ± sA

   Apq : ο½› 𝑨 ｝ ⊧ p ≋ q
   Apq refl = Ξ²

   Ξ³ : (𝒦 βˆͺ ο½› 𝑨 ｝) ⊧ p ≋ q
   Ξ³ {𝑩} (inj₁ x) = Ξ± x
   Ξ³ {𝑩} (injβ‚‚ y) = Apq y

 S-id1 p q Ξ± (ssubw{𝑨}{𝑩} sA B≀A) =
  ⊧-S-class-invar fe p q Ξ³ (𝑩 , 𝑨 , (𝑩 , B≀A) , injβ‚‚ refl , β‰…-refl)
   where  --Apply S-⊧ to the class 𝒦 βˆͺ ο½› 𝑨 ｝
   Ξ² : 𝑨 ⊧ p β‰ˆ q
   Ξ² = S-id1 p q Ξ± sA

   Apq : ο½› 𝑨 ｝ ⊧ p ≋ q
   Apq refl = Ξ²

   Ξ³ : (𝒦 βˆͺ ο½› 𝑨 ｝) ⊧ p ≋ q
   Ξ³ {𝑩} (inj₁ x) = Ξ± x
   Ξ³ {𝑩} (injβ‚‚ y) = Apq y

 S-id1 p q Ξ± (siso{𝑨}{𝑩} x x₁) = ⊧-I-invar fe 𝑩 p q (S-id1 p q Ξ± x) x₁

Again, the obvious converse is barely worth the bits needed to formalize it.


 S-id2 : βˆ€{𝓦}(p q : Term X) β†’ S{𝓀}{𝓦}𝒦 ⊧ p ≋ q β†’ 𝒦 ⊧ p ≋ q

 S-id2 p q Spq {𝑨} KA = ⊧-lower-invar fe p q (Spq (sbase KA))

P preserves identities


 P-id1 : (p q : Term X) β†’ 𝒦 ⊧ p ≋ q β†’ P{𝓀}{𝓀} 𝒦 ⊧ p ≋ q

 P-id1 p q α (pbase x) = ⊧-Lift-invar fe p q (α x)
 P-id1 p q α (pliftu x) = ⊧-Lift-invar fe p q ((P-id1 p q α) x)
 P-id1 p q α (pliftw x) = ⊧-Lift-invar fe p q ((P-id1 p q α) x)

 P-id1 p q Ξ± (produ{I}{π’œ} x) = ⊧-P-lift-invar I π’œ  fe {p}{q} IH
  where
  IH : βˆ€ i β†’ (Lift-alg (π’œ i) 𝓀) ⟦ p ⟧ ≑ (Lift-alg (π’œ i) 𝓀) ⟦ q ⟧
  IH i = ⊧-Lift-invar fe p q ((P-id1 p q α) (x i))

 P-id1 p q Ξ± (prodw{I}{π’œ} x) = ⊧-P-lift-invar I π’œ fe {p}{q}IH
  where
  IH : βˆ€ i β†’ Lift-alg (π’œ i) 𝓀 ⟦ p ⟧ ≑ Lift-alg (π’œ i) 𝓀 ⟦ q ⟧
  IH i = ⊧-Lift-invar fe p q ((P-id1 p q α) (x i))

 P-id1 p q Ξ± (pisou{𝑨}{𝑩} x x₁) = ⊧-I-invar fe 𝑩 p q (P-id1 p q Ξ± x) x₁
 P-id1 p q Ξ± (pisow{𝑨}{𝑩} x x₁) = ⊧-I-invar fe 𝑩 p q (P-id1 p q Ξ± x) x₁

…and conversely…


 P-id2 : βˆ€ {𝓦}(p q : Term X) β†’ P{𝓀}{𝓦} 𝒦 ⊧ p ≋ q β†’ 𝒦 ⊧ p ≋ q
 P-id2 p q PKpq KA = ⊧-lower-invar fe p q (PKpq (pbase KA))

V preserves identities

Finally, we prove the analogous preservation lemmas for the closure operator V.


 V-id1 : (p q : Term X) β†’ 𝒦 ⊧ p ≋ q β†’ V{𝓀}{𝓀} 𝒦 ⊧ p ≋ q
 V-id1 p q α (vbase x) = ⊧-Lift-invar fe p q (α x)
 V-id1 p q Ξ± (vlift{𝑨} x) = ⊧-Lift-invar  fe p q ((V-id1 p q Ξ±) x)
 V-id1 p q Ξ± (vliftw{𝑨} x) = ⊧-Lift-invar fe p q ((V-id1 p q Ξ±) x)

 V-id1 p q Ξ± (vhimg{𝑨}{π‘ͺ}VA((𝑩 , Ο• , (Ο•h , Ο•E)) , Bβ‰…C)) = ⊧-I-invar fe π‘ͺ p q Ξ³ Bβ‰…C
  where
  IH : 𝑨 ⊧ p β‰ˆ q
  IH = V-id1 p q Ξ± VA

  preim : βˆ€ 𝒃 (x : X) β†’ ∣ 𝑨 ∣
  preim 𝒃 x = (Inv Ο• (Ο•E (𝒃 x)))

  ΞΆ : βˆ€ 𝒃 β†’ Ο• ∘ (preim 𝒃) ≑ 𝒃
  ΞΆ 𝒃 = (fe 𝓧 𝓀) Ξ» x β†’ InvIsInv Ο• (Ο•E (𝒃 x))

  Ξ³ : (𝑩 ⟦ p ⟧) ≑ (𝑩 ⟦ q ⟧)
  Ξ³ = (fe 𝓾𝔁 𝓀) Ξ» 𝒃 β†’ (𝑩 ⟦ p ⟧) 𝒃      β‰‘βŸ¨ (ap (𝑩 ⟦ p ⟧) (ΞΆ 𝒃))⁻¹ ⟩
                (𝑩 ⟦ p ⟧)(Ο• ∘(preim 𝒃)) β‰‘βŸ¨(comm-hom-term (fe π“₯ 𝓀) 𝑩(Ο• , Ο•h) p(preim 𝒃))⁻¹ ⟩
                Ο• ((𝑨 ⟦ p ⟧)(preim 𝒃))  β‰‘βŸ¨ ap Ο• (happly IH (preim 𝒃)) ⟩
                Ο• ((𝑨 ⟦ q ⟧)(preim 𝒃))  β‰‘βŸ¨ comm-hom-term (fe π“₯ 𝓀) 𝑩 (Ο• , Ο•h) q (preim 𝒃) ⟩
                (𝑩 ⟦ q ⟧)(Ο• ∘(preim 𝒃)) β‰‘βŸ¨ ap (𝑩 ⟦ q ⟧) (ΞΆ 𝒃) ⟩
                (𝑩 ⟦ q ⟧) 𝒃             ∎

 V-id1 p q Ξ± (vssub {𝑨}{𝑩} VA B≀A) = ⊧-S-class-invar fe p q Ξ³ (𝑩 , 𝑨 , (𝑩 , B≀A) , injβ‚‚ refl , β‰…-refl)
   where
   IH : 𝑨 ⊧ p β‰ˆ q
   IH = V-id1 p q Ξ± VA

   Asinglepq : ο½› 𝑨 ｝ ⊧ p ≋ q
   Asinglepq refl = IH

   Ξ³ : (𝒦 βˆͺ ο½› 𝑨 ｝) ⊧ p ≋ q
   Ξ³ {𝑩} (inj₁ x) = Ξ± x
   Ξ³ {𝑩} (injβ‚‚ y) = Asinglepq y

 V-id1 p q Ξ± ( vssubw {𝑨}{𝑩} VA B≀A ) =
  ⊧-S-class-invar fe p q Ξ³ (𝑩 , 𝑨 , (𝑩 , B≀A) , injβ‚‚ refl , β‰…-refl)
   where
   IH : 𝑨 ⊧ p β‰ˆ q
   IH = V-id1 p q Ξ± VA

   Asinglepq : ο½› 𝑨 ｝ ⊧ p ≋ q
   Asinglepq refl = IH

   Ξ³ : (𝒦 βˆͺ ο½› 𝑨 ｝) ⊧ p ≋ q
   Ξ³ {𝑩} (inj₁ x) = Ξ± x
   Ξ³ {𝑩} (injβ‚‚ y) = Asinglepq y

 V-id1 p q Ξ± (vprodu{I}{π’œ} Vπ’œ) = ⊧-P-invar I π’œ fe {p}{q} Ξ» i β†’ V-id1 p q Ξ± (Vπ’œ i)
 V-id1 p q Ξ± (vprodw{I}{π’œ} Vπ’œ) = ⊧-P-invar I π’œ fe {p}{q} Ξ» i β†’ V-id1 p q Ξ± (Vπ’œ i)
 V-id1 p q Ξ± (visou{𝑨}{𝑩} VA Aβ‰…B) = ⊧-I-invar fe 𝑩 p q (V-id1 p q Ξ± VA) Aβ‰…B
 V-id1 p q Ξ± (visow{𝑨}{𝑩} VA Aβ‰…B) = ⊧-I-invar fe 𝑩 p q (V-id1 p q Ξ± VA) Aβ‰…B



-- module _ {𝓀 : Universe}{X : 𝓀 Μ‡}{fe : DFunExt} {𝒦 : Pred (Algebra 𝓀 𝑆)(ov 𝓀)} where

-- open id1 {𝓀}{X}{(fe 𝓀 𝓀) = fe 𝓀 𝓀}{(fe π“₯ 𝓀) = fe π“₯ 𝓀}

 V-id1' : (p q : Term X) β†’ 𝒦 ⊧ p ≋ q β†’ V{𝓀}{ov 𝓀 ⁺} 𝒦 ⊧ p ≋ q

 V-id1' p q α (vbase x) = ⊧-Lift-invar fe p q (α x)
 V-id1' p q Ξ± (vlift{𝑨} x) = ⊧-Lift-invar fe p q ((V-id1 p q Ξ±) x)
 V-id1' p q Ξ± (vliftw{𝑨} x) = ⊧-Lift-invar fe p q ((V-id1' p q Ξ±) x)

 V-id1' p q Ξ± (vhimg{𝑨}{π‘ͺ} VA ((𝑩 , Ο• , (Ο•h , Ο•E)) , Bβ‰…C)) =
  ⊧-I-invar fe π‘ͺ p q Ξ³ Bβ‰…C
   where
   IH : 𝑨 ⊧ p β‰ˆ q
   IH = V-id1' p q Ξ± VA

   preim : βˆ€ 𝒃 x β†’ ∣ 𝑨 ∣
   preim 𝒃 x = (Inv Ο• (Ο•E (𝒃 x)))

   ΞΆ : βˆ€ 𝒃 β†’ Ο• ∘ (preim 𝒃) ≑ 𝒃
   ΞΆ 𝒃 = (fe 𝓧 𝓕⁺) Ξ» x β†’ InvIsInv Ο• (Ο•E (𝒃 x))

   Ξ³ : 𝑩 ⟦ p ⟧ ≑ 𝑩 ⟦ q ⟧
   Ξ³ = (fe (𝓧 βŠ” 𝓕⁺) 𝓕⁺) Ξ» 𝒃 β†’ (𝑩 ⟦ p ⟧) 𝒃  β‰‘βŸ¨ (ap (𝑩 ⟦ p ⟧) (ΞΆ 𝒃))⁻¹  ⟩
                 (𝑩 ⟦ p ⟧) (Ο• ∘ (preim 𝒃)) β‰‘βŸ¨(comm-hom-term (fe π“₯ 𝓕⁺) 𝑩 (Ο• , Ο•h) p (preim 𝒃))⁻¹ ⟩
                 Ο•((𝑨 ⟦ p ⟧)(preim 𝒃))     β‰‘βŸ¨ ap Ο• (happly IH (preim 𝒃))⟩
                 Ο•((𝑨 ⟦ q ⟧)(preim 𝒃))     β‰‘βŸ¨ comm-hom-term (fe π“₯ 𝓕⁺) 𝑩 (Ο• , Ο•h) q (preim 𝒃)⟩
                 (𝑩 ⟦ q ⟧)(Ο• ∘ (preim 𝒃))  β‰‘βŸ¨ ap (𝑩 ⟦ q ⟧) (ΞΆ 𝒃)⟩
                 (𝑩 ⟦ q ⟧) 𝒃               ∎

 V-id1' p q Ξ± (vssub{𝑨}{𝑩} VA B≀A) = ⊧-S-invar fe 𝑩 {p}{q}(V-id1 p q Ξ± VA) B≀A
 V-id1' p q Ξ± (vssubw {𝑨}{𝑩} VA B≀A) = ⊧-S-invar fe 𝑩 {p}{q}(V-id1' p q Ξ± VA) B≀A
 V-id1' p q Ξ± (vprodu{I}{π’œ} Vπ’œ) = ⊧-P-invar I π’œ fe {p}{q} Ξ» i β†’ V-id1 p q Ξ± (Vπ’œ i)
 V-id1' p q Ξ± (vprodw{I}{π’œ} Vπ’œ) = ⊧-P-invar I π’œ fe {p}{q} Ξ» i β†’ V-id1' p q Ξ± (Vπ’œ i) -- {fwu = (fe 𝓕⁺ 𝓕⁺)}{(fe π“₯ 𝓕⁺)}{(fe 𝓕⁺ 𝓕⁺)}
 V-id1' p q Ξ± (visou {𝑨}{𝑩} VA Aβ‰…B) = ⊧-I-invar fe 𝑩 p q (V-id1 p q Ξ± VA) Aβ‰…B
 V-id1' p q Ξ± (visow{𝑨}{𝑩} VA Aβ‰…B) = ⊧-I-invar fe 𝑩 p q (V-id1' p q Ξ± VA)Aβ‰…B

Class identities

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.


 𝒱 : Pred (Algebra (ov 𝓀 ⁺) 𝑆) (ov 𝓀 ⁺ ⁺)
 𝒱 = V{𝓀}{ov 𝓀 ⁺} 𝒦

 class-ids-β‡’ : (p q : ∣ 𝑻 X ∣) β†’ 𝒦 ⊧ p ≋ q  β†’  (p , q) ∈ Th 𝒱
 class-ids-β‡’ p q pKq VCloA = V-id1' p q pKq VCloA


 class-ids-⇐ : (p q : ∣ 𝑻 X ∣) β†’ (p , q) ∈ Th 𝒱 β†’  𝒦 ⊧ p ≋ q
 class-ids-⇐ p q Thpq {𝑨} KA = ⊧-lower-invar fe p q (Thpq (vbase KA))


 class-identities : (p q : ∣ 𝑻 X ∣) β†’ 𝒦 ⊧ p ≋ q  ⇔  ((p , q) ∈ Th 𝒱)
 class-identities p q = class-ids-β‡’ p q , class-ids-⇐ p q

Once again, and for the last time, completeness dictates that we formalize the coverse of V-id1, however obvious it may be.


module _ {𝓦 : Universe}{𝒦 : Pred (Algebra 𝓀 𝑆)(ov 𝓀)} where

 V-id2 : DFunExt β†’ (p q : Term X) β†’ (V{𝓀}{𝓦} 𝒦 ⊧ p ≋ q) β†’ (𝒦 ⊧ p ≋ q)
 V-id2 fe p q Vpq {𝑨} KA = ⊧-lower-invar fe p q (Vpq (vbase KA))

← Varieties.Varieties FreeAlgebras β†’