↑ Top


Homomorphisms of General Structures

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

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

module Structures.Homs where

-- Imports from Agda and the Agda Standard Library -------------------------------------------
open import Agda.Primitive  using ( _⊔_ ; lsuc ) renaming ( lzero to ℓ₀ ; Set to Type )
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 ( Level ; Lift ; lift ; lower )
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.Preliminaries using ( _∙_ ; ∣_∣ ; ∥_∥ ; _⁻¹ ; Π-syntax )
open import Overture.Inverses      using ( Image_∋_ )
open import Overture.Surjective    using ( IsSurjective )
open import Overture.Injective     using ( IsInjective )
open import Relations.Discrete     using ( ker ; kerlift )
open import Relations.Quotients    using ( ⟪_⟫ ; mkblk )
open import Equality.Welldefined   using ( swelldef )
open import Structures.Basic       using ( signature ; structure ; Lift-Struc ; Lift-Strucʳ
                                         ; Lift-Strucˡ ; compatible ; siglʳ ; sigl )
open import Examples.Structures.Signatures
                                   using ( S∅ )
open import Structures.Congruences using ( con ; _╱_)
open import 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 𝐹 𝑅 {lsuc (α  β  ρᵃ)} {β  ρᵃ}
 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


← Structures.Congruences Structures.Isos →