↑ 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 Base.Algebras.Basic using (π“ž ; π“₯ ; Signature )

module Setoid.Homomorphisms.Basic {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library ------------------------------
open import Agda.Primitive    using ( _βŠ”_ ; Level )  renaming ( Set to Type )
open import Data.Product      using ( _,_ ; Ξ£ ; Ξ£-syntax )
open import Function.Bundles  using ()               renaming ( Func to _⟢_ )
open import Relation.Binary   using ( Setoid )

-- Imports from the Agda Universal Algebra Library ---------------------------
open import Base.Overture.Preliminaries    using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Setoid.Overture.Injective      using ( IsInjective )
open import Setoid.Overture.Surjective     using ( IsSurjective )
open import Setoid.Algebras.Basic {𝑆 = 𝑆}  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 β†’