↑ Top


Homomorphisms of Algebras over Setoids

This is the Setoid.Homomorphisms.Basic module of the Agda Universal Algebra Library.

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

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

module Setoid.Homomorphisms.Basic {𝑆 : 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 )
open import Function.Bundles  using () renaming ( Func to _⟢_ )
open import Level             using ( Level ; _βŠ”_ )
open import Relation.Binary   using ( Setoid )

-- Imports from the Agda Universal Algebra Library ---------------------------
open import Overture          using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Setoid.Functions  using ( IsInjective ; IsSurjective )

open import Setoid.Algebras {𝑆 = 𝑆} using ( Algebra ; _Μ‚_ )

private variable Ξ± Ξ² ρᡃ ρᡇ : Level

module _ (𝑨 : Algebra Ξ± ρᡃ)(𝑩 : Algebra Ξ² ρᡇ) where
 open Algebra 𝑨  using() renaming (Domain to A )
 open Algebra 𝑩  using() renaming (Domain to B )
 open Setoid A   using() renaming ( _β‰ˆ_ to _β‰ˆβ‚_ )
 open Setoid B   using() renaming ( _β‰ˆ_ to _β‰ˆβ‚‚_ )

 open _⟢_ {a = Ξ±}{ρᡃ}{Ξ²}{ρᡇ}{From = A}{To = B} renaming (f to _⟨$⟩_ )

 compatible-map-op : (A ⟢ B) β†’ ∣ 𝑆 ∣ β†’ Type (π“₯ βŠ” Ξ± βŠ” ρᡇ)
 compatible-map-op h f =  βˆ€ {a}
  β†’                       h ⟨$⟩ (f Μ‚ 𝑨) a β‰ˆβ‚‚ (f Μ‚ 𝑩) Ξ» x β†’ h ⟨$⟩ (a x)

 compatible-map : (A ⟢ B) β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡇ)
 compatible-map h = βˆ€ {f} β†’ compatible-map-op h f

 -- The property of being a homomorphism.
 record IsHom (h : A ⟢ B) : Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” ρᡇ) where
  field compatible : compatible-map h

 hom : Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 hom = Σ (A ⟢ B) IsHom

Monomorphisms and epimorphisms

 record IsMon (h : A ⟢ B) : Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ) where
  field
   isHom : IsHom h
   isInjective : IsInjective h

  HomReduct : hom
  HomReduct = h , isHom

 mon : Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 mon = Σ (A ⟢ B) IsMon

 mon→hom : mon → hom
 monβ†’hom h = IsMon.HomReduct βˆ₯ h βˆ₯

 record IsEpi (h : A ⟢ B) : Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ) where
  field
   isHom : IsHom h
   isSurjective : IsSurjective h

  HomReduct : hom
  HomReduct = h , isHom

 epi : Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ βŠ” Ξ² βŠ” ρᡇ)
 epi = Σ (A ⟢ B) IsEpi

 epi→hom : epi → hom
 epiβ†’hom h = IsEpi.HomReduct βˆ₯ h βˆ₯

module _ (𝑨 : Algebra Ξ± ρᡃ)(𝑩 : Algebra Ξ² ρᡇ) where
 open IsEpi
 open IsMon

 monβ†’intohom : mon 𝑨 𝑩 β†’ Ξ£[ h ∈ hom 𝑨 𝑩 ] IsInjective ∣ h ∣
 mon→intohom (hh , hhM) = (hh , isHom hhM) , isInjective hhM

 epiβ†’ontohom : epi 𝑨 𝑩 β†’ Ξ£[ h ∈ hom 𝑨 𝑩 ] IsSurjective ∣ h ∣
 epi→ontohom (hh , hhE) = (hh , isHom hhE) , isSurjective hhE

↑ Setoid.Homomorphisms Setoid.Homomorphisms.Properties β†’