Skip to content

Setoid.Varieties.FreeAlgebras

Free setoid algebras

This is the Setoid.Varieties.FreeAlgebras module of the Agda Universal Algebra Library.

The term algebra 𝑻 X is free among all algebras. Results like the HSP theorem need an algebra free among the members of a given class 𝒦, and that is what 𝔽[_], the relatively free algebra, provides: the quotient of 𝑻 X by the equations that hold throughout 𝒦. Two terms are identified in 𝔽[ X ] exactly when every algebra of 𝒦 satisfies the equation between them, so 𝔽[ X ] satisfies precisely the identities of 𝒦.

This module constructs the relatively free algebra, together with the natural epimorphism epi𝔽[_] from 𝑻 X onto it and its homomorphism reduct hom𝔽[_], and identifies the kernel of that epimorphism with the theory of the variety generated by 𝒦 (class-models-kernel, kernel-in-theory).

𝔽-ModTh-epi supplies the step the HSP theorem turns on: every model 𝑨 of the theory of V 𝒦 is a homomorphic image of the relatively free algebra on its own carrier, 𝔽[ π•Œ[ 𝑨 ] ], not of 𝔽[ X ] for an arbitrary X. The distinction matters: an arbitrary generator type need not surject onto 𝑨, whereas taking the generators to be the elements of 𝑨 makes the epimorphism immediate. See Setoid.Varieties.HSP for the argument in which these pieces are assembled.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Varieties.FreeAlgebras where

-- Imports from Agda and the Agda Standard Library -------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( Ξ£-syntax ; _,_ ; proj₁ ; projβ‚‚ )
open import Function         using ( _∘_ ; id ) renaming ( Func to _⟢_ )
open import Level            using ( Level ; _βŠ”_)
open import Relation.Binary  using ( Setoid )
open import Relation.Unary   using ( Pred ; _∈_ ; _βŠ†_ )

open import Relation.Binary.PropositionalEquality as ≑ using (_≑_)

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture                           using  ( 𝑆 )
open import Overture.Terms                     using  ( β„Š )
open import Setoid.Algebras                    using  ( Algebra ; ov ; Lift-Alg ; 𝔻[_] )
open import Setoid.Functions                   using  ( eq ; IsSurjective )
open import Setoid.Homomorphisms               using  ( epi ; IsEpi ; IsHom ; hom
                                                      ; epiβ†’hom ; βŠ™-epi ; ToLift-epi )
open import Setoid.Relations                   using  ( fkerPred )
open import Setoid.Terms                       using  ( 𝑻 ; _≐_ ; module Environment
                                                      ; free-lift ; free-lift-interp )
open import Setoid.Varieties.Closure           using  ( V ; S )
open import Setoid.Varieties.Preservation      using  ( classIds-βŠ†-VIds ; S-id1 )
open import Setoid.Varieties.SoundAndComplete  using  ( Eq ; _⊫_ ; ⊫-proof ; _β‰ˆΜ‡_
                                                      ; Th ; Mod ; module Soundness
                                                      ; _⊒_β–Ή_β‰ˆ_ ; module FreeAlgebra )
open _⟢_      using ( cong ) renaming ( to to _⟨$⟩_ )
open Algebra  using ( Domain )

In the code below, X will play the role of an arbitrary collection of variables; it would suffice to take X to be the cardinality of the largest algebra in 𝒦, but since we don't know that cardinality, we leave X arbitrary for now.

Alternatively, we could let X be the product of all algebras in the class 𝒦, like so.

𝕏 : Type oΞ± 𝕏 = Carrier ( Domain (β¨… (𝔄{𝒦 = S 𝒦})) )

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

  open Eq

We now define the algebra 𝔽, which plays the role of the relatively free algebra, along with the natural epimorphism epi𝔽 : epi (𝑻 𝕏) 𝔽 from 𝑻 𝕏 to 𝔽. The relatively free algebra (relative to Th 𝒦) is called M and is derived from TermSetoid 𝕏 and TermInterp 𝕏 and imported from the EquationalLogic module.

 -- ℐ indexes the collection of equations modeled by 𝒦
  ℐ : Type ΞΉ
  ℐ = Ξ£[ eq ∈ Eq {Ο‡ = Ο‡} ] 𝒦 ⊫ ((lhs eq) β‰ˆΜ‡ (rhs eq))

  β„° : ℐ β†’ Eq
  β„° (eqv , p) = eqv

  β„°βŠ’[_]β–ΉTh𝒦 : (X : Type Ο‡) β†’ βˆ€{p q} β†’ β„° ⊒ X β–Ή p β‰ˆ q β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
  β„°βŠ’[ X ]β–ΉTh𝒦 x .⊫-proof 𝑨 kA = sound (Ξ» i ρ β†’ (projβ‚‚ i) .⊫-proof 𝑨 kA ρ) x
    where open Soundness β„° 𝑨

 ----------- THE RELATIVELY FREE ALGEBRA -----------
  open FreeAlgebra {ΞΉ = ΞΉ}{I = ℐ} β„° using ( 𝔽[_] )

Finally, we define an epimorphism from 𝑻 X onto the relatively free algebra 𝔽[ X ]. Of course, the kernel of this epimorphism will be the congruence of 𝑻 X defined by identities modeled by (S 𝒦, hence) 𝒦.

  epi𝔽[_] : (X : Type Ο‡) β†’ epi (𝑻 X) 𝔽[ X ]
  epi𝔽[ X ] = h , hepi
    where
    open Algebra 𝔽[ X ]  using() renaming ( Domain to F ; Interp to InterpF )
    open Setoid F        using() renaming ( _β‰ˆ_  to _β‰ˆFβ‰ˆ_ ; refl to reflF )
    open Algebra (𝑻 X)   using() renaming (Domain to TX)
    open Setoid TX       using() renaming ( _β‰ˆ_ to _β‰ˆTβ‰ˆ_ ; refl to reflT )

    open _≐_ ; open IsEpi ; open IsHom

    c : βˆ€ {x y} β†’ x β‰ˆTβ‰ˆ y β†’ x β‰ˆFβ‰ˆ y
    c (rfl {x}{y} ≑.refl) = reflF
    c (gnl {f}{s}{t} x) = cong InterpF (≑.refl , c ∘ x)

    h : TX ⟢ F
    h = record { to = id ; cong = c }

    hepi : IsEpi (𝑻 X) 𝔽[ X ] h
    compatible (isHom hepi) = cong h reflT
    isSurjective hepi {y} = eq y reflF


  hom𝔽[_] : (X : Type Ο‡) β†’ hom (𝑻 X) 𝔽[ X ]
  hom𝔽[ X ] = epiβ†’hom (𝑻 X) 𝔽[ X ] epi𝔽[ X ]

  hom𝔽[_]-is-epic : (X : Type Ο‡) β†’ IsSurjective (proj₁ (hom𝔽[ X ]))
  hom𝔽[ X ]-is-epic = IsEpi.isSurjective (projβ‚‚ (epi𝔽[ X ]))


  class-models-kernel : βˆ€{X p q} β†’ (p , q) ∈ fkerPred (proj₁ (hom𝔽[ X ])) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
  class-models-kernel {X = X}{p}{q} pKq = β„°βŠ’[ X ]β–ΉTh𝒦 pKq

  kernel-in-theory : {X : Type Ο‡} β†’ fkerPred (proj₁ (hom𝔽[ X ])) βŠ† Th (V β„“ ΞΉ 𝒦)
  kernel-in-theory {X = X} {p , q} pKq =
    classIds-βŠ†-VIds {β„“ = β„“} (class-models-kernel pKq)


  module _  {X : Type Ο‡} {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}{sA : 𝑨 ∈ S {Ξ² = Ξ±}{ρᡃ} β„“ 𝒦} where
    open Environment 𝑨 using ( Equal )
    kerπ”½βŠ†Equal : βˆ€{p q} β†’ (p , q) ∈ fkerPred (proj₁ (hom𝔽[ X ])) β†’ Equal p q
    kerπ”½βŠ†Equal{p = p}{q} x = S-id1{β„“ = β„“} (β„°βŠ’[ X ]β–ΉTh𝒦 x) .⊫-proof 𝑨 sA

  π’¦βŠ«β†’β„°βŠ’ : {X : Type Ο‡} β†’ βˆ€{p q} β†’ 𝒦 ⊫ p β‰ˆΜ‡ q β†’ β„° ⊒ X β–Ή p β‰ˆ q
  π’¦βŠ«β†’β„°βŠ’ {p = p} {q} pKq = hyp (p β‰ˆΜ‡ q , pKq) where open _⊒_β–Ή_β‰ˆ_ using (hyp)

------------------------------------------------------------------------------

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

  module lower-universe-version {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ} where
    open FreeHom Ξ± {Ξ±}{ρᡃ}{β„“}{𝒦}
    open FreeAlgebra {ΞΉ = ΞΉ}{I = ℐ} β„°            using ( 𝔽[_] )
    open Algebra 𝑨  renaming (Domain to A)       using( Interp )
    open Setoid A   renaming ( Carrier to ∣A∣ )  using ( trans ; sym ; refl )

    𝔽-ModTh-epi : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] 𝑨
    𝔽-ModTh-epi A∈ModThK = Ο† , isEpi
      where
      Ο† : (Domain 𝔽[ ∣A∣ ]) ⟢ A
      Ο† ⟨$⟩ x = free-lift{𝑨 = 𝑨} id x
      Ο† .cong {p} {q} pq =
        trans  (sym (free-lift-interp{𝑨 = 𝑨} id p))
               (trans  (A∈ModThK{p = p}{q} (kernel-in-theory pq) id )
                       (free-lift-interp{𝑨 = 𝑨} id q))
      isEpi : IsEpi 𝔽[ ∣A∣ ] 𝑨 Ο†
      isEpi .isHom .compatible = cong Interp (≑.refl , Ξ» _ β†’ refl)
      isEpi .isSurjective = eq (β„Š _) refl

    𝔽-ModTh-epi-lift :
      𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] (Lift-Alg 𝑨 (ov {𝑆 = 𝑆} Ξ±) (ov {𝑆 = 𝑆} Ξ±))
    𝔽-ModTh-epi-lift A∈ModThK = βŠ™-epi (𝔽-ModTh-epi Ξ» {p q} β†’ A∈ModThK{p = p}{q}) ToLift-epi

  module _  -- higher-universe-version (needed by HSP theorem)
    {𝑨 : Algebra {𝑆 = 𝑆} (Ξ± βŠ” ρᡃ βŠ” β„“) (Ξ± βŠ” ρᡃ βŠ” β„“)}
    where

    open FreeHom (Ξ± βŠ” ρᡃ βŠ” β„“) {Ξ±}{ρᡃ}{β„“}{𝒦}
    open FreeAlgebra {ΞΉ = ΞΉ}{I = ℐ} β„° using ( 𝔽[_] )
    open Algebra 𝑨 using( Interp ) renaming (Domain to A)
    open Environment 𝑨  using ( ⟦_⟧ )
    open Setoid A renaming ( Carrier to ∣A∣ )  using ( trans ; sym ; refl ; _β‰ˆ_)
    open SetoidReasoning A

    𝔽-ModTh-epi : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] 𝑨
    𝔽-ModTh-epi A∈ModThK = Ο† , isEpi
      where
      Ο† : 𝔻[ 𝔽[ ∣A∣ ] ] ⟢ A
      Ο† ⟨$⟩ x = free-lift id x
      Ο† .cong {p} {q} pq = begin
          free-lift id p  β‰ˆΛ˜βŸ¨ free-lift-interp{𝑨 = 𝑨} id p ⟩
          ⟦ p ⟧ ⟨$⟩ id    β‰ˆβŸ¨ A∈ModThK{p = p}{q} (kernel-in-theory pq) id ⟩
          ⟦ q ⟧ ⟨$⟩ id    β‰ˆβŸ¨ free-lift-interp{𝑨 = 𝑨} id q ⟩
          free-lift id q  ∎

      isEpi : IsEpi 𝔽[ ∣A∣ ] 𝑨 Ο†
      isEpi .isHom .compatible = cong Interp (≑.refl , Ξ» _ β†’ refl)
      isEpi .isSurjective = eq (β„Š _) refl

    𝔽-ModTh-epi-lift : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] (Lift-Alg 𝑨 ΞΉ ΞΉ)
    𝔽-ModTh-epi-lift A∈ModThK =
      βŠ™-epi (𝔽-ModTh-epi (Ξ» {p q} β†’ A∈ModThK{p = p}{q})) ToLift-epi