Setoid.Homomorphisms.Basic

Homomorphisms of Algebras over Setoids

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

A homomorphism from 𝑨 to 𝑩 is a setoid function h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ] between the domains of the two algebras that is compatible with every basic operation: for each operation symbol f and each tuple a of arguments, h ⟨$⟩ (f ^ 𝑨) a and (f ^ 𝑩) λ x → h ⟨$⟩ a x are related by the equality of 𝑩.

Two things distinguish this from an ordinary type-based definition, where compatibility is an identification h ((f ^ 𝑨) a) ≡ (f ^ 𝑩) (h ∘ a).

1. The map is a setoid function, so it carries its own congruence proof and cannot fail to send equal arguments to equal results.
2. Compatibility is asserted up to the equality of the codomain, not up to propositional equality; that is what lets 𝑩 be a quotient algebra (the same carrier under a coarser equivalence) with no special quotient type and no appeal to extensionality.

This module defines the compatibility predicates, the homomorphism type hom and its predicate form IsHom, the injective and surjective variants (monomorphisms and epimorphisms) in both of those forms, the translations between them, and the identity homomorphism 𝒾𝒹. Everything else the library proves about homomorphisms is built on these, including the following:

• composition, ⊙-hom, and the homomorphisms that witness universe lifting in Setoid.Homomorphisms.Properties;
• the kernel of a homomorphism as a congruence, and the quotient it determines in Setoid.Homomorphisms.Kernels;
• isomorphism, _≅_, given by a pair of mutually inverse homomorphisms in Setoid.Homomorphisms.Isomorphisms;
• the first homomorphism theorem in Setoid.Homomorphisms.Noether;
• factoring one homomorphism through another in Setoid.Homomorphisms.Factor.

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

module Setoid.Homomorphisms.Basic  where

-- Imports from Agda and the Agda Standard Library ------------------------------
open import Agda.Primitive           using () renaming ( Set to Type )
open import Data.Product             using ( _,_ ; Σ ; Σ-syntax ; proj₁ ; proj₂ )
open import Function.Bundles         using () renaming ( Func to _⟶_ )
open import Level                    using ( Level ; _⊔_ )
open import Relation.Binary          using ( Setoid )
open import Relation.Binary.PropositionalEquality using ( refl )

-- Imports from the Agda Universal Algebra Library ---------------------------
open import Overture                 using ( OperationSymbolsOf ; 𝓞 ; 𝓥 ; Signature )
open import Setoid.Functions         using ( IsInjective ; IsSurjective ; 𝑖𝑑 )
open import Setoid.Algebras          using ( Algebra ; _^_ ; 𝔻[_])

private variable
  α β ρᵃ ρᵇ : Level

The homomorphism type is built in four steps. compatible-map-op says that a setoid function h commutes with one operation symbol f; compatible-map quantifies that over all operation symbols; IsHom packages the resulting property as a record with the single field compatible and the constructor mkIsHom; and hom is the type of homomorphisms proper. An inhabitant of hom 𝑨 𝑩 is therefore a pair (h , p): a setoid function h from the domain of 𝑨 to that of 𝑩, together with a proof that h is compatible.

mkhom is the smart constructor for that pair, so a caller who has h and a compatible-map proof never has to write the Σ-pair and the IsHom record by hand.

module _ {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ)(𝑩 : Algebra β ρᵇ) where
  open _⟶_ {a = α}{ρᵃ}{β}{ρᵇ}{From = 𝔻[ 𝑨 ]}{To = 𝔻[ 𝑩 ]} renaming (to to _⟨$⟩_ )

  compatible-map-op : (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) → OperationSymbolsOf 𝑆 → Type (𝓥 ⊔ α ⊔ ρᵇ)
  compatible-map-op h f =  ∀ {a} → h ⟨$⟩ (f ^ 𝑨) a ≈₂ (f ^ 𝑩) λ x → h ⟨$⟩ a x
    where open Setoid 𝔻[ 𝑩 ] using() renaming ( _≈_ to _≈₂_ )

  compatible-map : (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵇ)
  compatible-map h = ∀ {f} → compatible-map-op h f

  -- The property of being a homomorphism.
  record IsHom (h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ ρᵇ) where
    constructor mkIsHom
    field compatible : compatible-map h

  hom : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ β ⊔ ρᵇ)
  hom = Σ (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) IsHom

  -- Smart constructor for a homomorphism: bundle a setoid map with its
  -- compatibility proof, hiding the Σ / IsHom plumbing.
  mkhom : (h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) → compatible-map h → hom
  mkhom h c = h , mkIsHom c

Monomorphisms and epimorphisms

A monomorphism is an injective homomorphism and an epimorphism is a surjective one. Each comes in the two forms hom does:

• the predicates IsMon and IsEpi, whose fields pair the homomorphism property with IsInjective or IsSurjective;
• the bundled types mon and epi, which pair a setoid function with such a proof.

Both predicates export a HomReduct that forgets the extra condition, and mon→hom and epi→hom apply it to the bundled forms.

mon→intohom and epi→ontohom regroup the same data the other way, as a hom paired with the injectivity or the surjectivity of its underlying map. That regrouping earns a name because the two resulting types are, by definition, _IsSubalgebraOf_ of Setoid.Subalgebras.Basic and _IsHomImageOf_ of Setoid.Homomorphisms.HomomorphicImages; so these are the functions that turn a monomorphism into a subalgebra and an epimorphism into a homomorphic image.

  record IsMon (h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ β ⊔ ρᵇ) where
    field
      isHom : IsHom h
      isInjective : IsInjective h

    HomReduct : hom
    HomReduct = h , isHom

  mon : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ β ⊔ ρᵇ)
  mon = Σ (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) IsMon

  mon→hom : mon → hom
  mon→hom h = IsMon.HomReduct (proj₂ h)

  record IsEpi (h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ β ⊔ ρᵇ) where
    field
      isHom : IsHom h
      isSurjective : IsSurjective h

    HomReduct : hom
    HomReduct = h , isHom

  epi : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ β ⊔ ρᵇ)
  epi = Σ (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) IsEpi

  epi→hom : epi → hom
  epi→hom h = IsEpi.HomReduct (proj₂ h)

module _ {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ)(𝑩 : Algebra β ρᵇ) where
  open IsEpi
  open IsMon

  mon→intohom : mon 𝑨 𝑩 → Σ[ h ∈ hom 𝑨 𝑩 ] IsInjective (proj₁ h)
  mon→intohom (hh , hhM) = (hh , isHom hhM) , isInjective hhM

  epi→ontohom : epi 𝑨 𝑩 → Σ[ h ∈ hom 𝑨 𝑩 ] IsSurjective (proj₁ h)
  epi→ontohom (hh , hhE) = (hh , isHom hhE) , isSurjective hhE

Finally, we define the identity homomorphism for setoid algebras.

module _ {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} where
  open Setoid 𝔻[ 𝑨 ]   using ( reflexive )

  𝒾𝒹 :  hom 𝑨 𝑨
  𝒾𝒹 = 𝑖𝑑 , mkIsHom (reflexive refl)