Skip to content

Setoid.Varieties.Closure

Closure Operators for Setoid Algebras

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

  • H 𝒦 = algebras isomorphic to a homomorphic image of a member of 𝒦;
  • S 𝒦 = algebras isomorphic to a subalgebra of a member of 𝒦;
  • P 𝒦 = algebras isomorphic to a product of members of 𝒦.
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

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

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

open import Agda.Primitive using () renaming ( Set to Type )

-- imports from the Agda Standard Library ----------------------------------------
open import Data.Product           using ( _,_ ; Ξ£-syntax )
                                   renaming ( _Γ—_ to _∧_ )
open import Data.Unit.Polymorphic  using ( ⊀ ; tt )
open import Function               using () renaming ( Func to _⟢_ )
open import Level                  using ( Level ;  _βŠ”_ )
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 {𝑆 = 𝑆}
open import Setoid.Subalgebras {𝑆 = 𝑆}
open _⟢_ renaming ( to to _⟨$⟩_ )

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

  private
    a b : Level
    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-β‰…)

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

  H S : βˆ€ β„“ β†’ Pred(Algebra Ξ± ρᡃ) (a βŠ” ov β„“) β†’ Pred(Algebra Ξ² ρᡇ) (b βŠ” ov(a βŠ” β„“))
  H _ 𝒦 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± ρᡃ ] 𝑨 ∈ 𝒦 ∧ 𝑩 IsHomImageOf 𝑨
  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 : Level
    a = Ξ± βŠ” ρᡃ ; b = Ξ² βŠ” ρᡇ

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

  module _ {γ ρᢜ δ ρᡈ : Level} where

    private
      c d : Level
      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.

A common-case level specialization of V

The operator V carries eight independent universe levels. The input class lives at (Ξ±, ρᡃ) and the output algebra at (Ξ΄, ρᡈ), but the intermediate pairs (Ξ², ρᡇ) and (Ξ³, ρᢜ) are the levels of the algebras threaded through the H ∘ S ∘ P composition: they are determined by neither the input nor the output, so they stay free metavariables whenever V is applied without a goal that already pins them. That generality is essential for the HSP theorem, but is unnecessary friction for the everyday request "the variety generated by a fixed algebra".

Vβ€² is the specialization of V to the overwhelmingly common case in which the generated variety is considered at the same levels as the class that generates it. It collapses all four algebra positions to the input levels (Ξ±, ρᡃ) β€” exactly the pinning is-variety already performs above (Ξ² = Ξ³ = Ξ΄ = Ξ± and ρᡇ = ρᢜ = ρᡈ = ρᡃ), under which the output level d βŠ” ov(a βŠ” b βŠ” c βŠ” β„“ βŠ” ΞΉ) of V collapses to a βŠ” ov(a βŠ” β„“ βŠ” ΞΉ). This is a documented narrowing of the canonical operator, not a synonym: V remains the level-polymorphic form, while Vβ€² is the fixed-level entry point that downstream examples and tests should prefer.

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

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

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 S (S 𝒦) = S 𝒦. 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) )

The expansiveness lemmas above are stated with _βŠ†_, i.e. 𝒦 βŠ† βŠ™ β„“ … 𝒦, which unfolds to βˆ€ {𝑨} β†’ 𝑨 ∈ 𝒦 β†’ 𝑨 ∈ βŠ™ β„“ … 𝒦 with both the class 𝒦 and the element 𝑨 implicit. Recovering them from a single membership proof is a higher-order unification problem (_𝒦 _𝑨 β‰Ÿ (𝑨 ∈ 𝒦)) that Agda cannot solve once the class predicate reduces. The variants below take the class 𝒦 explicitly, so a membership in a closure operator follows directly from a membership in the class with nothing to infer. The _βŠ†_ forms above remain the abstract statements; these are the ergonomic entry points (V-expaβ€² is the one exercised by Examples.Setoid.HSPCommutativeMonoid).

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

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

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

  V-expaβ€² : βˆ€ β„“ ΞΉ (𝒦 : Pred (Algebra Ξ± ρᡃ)(a βŠ” ov β„“)) {𝑨} β†’ 𝑨 ∈ 𝒦 β†’ 𝑨 ∈ V β„“ ΞΉ 𝒦
  V-expaβ€² β„“ ΞΉ 𝒦 = V-expa β„“ ΞΉ {𝒦}

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β‰…β¨…π’œ (⨅≅⨅ℓρ{β„“ = Ξ³}{ρ = ρᢜ}))