Skip to content

Legacy.Base.Structures.Homs

Homomorphisms of General Structures

This is the Legacy.Base.Structures.Homs module of the Agda Universal Algebra Library.


{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.Structures.Homs where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -------------------------------------------
open import Axiom.Extensionality.Propositional
                             using () renaming (Extensionality to funext)
open import Data.Product     using ( _Γ—_ ; Ξ£-syntax ; _,_ )
                             renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Function.Base    using ( _∘_ ; id )
open import Level            using ( _βŠ”_ ; suc ; Level ; Lift ; lift ) renaming ( 0β„“ to β„“β‚€ )
open import Relation.Binary  using ( IsEquivalence )
open import Relation.Binary.PropositionalEquality
                             using ( _≑_ ; refl ; sym ; cong ; module ≑-Reasoning ; trans )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture              using ( _βˆ™_ ; ∣_∣ ; βˆ₯_βˆ₯ ; _⁻¹ ; Ξ -syntax )
open import Legacy.Base.Functions        using ( Image_βˆ‹_ ; IsSurjective ; IsInjective )
open import Legacy.Base.Relations        using ( ker ; kerlift ; βŸͺ_⟫ ; mkblk )
open import Legacy.Base.Equality         using ( swelldef )

open import Examples.Structures.Signatures  using ( Sβˆ… )

open import Legacy.Base.Structures.Basic  using ( signature ; structure ; Lift-Struc )
                                   using ( Lift-StrucΚ³ ; Lift-StrucΛ‘ )
                                   using ( compatible ; siglΚ³ ; sigl )

open import Legacy.Base.Structures.Congruences  using ( con ; _β•±_)
open import Legacy.Base.Structures.Products     using ( β¨… )
open structure ; open signature

private variable
 π“žβ‚€ π“₯β‚€ π“žβ‚ π“₯₁ : Level
 𝐹 : signature π“žβ‚€ π“₯β‚€
 𝑅 : signature π“žβ‚ π“₯₁
 Ξ± ρᡃ Ξ² ρᡇ Ξ³ ρᢜ β„“ : Level

module _ (𝑨 : structure 𝐹 𝑅 {Ξ±}{ρᡃ}) (𝑩 : structure 𝐹 𝑅 {Ξ²}{ρᡇ}) where
 private
  A = carrier 𝑨
  B = carrier 𝑩

 preserves : (symbol 𝑅) β†’ (A β†’ B) β†’ Type (siglΚ³ 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” ρᡇ)
 preserves π‘Ÿ h = βˆ€ a β†’ ((rel 𝑨) π‘Ÿ a) β†’ ((rel 𝑩) π‘Ÿ) (h ∘ a)

 is-hom-rel : (A β†’ B) β†’ Type (sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” ρᡇ)
 is-hom-rel h = βˆ€ (r : symbol 𝑅) β†’ preserves r h

 comm-op : (A β†’ B) β†’ (symbol 𝐹) β†’ Type (siglΚ³ 𝐹 βŠ” Ξ± βŠ” Ξ²)
 comm-op h f = βˆ€ a β†’ h (((op 𝑨) f) a) ≑ ((op 𝑩) f) (h ∘ a)

 is-hom-op : (A β†’ B) β†’ Type (sigl 𝐹 βŠ” Ξ± βŠ” Ξ²)
 is-hom-op h = βˆ€ f β†’ comm-op h f

 is-hom : (A β†’ B) β†’ Type (sigl 𝐹 βŠ” sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 is-hom h = is-hom-rel h Γ— is-hom-op h

 -- homomorphism
 hom : Type (sigl 𝐹 βŠ” sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 hom = Ξ£[ h ∈ (A β†’ B) ] is-hom h

-- endomorphism
end : structure 𝐹 𝑅 {Ξ±}{ρᡃ} β†’ Type (sigl 𝐹 βŠ” sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ)
end 𝑨 = hom 𝑨 𝑨

module _  {𝑨 : structure 𝐹 𝑅 {Ξ±}{ρᡃ}}
          {𝑩 : structure 𝐹 𝑅 {Ξ²}{ρᡇ}}
          {π‘ͺ : structure 𝐹 𝑅 {Ξ³}{ρᢜ}} where

 private A = carrier 𝑨 ; B = carrier 𝑩 ; C = carrier π‘ͺ

 ∘-is-hom-rel :  (f : A β†’ B)(g : B β†’ C)
  β†’              is-hom-rel 𝑨 𝑩 f β†’ is-hom-rel 𝑩 π‘ͺ g β†’ is-hom-rel 𝑨 π‘ͺ (g ∘ f)
 ∘-is-hom-rel f g fhr ghr R a = Ξ» z β†’ ghr R (Ξ» z₁ β†’ f (a z₁)) (fhr R a z)

 ∘-is-hom-op :  (f : A β†’ B)(g : B β†’ C)
  β†’             is-hom-op 𝑨 𝑩 f β†’ is-hom-op 𝑩 π‘ͺ g β†’ is-hom-op 𝑨 π‘ͺ (g ∘ f)
 ∘-is-hom-op f g fho gho 𝑓 a = cong g (fho 𝑓 a) βˆ™ gho 𝑓 (f ∘ a)

 ∘-is-hom :  (f : A β†’ B)(g : B β†’ C)
  β†’          is-hom 𝑨 𝑩 f β†’ is-hom 𝑩 π‘ͺ g β†’ is-hom 𝑨 π‘ͺ (g ∘ f)
 ∘-is-hom f g fhro ghro = ihr , iho
  where
  ihr : is-hom-rel 𝑨 π‘ͺ (g ∘ f)
  ihr = ∘-is-hom-rel f g ∣ fhro ∣ ∣ ghro ∣

  iho : is-hom-op 𝑨 π‘ͺ (g ∘ f)
  iho = ∘-is-hom-op f g βˆ₯ fhro βˆ₯ βˆ₯ ghro βˆ₯

 ∘-hom : hom 𝑨 𝑩 β†’ hom 𝑩 π‘ͺ β†’ hom 𝑨 π‘ͺ
 ∘-hom (f , fh) (g , gh) = g ∘ f , ∘-is-hom f g fh gh


𝒾𝒹 : {𝑨 : structure 𝐹 𝑅 {Ξ±}{ρᡃ}} β†’ end 𝑨
𝒾𝒹 = id , (Ξ» _ _ z β†’ z)  , (Ξ» _ _ β†’ refl)


module _ {𝑨 : structure 𝐹 𝑅 {Ξ±}{ρᡃ}} {𝑩 : structure 𝐹 𝑅  {Ξ²}{ρᡇ}} where

 private A = carrier 𝑨 ; B = carrier 𝑩

 is-mon : (A β†’ B) β†’ Type (sigl 𝐹 βŠ” sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 is-mon g = is-hom 𝑨 𝑩 g Γ— IsInjective g

 mon : Type (sigl 𝐹 βŠ” sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 mon = Ξ£[ g ∈ (A β†’ B) ] is-mon g

 monβ†’hom : mon β†’ hom 𝑨 𝑩
 monβ†’hom Ο• = ∣ Ο• ∣ , fst βˆ₯ Ο• βˆ₯

 is-epi : (A β†’ B) β†’ Type (sigl 𝐹 βŠ” sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 is-epi g = is-hom 𝑨 𝑩 g Γ— IsSurjective g

 epi : Type (sigl 𝐹 βŠ” sigl 𝑅 βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 epi = Ξ£[ g ∈ (A β†’ B) ] is-epi g

 epiβ†’hom : epi β†’ hom 𝑨 𝑩
 epiβ†’hom Ο• = ∣ Ο• ∣ , fst βˆ₯ Ο• βˆ₯

open Lift

𝓁𝒾𝒻𝓉ˑ : {β„“ : Level}{𝑨 : structure 𝐹 𝑅  {Ξ±}{ρᡃ}} β†’ hom 𝑨 (Lift-StrucΛ‘ β„“ 𝑨)
𝓁𝒾𝒻𝓉ˑ = lift , (Ξ» _ _ x β†’ x) , Ξ» _ _ β†’ refl

𝓁𝒾𝒻𝓉ʳ : {ρ : Level}{𝑨 : structure 𝐹 𝑅  {Ξ±}{ρᡃ}} β†’ hom 𝑨 (Lift-StrucΚ³ ρ 𝑨)
𝓁𝒾𝒻𝓉ʳ = id , (Ξ» _ _ x β†’ lift x) , Ξ» _ _ β†’ refl

𝓁𝒾𝒻𝓉 : {β„“Λ‘ β„“Κ³ : Level}{𝑨 : structure 𝐹 𝑅  {Ξ±}{ρᡃ}} β†’ hom 𝑨 (Lift-Struc β„“Λ‘ β„“Κ³ 𝑨)
𝓁𝒾𝒻𝓉 = lift , ((Ξ» _ _ x β†’ lift x) , Ξ» _ _ β†’ refl)

π“β„΄π“Œβ„―π“‡Λ‘ : {β„“ : Level}{𝑨 : structure 𝐹 𝑅 {Ξ±}{ρᡃ}} β†’ hom (Lift-StrucΛ‘ β„“ 𝑨) 𝑨
π“β„΄π“Œβ„―π“‡Λ‘ = lower , (Ξ» _ _ x β†’ x) , (Ξ» _ _ β†’ refl)

π“β„΄π“Œβ„―π“‡Κ³ : {ρ : Level}{𝑨 : structure 𝐹 𝑅 {Ξ±}{ρᡃ}} β†’ hom (Lift-StrucΚ³ ρ 𝑨) 𝑨
π“β„΄π“Œβ„―π“‡Κ³ = id , ((Ξ» _ _ x β†’ lower x) , Ξ» _ _ β†’ refl)

π“β„΄π“Œβ„―π“‡ : {β„“Λ‘ β„“Κ³ : Level}{𝑨 : structure 𝐹 𝑅  {Ξ±}{ρᡃ}} β†’ hom (Lift-Struc β„“Λ‘ β„“Κ³ 𝑨) 𝑨
π“β„΄π“Œβ„―π“‡ = lower , (Ξ» _ _ x β†’ lower x) , (Ξ» _ _ β†’ refl)

Kernels of homomorphisms


open ≑-Reasoning
module _ {𝑨 : structure 𝐹 𝑅  {Ξ±}{Ξ² βŠ” ρᡃ}}{𝑩 : structure 𝐹 𝑅 {Ξ²} {ρᡇ}} where

 homker-comp :  (h : hom 𝑨 𝑩){wd : swelldef (siglΚ³ 𝐹) Ξ²}
  β†’             compatible 𝑨 (ker ∣ h ∣)

 homker-comp (h , hhom) {wd} f {u}{v} kuv =
  h (((op 𝑨)f) u)    β‰‘βŸ¨ βˆ₯ hhom βˆ₯ f u ⟩
  ((op 𝑩) f)(h ∘ u)  β‰‘βŸ¨ wd ((op 𝑩)f) (h ∘ u) (h ∘ v) kuv ⟩
  ((op 𝑩) f)(h ∘ v)  β‰‘βŸ¨ (βˆ₯ hhom βˆ₯ f v)⁻¹ ⟩
  h (((op 𝑨)f) v)    ∎

 kerlift-comp :  (h : hom 𝑨 𝑩){wd : swelldef (siglΚ³ 𝐹) Ξ²}
  β†’              compatible 𝑨 (kerlift ∣ h ∣ (Ξ± βŠ” ρᡃ) )

 kerlift-comp (h , hhom) {wd} f {u}{v} kuv = lift goal
  where
  goal : h (op 𝑨 f u) ≑ h (op 𝑨 f v)
  goal =  h (op 𝑨 f u)     β‰‘βŸ¨ βˆ₯ hhom βˆ₯ f u ⟩
          (op 𝑩 f)(h ∘ u)  β‰‘βŸ¨ wd (op 𝑩 f)(h ∘ u)(h ∘ v)(lower ∘ kuv) ⟩
          (op 𝑩 f)(h ∘ v)  β‰‘βŸ¨ (βˆ₯ hhom βˆ₯ f v ) ⁻¹ ⟩
          h (op 𝑨 f v)     ∎


 kercon : hom 𝑨 𝑩 β†’ {wd : swelldef (siglΚ³ 𝐹) Ξ²} β†’ con 𝑨
 kercon (h , hhom) {wd} =  ((Ξ» x y β†’ Lift (Ξ± βŠ” ρᡃ) (h x ≑ h y)) , goal)
                           , kerlift-comp (h , hhom) {wd}
  where
  goal : IsEquivalence (Ξ» x y β†’ Lift (Ξ± βŠ” ρᡃ) (h x ≑ h y))
  goal = record  { refl = lift refl
                 ; sym = Ξ» p β†’ lift (sym (lower p))
                 ; trans = Ξ» p q β†’ lift (trans (lower p)(lower q))
                 }

 kerquo :  hom 𝑨 𝑩 β†’ {wd : swelldef (siglΚ³ 𝐹) Ξ²}
  β†’        structure 𝐹 𝑅 {suc (Ξ± βŠ” Ξ² βŠ” ρᡃ)} {Ξ² βŠ” ρᡃ}

 kerquo h {wd} = 𝑨 β•± (kercon h {wd})

ker[_β‡’_] :  (𝑨 : structure 𝐹 𝑅 {Ξ±} {Ξ² βŠ” ρᡃ} )(𝑩 : structure 𝐹 𝑅 {Ξ²}{ρᡇ} )
 β†’          hom 𝑨 𝑩 β†’ {wd : swelldef (siglΚ³ 𝐹) Ξ²} β†’ structure 𝐹 𝑅

ker[_β‡’_] {ρᡃ = ρᡃ} 𝑨 𝑩 h {wd} = kerquo{ρᡃ = ρᡃ}{𝑨 = 𝑨}{𝑩} h {wd}

Canonical projections


module _ {𝑨 : structure 𝐹 𝑅 {Ξ±}{ρᡃ} } where

 open Image_βˆ‹_

 Ο€epi : (ΞΈ : con 𝑨) β†’ epi {𝑨 = 𝑨}{𝑩 = 𝑨 β•± ΞΈ}
 Ο€epi ΞΈ = (Ξ» a β†’ βŸͺ a ⟫ {fst ∣ ΞΈ ∣}) , (Ξ³rel , (Ξ» _ _ β†’ refl)) , cΟ€-is-epic
  where
  Ξ³rel : is-hom-rel 𝑨 (𝑨 β•± ΞΈ) (Ξ» a β†’ βŸͺ a ⟫ {fst ∣ ΞΈ ∣})
  Ξ³rel R a x = x
  cΟ€-is-epic : IsSurjective (Ξ» a β†’ βŸͺ a ⟫ {fst ∣ ΞΈ ∣})
  cΟ€-is-epic (C , mkblk a refl) = eq a refl

 Ο€hom : (ΞΈ : con 𝑨) β†’ hom 𝑨 (𝑨 β•± ΞΈ)
 Ο€hom ΞΈ = epiβ†’hom {𝑨 = 𝑨} {𝑩 = (𝑨 β•± ΞΈ)} (Ο€epi ΞΈ)

module _ {𝑨 : structure 𝐹 𝑅  {Ξ±}{Ξ² βŠ” ρᡃ}}{𝑩 : structure 𝐹 𝑅 {Ξ²} {ρᡇ}} where

 Ο€ker :  (h : hom 𝑨 𝑩){wd : swelldef (siglΚ³ 𝐹) Ξ²}
  β†’      epi {𝑨 = 𝑨} {𝑩 = (ker[_β‡’_]{ρᡃ = ρᡃ} 𝑨 𝑩 h {wd})}

 Ο€ker h {wd} = Ο€epi (kercon{ρᡃ = ρᡃ} {𝑨 = 𝑨}{𝑩 = 𝑩} h {wd})


module _ {I : Type β„“} where

  module _  {𝑨 : structure 𝐹 𝑅  {Ξ±}{ρᡃ}}{ℬ : I β†’ structure 𝐹 𝑅  {Ξ²}{ρᡇ}} where

   β¨…-hom-co : funext β„“ Ξ² β†’ (βˆ€(i : I) β†’ hom 𝑨 (ℬ i)) β†’ hom 𝑨 (β¨… ℬ)
   β¨…-hom-co fe h =  (Ξ» a i β†’ ∣ h i ∣ a)
                    , (Ξ» R a x 𝔦 β†’ fst βˆ₯ h 𝔦 βˆ₯ R a x)
                    , Ξ» f a β†’ fe (Ξ» i β†’ snd βˆ₯ h i βˆ₯ f a)

  module _  {π’œ : I β†’ structure 𝐹 𝑅 {Ξ±}{ρᡃ}}
            {ℬ : I β†’ structure 𝐹 𝑅  {Ξ²}{ρᡇ}} where

   β¨…-hom : funext β„“ Ξ² β†’ Ξ [ i ∈ I ] hom (π’œ i)(ℬ i) β†’ hom (β¨… π’œ)(β¨… ℬ)
   β¨…-hom fe h =  (Ξ» a i β†’ ∣ h i ∣ (a i))
                 , (Ξ» R a x 𝔦 β†’ fst βˆ₯ h 𝔦 βˆ₯ R (Ξ» z β†’ a z 𝔦) (x 𝔦))
                 , Ξ» f a β†’ fe (Ξ» i β†’ snd βˆ₯ h i βˆ₯ f Ξ» z β†’ a z i)

  -- Projection out of products
  module _ {π’œ : I β†’ structure 𝐹 𝑅 {Ξ±}{ρᡃ}} where
   β¨…-projection-hom : Ξ [ i ∈ I ] hom (β¨… π’œ) (π’œ i)
   β¨…-projection-hom = Ξ» x β†’ (Ξ» z β†’ z x) , (Ξ» R a z β†’ z x)  , Ξ» f a β†’ refl

-- The special case when 𝑅 = βˆ… (i.e., purely algebraic structures)
module _ {𝑨 : structure 𝐹 Sβˆ… {Ξ±}{β„“β‚€}} {𝑩 : structure 𝐹 Sβˆ… {Ξ²}{β„“β‚€}} where

 -- The type of homomorphisms from one algebraic structure to another.
 hom-alg : Type (sigl 𝐹 βŠ” Ξ± βŠ” Ξ²)
 hom-alg = Ξ£[ h ∈ ((carrier 𝑨) β†’ (carrier 𝑩)) ] is-hom-op 𝑨 𝑩 h