↑ Top


Properties of the Subalgebra Inclusion Relation

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

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

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

-- Imports from Agda and the Agda Standard Library -------------------------------
open import Data.Product     using ( _,_ ) renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Function         using ( _∘_ ; id ; flip ; Injection )
open import Level            using ( Level; _βŠ”_ )
open import Relation.Unary   using ( Pred ; _βŠ†_ )
open import Relation.Binary  using ( _RespectsΚ³_ ; _RespectsΛ‘_ )

open  import Relation.Binary.PropositionalEquality as ≑
      using ( _≑_ ; module ≑-Reasoning )

-- Imports from the Agda Universal Algebra Library --------------------
open  import Overture        using ( ∣_∣ ; βˆ₯_βˆ₯ ; _⁻¹ )
open  import Base.Functions  using ( id-is-injective ; IsInjective ; ∘-injective )

open  import Base.Algebras       {𝑆 = 𝑆}  using ( Algebra ; Lift-Alg ; ov )
open  import Base.Homomorphisms  {𝑆 = 𝑆}  using ( is-homomorphism ; ∘-hom )
                                          using ( ∘-is-hom ; _β‰…_ ; β‰…toInjective )
                                          using ( β‰…fromInjective ; β‰…-refl ; β‰…-sym )
                                          using ( β‰…-trans ; Lift-β‰… ; mkiso )
open  import Base.Subalgebras.Subalgebras
                                 {𝑆 = 𝑆}  using  ( _≀_ ; _β‰₯_ ; _IsSubalgebraOfClass_ )

private variable Ξ± Ξ² Ξ³ 𝓧 : Level

-- The subalgebra relation is a *preorder* (a reflexive, transitive, binary relation).

open _β‰…_

≀-refl : {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra Ξ² 𝑆} β†’ 𝑨 β‰… 𝑩 β†’ 𝑨 ≀ 𝑩
≀-refl Ο† = (to Ο†) , β‰…toInjective Ο†

β‰₯-refl : {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra Ξ² 𝑆} β†’ 𝑨 β‰… 𝑩 β†’ 𝑨 β‰₯ 𝑩
β‰₯-refl Ο† = (from Ο†) , β‰…fromInjective Ο†

≀-reflexive : (𝑨 : Algebra Ξ± 𝑆) β†’ 𝑨 ≀ 𝑨
≀-reflexive 𝑨 = (id , Ξ» 𝑓 π‘Ž β†’ ≑.refl) , Injection.injective id-is-injective

≀-trans :  (𝑨 : Algebra Ξ± 𝑆){𝑩 : Algebra Ξ² 𝑆}(π‘ͺ : Algebra Ξ³ 𝑆)
 β†’         𝑨 ≀ 𝑩 β†’ 𝑩 ≀ π‘ͺ β†’ 𝑨 ≀ π‘ͺ

≀-trans 𝑨 π‘ͺ A≀B B≀C = (∘-hom 𝑨 π‘ͺ ∣ A≀B ∣ ∣ B≀C ∣) , ∘-injective βˆ₯ A≀B βˆ₯ βˆ₯ B≀C βˆ₯


β‰₯-trans :  (𝑨 : Algebra Ξ± 𝑆){𝑩 : Algebra Ξ² 𝑆}(π‘ͺ : Algebra Ξ³ 𝑆)
 β†’         𝑨 β‰₯ 𝑩 β†’ 𝑩 β‰₯ π‘ͺ β†’ 𝑨 β‰₯ π‘ͺ

β‰₯-trans 𝑨 π‘ͺ Aβ‰₯B Bβ‰₯C = ≀-trans π‘ͺ 𝑨 Bβ‰₯C Aβ‰₯B

Relations between ≀, β‰₯, and β‰…

In case all algebras live in the same universe level, we can use some of the definitions in the standard library. However, to obtain more general versions, we need to either extend the standard library’s Binary.Structures module to be universe polymorphic, or just implement what we need here. For now we do the latter (below).

module _ {Ξ± : Level} where

 open import Relation.Binary.Structures {a = (ov Ξ±)}{β„“ = (π“ž βŠ” π“₯ βŠ” Ξ±)} (_β‰…_ {Ξ±}{Ξ±})

 open IsPreorder

 ≀-preorder : IsPreorder _≀_
 isEquivalence ≀-preorder = record { refl = β‰…-refl ; sym = β‰…-sym ; trans = β‰…-trans }
 reflexive ≀-preorder = ≀-refl
 trans ≀-preorder {𝑨}{𝑩}{π‘ͺ} A≀B B≀C = ≀-trans 𝑨 π‘ͺ A≀B B≀C

 β‰₯-preorder : IsPreorder _β‰₯_
 isEquivalence β‰₯-preorder = record { refl = β‰…-refl ; sym = β‰…-sym ; trans = β‰…-trans }
 reflexive β‰₯-preorder = β‰₯-refl
 trans β‰₯-preorder {𝑨}{𝑩}{π‘ͺ} Aβ‰₯B Bβ‰₯C = β‰₯-trans 𝑨 π‘ͺ Aβ‰₯B Bβ‰₯C

Here are some consequences of the fact that _≀_ and _β‰₯_ are preorders relative to _β‰…_. These are essentially equivalent variations on the following obvious fact: If two algebras are isomorphic and one of them is a subalgebra, then so is the other.

 -- 1a. If 𝑨 ≀ 𝑩  and  𝑩 β‰… π‘ͺ, then  𝑨 ≀ π‘ͺ
 ≀-resp-β‰… : _≀_ RespectsΚ³ _β‰…_     -- usage: (note the argument order)
 ≀-resp-β‰… = ∼-respΛ‘-β‰ˆ β‰₯-preorder  -- (p : 𝑩 β‰… π‘ͺ) (q : 𝑨 ≀ 𝑩) β†’ (≀-resp-β‰… p q) : 𝑨 ≀ π‘ͺ

 -- 2a. If 𝑨 β‰₯ 𝑩  and  𝑩 β‰… π‘ͺ,   then 𝑨 β‰₯ π‘ͺ
 β‰₯-resp-β‰… : _β‰₯_ RespectsΚ³ _β‰…_
 β‰₯-resp-β‰… {𝑨} = ∼-respΛ‘-β‰ˆ ≀-preorder {𝑨}

 -- 1b. If 𝑩 β‰… π‘ͺ   and 𝑩 β‰₯ 𝑨, then  π‘ͺ β‰₯ 𝑨
 β‰…-resp-β‰₯ : _β‰₯_ RespectsΛ‘ _β‰…_
 β‰…-resp-β‰₯ = ≀-resp-β‰…

 -- 2b. If 𝑩 β‰… π‘ͺ  and 𝑩 ≀ 𝑨, then  π‘ͺ ≀ 𝑨
 β‰…-resp-≀ : _≀_ RespectsΛ‘ _β‰…_
 β‰…-resp-≀ {𝑨} = β‰₯-resp-β‰… {𝑨}

Relations between ≀, β‰₯, and β‰… (universe-polymorphic versions)

module _ {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra Ξ² 𝑆}{π‘ͺ : Algebra Ξ³ 𝑆} where
 ≀-RESP-β‰… : 𝑨 ≀ 𝑩 β†’ 𝑩 β‰… π‘ͺ β†’ 𝑨 ≀ π‘ͺ
 ≀-RESP-β‰… a<b bc = ≀-trans 𝑨 π‘ͺ a<b (≀-refl bc)

 β‰₯-RESP-β‰… : 𝑨 β‰₯ 𝑩 β†’ 𝑩 β‰… π‘ͺ β†’ 𝑨 β‰₯ π‘ͺ
 β‰₯-RESP-β‰… a<b ac = ≀-trans π‘ͺ 𝑨 (≀-refl (β‰…-sym ac)) a<b

module _ {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra Ξ² 𝑆}{π‘ͺ : Algebra Ξ³ 𝑆} where

 β‰…-RESP-≀ : 𝑨 β‰… 𝑩 β†’ 𝑩 ≀ π‘ͺ β†’ 𝑨 ≀ π‘ͺ
 β‰…-RESP-≀ ab b<c = β‰₯-RESP-β‰…{𝑨 = π‘ͺ} b<c (β‰…-sym ab)

 β‰…-RESP-β‰₯ : 𝑨 β‰… 𝑩 β†’ 𝑩 β‰₯ π‘ͺ β†’ 𝑨 β‰₯ π‘ͺ
 β‰…-RESP-β‰₯ ab b<c = ≀-RESP-β‰… b<c (β‰…-sym ab)


open ≑-Reasoning
isoβ†’injective :  {𝑨 : Algebra Ξ± 𝑆}{𝑩 : Algebra Ξ² 𝑆}
 β†’               (Ο† : 𝑨 β‰… 𝑩) β†’ IsInjective ∣ to Ο† ∣

isoβ†’injective {𝑨 = 𝑨} (mkiso f g f∼g g∼f) {x} {y} fxfy =
 x                  β‰‘βŸ¨ (g∼f x)⁻¹ ⟩
 (∣ g ∣ ∘ ∣ f ∣) x  β‰‘βŸ¨ ≑.cong ∣ g ∣ fxfy ⟩
 (∣ g ∣ ∘ ∣ f ∣) y  β‰‘βŸ¨ g∼f y ⟩
 y                  ∎

≀-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 Ξ² 𝑆){β„“ : Level} β†’ 𝑨 ≀ 𝑩 β†’ 𝑨 ≀ Lift-Alg 𝑩 β„“
≀-Lift 𝑩 a<b = ≀-RESP-β‰…{𝑩 = 𝑩} a<b Lift-β‰…

β‰₯-Lift : (𝑨 : Algebra Ξ± 𝑆){𝑩 : Algebra Ξ² 𝑆}{β„“ : Level} β†’ 𝑨 β‰₯ 𝑩 β†’ 𝑨 β‰₯ Lift-Alg 𝑩 β„“
β‰₯-Lift 𝑨 a>b = β‰₯-RESP-β‰…{𝑨 = 𝑨} a>b Lift-β‰…

Lift-≀-Lift :  {𝑨 : Algebra Ξ± 𝑆}(ℓᡃ : Level){𝑩 : Algebra Ξ² 𝑆}(ℓᡇ : Level)
 β†’             𝑨 ≀ 𝑩 β†’ Lift-Alg 𝑨 ℓᡃ ≀ Lift-Alg 𝑩 ℓᡇ

Lift-≀-Lift ℓᡃ {𝑩} ℓᡇ a<b = β‰₯-Lift (Lift-Alg 𝑩 ℓᡇ) (≀-Lift 𝑩 a<b)

← Base.Subalgebras.Subalgebras Base.Varieties β†’