↑ Top


Factoring Homomorphism of Algebras

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

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

open import Overture using (𝓞 ; 𝓥 ; Signature)

module Setoid.Homomorphisms.Factor {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library -------------------------------------------------
open import Data.Product     using ( _,_ ; Σ-syntax )  renaming ( proj₁ to fst ; proj₂ to snd )
open import Function         using ( _∘_ )             renaming ( Func to _⟶_ )
open import Level            using ( Level )
open import Relation.Binary  using ( Setoid )
open import Relation.Unary   using ( _⊆_ )

open import Relation.Binary.PropositionalEquality  as            using ()
import Relation.Binary.Reasoning.Setoid            as SReasoning  using ( begin_ ; step-≈˘; step-≈; _∎)

-- Imports from the Agda Universal Algebra Library ------------------------------------------------
open import Overture         using ( ∣_∣ ; ∥_∥ )
open import Setoid.Functions using ( Image_∋_ ; IsSurjective ; SurjInv )
                             using ( SurjInvIsInverseʳ ; epic-factor )
open import Base.Relations   using ( kernelRel )

open import Setoid.Algebras {𝑆 = 𝑆}             using ( Algebra ; 𝕌[_] ; _̂_ )
open import Setoid.Homomorphisms.Basic {𝑆 = 𝑆}  using ( hom ; IsHom ; compatible-map ; epi ; IsEpi)

private variable α ρᵃ β ρᵇ γ ρᶜ : Level

If g : hom 𝑨 𝑩, h : hom 𝑨 𝑪, h is surjective, and ker h ⊆ ker g, then there exists φ : hom 𝑪 𝑩 such that g = φ ∘ h so the following diagram commutes:

𝑨 --- h -->> 𝑪
 \         .
  \       .
   g     φ
    \   .
     \ .
      V
      𝑩

We will prove this in case h is both surjective and injective.

module _  {𝑨 : Algebra α ρᵃ} (𝑩 : Algebra β ρᵇ) {𝑪 : Algebra γ ρᶜ}
          (gh : hom 𝑨 𝑩)(hh : hom 𝑨 𝑪) where

 open Algebra 𝑩  using ()          renaming (Domain to B )
 open Algebra 𝑪  using ( Interp )  renaming (Domain to C )
 open Setoid B   using ()          renaming ( _≈_ to _≈₂_ ; sym to sym₂ )
 open Setoid C   using ( trans )   renaming ( _≈_ to _≈₃_ ; sym to sym₃ )
 open _⟶_        using ( cong )    renaming (f to _⟨$⟩_ )

 open SReasoning B

 private
  gfunc =  gh 
  hfunc =  hh 
  g = _⟨$⟩_ gfunc
  h = _⟨$⟩_ hfunc

 open IsHom
 open Image_∋_

 HomFactor :  kernelRel _≈₃_ h  kernelRel _≈₂_ g  IsSurjective hfunc
              ---------------------------------------------------------
             Σ[ φ  hom 𝑪 𝑩 ]  a  (g a) ≈₂  φ  ⟨$⟩ (h a)

 HomFactor Khg hE = (φmap , φhom) , gφh
  where
  kerpres :  a₀ a₁  h a₀ ≈₃ h a₁  g a₀ ≈₂ g a₁
  kerpres a₀ a₁ hyp = Khg hyp

  h⁻¹ : 𝕌[ 𝑪 ]  𝕌[ 𝑨 ]
  h⁻¹ = SurjInv hfunc hE

  η :  {c}  h (h⁻¹ c) ≈₃ c
  η = SurjInvIsInverseʳ hfunc hE

  ξ :  {a}  h a ≈₃ h (h⁻¹ (h a))
  ξ = sym₃ η

  ζ : ∀{x y}  x ≈₃ y  h (h⁻¹ x) ≈₃ h (h⁻¹ y)
  ζ xy = trans η (trans xy (sym₃ η))


  φmap : C  B
  _⟨$⟩_ φmap = g  h⁻¹
  cong φmap = Khg  ζ

  gφh : (a : 𝕌[ 𝑨 ])  g a ≈₂ φmap ⟨$⟩ (h a)
  gφh a = Khg ξ


  open _⟶_ φmap using () renaming (cong to φcong)
  φcomp : compatible-map 𝑪 𝑩 φmap
  φcomp {f}{c} =
   begin
    φmap ⟨$⟩ ((f ̂ 𝑪) c)              ≈˘⟨ φcong (cong Interp (≡.refl ,  _  η)))  
    g (h⁻¹ ((f ̂ 𝑪)(h  (h⁻¹  c))))  ≈˘⟨ φcong (compatible  hh )                 
    g (h⁻¹ (h ((f ̂ 𝑨)(h⁻¹  c))))    ≈˘⟨ gφh ((f ̂ 𝑨)(h⁻¹  c))                     
    g ((f ̂ 𝑨)(h⁻¹  c))              ≈⟨ compatible  gh                           
    (f ̂ 𝑩)(g  (h⁻¹  c))            

  φhom : IsHom 𝑪 𝑩 φmap
  compatible φhom = φcomp

If, in addition, g is surjective, then so will be the factor φ.


 HomFactorEpi :  kernelRel _≈₃_ h  kernelRel _≈₂_ g
                IsSurjective hfunc  IsSurjective gfunc
                 -------------------------------------------------
                Σ[ φ  epi 𝑪 𝑩 ]  a  (g a) ≈₂  φ  ⟨$⟩ (h a)

 HomFactorEpi Khg hE gE = (φmap , φepi) , gφh
  where
  homfactor : Σ[ φ  hom 𝑪 𝑩 ]  a  (g a) ≈₂  φ  ⟨$⟩ (h a)
  homfactor = HomFactor Khg hE

  φmap : C  B
  φmap = fst  homfactor 

  gφh : (a : 𝕌[ 𝑨 ])  g a ≈₂ φmap ⟨$⟩ (h a)
  gφh = snd homfactor -- Khg ξ

  φhom : IsHom 𝑪 𝑩 φmap
  φhom = snd  homfactor 

  φepi : IsEpi 𝑪 𝑩 φmap
  φepi = record  { isHom = φhom
                 ; isSurjective = epic-factor gfunc hfunc φmap gE gφh
                 }

← Setoid.Homomorphisms.Noether Setoid.Homomorphisms.Isomorphisms →