Setoid.Homomorphisms.Properties

Properties of Homomorphisms of Algebras

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

This module collects some of the facts that follow from the definition of a homomorphism alone, before any theory. These include the following:

• homomorphisms and epimorphisms compose;
• if a relation R is contained in the kernel of a homomorphism, then the congruence generated by R is also contained in the kernel;
• the universe liftings and lowerings of an algebra are homomorphisms, and surjective in the lifting direction.

The lifting results are the ones we use most. Agda's universes are not cumulative, so an algebra defined at one universe level cannot be used directly at a higher universe level. Lift-Alg of Setoid.Algebras.Basic lifts an algebra to a higher level, and the homomorphisms defined here (ToLift, FromLift, Lift-hom and their one-sided variants) are what prove this lift harmless. Setoid.Homomorphisms.Isomorphisms assembles these facts into Lift-≅, and the closure operators of Setoid.Varieties.Closure rely on them at every change of level.

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

module Setoid.Homomorphisms.Properties  where

-- Imports from Agda and the Agda Standard Library ------------------------------------------
open import Data.Product                           using ( _,_ ; proj₁ ; proj₂ )
open import Function     renaming ( Func to _⟶_ )  using ( id ; _$_ ; _∘_ )
open import Level                                  using ( Level ; _⊔_ )
open import Relation.Binary                        using ( Setoid )
                                                   renaming ( Rel to BinaryRel ; _⇒_ to _⊆_)
open import Relation.Binary.PropositionalEquality  using ( refl)

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open import Overture                       using  ( 𝓞 ; 𝓥 ; Signature )
open import Setoid.Algebras                using  ( Algebra ; _^_; Lift-Algˡ ; Lift-Algʳ
                                                  ; Lift-Alg; 𝕌[_] ; 𝔻[_] )
open import Setoid.Congruences.Generation  using  ( Gen ; Cg-least )
open import Setoid.Functions               using  ( _⊙_ ; eq ; ⊙-IsSurjective )
open import Setoid.Homomorphisms.Basic     using  ( hom ; IsHom ; epi ; IsEpi )
open import Setoid.Homomorphisms.Kernels   using  ( kercon )

open _⟶_ using ( cong ) renaming ( to to _⟨$⟩_ )

private variable
  α β γ ρᵃ ρᵇ ρᶜ ℓ : Level
  𝑆 : Signature 𝓞 𝓥

Composition of homs

The composite of two homomorphisms is a homomorphism, and the composite of two epimorphisms is an epimorphism.

• ⊙-is-hom is the predicate form: from IsHom 𝑨 𝑩 g and IsHom 𝑩 𝑪 h it proves IsHom 𝑨 𝑪 (h ⊙ g), by transitivity through two steps, first pushing g's compatibility across h with cong h, then applying h's own compatibility.
• ⊙-is-epi adds surjectivity of the composite, which is ⊙-IsSurjective of Setoid.Functions.Surjective.
• ⊙-hom and ⊙-epi are the bundled forms.

All four take their arguments in diagrammatic order, the map out of 𝑨 first and the map out of 𝑩 second, although the underlying composition _⊙_ of Setoid.Functions.Basic is written right to left; so ⊙-hom f g is read as "apply f, then g".

module _
  {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}
  {𝑩 : Algebra β ρᵇ}
  {𝑪 : Algebra γ ρᶜ}
  where
  open Setoid 𝔻[ 𝑨 ] renaming ( _≈_ to _≈₁_ ) using ()
  open Setoid 𝔻[ 𝑪 ] renaming ( _≈_ to _≈₃_ ) using ( trans )
  open IsHom
  open IsEpi

  -- The composition of homomorphisms is again a homomorphism
  ⊙-is-hom : {g : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]} {h : 𝔻[ 𝑩 ] ⟶ 𝔻[ 𝑪 ]}
    → IsHom 𝑨 𝑩 g → IsHom 𝑩 𝑪 h → IsHom 𝑨 𝑪 (h ⊙ g)
  ⊙-is-hom {g} {h} ghom hhom .compatible {f}{a} = trans lemg lemh
    where
    lemg : h ⟨$⟩ (g ⟨$⟩ (f ^ 𝑨) a) ≈₃ h ⟨$⟩ (f ^ 𝑩) λ x → g ⟨$⟩ a x
    lemg = cong h (compatible ghom)

    lemh : h ⟨$⟩ ((f ^ 𝑩) λ x → g ⟨$⟩ a x) ≈₃ (f ^ 𝑪) λ x → h ⟨$⟩ (g ⟨$⟩ a x)
    lemh = compatible hhom

  ⊙-hom : hom 𝑨 𝑩 → hom 𝑩 𝑪  → hom 𝑨 𝑪
  ⊙-hom (h , hhom) (g , ghom) = g ⊙ h , ⊙-is-hom hhom ghom

  -- The composition of epimorphisms is again an epimorphism
  ⊙-is-epi : {g : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]} {h : 𝔻[ 𝑩 ] ⟶ 𝔻[ 𝑪 ]}
    → IsEpi 𝑨 𝑩 g → IsEpi 𝑩 𝑪 h → IsEpi 𝑨 𝑪 (h ⊙ g)
  ⊙-is-epi gE hE .isHom = ⊙-is-hom (isHom gE) (isHom hE)
  ⊙-is-epi gE hE .isSurjective = ⊙-IsSurjective (isSurjective gE) (isSurjective hE)

  ⊙-epi : epi 𝑨 𝑩 → epi 𝑩 𝑪  → epi 𝑨 𝑪
  ⊙-epi (h , hepi) (g , gepi) = g ⊙ h , ⊙-is-epi hepi gepi

A kernel that collapses R contains the congruence generated by R

If a relation R is contained in the kernel of a homomorphism h (i.e., h collapses every R-pair), then the congruence Cg R generated by R is also contained in that kernel. This is exactly Cg-least applied to the kernel congruence kercon h: the kernel is a congruence above R, hence above the least such, Cg R.

Cg⊆ker : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ}
  (h : hom 𝑨 𝑩) {R : BinaryRel 𝕌[ 𝑨 ] ℓ}
  → R ⊆ proj₁ (kercon h) → Gen R ⊆ proj₁ (kercon h)

Cg⊆ker h R⊆k = Cg-least (kercon h) R⊆k

Lifting and lowering of homs

This section establishes that the operations of lifting and lowering of a setoid algebra are homomorphisms.

module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{ℓ : Level} where
  open Level                       using ( lift ; lower )
  open IsHom                       using (compatible)
  open Setoid 𝔻[ 𝑨 ]              using () renaming ( _≈_ to _≈₁_ ; refl to refl₁ )
  open Setoid 𝔻[ Lift-Algˡ 𝑨 ℓ ]  using () renaming ( _≈_ to _≈ˡ_ )
  open Setoid 𝔻[ Lift-Algʳ 𝑨 ℓ ]  using () renaming ( _≈_ to _≈ʳ_ )

  ToLiftˡ : hom 𝑨 (Lift-Algˡ 𝑨 ℓ)
  ToLiftˡ .proj₁ ⟨$⟩ x = lift x
  ToLiftˡ .proj₁ .cong = id
  ToLiftˡ .proj₂ .compatible = refl₁

  FromLiftˡ : hom (Lift-Algˡ 𝑨 ℓ) 𝑨
  FromLiftˡ .proj₁ ⟨$⟩ x = lower x
  FromLiftˡ .proj₁ .cong = id
  FromLiftˡ .proj₂ .compatible = refl₁

  ToFromLiftˡ : ∀ b →  ToLiftˡ .proj₁ ⟨$⟩ (FromLiftˡ .proj₁ ⟨$⟩ b) ≈ˡ b
  ToFromLiftˡ _ = refl₁

  FromToLiftˡ : ∀ a → FromLiftˡ .proj₁ ⟨$⟩ (ToLiftˡ .proj₁ ⟨$⟩ a) ≈₁ a
  FromToLiftˡ _ = refl₁

  ToLiftʳ : hom 𝑨 (Lift-Algʳ 𝑨 ℓ)
  ToLiftʳ .proj₁ ⟨$⟩ x = x
  ToLiftʳ .proj₁ .cong = lift
  ToLiftʳ .proj₂ .compatible = lift refl₁

  FromLiftʳ : hom (Lift-Algʳ 𝑨 ℓ) 𝑨
  FromLiftʳ .proj₁ ⟨$⟩ x = x
  FromLiftʳ .proj₁ .cong = lower
  FromLiftʳ .proj₂ .compatible = refl₁

  ToFromLiftʳ : ∀ b → ToLiftʳ .proj₁ ⟨$⟩ (FromLiftʳ .proj₁ ⟨$⟩ b) ≈ʳ b
  ToFromLiftʳ _ = lift refl₁

  FromToLiftʳ : ∀ a → FromLiftʳ .proj₁ ⟨$⟩ (ToLiftʳ .proj₁ ⟨$⟩ a) ≈₁ a
  FromToLiftʳ _ = refl₁

module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{ℓ r : Level} where
  open Setoid 𝔻[ 𝑨 ]               using () renaming (refl to ≈refl)
  open Setoid 𝔻[ Lift-Alg 𝑨 ℓ r ]  using ( _≈_ )

  ToLift : hom 𝑨 (Lift-Alg 𝑨 ℓ r)
  ToLift = ⊙-hom ToLiftˡ ToLiftʳ

  FromLift : hom (Lift-Alg 𝑨 ℓ r) 𝑨
  FromLift = ⊙-hom FromLiftʳ FromLiftˡ

  ToFromLift : ∀ {b} → ToLift .proj₁ ⟨$⟩ (FromLift .proj₁ ⟨$⟩ b) ≈ b
  ToFromLift = Level.lift ≈refl

  ToLift-epi : epi 𝑨 (Lift-Alg 𝑨 ℓ r)
  ToLift-epi =  ToLift .proj₁ ,
                record  { isHom = ToLift .proj₂
                        ; isSurjective = λ {y} → eq (FromLift .proj₁ ⟨$⟩ y) ToFromLift
                        }

Next we formalize the fact that a homomorphism from 𝑨 to 𝑩 can be lifted to a homomorphism from Lift-Alg 𝑨 ℓᵃ to Lift-Alg 𝑩 ℓᵇ.

module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} where
  open Level using ( lift ; lower )

  Lift-homˡ : hom 𝑨 𝑩  → (ℓᵃ ℓᵇ : Level) →  hom (Lift-Algˡ 𝑨 ℓᵃ) (Lift-Algˡ 𝑩 ℓᵇ)
  Lift-homˡ (f , fhom) ℓᵃ ℓᵇ = ϕ , ⊙-is-hom lABh (ToLiftˡ .proj₂)
    where
    lA : Algebra (α ⊔ ℓᵃ) ρᵃ
    lA = Lift-Algˡ 𝑨 ℓᵃ

    lB : Algebra (β ⊔ ℓᵇ) ρᵇ
    lB = Lift-Algˡ 𝑩 ℓᵇ

    ψ : 𝔻[ lA ] ⟶ 𝔻[ 𝑩 ]
    ψ ⟨$⟩ x = f ⟨$⟩ (Level.lower x)
    ψ .cong = f .cong

    lABh : IsHom lA 𝑩 ψ
    lABh = ⊙-is-hom (FromLiftˡ .proj₂) fhom

    ϕ : 𝔻[ lA ] ⟶ 𝔻[ lB ]
    ϕ ⟨$⟩ x = lift (f ⟨$⟩ (lower x))
    ϕ .cong = f .cong

  Lift-homʳ : hom 𝑨 𝑩  → (rᵃ rᵇ : Level) →  hom (Lift-Algʳ 𝑨 rᵃ) (Lift-Algʳ 𝑩 rᵇ)
  Lift-homʳ (f , fhom) rᵃ rᵇ = ϕ , Goal
    where
    lA : Algebra α (ρᵃ ⊔ rᵃ)
    lA = Lift-Algʳ 𝑨 rᵃ
    lB : Algebra β (ρᵇ ⊔ rᵇ)
    lB = Lift-Algʳ 𝑩 rᵇ
    ψ : 𝔻[ lA ] ⟶ 𝔻[ 𝑩 ]
    ψ ⟨$⟩ x = f ⟨$⟩ x
    ψ .cong = f .cong ∘ lower

    lABh : IsHom lA 𝑩 ψ
    lABh = ⊙-is-hom (proj₂ FromLiftʳ) fhom

    ϕ : 𝔻[ lA ] ⟶ 𝔻[ lB ]
    ϕ ⟨$⟩ x = f ⟨$⟩ x
    ϕ .cong xy .lower = f .cong $ xy .lower

    Goal : IsHom lA lB ϕ
    Goal = ⊙-is-hom lABh (ToLiftʳ .proj₂)

  module _ (h : hom 𝑨 𝑩) (a : 𝕌[ 𝑨 ]) (ℓᵃ ℓᵇ : Level) where
    open Setoid 𝔻[ Lift-Algˡ 𝑩 ℓᵇ ] using ( _≈_ )
    lift-hom-lemma : lift (h .proj₁ ⟨$⟩ a) ≈ (Lift-homˡ h ℓᵃ ℓᵇ) .proj₁ ⟨$⟩ lift a
    lift-hom-lemma = Setoid.refl 𝔻[ 𝑩 ]

module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} where
  Lift-hom : hom 𝑨 𝑩  → (ℓᵃ rᵃ ℓᵇ rᵇ : Level) → hom (Lift-Alg 𝑨 ℓᵃ rᵃ) (Lift-Alg 𝑩 ℓᵇ rᵇ)
  Lift-hom φ ℓᵃ rᵃ ℓᵇ rᵇ = Lift-homʳ (Lift-homˡ φ ℓᵃ ℓᵇ) rᵃ rᵇ

  Lift-hom-fst : hom 𝑨 𝑩 → (ℓ r : Level) → hom (Lift-Alg 𝑨 ℓ r) 𝑩
  Lift-hom-fst φ _ _ = ⊙-hom FromLift φ

  Lift-hom-snd : hom 𝑨 𝑩 → (ℓ r : Level) → hom 𝑨 (Lift-Alg 𝑩 ℓ r)
  Lift-hom-snd φ _ _ = ⊙-hom φ ToLift