↑ Top

Subalgebras of setoid algebras

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


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

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.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 ( _Γ—_ to _∧_ ; projβ‚‚ to snd )
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 ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Setoid.Functions  using ( IsInjective )

open import Setoid.Algebras       {𝑆 = 𝑆} using ( Algebra ; ov )
open import Setoid.Homomorphisms  {𝑆 = 𝑆} using
 ( hom ; mon ; mon→intohom ; kerquo ; FirstHomTheorem )

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

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

_≀_  -- (alias for subalgebra relation))
 _IsSubalgebraOf_ : Algebra Ξ± ρᡃ β†’ Algebra Ξ² ρᡇ β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
𝑨 IsSubalgebraOf 𝑩 = Ξ£[ h ∈ hom 𝑨 𝑩 ] IsInjective ∣ 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 Ξ± ρᡃ, inhabitant of `Subalgebra 𝑨` is a pair
               `(𝑩 , p) : Subalgebra 𝑨`  providing
                                         - `𝑩 : Algebra Ξ² ρᡇ` and
                                         - `p : 𝑩 ≀ 𝑨`, a proof that 𝑩 is a subalgebra of 𝐴. -}

IsSubalgebraREL : {Ξ± ρᡃ Ξ² ρᡇ : Level} β†’ REL (Algebra Ξ± ρᡃ)(Algebra Ξ² ρᡇ) β„“ β†’ Type _
IsSubalgebraREL {Ξ±}{ρᡃ}{Ξ²}{ρᡇ} R = βˆ€ {𝑨 : Algebra Ξ± ρᡃ}{𝑩 : Algebra Ξ² ρᡇ} β†’ 𝑨 ≀ 𝑩

record SubalgebraREL(R : REL (Algebra Ξ² ρᡇ)(Algebra Ξ± ρᡃ) β„“) : Type (ov (Ξ± βŠ” Ξ² βŠ” ρᡇ βŠ” β„“))
 where
 field isSubalgebraREL : IsSubalgebraREL R

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


_≀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 = ∣ FirstHomTheorem hh ∣ , snd βˆ₯ FirstHomTheorem hh βˆ₯

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