↑ Top


Closure Operators

Fix a signature 𝑆, let 𝒦 be a class of 𝑆-algebras, and define

A straight-forward verification confirms that H, S, and P are closure operators (expansive, monotone, and idempotent). A class 𝒦 of 𝑆-algebras is said to be closed under the taking of homomorphic images provided H 𝒦 βŠ† 𝒦. Similarly, 𝒦 is closed under the taking of subalgebras (resp., arbitrary products) provided S 𝒦 βŠ† 𝒦 (resp., P 𝒦 βŠ† 𝒦). The operators H, S, and P can be composed with one another repeatedly, forming yet more closure operators.

An algebra is a homomorphic image (resp., subalgebra; resp., product) of every algebra to which it is isomorphic. Thus, the class H 𝒦 (resp., S 𝒦; resp., P 𝒦) is closed under isomorphism.

A variety is a class of algebras, in the same signature, that is closed under the taking of homomorphic images, subalgebras, and arbitrary products. To represent varieties we define inductive types for the closure operators H, S, and P that are composable. Separately, we define an inductive type V which simultaneously represents closure under all three operators, H, S, and P.

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

open import Overture using ( π“ž ; π“₯ ; Signature )

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

-- Imports from Agda and the Agda Standard Library ---------------------------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Level           using ( Level ;  Lift ; _βŠ”_ ; suc )
open import Relation.Unary  using ( Pred ; _∈_ ; _βŠ†_ )
open import Data.Product    using ( _,_ ; Ξ£-syntax )
                            renaming ( proj₁ to fst ; projβ‚‚ to snd )

open  import Axiom.Extensionality.Propositional
      using () renaming ( Extensionality to funext )

-- Imports from the Agda Universal Algebra Library ---------------------------------------
open import Overture               using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Base.Algebras {𝑆 = 𝑆}  using ( Algebra ; Lift-Alg ; ov ; β¨… )

open  import Base.Homomorphisms {𝑆 = 𝑆}
      using ( _β‰…_ ; β‰…-sym ; Lift-β‰… ; β‰…-trans ; β‰…-refl ; Lift-Alg-iso ; Lift-Alg-β¨…β‰… )
      using ( Lift-Alg-assoc ; HomImages ; _IsHomImageOf_ ; Lift-Alg-hom-image )

open  import Base.Subalgebras {𝑆 = 𝑆}
      using ( _≀_ ; _IsSubalgebraOfClass_ ; Subalgebra ; ≀-refl ; β‰…-RESP-≀ )
      using ( ≀-RESP-β‰… ; ≀-trans ; Lift-≀-Lift )

The Inductive Type H

We define the inductive type H to represent classes of algebras that include all homomorphic images of algebras in the class; i.e., classes that are closed under the taking of homomorphic images.

data H{Ξ± Ξ² : Level}(𝒦 : Pred(Algebra Ξ± 𝑆)(ov Ξ±)) : Pred(Algebra (Ξ± βŠ” Ξ²) 𝑆)(ov(Ξ± βŠ” Ξ²))
 where
 hbase : {𝑨 : Algebra Ξ± 𝑆} β†’ 𝑨 ∈ 𝒦 β†’ Lift-Alg 𝑨 Ξ² ∈ H 𝒦
 hhimg : {𝑨 𝑩 : Algebra (Ξ± βŠ” Ξ²) 𝑆} β†’ 𝑨 ∈ H {Ξ±} {Ξ²} 𝒦 β†’ ((𝑩 , _) : HomImages 𝑨) β†’ 𝑩 ∈ H 𝒦

The Inductive Type S

Here we define the inductive type S to represent classes of algebras closed under the taking of subalgebras.

data S {Ξ± Ξ² : Level}(𝒦 : Pred(Algebra Ξ± 𝑆)(ov Ξ±)) : Pred(Algebra(Ξ± βŠ” Ξ²)𝑆)(ov(Ξ± βŠ” Ξ²))
 where
 sbase : {𝑨 : Algebra Ξ± 𝑆} β†’ 𝑨 ∈ 𝒦 β†’ Lift-Alg 𝑨 Ξ² ∈ S 𝒦
 slift : {𝑨 : Algebra Ξ± 𝑆} β†’ 𝑨 ∈ S{Ξ±}{Ξ±} 𝒦 β†’ Lift-Alg 𝑨 Ξ² ∈ S 𝒦
 ssub  : {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra _ 𝑆} β†’ 𝑨 ∈ S{Ξ±}{Ξ±} 𝒦 β†’ 𝑩 ≀ 𝑨 β†’ 𝑩 ∈ S 𝒦
 siso  : {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra _ 𝑆} β†’ 𝑨 ∈ S{Ξ±}{Ξ±} 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ S 𝒦

The Inductive Type P

Here we define the inductive type P to represent classes of algebras closed under the taking of arbitrary products.

data P {Ξ± Ξ² : Level}(𝒦 : Pred(Algebra Ξ± 𝑆)(ov Ξ±)) : Pred(Algebra(Ξ± βŠ” Ξ²)𝑆)(ov(Ξ± βŠ” Ξ²))
 where
 pbase  : {𝑨 : Algebra Ξ± 𝑆} β†’ 𝑨 ∈ 𝒦 β†’ Lift-Alg 𝑨 Ξ² ∈ P 𝒦
 pliftu : {𝑨 : Algebra Ξ± 𝑆} β†’ 𝑨 ∈ P{Ξ±}{Ξ±} 𝒦 β†’ Lift-Alg 𝑨 Ξ² ∈ P 𝒦
 pliftw : {𝑨 : Algebra (Ξ± βŠ” Ξ²) 𝑆} β†’ 𝑨 ∈ P{Ξ±}{Ξ²} 𝒦 β†’ Lift-Alg 𝑨 (Ξ± βŠ” Ξ²) ∈ P 𝒦
 produ  : {I : Type Ξ² }{π’œ : I β†’ Algebra Ξ± 𝑆} β†’ (βˆ€ i β†’ (π’œ i) ∈ P{Ξ±}{Ξ±} 𝒦) β†’ β¨… π’œ ∈ P 𝒦
 prodw  : {I : Type Ξ² }{π’œ : I β†’ Algebra _ 𝑆} β†’ (βˆ€ i β†’ (π’œ i) ∈ P{Ξ±}{Ξ²} 𝒦) β†’ β¨… π’œ ∈ P 𝒦
 pisow  : {𝑨 𝑩 : Algebra _ 𝑆} β†’ 𝑨 ∈ P{Ξ±}{Ξ²} 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ P 𝒦

The Inductive Types V

A class 𝒦 of 𝑆-algebras is called a variety if it is closed under each of the closure operators H, S, and P introduced elsewhere; the corresponding closure operator is often denoted 𝕍, but we will denote it by V.

We now define V as an inductive type which is crafted to contain all the parts of H, S and P, under different names.

data V {Ξ± Ξ² : Level}(𝒦 : Pred(Algebra Ξ± 𝑆)(ov Ξ±)) : Pred(Algebra(Ξ± βŠ” Ξ²)𝑆)(ov(Ξ± βŠ” Ξ²))
 where
 vbase   : {𝑨 : Algebra Ξ± 𝑆} β†’ 𝑨 ∈ 𝒦 β†’ Lift-Alg 𝑨 Ξ² ∈ V 𝒦
 vlift   : {𝑨 : Algebra Ξ± 𝑆} β†’ 𝑨 ∈ V{Ξ±}{Ξ±} 𝒦 β†’ Lift-Alg 𝑨 Ξ² ∈ V 𝒦
 vliftw  : {𝑨 : Algebra _ 𝑆} β†’ 𝑨 ∈ V{Ξ±}{Ξ²} 𝒦 β†’ Lift-Alg 𝑨 (Ξ± βŠ” Ξ²) ∈ V 𝒦
 vhimg   : {𝑨 𝑩 : Algebra _ 𝑆} β†’ 𝑨 ∈ V{Ξ±}{Ξ²} 𝒦 β†’ ((𝑩 , _) : HomImages 𝑨) β†’ 𝑩 ∈ V 𝒦
 vssubw  : {𝑨 𝑩 : Algebra _ 𝑆} β†’ 𝑨 ∈ V{Ξ±}{Ξ²} 𝒦 β†’ 𝑩 ≀ 𝑨 β†’ 𝑩 ∈ V 𝒦
 vprodu  : {I : Type Ξ²}{π’œ : I β†’ Algebra Ξ± 𝑆} β†’ (βˆ€ i β†’ (π’œ i) ∈ V{Ξ±}{Ξ±} 𝒦) β†’ β¨… π’œ ∈ V 𝒦
 vprodw  : {I : Type Ξ²}{π’œ : I β†’ Algebra _ 𝑆} β†’ (βˆ€ i β†’ (π’œ i) ∈ V{Ξ±}{Ξ²} 𝒦) β†’ β¨… π’œ ∈ V 𝒦
 visou   : {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra _ 𝑆} β†’ 𝑨 ∈ V{Ξ±}{Ξ±} 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ V 𝒦
 visow   : {𝑨 𝑩 : Algebra _ 𝑆} β†’ 𝑨 ∈ V{Ξ±}{Ξ²} 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ V 𝒦

Thus, if 𝒦 is a class of 𝑆-algebras, then the variety generated by 𝒦 is denoted by V 𝒦 and defined to be the smallest class that contains 𝒦 and is closed under H, S, and P.

With the closure operator V representing closure under HSP, we represent formally what it means to be a variety of algebras as follows.

is-variety : {Ξ± : Level}(𝒱 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)) β†’ Type(ov Ξ±)
is-variety{Ξ±} 𝒱 = V{Ξ±}{Ξ±} 𝒱 βŠ† 𝒱

variety : (Ξ± : Level) β†’ Type(suc (π“ž βŠ” π“₯ βŠ” (suc Ξ±)))
variety Ξ± = Ξ£[ 𝒱 ∈ (Pred (Algebra Ξ± 𝑆)(ov Ξ±)) ] is-variety 𝒱

Closure properties of S

S is a closure operator. The facts that S is idempotent and expansive won’t be needed, so we omit these, but we will make use of monotonicity of S. Here is the proof of the latter.

S-mono :  {Ξ± Ξ² : Level}{𝒦 𝒦' : Pred (Algebra Ξ± 𝑆)(ov Ξ±)}
 β†’        𝒦 βŠ† 𝒦' β†’ S{Ξ±}{Ξ²} 𝒦 βŠ† S{Ξ±}{Ξ²} 𝒦'

S-mono kk (sbase x)            = sbase (kk x)
S-mono kk (slift{𝑨} x)         = slift (S-mono kk x)
S-mono kk (ssub{𝑨}{𝑩} sA B≀A)  = ssub (S-mono kk sA) B≀A
S-mono kk (siso x x₁)          = siso (S-mono kk x) x₁

We sometimes want to go back and forth between our two representations of subalgebras of algebras in a class. The tools subalgebra→S and S→subalgebra are made for that purpose.

module _ {Ξ± Ξ² : Level}{𝒦 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)} where

 subalgebraβ†’S : {𝑩 : Algebra (Ξ± βŠ” Ξ²) 𝑆} β†’ 𝑩 IsSubalgebraOfClass 𝒦 β†’ 𝑩 ∈ S{Ξ±}{Ξ²} 𝒦
 subalgebraβ†’S {𝑩} (𝑨 , ((π‘ͺ , C≀A) , KA , Bβ‰…C)) = ssub sA B≀A
  where
   B≀A : 𝑩 ≀ 𝑨
   B≀A = β‰…-RESP-≀ {π‘ͺ = 𝑨} Bβ‰…C C≀A

   slAu : Lift-Alg 𝑨 Ξ± ∈ S{Ξ±}{Ξ±} 𝒦
   slAu = sbase KA

   sA : 𝑨 ∈ S{Ξ±}{Ξ±} 𝒦
   sA = siso slAu (β‰…-sym Lift-β‰…)


module _ {Ξ± : Level}{𝒦 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)} where

 Sβ†’subalgebra : {𝑩 : Algebra Ξ± 𝑆} β†’ 𝑩 ∈ S{Ξ±}{Ξ±} 𝒦  β†’  𝑩 IsSubalgebraOfClass 𝒦
 Sβ†’subalgebra (sbase{𝑩} x) =  𝑩 , ((𝑩 , (≀-refl β‰…-refl)) , x , β‰…-sym Lift-β‰…)
 Sβ†’subalgebra (slift{𝑩} x) =  ∣ BS ∣ ,
                              SA , ∣ snd βˆ₯ BS βˆ₯ ∣ , β‰…-trans (β‰…-sym Lift-β‰…) Bβ‰…SA
  where
   BS : 𝑩 IsSubalgebraOfClass 𝒦
   BS = S→subalgebra x
   SA : Subalgebra ∣ BS ∣
   SA = fst βˆ₯ BS βˆ₯
   Bβ‰…SA : 𝑩 β‰… ∣ SA ∣
   Bβ‰…SA = βˆ₯ snd βˆ₯ BS βˆ₯ βˆ₯

 Sβ†’subalgebra {𝑩} (ssub{𝑨} sA B≀A) = ∣ AS ∣ , (𝑩 , B≀AS) , ∣ snd βˆ₯ AS βˆ₯ ∣ , β‰…-refl
  where
   AS : 𝑨 IsSubalgebraOfClass 𝒦
   AS = S→subalgebra sA
   SA : Subalgebra ∣ AS ∣
   SA = fst βˆ₯ AS βˆ₯
   B≀SA : 𝑩 ≀ ∣ SA ∣
   B≀SA = ≀-RESP-β‰… B≀A (βˆ₯ snd βˆ₯ AS βˆ₯ βˆ₯)
   B≀AS : 𝑩 ≀ ∣ AS ∣
   B≀AS = ≀-trans 𝑩 ∣ AS ∣ B≀SA βˆ₯ SA βˆ₯

 Sβ†’subalgebra {𝑩} (siso{𝑨} sA Aβ‰…B) =  ∣ AS ∣ ,
                                      SA ,
                                      ∣ snd βˆ₯ AS βˆ₯ ∣ , (β‰…-trans (β‰…-sym Aβ‰…B) Aβ‰…SA)
  where
   AS : 𝑨 IsSubalgebraOfClass 𝒦
   AS = S→subalgebra sA
   SA : Subalgebra ∣ AS ∣
   SA = fst βˆ₯ AS βˆ₯
   Aβ‰…SA : 𝑨 β‰… ∣ SA ∣
   Aβ‰…SA = snd βˆ₯ snd AS βˆ₯

Closure properties of P

P is a closure operator. This is proved by checking that P is monotone, expansive, and idempotent. The meaning of these terms will be clear from the definitions of the types that follow.

P-mono :  {Ξ± Ξ² : Level}{𝒦 𝒦' : Pred(Algebra Ξ± 𝑆)(ov Ξ±)}
 β†’        𝒦 βŠ† 𝒦' β†’ P{Ξ±}{Ξ²} 𝒦 βŠ† P{Ξ±}{Ξ²} 𝒦'

P-mono kk' (pbase x)     = pbase (kk' x)
P-mono kk' (pliftu x)    = pliftu (P-mono kk' x)
P-mono kk' (pliftw x)    = pliftw (P-mono kk' x)
P-mono kk' (produ x)     = produ (Ξ» i β†’ P-mono kk' (x i))
P-mono kk' (prodw x)     = prodw (Ξ» i β†’ P-mono kk' (x i))
P-mono kk' (pisow x x₁)  = pisow (P-mono kk' x) x₁


P-expa : {Ξ± : Level}{𝒦 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)} β†’ 𝒦 βŠ† P{Ξ±}{Ξ±} 𝒦
P-expa{Ξ±}{𝒦} {𝑨} KA = pisow {𝑩 = 𝑨} (pbase KA) (β‰…-sym Lift-β‰…)

module _ {Ξ± Ξ² : Level} where

 P-idemp :  {𝒦 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)}
  β†’         P{Ξ± βŠ” Ξ²}{Ξ± βŠ” Ξ²} (P{Ξ±}{Ξ± βŠ” Ξ²} 𝒦) βŠ† P{Ξ±}{Ξ± βŠ” Ξ²} 𝒦

 P-idemp (pbase x)     = pliftw x
 P-idemp (pliftu x)    = pliftw (P-idemp x)
 P-idemp (pliftw x)    = pliftw (P-idemp x)
 P-idemp (produ x)     = prodw (Ξ» i β†’ P-idemp (x i))
 P-idemp (prodw x)     = prodw (Ξ» i β†’ P-idemp (x i))
 P-idemp (pisow x x₁)  = pisow (P-idemp x) x₁

Next we observe that lifting to a higher universe does not break the property of being a subalgebra of an algebra of a class. In other words, if we lift a subalgebra of an algebra in a class, the result is still a subalgebra of an algebra in the class.

module _ {Ξ± Ξ² : Level}{𝒦 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)} where

 Lift-Alg-subP :  {𝑩 : Algebra Ξ² 𝑆}
  β†’               𝑩 IsSubalgebraOfClass (P{Ξ±}{Ξ²} 𝒦)
  β†’               (Lift-Alg 𝑩 Ξ±) IsSubalgebraOfClass (P{Ξ±}{Ξ²} 𝒦)

 Lift-Alg-subP (𝑨 , (π‘ͺ , C≀A) , pA , Bβ‰…C ) =  lA ,
                                              (lC , lC≀lA) ,
                                              plA , (Lift-Alg-iso B≅C)
   where
   lA lC : Algebra (Ξ± βŠ” Ξ²)  𝑆
   lA = Lift-Alg 𝑨 (Ξ± βŠ” Ξ²)
   lC = Lift-Alg π‘ͺ Ξ±

   lC≀lA : lC ≀ lA
   lC≀lA = Lift-≀-Lift Ξ± {𝑨} (Ξ± βŠ” Ξ²) C≀A
   plA : lA ∈ P{Ξ±}{Ξ²} 𝒦
   plA = pliftw pA

 Lift-Alg-subP' :  {𝑨 : Algebra Ξ± 𝑆}
  β†’                𝑨 IsSubalgebraOfClass (P{Ξ±}{Ξ±} 𝒦)
  β†’                (Lift-Alg 𝑨 Ξ²) IsSubalgebraOfClass (P{Ξ±}{Ξ²} 𝒦)

 Lift-Alg-subP' (𝑩 , (π‘ͺ , C≀B) , pB , Aβ‰…C ) = lB , (lC , lC≀lB) , plB , (Lift-Alg-iso Aβ‰…C)
   where
   lB lC : Algebra (Ξ± βŠ” Ξ²)  𝑆
   lB = Lift-Alg 𝑩 Ξ²
   lC = Lift-Alg π‘ͺ Ξ²

   lC≀lB : lC ≀ lB
   lC≀lB = Lift-≀-Lift Ξ² {𝑩} Ξ² C≀B
   plB : lB ∈ P{Ξ±}{Ξ²} 𝒦
   plB = pliftu pB

V is closed under lift

As mentioned earlier, a technical hurdle that must be overcome when formalizing proofs in Agda is the proper handling of universe levels. In particular, in the proof of the Birkhoff’s theorem, for example, we will need to know that if an algebra 𝑨 belongs to the variety V 𝒦, then so does the lift of 𝑨. Let us get the tedious proof of this technical lemma out of the way.

open Level

module Vlift  {Ξ± : Level} {feβ‚€ : funext (ov Ξ±) Ξ±}
              {fe₁ : funext ((ov Ξ±) βŠ” (suc (ov Ξ±))) (suc (ov Ξ±))}
              {feβ‚‚ : funext (ov Ξ±) (ov Ξ±)}
              {𝒦 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)} where

 VlA :  {𝑨 : Algebra (ov Ξ±) 𝑆} β†’ 𝑨 ∈ V{Ξ±}{ov Ξ±} 𝒦
  β†’     Lift-Alg 𝑨 (suc (ov Ξ±)) ∈ V{Ξ±}{suc (ov Ξ±)} 𝒦
 VlA (vbase{𝑨} x) = visow (vbase x) (Lift-Alg-assoc _ _ {𝑨})
 VlA (vlift{𝑨} x) = visow (vlift x) (Lift-Alg-assoc _ _ {𝑨})
 VlA (vliftw{𝑨} x) = visow (VlA x) (Lift-Alg-assoc _ _ {𝑨})

 VlA (vhimg{𝑨}{𝑩} x hB) = vhimg {𝑩 = Lift-Alg 𝑩 (suc (ov Ξ±))} (VlA x) (lC , lChi)
  where
  lC : Algebra (suc (ov(Ξ±))) 𝑆
  lC = Lift-Alg ∣ hB ∣ (suc (ov(α)))
  lChi : lC IsHomImageOf _
  lChi = (Lift-Alg-hom-image (suc (ov(Ξ±))) {∣ hB ∣} (suc (ov(Ξ±))) βˆ₯ hB βˆ₯)

 VlA (vssubw{𝑨}{𝑩} x B≀A) =
  vssubw (VlA x) (Lift-≀-Lift (suc (ov(Ξ±))) {𝑨} (suc (ov(Ξ±))) B≀A)

 VlA (vprodu{I}{π’œ} x) = visow (vprodw vlA) (β‰…-sym Bβ‰…A)
  where
  𝑰 : Type (suc (ov Ξ±))
  𝑰 = Lift (suc (ov Ξ±)) I

  lA : 𝑰 β†’ Algebra (suc (ov Ξ±)) 𝑆
  lA i = Lift-Alg (π’œ (lower i)) (suc (ov Ξ±))

  vlA : βˆ€ i β†’ (lA i) ∈ V{Ξ±}{suc (ov Ξ±)} 𝒦
  vlA i = vlift (x (lower i))

  iso-components : βˆ€ i β†’ π’œ i β‰… lA (lift i)
  iso-components i = Lift-β‰…

  Bβ‰…A : Lift-Alg (β¨… π’œ) (suc (ov Ξ±)) β‰… β¨… lA
  Bβ‰…A = Lift-Alg-β¨…β‰…  {fizw = fe₁}{fiu = feβ‚€} iso-components

 VlA (vprodw{I}{π’œ} x) = visow (vprodw vlA) (β‰…-sym Bβ‰…A)
  where
  𝑰 : Type (suc (ov Ξ±))
  𝑰 = Lift (suc (ov Ξ±)) I

  lA : 𝑰 β†’ Algebra (suc (ov Ξ±)) 𝑆
  lA i = Lift-Alg (π’œ (lower i)) (suc (ov Ξ±))

  vlA : βˆ€ i β†’ (lA i) ∈ V{Ξ±}{suc (ov Ξ±)} 𝒦
  vlA i = VlA (x (lower i))

  iso-components : βˆ€ i β†’ π’œ i β‰… lA (lift i)
  iso-components i = Lift-β‰…

  Bβ‰…A : Lift-Alg (β¨… π’œ) (suc (ov Ξ±)) β‰… β¨… lA
  Bβ‰…A = Lift-Alg-β¨…β‰… {fizw = fe₁}{fiu = feβ‚‚} iso-components

 VlA (visou{𝑨}{𝑩} x Aβ‰…B) = visow (vlift x) (Lift-Alg-iso Aβ‰…B)
 VlA (visow{𝑨}{𝑩} x Aβ‰…B) = visow (VlA x) (Lift-Alg-iso Aβ‰…B)

← Base.Varieties.EquationalLogic Base.Varieties.Properties β†’