Skip to content

Setoid.Varieties.Reducts

Reduct classes of varieties

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

Like its companion Setoid.Varieties.Invariance, this module lives in the Setoid/ foundation; reducts are in the domain of universal algebra.

Fix two signatures 𝑆₁, 𝑆₂ and a signature morphism Ο† : 𝑆₁ β†’ 𝑆₂. The reduct functor reduct Ο† : Alg 𝑆₂ β†’ Alg 𝑆₁ (Setoid.Categories.Reduct) turns each 𝑆₂-algebra into an 𝑆₁-algebra by remembering only the operations named by Ο†.

Given a variety 𝒱 of 𝑆₂-algebras, this module studies the reduct class

reduct Ο† 𝒱  =  { 𝑩 : 𝑩 β‰… reduct Ο† 𝑨 for some 𝑨 ∈ 𝒱 },

a class of 𝑆₁-algebras, and asks, "under which of the operators S, H, P is reduct Ο† 𝒱 closed?"1

At first glance, we might anticipate that reduct Ο† 𝒱 is closed under S and P but not H, which would make it a prevariety.2

Working it through against the library's definitions shows that the truth is different, and sharper, so we record it formally here. (This is research-tracking, where discovering which assertion is the correct one is part of the process.)

Two layers must be distinguished.

  • Functorial preservation (true for S, P, and H). reduct Ο† preserves the subalgebra relation, products, and the homomorphic-image relation between individual algebras. A mono maps to a mono, a product to a product, an epi to an epi. This is what "reduct Ο† preserves subobjects and limits" means, and it is exactly the morphism action of the functor reductF read off on the three kinds of homomorphism. All three hold, with one-line proofs, because reduct Ο† keeps the underlying setoid map of a homomorphism unchanged and only reindexes the operation it must respect.

  • Class-level closure (true for P only). Whether the class reduct Ο† (𝒱) is closed under an operator O is the question whether every O-construction performed on reducts can be reconstructed upstairs β€” realized as the reduct of an O-construction inside 𝒱. For products this reconstruction always succeeds (reduct-β¨… below): a product of reducts is the reduct of a product, because the dropped operations on a product are computed coordinate-by-coordinate and are therefore always available. For subalgebras and homomorphic images it can fail, because a sub- or quotient-algebra of a reduct generally cannot be re-equipped with the operations Ο† forgot.

The upshot: reduct Ο† (𝒱) is closed under P (and isomorphism) but not, in general, under S or H. It is a product class (model theory calls reducts of an elementary class pseudo-elementary), and is not a prevariety β€” S-closure already fails. A concrete S-counterexample is recorded in the final section; the failure of H is discussed there too, including the instructive fact that for the variety of groups H-closure happens to hold, so neither the issue's "S, P yes, H no" pattern nor its mirror is the general truth: the general truth is "P always; S and H not in general."

There is a genuine grain of truth behind "prevariety", supplied by reduct-invariance of satisfaction (⊧-reduct): every reduct of a 𝒱-algebra satisfies the Ο†-pullback of 𝒱's equational theory, so reduct Ο† (𝒱) is contained in a variety of 𝑆₁-algebras even though it need not equal one. That containment is reduct-⊧ below.

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

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

module Setoid.Varieties.Reducts where

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

-- Imports from the Agda Standard Library -----------------------------------
open import Data.Product                   using ( _,_ ; Ξ£-syntax ; proj₁ ; projβ‚‚ )
                                           renaming ( _Γ—_ to _∧_ )
open import Function                       using ( Func ; _∘_ )
open import Level                          using ( Level ; _βŠ”_ ) renaming ( suc to lsuc )
open import Relation.Binary                using ( Setoid )
open import Relation.Unary                 using ( Pred ; _∈_ ; _βŠ†_ )

open import Relation.Binary.PropositionalEquality using ( _≑_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Setoid.Algebras.Reduct             using  ( reduct )
open import Setoid.Categories.Reduct             using  ( reductF )
open import Setoid.Varieties.Invariance          using  ( ⊧-reduct )
open import Overture.Signatures.Morphisms           using  ( SigMorphism )
                                                    renaming ( ΞΉ to ΞΉ-op ; ΞΊ to ΞΊ-ar )
open import Overture.Terms                          using  ( Term )
open import Overture.Terms.Translation              using  ( _✢_ )
open import Setoid.Algebras.Basic                   using  ( Algebra ; 𝔻[_] )
open import Setoid.Algebras.Products                using  ( β¨… )
open import Setoid.Homomorphisms.Basic              using  ( hom ; IsHom ; mkIsHom )
open import Setoid.Homomorphisms.Isomorphisms       using  ( _β‰…_ ; mkiso ; β‰…-refl
                                                           ; β‰…-sym ; β‰…-trans ; β¨…β‰… )
open import Setoid.Homomorphisms.HomomorphicImages  using  ( _IsHomImageOf_ )
open import Setoid.Subalgebras.Basic                using  ( _≀_ )
open import Setoid.Categories.Functor               using  ( Functor )
open import Setoid.Varieties.Closure                using  ( P )

open IsHom using ( compatible )
open _β‰…_ using ( to ; from ; to∼from ; from∼to )

import Setoid.Varieties.EquationalLogic as EqLogic

private variable
  Ξ± ρ Ξ² ρᡇ Ξ³ ρᢜ β„“ ΞΉ Ο‡ : Level

Reduct preserves homomorphisms

Everything rests on one observation: a homomorphism is preserved by reduct Ο† on the nose. Concretely, if h : 𝑨 ⟢ 𝑩 is an 𝑆₂-homomorphism, the very same underlying setoid map is an 𝑆₁-homomorphism reduct Ο† 𝑨 ⟢ reduct Ο† 𝑩. The reason is definitional: reduct Ο† interprets an 𝑆₁-symbol o as the interpretation in 𝑨 of ΞΉ Ο† o precomposed with the ΞΊ Ο† o-reindex, and h already respects every 𝑆₂-operation β€” in particular ΞΉ Ο† o β€” so it respects the reindexed one with no extra work. This is the morphism action F₁ of the functor reductF (Setoid.Categories.Reduct); we restate it directly here because the closure arguments need it between algebras at different universe levels (subalgebra, isomorphism and homomorphic-image relations are all level-heterogeneous), whereas reductF is the single-level packaging.

module _ {𝑆₁ 𝑆₂ : Signature π“ž π“₯} (Ο† : SigMorphism 𝑆₁ 𝑆₂) where
  -- the signature's level bump, pinned to the module's `π“ž`/`π“₯` (no stray implicits).
  private
    ov : Level β†’ Level
    ov β„“ = π“ž βŠ” π“₯ βŠ” lsuc β„“

  reduct-hom : {𝑨 : Algebra {𝑆 = 𝑆₂} Ξ± ρ}{𝑩 : Algebra {𝑆 = 𝑆₂} Ξ² ρᡇ}
    β†’ hom 𝑨 𝑩 β†’ hom (reduct Ο† 𝑨) (reduct Ο† 𝑩)
  reduct-hom (h , hhom) =
    h , mkIsHom (Ξ» {o}{a} β†’ compatible hhom {f = ΞΉ-op Ο† o} {a = a ∘ ΞΊ-ar Ο† o})

The single-level instance agrees with the functor's morphism map definitionally β€” they are the same construction β€” which we record to make the dependence on reductF explicit.

  reduct-hom≑F₁ : {𝑨 𝑩 : Algebra {𝑆 = 𝑆₂} Ξ± ρ}(h : hom 𝑨 𝑩)
    β†’ reduct-hom h ≑ Functor.F₁ (reductF Ο†) h
  reduct-hom≑F₁ _ = refl

Reduct preserves subalgebras, isomorphisms, and homomorphic images

Each of the three relation-preservations is now immediate. reduct-hom keeps the underlying map identical, so injectivity, surjectivity and the isomorphism round-trip conditions β€” all of which are statements about the underlying map and the (unchanged) codomain setoid β€” transfer verbatim. These are the honest content of "reduct Ο† preserves S, P and H": it carries subobjects to subobjects, isomorphisms to isomorphisms, and epis to epis.

  -- reduct preserves the subalgebra relation (S, functorially).
  reduct-≀ : {𝑨 : Algebra {𝑆 = 𝑆₂} Ξ± ρ}{𝑩 : Algebra {𝑆 = 𝑆₂} Ξ² ρᡇ}
   β†’         𝑨 ≀ 𝑩 β†’ reduct Ο† 𝑨 ≀ reduct Ο† 𝑩
  reduct-≀ (h , hinj) = reduct-hom h , hinj

  -- reduct preserves isomorphism.
  reduct-β‰… : {𝑨 : Algebra {𝑆 = 𝑆₂} Ξ± ρ}{𝑩 : Algebra {𝑆 = 𝑆₂} Ξ² ρᡇ}
   β†’         𝑨 β‰… 𝑩 β†’ reduct Ο† 𝑨 β‰… reduct Ο† 𝑩
  reduct-≅ A≅B = mkiso  (reduct-hom (to A≅B)) (reduct-hom (from A≅B))
                        (to∼from Aβ‰…B) (from∼to Aβ‰…B)

  -- reduct preserves the homomorphic-image relation (H, functorially).
  reduct-img : {𝑨 : Algebra {𝑆 = 𝑆₂} Ξ± ρ}{𝑩 : Algebra {𝑆 = 𝑆₂} Ξ² ρᡇ}
   β†’           𝑩 IsHomImageOf 𝑨 β†’ reduct Ο† 𝑩 IsHomImageOf reduct Ο† 𝑨
  reduct-img (h , hsur) = reduct-hom h , hsur

Reduct preserves products

The product preservation is the one that lifts to a genuine class-level closure, so we state it as an isomorphism. The reduct of a product and the product of the reducts have the same carrier (reduct Ο† never touches the domain) and interpret each 𝑆₁-symbol identically: in both, the o-operation acts coordinatewise as ΞΉ Ο† o of the factors, reindexed by ΞΊ Ο† o β€” and reindexing commutes with the coordinate projections. So the two algebras are equal on the nose up to the identity map, and the isomorphism is built from it, with every law holding by the product setoid's reflexivity.

  module _ {I : Type ΞΉ}(π’œ : I β†’ Algebra {𝑆 = 𝑆₂} Ξ± ρ) where

    reduct-β¨… : reduct Ο† (β¨… π’œ) β‰… β¨… (Ξ» i β†’ reduct Ο† (π’œ i))
    reduct-β¨… = mkiso  ( idmap-to    , mkIsHom (Ξ» {o}{a} β†’ Setoid.refl 𝔻[ β¨…R ]) )
                      ( idmap-from  , mkIsHom (Ξ» {o}{a} β†’ Setoid.refl 𝔻[ Rβ¨… ]) )
                      (Ξ» b β†’ Setoid.refl 𝔻[ β¨…R ])
                      (Ξ» a β†’ Setoid.refl 𝔻[ Rβ¨… ])
      where
      Rβ¨… : Algebra {𝑆 = 𝑆₁} (Ξ± βŠ” ΞΉ) (ρ βŠ” ΞΉ)
      Rβ¨… = reduct Ο† (β¨… π’œ)
      β¨…R : Algebra {𝑆 = 𝑆₁} (Ξ± βŠ” ΞΉ) (ρ βŠ” ΞΉ)
      β¨…R = β¨… (Ξ» i β†’ reduct Ο† (π’œ i))
      -- `R⨅` and `⨅R` have definitionally equal domains, so the identity map is a
      -- homomorphism in both directions; its compatibility and the round-trips are refl.
      idmap-to : Func 𝔻[ Rβ¨… ] 𝔻[ β¨…R ]
      idmap-to = record { to = Ξ» x β†’ x ; cong = Ξ» xβ‰ˆy β†’ xβ‰ˆy }
      idmap-from : Func 𝔻[ β¨…R ] 𝔻[ Rβ¨… ]
      idmap-from = record { to = Ξ» x β†’ x ; cong = Ξ» xβ‰ˆy β†’ xβ‰ˆy }

The reduct image and closure under P

The reduct image Reduct[ 𝒲 ] of a class 𝒲 of 𝑆₂-algebras is the class of 𝑆₁-algebras isomorphic to the reduct of some member of 𝒲. Closing under isomorphism (rather than taking the bare set-image) is what makes it a class in the sense the closure operators expect β€” S, H, P all produce iso-closed classes β€” and it is the only honest notion under setoid semantics, where "the same algebra" means "isomorphic".

  Reduct[_] :  Pred (Algebra {𝑆 = 𝑆₂} Ξ³ ρᢜ) β„“
    β†’ Pred (Algebra {𝑆 = 𝑆₁} Ξ² ρᡇ) (ov (Ξ³ βŠ” ρᢜ) βŠ” β„“ βŠ” Ξ² βŠ” ρᡇ)
  Reduct[ 𝒲 ] 𝑩 = Ξ£[ 𝑨 ∈ Algebra _ _ ] (𝑨 ∈ 𝒲) ∧ (𝑩 β‰… reduct Ο† 𝑨)

Reduct[_] is monotone: a bigger source class has a bigger reduct image.

  Reduct-mono :  {𝒲 𝒲' : Pred (Algebra {𝑆 = 𝑆₂} Ξ³ ρᢜ) β„“}{𝑩 : Algebra {𝑆 = 𝑆₁} Ξ² ρᡇ}
    β†’ 𝒲 βŠ† 𝒲' β†’ 𝑩 ∈ Reduct[ 𝒲 ] β†’ 𝑩 ∈ Reduct[ 𝒲' ]
  Reduct-mono π’²βŠ†π’²' (𝑨 , π‘¨βˆˆπ’² , 𝑩≅r) = 𝑨 , π’²βŠ†π’²' π‘¨βˆˆπ’² , 𝑩≅r

Now the class-level product result. The clean, hypothesis-free statement is that the reduct image commutes past P: a product of reduct-images is a reduct-image of a product,

P Reduct[ 𝒱 ]  βŠ†  Reduct[ P 𝒱 ].

The proof assembles the witnessing 𝒱-algebras 𝓐 from the membership data of the factors, takes their product β¨… 𝓐 (a member of P 𝒱 by construction), and chains three isomorphisms: the given 𝑩 β‰… β¨… π’ž, the product of the per-factor isos β¨… π’ž β‰… β¨… (reduct Ο† ∘ 𝓐) (β¨…β‰…), and the product-preservation β¨… (reduct Ο† ∘ 𝓐) β‰… reduct Ο† (β¨… 𝓐) (reduct-β¨…, reversed).

  P-Reduct : {𝒱 : Pred (Algebra {𝑆 = 𝑆₂} Ξ± ρ) (Ξ± βŠ” ρ βŠ” ov β„“)}
    β†’ P {Ξ± = Ξ±}{ρ}{Ξ±}{ρ} (Ξ± βŠ” ρ βŠ” β„“) ΞΉ Reduct[ 𝒱 ] βŠ† Reduct[ P β„“ ΞΉ 𝒱 ]
  P-Reduct {Ξ± = Ξ±} {ρ} {𝒱 = 𝒱} {𝑩} ( I , π’ž , π’žβˆˆR , π‘©β‰…β¨…π’ž ) =
    β¨… 𝓐 , (I , 𝓐 , π“βˆˆπ’± , β‰…-refl) , 𝑩≅red⨅𝓐
    where
    𝓐 : I β†’ Algebra {𝑆 = 𝑆₂} Ξ± ρ
    𝓐 i = proj₁ (π’žβˆˆR i)
    π“βˆˆπ’± : βˆ€ i β†’ 𝓐 i ∈ 𝒱
    π“βˆˆπ’± i = proj₁ (projβ‚‚ (π’žβˆˆR i))
    π’žβ‰…red𝓐 : βˆ€ i β†’ π’ž i β‰… reduct Ο† (𝓐 i)
    π’žβ‰…red𝓐 i = projβ‚‚ (projβ‚‚ (π’žβˆˆR i))
    𝑩≅red⨅𝓐 : 𝑩 β‰… reduct Ο† (β¨… 𝓐)
    𝑩≅red⨅𝓐 = β‰…-trans π‘©β‰…β¨…π’ž (β‰…-trans (β¨…β‰… π’žβ‰…red𝓐) (β‰…-sym (reduct-β¨… 𝓐)))

This is the substance of "reduct Ο† (𝒱) is closed under products". The final step β€” concluding P (Reduct[ 𝒱 ]) βŠ† Reduct[ 𝒱 ] itself when 𝒱 is a variety β€” combines P-Reduct with Reduct-mono and the P-closure of 𝒱: P 𝒱 βŠ† 𝒱; the only remaining gap is the universe-level bump that products introduce (β¨… 𝓐 lands one level up), which the library bridges with Lift-Alg and Level-closure (Setoid.Varieties.Closure) exactly as it does for the HSP theorem. We stop at P-Reduct, the level-clean heart of the matter, in keeping with the bounded, research-tracking scope of this milestone.

Reducts satisfy the pulled-back theory

The genuine grain of truth behind "prevariety" is supplied by reduct-invariance of satisfaction (⊧-reduct, Setoid.Varieties.Invariance). For any family β„° of 𝑆₁-equations, if an 𝑆₂-algebra 𝑨 satisfies every Ο†-translated equation Ο† ✢ s β‰ˆ Ο† ✢ t, then its reduct satisfies the original family. In closure-operator terms this says

reduct Ο† (Mod (Ο† ✢ β„°))  βŠ†  Mod β„°,

so the reduct image of a variety is contained in a variety of 𝑆₁-algebras (the model class of the pulled-back theory). That is the precise, true residue of the prevariety intuition: the reduct class is cut out from a variety by equations β€” it simply need not be all of that variety, nor closed under S.

  module _
    {X : Type Ο‡}{I : Type ΞΉ}
    (β„° : I β†’ Term {𝑆 = 𝑆₁} X ∧ Term {𝑆 = 𝑆₁} X)
    (𝑨 : Algebra {𝑆 = 𝑆₂} Ξ± ρ)
    where
    open EqLogic {𝑆 = 𝑆₁} using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚_β‰ˆ_ )
    open EqLogic {𝑆 = 𝑆₂} using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚‚_β‰ˆ_ )

    reduct-⊧ : (βˆ€ i β†’ 𝑨 βŠ§β‚‚ (Ο† ✢ proj₁ (β„° i)) β‰ˆ Ο† ✢ projβ‚‚ (β„° i))
      β†’ βˆ€ i β†’ reduct Ο† 𝑨 βŠ§β‚ proj₁ (β„° i) β‰ˆ projβ‚‚ (β„° i)
    reduct-⊧ A⊧ i = ⊧-reduct Ο† 𝑨 {s = proj₁ (β„° i)} {t = projβ‚‚ (β„° i)} (A⊧ i)

Why S and H fail at the class level

It remains to substantiate the claim that reduct Ο† 𝒱 is not closed under S (and, in general, not under H), so it is a product class rather than a prevariety. The asymmetry with P is structural: the functorial preservations above all run 𝑆₂ β†’ 𝑆₁ (reduct of a subalgebra is a subalgebra, etc.), but class-level closure needs the reverse, 𝑆₁ β†’ 𝑆₂, reconstruction β€” every 𝑆₁-subalgebra/quotient/product of a reduct must arise as the reduct of an 𝑆₂-subalgebra/quotient/product inside 𝒱.

For products that reconstruction is automatic (reduct-β¨…): the dropped operations on a product are computed coordinatewise from the factors, so they are always present.

For subalgebras and quotients it can fail, because a sub- or quotient-algebra of a reduct generally cannot be re-equipped with the operations Ο† forgot.

Categorically: reduct Ο† is a right adjoint β€” F ⊣ reduct Ο† β€” so it preserves limits, which is why products are the well-behaved case.

Counterexamples

  1. Let 𝑆₂ be the group signature with binary Β·, unary ⁻¹, and nullary e; let 𝑆₁ be the monoid signature with binary Β· and nullary e; let Ο† : 𝑆₁ β†ͺ 𝑆₂ be the natural inclusion; then reduct Ο† forgets ⁻¹ keeping Β· and e. Take 𝒱 to be the variety of groups. Then reduct Ο† 𝒱 is the class of monoid reducts of 𝒱 β€” monoids (M , Β·, e) such that (M , Β·, ⁻¹, e) forms a group.

    • The monoid (β„€ , + , 0) is a reduct of the group (β„€ , + , - , 0), so (β„€ , + , 0) ∈ reduct Ο† 𝒱.
    • As monoids, (β„• , + , 0) ≀ (β„€ , + , 0) β€” β„• is closed under + and the inclusion is an injective monoid homomorphism β€” so (β„• , + , 0) ∈ S (reduct Ο† 𝒱).
    • But (β„• , + , 0) is not a monoid reduct of some group; there is no group whose carrier is β„• and whose binary operation is +, since any nonzero natural number has no additive inverse in β„•, so (β„• , + , 0) βˆ‰ reduct Ο† 𝒱.

    This proves that S (reduct Ο† 𝒱) ⊈ reduct Ο† 𝒱, so reduct Ο† 𝒱 is not closed under S, and therefore is not a prevariety.

    Stated against the operator, the false inclusion is S Reduct[ 𝒱 ] βŠ† Reduct[ S 𝒱 ]; it would require a sub-monoid of a group to be the reduct of a subgroup, which β„• βŠ† β„€ refutes.

  2. Class-level H-closure, H Reduct[ 𝒱 ] βŠ† Reduct[ H 𝒱 ], also fails in general, for the same reconstruction reason: the kernel of a surjective 𝑆₁-homomorphism out of a reduct is an 𝑆₁-congruence, but need not be an 𝑆₂-congruence, so the quotient need not carry the dropped operations. Notably, for the group example above it happens to hold β€” every monoid-congruence of a group is a group-congruence (from a ΞΈ b one derives b⁻¹ ΞΈ a⁻¹ by multiplying on both sides), so a monoid-quotient of a group is again a group-monoid.

In short, reduct Ο† 𝒱 is a product-closed (pseudo-elementary) class, contained in a variety by reduct-⊧, but is not a prevariety.

  1. The closure operators H, S, and P are defined in the Setoid.Varieties.Closure module. ↩

  2. This was indeed what GitHub Issue #345 proposed, prompting this exploration of the reduct functor in a submodule of the Varieties module. ↩