---
layout: default
title : "Setoid.Subalgebras.Basic module (The Agda Universal Algebra Library)"
date : "2021-07-17"
author: "agda-algebras development team"
---

#### 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 `_≀_`{.AgdaFunction} is clearly reflexive and transitive,
so it is a *preorder*; that is exactly what [Setoid.Subalgebras.Properties][]
proves, as `≀-preorder`{.AgdaFunction}, and it is the only order-theoretic fact
about `_≀_`{.AgdaFunction} 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→≅`{.AgdaFunction} of [Setoid.Homomorphisms.Isomorphisms][].  So on
finite algebras `_≀_`{.AgdaFunction} is antisymmetric up to isomorphism, hence a
partial order on isomorphism classes.  That chain of reasoning is *not* formalized
here; only `Bijective→≅`{.AgdaFunction}, its last step, is.

This module defines the subalgebra relation `_≀_`{.AgdaFunction} 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_`{.AgdaFunction} is the
one the closure operator `S`{.AgdaFunction} of [Setoid.Varieties.Closure][] is
built from.

<!--
```agda
{-# 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_`{.AgdaFunction}, with the infix alias `_≀_`{.AgdaFunction},
   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_`{.AgdaFunction}, aliased `_β‰₯_`{.AgdaFunction}, is the
   converse, and is *definitionally* the same type read the other way round:
   `𝑨 ≀ 𝑩` and `𝑩 β‰₯ 𝑨` both unfold to an injective homomorphism from `𝑨` into
   `𝑩`.
+  `mon→≀`{.AgdaFunction} turns a monomorphism into a proof of the subalgebra
   relation.  It is immediate, because `mon→intohom`{.AgdaFunction} of
   [Setoid.Homomorphisms.Basic][] already produces exactly this type.
+  `SubalgebraOf`{.AgdaRecord} bundles both algebras and the proof into a single
   record.  `Subalgebra`{.AgdaFunction} instead fixes the larger algebra and
   collects the smaller one with its embedding, so an inhabitant of
   `Subalgebra 𝑨` is a pair `(𝑩 , p)` with `p : 𝑩 ≀ 𝑨`.

```agda
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 𝒦`.

```agda
  _≀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 `𝑩`.

```agda
  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, `_≀_`{.AgdaFunction}.  The two do not collide, because the
      subuniverse order lives inside the named module `Sublattice`{.AgdaModule} 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 `_≀_`{.AgdaFunction} only where `Sublattice`{.AgdaModule} is opened, as in
      `open Sublattice 𝑨 β„“β‚€`.