↑ Top


The Subalgebras.Subalgebras module of the Agda Universal Algebra Library defines the Subalgebra type, representing the subalgebra of a given algebra, as well as the collection of all subalgebras of a given class of algebras.

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

open import Algebras.Basic using (π“ž ; π“₯ ; Signature )

module Subalgebras.Subalgebras {𝑆 : Signature π“ž π“₯} where

-- imports from Agda and the Agda Standard Library ------------------------------------
open import Agda.Primitive   using ( _βŠ”_ ; lsuc ; Level ) renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Ξ£-syntax ; _Γ—_ ) renaming ( projβ‚‚ to snd )
open import Relation.Unary   using ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library ------------------------------------
open import Overture.Preliminaries             using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Overture.Injective                 using ( IsInjective )
open import Equality.Welldefined               using ( swelldef )
open import Equality.Truncation                using ( is-set ; blk-uip )
open import Equality.Extensionality            using ( pred-ext )
open import Algebras.Basic                     using ( Algebra )
open import Algebras.Products          {𝑆 = 𝑆} using ( ov )
open import Homomorphisms.Basic        {𝑆 = 𝑆} using ( hom )
open import Homomorphisms.Kernels      {𝑆 = 𝑆} using ( kercon ; ker[_β‡’_]_β†Ύ_ )
open import Homomorphisms.Noether      {𝑆 = 𝑆} using ( FirstHomTheorem|Set )
open import Homomorphisms.Isomorphisms {𝑆 = 𝑆} using ( _β‰…_ )
open import Terms.Basic                {𝑆 = 𝑆} using ( 𝑻 ; Term )
private variable Ξ± Ξ² Ξ³ 𝓧 : Level

Subalgebra type

Given algebras 𝑨 : Algebra Ξ± 𝑆 and 𝑩 : Algebra 𝓦 𝑆, we say that 𝑩 is a subalgebra of 𝑨 just in case 𝑩 can be homomorphically embedded in 𝑨; that is, there exists a map h : ∣ 𝑩 ∣ β†’ ∣ 𝑨 ∣ that is both a homomorphism and an embedding.

_≀_  -- (alias for subalgebra relation))
 _IsSubalgebraOf_ : Algebra Ξ± 𝑆 β†’ Algebra Ξ² 𝑆 β†’ Type _
𝑨 IsSubalgebraOf 𝑩 = Ξ£[ h ∈ hom 𝑨 𝑩 ] IsInjective ∣ h ∣

_β‰₯_  -- (alias for supalgebra (aka overalgebra))
 _IsSupalgebraOf_ : Algebra Ξ± 𝑆 β†’ Algebra Ξ² 𝑆 β†’ Type _
𝑨 IsSupalgebraOf 𝑩 = Ξ£[ h ∈ hom 𝑩 𝑨 ] IsInjective ∣ h ∣

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

-- From now on we use `𝑨 ≀ 𝑩` to express the assertion that `𝑨` is a subalgebra of `𝑩`.
record SubalgebraOf : Type (ov (Ξ± βŠ” Ξ²)) where
  algebra : Algebra Ξ± 𝑆
  subalgebra : Algebra Ξ² 𝑆
  issubalgebra : subalgebra ≀ algebra

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

Note the order of the arguments. The universe Ξ² comes first because in certain situations we must explicitly specify this universe, whereas we can almost always leave the universe Ξ± implicit. (See, for example, the definition of _IsSubalgebraOfClass_ below.)

Consequences of First Homomorphism Theorem

We take this opportunity to prove an important lemma that makes use of the IsSubalgebraOf type defined above. It is the following: If 𝑨 and 𝑩 are 𝑆-algebras and h : hom 𝑨 𝑩 a homomorphism from 𝑨 to 𝑩, then the quotient 𝑨 β•± ker h is (isomorphic to) a subalgebra of 𝑩. This is an easy corollary of the First Homomorphism Theorem proved in the Homomorphisms.Noether module.

module _ (𝑨 : Algebra Ξ± 𝑆)(𝑩 : Algebra Ξ² 𝑆)(h : hom 𝑨 𝑩)
         -- extensionality assumptions:
         (pe : pred-ext Ξ± Ξ²)(fe : swelldef π“₯ Ξ²)

         -- truncation assumptions:
         (Bset : is-set ∣ 𝑩 ∣)
         (buip : blk-uip ∣ 𝑨 ∣ ∣ kercon fe {𝑩} h ∣)

 FirstHomCorollary|Set : (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) IsSubalgebraOf 𝑩
 FirstHomCorollary|Set = Ο•hom , Ο•inj
   hh = FirstHomTheorem|Set 𝑨 𝑩 h pe fe Bset buip
   Ο•hom : hom (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩
   Ο•hom = ∣ hh ∣

   Ο•inj : IsInjective ∣ Ο•hom ∣
   Ο•inj = ∣ snd βˆ₯ hh βˆ₯ ∣

If we apply the foregoing theorem to the special case in which the 𝑨 is term algebra 𝑻 X, we obtain the following result which will be useful later.

module _ (X : Type 𝓧)(𝑩 : Algebra Ξ² 𝑆)(h : hom (𝑻 X) 𝑩)
         -- extensionality assumptions:
         (pe : pred-ext (ov 𝓧) Ξ²)(fe : swelldef π“₯ Ξ²)

         -- truncation assumptions:
         (Bset : is-set ∣ 𝑩 ∣)
         (buip : blk-uip (Term X) ∣ kercon fe {𝑩} h ∣)

 free-quot-subalg : (ker[ 𝑻 X β‡’ 𝑩 ] h β†Ύ fe) IsSubalgebraOf 𝑩
 free-quot-subalg = FirstHomCorollary|Set{Ξ± = ov 𝓧}(𝑻 X) 𝑩 h pe fe Bset buip

Subalgebras of a class

One of our goals is to formally express and prove properties of classes of algebraic structures. Fixing a signature 𝑆 and a universe Ξ±, we represent classes of 𝑆-algebras with domains of type Type Ξ± as predicates over the Algebra Ξ± 𝑆 type. In the syntax of the agda-algebras library, such predicates inhabit the type Pred (Algebra Ξ± 𝑆) Ξ³, for some universe Ξ³.

Suppose 𝒦 : Pred (Algebra Ξ± 𝑆) Ξ³ denotes a class of 𝑆-algebras and 𝑩 : Algebra Ξ² 𝑆 denotes an arbitrary 𝑆-algebra. Then we might wish to consider the assertion that 𝑩 is a subalgebra of an algebra in the class 𝒦. The next type we define allows us to express this assertion as 𝑩 IsSubalgebraOfClass 𝒦.

module _ {Ξ± Ξ² : Level} where

 _IsSubalgebraOfClass_ : Algebra Ξ² 𝑆 β†’ Pred (Algebra Ξ± 𝑆) Ξ³ β†’ Type (Ξ³ βŠ” ov (Ξ± βŠ” Ξ²))
 𝑩 IsSubalgebraOfClass 𝒦 = Ξ£[ 𝑨 ∈ Algebra Ξ± 𝑆 ] Ξ£[ sa ∈ Subalgebra 𝑨 {Ξ²} ] ((𝑨 ∈ 𝒦) Γ— (𝑩 β‰… ∣ sa ∣))

Using this type, we express the collection of all subalgebras of algebras in a class by the type SubalgebraOfClass, which we now define.

 SubalgebraOfClass : Pred (Algebra Ξ± 𝑆)(ov Ξ±) β†’ Type (ov (Ξ± βŠ” Ξ²))
 SubalgebraOfClass 𝒦 = Ξ£[ 𝑩 ∈ Algebra Ξ² 𝑆 ] 𝑩 IsSubalgebraOfClass 𝒦

← Subalgebras.Subuniverses Subalgebras.Properties β†’