↑ Top

Closure Operators for Setoid Algebras

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


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

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

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

-- imports from Agda and the Agda Standard Library -------------------------------
open import Agda.Primitive         using () renaming ( Set to Type )
open import Data.Product           using ( _,_ ; Ξ£-syntax )
                                   renaming ( _Γ—_ to _∧_ )
open import Data.Unit.Polymorphic  using ( ⊀ ; tt )
open import Function               using ( id ) renaming ( Func to _⟢_ )
open import Level                  using ( Level ;  _βŠ”_ ; Lift ; lift ; lower )
open import Relation.Binary        using ( Setoid )
open import Relation.Unary         using ( Pred ; _∈_ ; _βŠ†_ )

-- Imports from the Agda Universal Algebra Library -------------------------------
open  import Setoid.Algebras       {𝑆 = 𝑆}  using ( Algebra ; ov ; Lift-Alg ; β¨… )
open  import Setoid.Homomorphisms  {𝑆 = 𝑆}
      using ( IsHom ; _β‰…_ ; β‰…-trans ; β‰…-sym ; Lift-β‰… ; ⨅≅⨅ℓρ ; _IsHomImageOf_ )
      using ( IdHomImage ; HomImage-β‰… ; HomImage-β‰…' ; Lift-HomImage-lemma )
open  import Setoid.Subalgebras    {𝑆 = 𝑆}
      using ( _≀_ ; _≀c_ ; ≀-reflexive ; ≀-trans ; β‰…-trans-≀ )
      using ( ≀-trans-β‰… ; Lift-≀-Lift ; ≀-Lift )

open _⟢_ renaming ( to to _⟨$⟩_ )

module _ {Ξ± ρᡃ Ξ² ρᡇ : Level} where

 private a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ

 Level-closure : βˆ€ β„“ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“))
 Level-closure β„“ 𝒦 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± ρᡃ ]  (𝑨 ∈ 𝒦)  ∧  𝑨 β‰… 𝑩

module _ {Ξ± ρᡃ Ξ² ρᡇ : Level} where

 Lift-closed :  βˆ€ β„“ β†’ {𝒦 : Pred(Algebra Ξ± ρᡃ) _}{𝑨 : Algebra Ξ± ρᡃ} β†’ 𝑨 ∈ 𝒦
  β†’             Lift-Alg 𝑨 Ξ² ρᡇ ∈ (Level-closure β„“ 𝒦)
 Lift-closed _ {𝑨 = 𝑨} kA = 𝑨 , (kA , Lift-β‰…)

module _  {Ξ± ρᡃ Ξ² ρᡇ : Level} where
 private a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ

 H : βˆ€ β„“ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“))
 H _ 𝒦 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± ρᡃ ] 𝑨 ∈ 𝒦 ∧ 𝑩 IsHomImageOf 𝑨

 S : βˆ€ β„“ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“))
 S _ 𝒦 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± ρᡃ ] 𝑨 ∈ 𝒦 ∧ 𝑩 ≀ 𝑨

 P : βˆ€ β„“ ΞΉ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“ βŠ” ΞΉ))
 P β„“ ΞΉ 𝒦 𝑩 = Ξ£[ I ∈ Type ΞΉ ] (Ξ£[ π’œ ∈ (I β†’ Algebra Ξ± ρᡃ) ] (βˆ€ i β†’ π’œ i ∈ 𝒦) ∧ (𝑩 β‰… β¨… π’œ))

module _  {Ξ± ρᡃ Ξ² ρᡇ : Level} where
 private a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ

 SP : βˆ€ β„“ ΞΉ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“ βŠ” ΞΉ))
 SP β„“ ΞΉ 𝒦 = S{Ξ±}{ρᡃ} (a βŠ” β„“ βŠ” ΞΉ) (P β„“ ΞΉ 𝒦)

module _  {Ξ± ρᡃ Ξ² ρᡇ Ξ³ ρᢜ Ξ΄ ρᡈ : Level} where
 private a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ ; c = Ξ³ βŠ” ρᢜ ; d = Ξ΄ βŠ” ρᡈ

 V : βˆ€ β„“ ΞΉ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’  Pred(Algebra Ξ΄ ρᡈ) (d βŠ” ov(a βŠ” b βŠ” c βŠ” β„“ βŠ” ΞΉ))
 V β„“ ΞΉ 𝒦 = H{Ξ³}{ρᢜ}{Ξ΄}{ρᡈ} (a βŠ” b βŠ” β„“ βŠ” ΞΉ) (S{Ξ²}{ρᡇ} (a βŠ” β„“ βŠ” ΞΉ) (P β„“ ΞΉ 𝒦))

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.


module _ {Ξ± ρᡃ β„“ ΞΉ : Level} where

 is-variety : (𝒱 : Pred (Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)) β†’ Type (ov (Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
 is-variety 𝒱 = V{Ξ² = Ξ±}{ρᡇ = ρᡃ}{Ξ³ = Ξ±}{ρᢜ = ρᡃ} β„“ ΞΉ 𝒱 βŠ† 𝒱

 variety : Type (ov (Ξ± βŠ” ρᡃ βŠ” ov β„“ βŠ” ΞΉ))
 variety = Ξ£[ 𝒱 ∈ (Pred (Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)) ] is-variety 𝒱

Closure properties of S

S is a closure operator. The fact that S is expansive won’t be needed, so we omit the proof, but we will make use of monotonicity and idempotence of S.

module _ {Ξ± ρᡃ : Level} where

 private a = Ξ± βŠ” ρᡃ

 S-mono :  βˆ€{β„“} β†’ {𝒦 𝒦' : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)}
  β†’        𝒦 βŠ† 𝒦' β†’ S{Ξ² = Ξ±}{ρᡃ} β„“ 𝒦 βŠ† S β„“ 𝒦'

 S-mono kk {𝑩} (𝑨 , (kA , B≀A)) = 𝑨 , ((kk kA) , B≀A)

We say S is idempotent provided \af{S} (\af{S} \ab{𝒦}) \as{=} \af{S} \ab{𝒦}. Of course, this is proved by establishing two inclusions, but one of them is trivial, so only the other need be formalized, which we do as follows.


 S-idem :  βˆ€{Ξ² ρᡇ Ξ³ ρᢜ β„“} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)}
  β†’        S{Ξ² = Ξ³}{ρᢜ} (a βŠ” β„“) (S{Ξ² = Ξ²}{ρᡇ} β„“ 𝒦) βŠ† S{Ξ² = Ξ³}{ρᢜ} β„“ 𝒦

 S-idem (𝑨 , (𝑩 , sB , A≀B) , x≀A) = 𝑩 , (sB , ≀-trans x≀A A≀B)

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.


 H-expa : βˆ€{β„“} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† H β„“ 𝒦
 H-expa {β„“} {𝒦}{𝑨} kA = 𝑨 , kA , IdHomImage

 S-expa : βˆ€{β„“} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† S β„“ 𝒦
 S-expa {β„“}{𝒦}{𝑨} kA = 𝑨 , (kA , ≀-reflexive)

 P-mono :  βˆ€{β„“ ΞΉ} β†’ {𝒦 𝒦' : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)}
  β†’        𝒦 βŠ† 𝒦' β†’ P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦 βŠ† P β„“ ΞΉ 𝒦'

 P-mono {β„“}{ΞΉ}{𝒦}{𝒦'} kk {𝑩} (I , π’œ , (kA , Bβ‰…β¨…A)) = I , (π’œ , ((Ξ» i β†’ kk (kA i)) , Bβ‰…β¨…A))

 open _β‰…_
 open IsHom

 P-expa : βˆ€{β„“ ΞΉ} β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† P β„“ ΞΉ 𝒦
 P-expa {β„“}{ΞΉ}{𝒦}{𝑨} kA = ⊀ , (Ξ» x β†’ 𝑨) , ((Ξ» i β†’ kA) , Goal)
  where
  open Algebra 𝑨 using () renaming (Domain to A)
  open Algebra (β¨… (Ξ» _ β†’ 𝑨)) using () renaming (Domain to β¨…A)
  open Setoid A using ( refl )
  open Setoid ⨅A using () renaming ( refl to refl⨅ )

  toβ¨… : A ⟢ β¨…A
  (toβ¨… ⟨$⟩ x) = Ξ» _ β†’ x
  cong to⨅ xy = λ _ → xy
  toβ¨…IsHom : IsHom 𝑨 (β¨… (Ξ» _ β†’ 𝑨)) toβ¨…
  compatible to⨅IsHom =  refl⨅

  fromβ¨… : β¨…A ⟢ A
  (fromβ¨… ⟨$⟩ x) = x tt
  cong from⨅ xy = xy tt
  fromβ¨…IsHom : IsHom (β¨… (Ξ» _ β†’ 𝑨)) 𝑨 fromβ¨…
  compatible from⨅IsHom = refl

  Goal : 𝑨 β‰… β¨… (Ξ» x β†’ 𝑨)
  to Goal = to⨅ , to⨅IsHom
  from Goal = from⨅ , from⨅IsHom
  to∼from Goal = Ξ» _ _ β†’ refl
  from∼to Goal = Ξ» _ β†’ refl


 V-expa : βˆ€ β„“ ΞΉ β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)} β†’ 𝒦 βŠ† V β„“ ΞΉ 𝒦
 V-expa β„“ ΞΉ {𝒦} {𝑨} x = H-expa {a βŠ” β„“ βŠ” ΞΉ} (S-expa {a βŠ” β„“ βŠ” ΞΉ} (P-expa {β„“}{ΞΉ} 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 β„“)}
          {𝑨 : Algebra Ξ± ρᡃ}{𝑩 : Algebra Ξ² ρᡇ} where

 S-β‰… : 𝑨 ∈ S β„“ 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ S{Ξ± βŠ” Ξ²}{ρᡃ βŠ” ρᡇ}(Ξ± βŠ” ρᡃ βŠ” β„“) (Level-closure β„“ 𝒦)
 S-β‰… (𝑨' , kA' , A≀A') Aβ‰…B = lA' , (lklA' , B≀lA')
  where
  lA' : Algebra (Ξ± βŠ” Ξ²) (ρᡃ βŠ” ρᡇ)
  lA' = Lift-Alg 𝑨' Ξ² ρᡇ
  lklA' : lA' ∈ Level-closure β„“ 𝒦
  lklA' = Lift-closed β„“ kA'
  subgoal : 𝑨 ≀ lA'
  subgoal = ≀-trans-β‰… A≀A' Lift-β‰…
  B≀lA' : 𝑩 ≀ lA'
  B≀lA' = β‰…-trans-≀ (β‰…-sym Aβ‰…B) subgoal

 V-β‰… : 𝑨 ∈ V β„“ ΞΉ 𝒦 β†’ 𝑨 β‰… 𝑩 β†’ 𝑩 ∈ V{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦
 V-β‰… (𝑨' , spA' , AimgA') Aβ‰…B = 𝑨' , spA' , HomImage-β‰… AimgA' Aβ‰…B

module _  {Ξ± ρᡃ β„“ : Level}
          (𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“))
          (𝑨 : Algebra (Ξ± βŠ” ρᡃ βŠ” β„“) (Ξ± βŠ” ρᡃ βŠ” β„“)) where
 private ΞΉ = ov(Ξ± βŠ” ρᡃ βŠ” β„“)

 V-β‰…-lc : Lift-Alg 𝑨 ΞΉ ΞΉ ∈ V{Ξ² = ΞΉ}{ΞΉ} β„“ ΞΉ 𝒦 β†’ 𝑨 ∈ V{Ξ³ = ΞΉ}{ΞΉ} β„“ ΞΉ 𝒦
 V-β‰…-lc (𝑨' , spA' , lAimgA') = 𝑨' , (spA' , AimgA')
  where
  AimgA' : 𝑨 IsHomImageOf 𝑨'
  AimgA' = Lift-HomImage-lemma lAimgA'

The remaining theorems in this file are as yet unused, but may be useful later and/or for reference.


module _ {Ξ± ρᡃ β„“ ΞΉ : Level}{𝒦 : Pred (Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)} where

 -- For reference, some useful type levels:
 classP : Pred (Algebra Ξ± ρᡃ) (ov(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
 classP = P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦

 classSP : Pred (Algebra Ξ± ρᡃ) (ov(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
 classSP = S{Ξ² = Ξ±}{ρᡃ} (Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ) (P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦)

 classHSP : Pred (Algebra Ξ± ρᡃ) (ov(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ))
 classHSP = H{Ξ² = Ξ±}{ρᡃ}(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ) (S{Ξ² = Ξ±}{ρᡃ}(Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ) (P{Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦))

 classS : βˆ€{Ξ² ρᡇ} β†’ Pred (Algebra Ξ² ρᡇ) (Ξ² βŠ” ρᡇ βŠ” ov(Ξ± βŠ” ρᡃ βŠ” β„“))
 classS = S β„“ 𝒦
 classK : βˆ€{Ξ² ρᡇ} β†’ Pred (Algebra Ξ² ρᡇ) (Ξ² βŠ” ρᡇ βŠ” ov(Ξ± βŠ” ρᡃ βŠ” β„“))
 classK = Level-closure{Ξ±}{ρᡃ} β„“ 𝒦

module _ {Ξ± ρᡃ Ξ² ρᡇ Ξ³ ρᢜ β„“ : Level}{𝒦 : Pred (Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
 private a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ ; c = Ξ³ βŠ” ρᢜ

 LevelClosure-S : Pred (Algebra (Ξ± βŠ” Ξ³) (ρᡃ βŠ” ρᢜ)) (c βŠ” ov(a βŠ” b βŠ” β„“))
 LevelClosure-S = Level-closure{Ξ²}{ρᡇ} (a βŠ” β„“) (S β„“ 𝒦)

 S-LevelClosure : Pred (Algebra (Ξ± βŠ” Ξ³) (ρᡃ βŠ” ρᢜ)) (ov(a βŠ” c βŠ” β„“))
 S-LevelClosure = S{Ξ± βŠ” Ξ³}{ρᡃ βŠ” ρᢜ}(a βŠ” β„“) (Level-closure β„“ 𝒦)

 S-Lift-lemma : LevelClosure-S βŠ† S-LevelClosure
 S-Lift-lemma {π‘ͺ} (𝑩 , (𝑨 , (kA , B≀A)) , Bβ‰…C) =
  Lift-Alg 𝑨 Ξ³ ρᢜ , (Lift-closed{Ξ² = Ξ³}{ρᢜ} β„“ kA) , C≀lA
  where
  B≀lA : 𝑩 ≀ Lift-Alg 𝑨 Ξ³ ρᢜ
  B≀lA = ≀-Lift B≀A
  C≀lA : π‘ͺ ≀ Lift-Alg 𝑨 Ξ³ ρᢜ
  C≀lA = β‰…-trans-≀ (β‰…-sym Bβ‰…C) B≀lA


module _ {Ξ± ρᡃ : Level} where

 P-Lift-closed :  βˆ€ β„“ ΞΉ β†’ {𝒦 : Pred (Algebra Ξ± ρᡃ)(Ξ± βŠ” ρᡃ βŠ” ov β„“)}{𝑨 : Algebra Ξ± ρᡃ}
  β†’               𝑨 ∈ P{Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦
  β†’               {Ξ³ ρᢜ : Level} β†’ Lift-Alg 𝑨 Ξ³ ρᢜ ∈ P (Ξ± βŠ” ρᡃ βŠ” β„“) ΞΉ (Level-closure β„“ 𝒦)
 P-Lift-closed β„“ ΞΉ {𝒦}{𝑨} (I , π’œ , kA , Aβ‰…β¨…π’œ) {Ξ³}{ρᢜ} =
  I , (Ξ» x β†’ Lift-Alg (π’œ x) Ξ³ ρᢜ) , goal1 , goal2
  where
  goal1 : (i : I) β†’ Lift-Alg (π’œ i) Ξ³ ρᢜ ∈ Level-closure β„“ 𝒦
  goal1 i = Lift-closed β„“ (kA i)
  goal2 : Lift-Alg 𝑨 Ξ³ ρᢜ β‰… β¨… (Ξ» x β†’ Lift-Alg (π’œ x) Ξ³ ρᢜ)
  goal2 = β‰…-trans (β‰…-sym Lift-β‰…) (β‰…-trans Aβ‰…β¨…π’œ (⨅≅⨅ℓρ{β„“ = Ξ³}{ρ = ρᢜ}))

← Setoid.Varieties.SoundAndComplete Setoid.Varieties.Properties β†’