↑ Top

Free setoid algebras


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

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

module Setoid.Varieties.FreeAlgebras {𝑆 : 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 ( proj₁ to fst ; projβ‚‚ to snd )
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 (_≑_)

-- Imports from the Agda Universal Algebra Library -------------------------------
open  import Overture          using ( ∣_∣ ; βˆ₯_βˆ₯ )
open  import Setoid.Relations  using ( fkerPred )
open  import Setoid.Functions  using ( eq ; IsSurjective )

open  import Base.Terms {𝑆 = 𝑆}       using ( β„Š )
open  import Setoid.Algebras {𝑆 = 𝑆}  using ( Algebra ; ov ; Lift-Alg )

open  import Setoid.Homomorphisms {𝑆 = 𝑆}
      using ( epi ; IsEpi ; IsHom ; hom ; epiβ†’hom ; βŠ™-epi ; ToLift-epi )

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 ; _⊫_ ; _β‰ˆΜ‡_ ; _⊒_β–Ή_β‰ˆ_ ; 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 aribtrary 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
  ΞΉ = 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 𝑨 kA = sound (Ξ» i ρ β†’ βˆ₯ i βˆ₯ 𝑨 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 ∣ hom𝔽[ X ] ∣
 hom𝔽[ X ]-is-epic = IsEpi.isSurjective (snd (epi𝔽[ X ]))


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

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


 module _  {X : Type Ο‡} {𝑨 : Algebra Ξ± ρᡃ}{sA : 𝑨 ∈ S {Ξ² = Ξ±}{ρᡃ} β„“ 𝒦} where
  open Environment 𝑨 using ( Equal )
  kerπ”½βŠ†Equal : βˆ€{p q} β†’ (p , q) ∈ fkerPred ∣ hom𝔽[ X ] ∣ β†’ Equal p q
  kerπ”½βŠ†Equal{p = p}{q} x = S-id1{β„“ = β„“}{p = p}{q} (β„°βŠ’[ X ]β–ΉTh𝒦 x) 𝑨 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
    _⟨$⟩_ Ο† = free-lift{𝑨 = 𝑨} id
    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∣ ] 𝑨 Ο†
    compatible (isHom isEpi) = cong Interp (≑.refl , (Ξ» _ β†’ refl))
    isSurjective isEpi {y} = eq (β„Š y) 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
           -- (HSP theorem needs 𝑨 in higher universe level)
           {𝑨 : 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
   _⟨$⟩_ Ο† = free-lift{𝑨 = 𝑨} id
   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∣ ] 𝑨 Ο†
   compatible (isHom isEpi) = cong Interp (≑.refl , (Ξ» _ β†’ refl))
   isSurjective isEpi {y} = eq (β„Š y) 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

← Setoid.Varieties.Closure Setoid.Varieties.HSP