Skip to content

Setoid.Subalgebras.Subdirect

Subdirect products

This is the Setoid.Subalgebras.Subdirect module of the Agda Universal Algebra Library.

A subdirect product of a family of algebras is a subalgebra of their product that projects onto every factor. The surjective-projections condition is what makes the notion useful: an arbitrary subalgebra of a product may ignore some coordinates entirely, whereas a subdirect product retains information about each one. Subdirect decompositions are how a single algebra is analysed into simpler pieces, and the pieces that cannot be decomposed further are the subdirectly irreducible algebras.

This is a barrel module, re-exporting the following:

  • Setoid.Subalgebras.Subdirect.Basic: coord for the coordinate homomorphisms of a map into a product, SubdirectEmbedding and subdirect→≤, and the bridge from a Separates family of congruences to a subdirect embedding via the natural map natmap;
  • Setoid.Subalgebras.Subdirect.Irreducible: the structural characterisation, relating injectivity of a coordinate map to its kernel lying BelowDiagonal, and embed→separates;
  • Setoid.Subalgebras.Subdirect.BirkhoffSI: the two statements SubdirectlyRepresentable and SubdirectSIRep, the implication SIRep→Representable from the second to the first, and Birkhoff-subdirect. That last is Birkhoff's subdirect representation theorem relative to a choice principle: it takes a module parameter supplying an SI-representation for every algebra, because producing one for an arbitrary algebra is a Zorn's-lemma step and so is not available postulate-free. What that module proves outright is the choice-free core;
  • Setoid.Subalgebras.Subdirect.Finite: the same theorem made unconditional for finite algebras. finiteSubdirectSIRep constructs the SI-representation by search, with no choice and no postulate, and finite-Birkhoff feeds it to the choice-free core. "Finite" has to be pinned down with some care, and that module opens by doing so.
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Subalgebras.Subdirect where

open import Setoid.Subalgebras.Subdirect.Basic public
open import Setoid.Subalgebras.Subdirect.BirkhoffSI public
open import Setoid.Subalgebras.Subdirect.Finite public
open import Setoid.Subalgebras.Subdirect.Irreducible public