↑ Top

Subalgebras

The Base.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 Overture using (π“ž ; π“₯ ; Signature )

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

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

-- Imports from the Agda Universal Algebra Library ------------------------------------
open  import Overture       using ( ∣_∣ ; βˆ₯_βˆ₯ )
open  import Base.Functions using ( IsInjective )
open  import Base.Equality  using ( swelldef ; is-set ; blk-uip ; pred-ext )

open  import Base.Algebras       {𝑆 = 𝑆} using ( Algebra ; ov )
open  import Base.Terms          {𝑆 = 𝑆} using ( 𝑻 ; Term )
open  import Base.Homomorphisms  {𝑆 = 𝑆} using ( hom ; kercon ; ker[_β‡’_]_β†Ύ_ )
                                         using ( FirstHomTheorem|Set ; _β‰…_ )

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
 field
  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 the 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 Base.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 ∣)
          where

 FirstHomCorollary|Set : (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) IsSubalgebraOf 𝑩
 FirstHomCorollary|Set = Ο•hom , Ο•inj
  where
   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 𝑨 is the 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 ∣)
          where

 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 _
 𝑩 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 𝒦

← Base.Subalgebras.Subuniverses Base.Subalgebras.Properties β†’