Skip to content

Setoid.Subalgebras.Basic

Subalgebras of setoid algebras

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

𝑨 is a subalgebra of 𝑩, written 𝑨 ≀ 𝑩, just in case 𝑨 can be homomorphically embedded in 𝑩: there is a homomorphism from 𝑨 to 𝑩 whose underlying map is injective.

Note that the notion of subalgebra that we define here is different from the standard textbook definition, which defines a subuniverse to be a subset of the carrier of an algebra that is closed under the operations (as we do in the Setoid.Subalgebras.Subuniverses module); a subalgebra is then a subuniverse together with the operations of the larger algebra restricted to it. Nothing in our definition requires the carrier of a subalgebra of 𝑩 to be a subset of the carrier of 𝑩.1

Our subalgebra relation _≀_ is clearly reflexive and transitive, so it is a preorder; that is exactly what Setoid.Subalgebras.Properties proves, as ≀-preorder, and it is the only order-theoretic fact about _≀_ that this subtree establishes.

It is not a partial order. Antisymmetry would require that 𝑨 ≀ 𝑩 and 𝑩 ≀ 𝑨 imply 𝑨 β‰ˆ 𝑩 for some suitable β‰ˆ, and read as "on the nose" equality that plainly fails. The tempting repair is to read β‰ˆ as isomorphism, but that fails too: 𝑨 ≀ 𝑩 and 𝑩 ≀ 𝑨 supply injective homomorphisms in both directions, and a pair of injections is not an isomorphism. Neither map need invert the other, and in general no isomorphism need exist at all β€” the free groups on two and on three generators embed in each other yet are not isomorphic, as their abelianizations β„€Β² and β„€Β³ already show. Extracting a bijection from two injections is Cantor–Bernstein, which is unavailable constructively, and the bijection it yields classically need not be a homomorphism.

For finite algebras the repair does work, and that is the setting much of this library's later work lives in. Mutual injections between finite carriers force equal cardinality; an injective map between finite sets of equal cardinality is surjective; and an injective, surjective homomorphism is an isomorphism, by Bijectiveβ†’β‰… of Setoid.Homomorphisms.Isomorphisms. So on finite algebras _≀_ is antisymmetric up to isomorphism, hence a partial order on isomorphism classes. That chain of reasoning is not formalized here; only Bijectiveβ†’β‰…, its last step, is.

This module defines the subalgebra relation _≀_ and the several ways of packaging it: as a record bundling both algebras, as a Ξ£-type over the smaller algebra with the larger one fixed, and relative to a whole class rather than to a single algebra. The class-relative form _≀c_ is the one the closure operator S of Setoid.Varieties.Closure is built from.

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

module Setoid.Subalgebras.Basic 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 Level                 using ( Level ; _βŠ”_ )
open import Relation.Binary       using ( REL )
open import Relation.Unary        using ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open import Overture              using ( proj₁ ; projβ‚‚ ; Signature ; π“ž ; π“₯ )
open import Setoid.Algebras       using ( Algebra ; ov )
open import Setoid.Functions      using ( IsInjective )
open import Setoid.Homomorphisms  using ( hom ; mon ; mon→intohom ; kerquo ; FirstHomTheorem )

private variable Ξ± ρᡃ Ξ² ρᡇ β„“ : Level

The relation comes in two directions and three packagings.

  • _IsSubalgebraOf_, with the infix alias _≀_, is the relation itself: 𝑨 ≀ 𝑩 is the type of pairs (h , inj) with h : hom 𝑨 𝑩 and inj a proof that the underlying map of h is injective.
  • _IsSupalgebraOf_, aliased _β‰₯_, is the converse, and is definitionally the same type read the other way round: 𝑨 ≀ 𝑩 and 𝑩 β‰₯ 𝑨 both unfold to an injective homomorphism from 𝑨 into 𝑩.
  • mon→≀ turns a monomorphism into a proof of the subalgebra relation. It is immediate, because monβ†’intohom of Setoid.Homomorphisms.Basic already produces exactly this type.
  • SubalgebraOf bundles both algebras and the proof into a single record. Subalgebra instead fixes the larger algebra and collects the smaller one with its embedding, so an inhabitant of Subalgebra 𝑨 is a pair (𝑩 , p) with p : 𝑩 ≀ 𝑨.
module _ {𝑆 : Signature π“ž π“₯} where
  _β‰₯_   -- alias for supalgebra (aka overalgebra)
    _IsSupalgebraOf_ : Algebra {𝑆 = 𝑆} Ξ± ρᡃ β†’ Algebra {𝑆 = 𝑆} Ξ² ρᡇ β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
  𝑨 IsSupalgebraOf 𝑩 = Ξ£[ h ∈ hom 𝑩 𝑨 ] IsInjective (proj₁ h)

  _≀_   -- alias for subalgebra relation
    _IsSubalgebraOf_ : Algebra {𝑆 = 𝑆} Ξ± ρᡃ β†’ Algebra {𝑆 = 𝑆} Ξ² ρᡇ β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
  𝑨 IsSubalgebraOf 𝑩 = Ξ£[ h ∈ hom 𝑨 𝑩 ] IsInjective (proj₁ h)

  -- Syntactic sugar for sup/sub-algebra relations.
  𝑨 β‰₯ 𝑩 = 𝑨 IsSupalgebraOf 𝑩
  𝑨 ≀ 𝑩 = 𝑨 IsSubalgebraOf 𝑩

  mon→≀ : {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}{𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ} β†’ mon 𝑨 𝑩 β†’ 𝑨 ≀ 𝑩
  mon→≀ {𝑨 = 𝑨}{𝑩} x = monβ†’intohom 𝑨 𝑩 x

  record SubalgebraOf : Type (ov {𝑆 = 𝑆} (Ξ± βŠ” Ξ² βŠ” ρᡃ βŠ” ρᡇ)) where
    field
      algebra : Algebra {𝑆 = 𝑆} Ξ± ρᡃ
      subalgebra : Algebra {𝑆 = 𝑆} Ξ² ρᡇ
      issubalgebra : subalgebra ≀ algebra

  Subalgebra : Algebra {𝑆 = 𝑆} Ξ± ρᡃ β†’ {Ξ² ρᡇ : Level} β†’ Type _
  Subalgebra 𝑨 {Ξ²}{ρᡇ} = Ξ£[ 𝑩 ∈ (Algebra Ξ² ρᡇ) ] 𝑩 ≀ 𝑨

{- usage note: for 𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ, an inhabitant of `Subalgebra 𝑨` is a pair
   `(𝑩 , p) : Subalgebra 𝑨`  providing
   - `𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ` and
   - `p : 𝑩 ≀ 𝑨`, a proof that 𝑩 is a subalgebra of 𝐴. -}

From now on we will use 𝑩 ≀ 𝑨 to express the assertion that 𝑩 is a subalgebra of 𝑨.

Subalgebras of classes of setoid algebras

Suppose 𝒦 : Pred (Algebra Ξ± 𝑆) Ξ³ denotes a class of 𝑆-algebras and 𝑩 : Algebra Ξ² ρᡇ denotes an arbitrary 𝑆-algebra. Consider the assertion that 𝑩 is a subalgebra of an algebra in the class 𝒦. With the next definition we can express this assertion as 𝑩 IsSubalgebraOfClass 𝒦.

  _≀c_
    _IsSubalgebraOfClass_ : Algebra {𝑆 = 𝑆} Ξ² ρᡇ β†’ Pred (Algebra {𝑆 = 𝑆} Ξ± ρᡃ) β„“ β†’ Type _
  𝑩 IsSubalgebraOfClass 𝒦 = Ξ£[ 𝑨 ∈ Algebra _ _ ] ((𝑨 ∈ 𝒦) ∧ (𝑩 ≀ 𝑨))

  𝑩 ≀c 𝒦 = 𝑩 IsSubalgebraOfClass 𝒦  -- (alias)

  record SubalgebraOfClass : Type (ov {𝑆 = 𝑆} (Ξ± βŠ” Ξ² βŠ” ρᡃ βŠ” ρᡇ βŠ” β„“)) where
    field
      class : Pred (Algebra {𝑆 = 𝑆} Ξ± ρᡃ) β„“
      subalgebra : Algebra {𝑆 = 𝑆} Ξ² ρᡇ
      issubalgebraofclass : subalgebra ≀c class

  record SubalgebraOfClass' : Type (ov {𝑆 = 𝑆} (Ξ± βŠ” Ξ² βŠ” ρᡃ βŠ” ρᡇ βŠ” β„“)) where
    field
      class : Pred (Algebra {𝑆 = 𝑆} Ξ± ρᡃ) β„“
      classalgebra : Algebra {𝑆 = 𝑆} Ξ± ρᡃ
      isclassalgebra : classalgebra ∈ class
      subalgebra : Algebra {𝑆 = 𝑆} Ξ² ρᡇ
      issubalgebra : subalgebra ≀ classalgebra

  -- The collection of subalgebras of algebras in class 𝒦.
  SubalgebrasOfClass : Pred (Algebra {𝑆 = 𝑆} Ξ± ρᡃ) β„“ β†’ {Ξ² ρᡇ : Level} β†’ Type _
  SubalgebrasOfClass 𝒦 {Ξ²}{ρᡇ} = Ξ£[ 𝑩 ∈ Algebra Ξ² ρᡇ ] 𝑩 ≀c 𝒦

Consequences of First Homomorphism Theorem

As an example use-case of the IsSubalgebraOf type defined above, we prove the following easy but useful corollary of the First Homomorphism Theorem (proved in the Setoid.Homomorphisms.Noether module): If 𝑨 and 𝑩 are 𝑆-algebras and h : hom 𝑨 𝑩 a homomorphism from 𝑨 to 𝑩, then the quotient 𝑨 β•± ker h is (isomorphic to) a subalgebra of 𝑩.

  FirstHomCorollary : {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ} {𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ}
    (hh : hom 𝑨 𝑩) β†’ (kerquo hh) IsSubalgebraOf 𝑩
  FirstHomCorollary hh = proj₁ (FirstHomTheorem hh) , projβ‚‚ (projβ‚‚ (FirstHomTheorem hh))

  1. Note that we denote both the subalgebra and subuniverse relations by the same symbol, _≀_. The two do not collide, because the subuniverse order lives inside the named module Sublattice of Setoid.Subalgebras.CompleteLattice, which qualifies it rather than exporting it. So importing the Setoid.Subalgebras barrel gives the subalgebra relation unqualified, and the subuniverse order becomes available as _≀_ only where Sublattice is opened, as in open Sublattice 𝑨 β„“β‚€. ↩