Agda UALib ↑

Subalgebras

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

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

open import Subalgebras.Subuniverses {𝑆 = 𝑆} public
open import MGS-Embeddings using (∘-embedding; id-is-embedding) public

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.1


_IsSubalgebraOf_ : {𝓦 𝓀 : Universe}(𝑩 : Algebra 𝓦 𝑆)(𝑨 : Algebra 𝓀 𝑆) β†’ π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
𝑩 IsSubalgebraOf 𝑨 = Ξ£ h κž‰ hom 𝑩 𝑨 , is-embedding ∣ h ∣

Subalgebra : {𝓦 𝓀 : Universe} β†’ Algebra 𝓀 𝑆 β†’ ov 𝓦 βŠ” 𝓀 Μ‡
Subalgebra {𝓦} 𝑨 = Ξ£ 𝑩 κž‰ (Algebra 𝓦 𝑆) , 𝑩 IsSubalgebraOf 𝑨

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.


-- open Congruence

module _ {𝓀 𝓦 : Universe}(𝑨 : Algebra 𝓀 𝑆)(𝑩 : Algebra 𝓦 𝑆)(h : hom 𝑨 𝑩)
         -- extensionality assumptions:
         (pe : pred-ext 𝓀 𝓦)(fe : dfunext π“₯ 𝓦)

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

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

  Ο•emb : is-embedding ∣ Ο•hom ∣
  Ο•emb = βˆ₯ 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 _ {𝓀 𝓦 𝓧 : Universe}(X : 𝓧 Μ‡)(𝑩 : Algebra 𝓦 𝑆)(h : hom (𝑻 X) 𝑩)
        -- extensionality assumptions:
         (pe : pred-ext (ov 𝓧) 𝓦)(fe : dfunext π“₯ 𝓦)

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

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

Notation. For convenience, we define the following shorthand for the subalgebra relation.


_≀_ : {𝓦 𝓀 : Universe} β†’ Algebra 𝓦 𝑆 β†’ Algebra 𝓀 𝑆 β†’ π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
𝑩 ≀ 𝑨 = 𝑩 IsSubalgebraOf 𝑨

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

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 𝓀 Μ‡ as predicates over the Algebra 𝓀 𝑆 type. In the syntax of the UALib, 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 _ {𝓦 𝓀 𝓩 : Universe} where

 _IsSubalgebraOfClass_ : Algebra 𝓦 𝑆 β†’ Pred (Algebra 𝓀 𝑆) 𝓩 β†’ 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 : {𝓦 𝓀 : Universe} β†’ Pred (Algebra 𝓀 𝑆)(ov 𝓀) β†’ ov (𝓀 βŠ” 𝓦) Μ‡
SubalgebraOfClass {𝓦} 𝒦 = Ξ£ 𝑩 κž‰ Algebra 𝓦 𝑆 , 𝑩 IsSubalgebraOfClass 𝒦

Subalgebra lemmas

We conclude this module by proving a number of useful facts about subalgebras. Some of the formal statements below may appear to be redundant, and indeed they are to some extent. However, each one differs slightly from the next, if only with respect to the explicitness or implicitness of their arguments. The aim is to make it as convenient as possible to apply the lemmas in different situations. (We’re in the UALib utility closet now; elegance is not the priority.)

First we show that the subalgebra relation is a preorder; i.e., it is a reflexive, transitive binary relation.2


≀-reflexive : (𝑨 : Algebra 𝓀 𝑆) β†’ 𝑨 ≀ 𝑨
≀-reflexive 𝑨 = (𝑖𝑑 ∣ 𝑨 ∣ , Ξ» 𝑓 π‘Ž β†’ refl) , id-is-embedding

≀-refl : {𝑨 : Algebra 𝓀 𝑆} β†’ 𝑨 ≀ 𝑨
≀-refl {𝑨 = 𝑨} = ≀-reflexive 𝑨


≀-transitivity : (𝑨 : Algebra 𝓧 𝑆)(𝑩 : Algebra 𝓨 𝑆)(π‘ͺ : Algebra 𝓩 𝑆)
 β†’               π‘ͺ ≀ 𝑩 β†’ 𝑩 ≀ 𝑨 β†’ π‘ͺ ≀ 𝑨

≀-transitivity 𝑨 𝑩 π‘ͺ CB BA = (∘-hom π‘ͺ 𝑨 ∣ CB ∣ ∣ BA ∣) , ∘-embedding βˆ₯ BA βˆ₯ βˆ₯ CB βˆ₯

≀-trans : (𝑨 : Algebra 𝓧 𝑆){𝑩 : Algebra 𝓨 𝑆}{π‘ͺ : Algebra 𝓩 𝑆} β†’ π‘ͺ ≀ 𝑩 β†’ 𝑩 ≀ 𝑨 β†’ π‘ͺ ≀ 𝑨
≀-trans 𝑨 {𝑩}{π‘ͺ} = ≀-transitivity 𝑨 𝑩 π‘ͺ

Next we prove that if two algebras are isomorphic and one of them is a subalgebra of 𝑨, then so is the other.


≀-iso : (𝑨 : Algebra 𝓧 𝑆){𝑩 : Algebra 𝓨 𝑆}{π‘ͺ : Algebra 𝓩 𝑆}
 β†’      π‘ͺ β‰… 𝑩 β†’ 𝑩 ≀ 𝑨 β†’ π‘ͺ ≀ 𝑨

≀-iso 𝑨 {𝑩} {π‘ͺ} CB BA = (g ∘ f , gfhom) , gfemb
 where
  f : ∣ π‘ͺ ∣ β†’ ∣ 𝑩 ∣
  f = fst ∣ CB ∣
  g : ∣ 𝑩 ∣ β†’ ∣ 𝑨 ∣
  g = fst ∣ BA ∣

  gfemb : is-embedding (g ∘ f)
  gfemb = ∘-embedding (βˆ₯ BA βˆ₯) (isoβ†’embedding CB)

  gfhom : is-homomorphism π‘ͺ 𝑨 (g ∘ f)
  gfhom = ∘-is-hom π‘ͺ 𝑨 {f}{g} (snd ∣ CB ∣) (snd ∣ BA ∣)


≀-trans-β‰… : (𝑨 : Algebra 𝓧 𝑆){𝑩 : Algebra 𝓨 𝑆}(π‘ͺ : Algebra 𝓩 𝑆)
 β†’          𝑨 ≀ 𝑩 β†’ 𝑨 β‰… π‘ͺ β†’ π‘ͺ ≀ 𝑩

≀-trans-β‰… 𝑨 {𝑩} π‘ͺ A≀B Bβ‰…C = ≀-iso 𝑩 (β‰…-sym Bβ‰…C) A≀B -- 𝑨 π‘ͺ A≀B (sym-β‰… Bβ‰…C)


≀-TRANS-β‰… : (𝑨 : Algebra 𝓧 𝑆){𝑩 : Algebra 𝓨 𝑆}(π‘ͺ : Algebra 𝓩 𝑆)
 β†’          𝑨 ≀ 𝑩 β†’ 𝑩 β‰… π‘ͺ β†’ 𝑨 ≀ π‘ͺ

≀-TRANS-β‰… 𝑨 π‘ͺ A≀B Bβ‰…C = (∘-hom 𝑨 π‘ͺ ∣ A≀B ∣ ∣ Bβ‰…C ∣) , ∘-embedding (isoβ†’embedding Bβ‰…C)(βˆ₯ A≀B βˆ₯)


≀-mono : (𝑩 : Algebra 𝓦 𝑆){𝒦 𝒦' : Pred (Algebra 𝓀 𝑆) 𝓩}
 β†’       𝒦 βŠ† 𝒦' β†’ 𝑩 IsSubalgebraOfClass 𝒦 β†’ 𝑩 IsSubalgebraOfClass 𝒦'

≀-mono 𝑩 KK' KB = ∣ KB ∣ , fst βˆ₯ KB βˆ₯ , KK' (∣ snd βˆ₯ KB βˆ₯ ∣) , βˆ₯ (snd βˆ₯ KB βˆ₯) βˆ₯

Lifts of subalgebras


module _ {𝒦 : Pred (Algebra 𝓀 𝑆)(ov 𝓀)}{𝑩 : Algebra 𝓀 𝑆} where

 Lift-is-sub : 𝑩 IsSubalgebraOfClass 𝒦 β†’ (Lift-alg 𝑩 𝓀) IsSubalgebraOfClass 𝒦
 Lift-is-sub (𝑨 , (sa , (KA , Bβ‰…sa))) = 𝑨 , sa , KA , β‰…-trans (β‰…-sym Lift-β‰…) Bβ‰…sa


Lift-≀ : (𝑨 : Algebra 𝓧 𝑆){𝑩 : Algebra 𝓨 𝑆}{𝓩 : Universe} β†’ 𝑩 ≀ 𝑨 β†’ Lift-alg 𝑩 𝓩 ≀ 𝑨
Lift-≀ 𝑨 B≀A = ≀-iso 𝑨 (β‰…-sym Lift-β‰…) B≀A

≀-Lift : (𝑨 : Algebra 𝓧 𝑆){𝓩 : Universe}{𝑩 : Algebra 𝓨 𝑆} β†’ 𝑩 ≀ 𝑨 β†’ 𝑩 ≀ Lift-alg 𝑨 𝓩
≀-Lift 𝑨 {𝓩} {𝑩} B≀A = ≀-TRANS-β‰… 𝑩 {𝑨} (Lift-alg 𝑨 𝓩) B≀A Lift-β‰…


module _ {𝓧 𝓨 𝓩 𝓦 : Universe} where

 Lift-≀-Lift : {𝑨 : Algebra 𝓧 𝑆}(𝑩 : Algebra 𝓨 𝑆) β†’ 𝑨 ≀ 𝑩 β†’ Lift-alg 𝑨 𝓩 ≀ Lift-alg 𝑩 𝓦
 Lift-≀-Lift {𝑨} 𝑩 A≀B = ≀-trans (Lift-alg 𝑩 𝓦) (≀-trans 𝑩 lAA A≀B) B≀lB
   where

   lAA : (Lift-alg 𝑨 𝓩) ≀ 𝑨
   lAA = Lift-≀ 𝑨 {𝑨} ≀-refl

   B≀lB : 𝑩 ≀ Lift-alg 𝑩 𝓦
   B≀lB = ≀-Lift 𝑩 ≀-refl

1 An alternative which could end up being simpler and easier to work with would be to proclaim that 𝑩 is a subalgebra of 𝑨 iff there is a monic homomorphism from 𝐡 into 𝑨. In preparation for the next major release of the UALib, we will investigate the consequences of taking that path instead of the stricter embedding requirement we chose for the definition of the type IsSubalgebraOf.

2 Recall, in the Relations.Quotients module, we defined preorder for binary relation types. Here, however, we will content ourselves with merely proving reflexivity and transitivity of the subalgebra relation _≀_, without worry about first defining it as an inhabitant of an honest-to-goodness binary relation type, of the sort introduced in the Relations.Discrete module. Perhaps we will address this matter in a future release of the UALib.



← Subalgebras.Subuniverses Subalgebras.Univalent β†’