↑ Top


Homomorphism decomposition

This is the Homomorphisms.Factor module of the Agda Universal Algebra Library in which we prove the following theorem:

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

𝑨 --- ν ->> 𝑪
 \         .
  \       .
   τ     φ
    \   .
     \ .
      V
      𝑩
{-# OPTIONS --without-K --exact-split --safe #-}

open import Algebras.Basic using ( 𝓞 ; 𝓥 ; Signature )

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

-- Imports from Agda and the Agda Standard Library ---------------------------------------
open import Agda.Primitive using ( Level )
open import Data.Product   using ( Σ-syntax ; _,_ ) renaming (proj₁ to fst ; proj₂ to snd)
open import Function.Base  using ( _∘_ )
open import Relation.Binary.PropositionalEquality using ( module ≡-Reasoning ; _≡_ ; cong )
open import Relation.Unary using ( _⊆_ )

-- Imports from agda-algebras --------------------------------------------------------------
open import Overture.Preliminaries      using ( ∣_∣ ; ∥_∥ ; _⁻¹ )
open import Overture.Surjective         using ( IsSurjective ; SurjInv ; SurjInvIsInverseʳ
                                              ; epic-factor )
open import Relations.Discrete          using ( kernel )
open import Equality.Welldefined        using ( swelldef )
open import Algebras.Basic              using ( Algebra ; _̂_)
open import Homomorphisms.Basic {𝑆 = 𝑆} using ( hom ; epi )

private variable α β γ : Level

module _ {𝑨 : Algebra α 𝑆}{𝑪 : Algebra γ 𝑆} where

 open ≡-Reasoning

 HomFactor : swelldef 𝓥 γ
            (𝑩 : Algebra β 𝑆)(τ : hom 𝑨 𝑩)(ν : hom 𝑨 𝑪)
            kernel  ν   kernel  τ   IsSurjective  ν 
             --------------------------------------------------
            Σ[ φ  (hom 𝑪 𝑩)]  x   τ  x   φ  ( ν  x)

 HomFactor wd 𝑩 τ ν Kντ νE = (φ , φIsHomCB) , τφν
  where
   νInv :  𝑪    𝑨 
   νInv = SurjInv  ν  νE

   η :  c   ν  (νInv c)  c
   η c = SurjInvIsInverseʳ  ν  νE c

   φ :  𝑪    𝑩 
   φ =  τ   νInv

   ξ :  a  kernel  ν  (a , νInv ( ν  a))
   ξ a = (η ( ν  a))⁻¹

   τφν :  x   τ  x  φ ( ν  x)
   τφν = λ x  Kντ (ξ x)

   φIsHomCB :  𝑓 c  φ ((𝑓 ̂ 𝑪) c)  ((𝑓 ̂ 𝑩)(φ  c))
   φIsHomCB 𝑓 c =
    φ ((𝑓 ̂ 𝑪) c)                    ≡⟨ cong φ (wd (𝑓 ̂ 𝑪) c ( ν   (νInv  c))  i  (η (c i))⁻¹))
    φ ((𝑓 ̂ 𝑪)( ν  (νInv  c)))   ≡⟨ cong φ ( ν  𝑓 (νInv  c))⁻¹ 
    φ ( ν ((𝑓 ̂ 𝑨)(νInv  c)))     ≡⟨ (τφν ((𝑓 ̂ 𝑨)(νInv  c)))⁻¹ 
     τ ((𝑓 ̂ 𝑨)(νInv  c))         ≡⟨  τ  𝑓 (νInv  c) 
    (𝑓 ̂ 𝑩)(λ x   τ (νInv (c x))) 

If, in addition to the hypotheses of the last theorem, we assume τ is epic, then so is φ. (Note that the proof also requires an additional local function extensionality postulate, funext β β.)

 HomFactorEpi : swelldef 𝓥 γ
               (𝑩 : Algebra β 𝑆)(τ : hom 𝑨 𝑩)(ν : hom 𝑨 𝑪)
               kernel  ν   kernel  τ 
               IsSurjective  ν   IsSurjective  τ 
                ---------------------------------------------
               Σ[ φ  epi 𝑪 𝑩 ]  x   τ  x   φ  ( ν  x)

 HomFactorEpi wd 𝑩 τ ν kerincl νe τe = (fst  φF  ,(snd  φF  , φE)),  φF 
  where
   φF : Σ[ φ  hom 𝑪 𝑩 ]  x   τ  x   φ  ( ν  x)
   φF = HomFactor wd 𝑩 τ ν kerincl νe

   φ :  𝑪    𝑩 
   φ =  τ   (SurjInv  ν  νe)

   φE : IsSurjective φ
   φE = epic-factor  τ   ν  φ  φF  τe


← Homomorphisms.Noether Homomorphisms.Isomorphisms →