### Homomorphism decomposition

This is the Base.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 Overture using ( 𝓞 ; 𝓥 ; Signature )

module Base.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 ( _∘_ )
open import Level           using ( Level )
open import Relation.Unary  using ( _⊆_ )

open  import Relation.Binary.PropositionalEquality as ≡
using ( module ≡-Reasoning ; _≡_ )

-- Imports from agda-algebras --------------------------------------------------------------
open import Overture        using ( ∣_∣ ; ∥_∥ ; _⁻¹ )
open import Base.Equality   using ( swelldef )
open import Base.Relations  using ( kernel )
open import Base.Functions  using ( IsSurjective ; SurjInv )
using ( SurjInvIsInverseʳ ; epic-factor )

open import Base.Algebras             {𝑆 = 𝑆}  using ( Algebra ; _̂_)
open import Base.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)                    ≡⟨ goal ⟩
φ ((𝑓 ̂ 𝑪)(∣ ν ∣ ∘(νInv ∘ c)))   ≡⟨ ≡.cong φ (∥ ν ∥ 𝑓 (νInv ∘ c))⁻¹ ⟩
φ (∣ ν ∣((𝑓 ̂ 𝑨)(νInv ∘ c)))     ≡⟨ (τφν ((𝑓 ̂ 𝑨)(νInv ∘ c)))⁻¹ ⟩
∣ τ ∣((𝑓 ̂ 𝑨)(νInv ∘ c))         ≡⟨ ∥ τ ∥ 𝑓 (νInv ∘ c) ⟩
(𝑓 ̂ 𝑩)(λ x → ∣ τ ∣(νInv (c x))) ∎
where
goal : φ ((𝑓 ̂ 𝑪) c) ≡ φ ((𝑓 ̂ 𝑪) (∣ ν ∣ ∘(νInv ∘ c)))
goal = ≡.cong φ (wd (𝑓 ̂ 𝑪) c (∣ ν ∣ ∘ (νInv ∘ c)) λ i → (η (c i))⁻¹)

```

If, in addition to the hypotheses of the last theorem, we assume `τ` is epic, then so is `φ`.

``` 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
```