↑ Top

Surjective functions on setoids

This is the [Setoid.Overture.Surjective][] module of the agda-algebras library.

A surjective function from a setoid 𝑨 = (A, β‰ˆβ‚€) to a setoid 𝑩 = (B, β‰ˆβ‚) is a function f : 𝑨 ⟢ 𝑩 such that for all b : B there exists a : A such that (f ⟨$⟩ a) β‰ˆβ‚ b. In other words, the range and codomain of f agree.


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

module Setoid.Overture.Surjective where

-- Imports from Agda and the Agda Standard Library --------------------------
open import Agda.Primitive    using ( _βŠ”_ ; Level )  renaming ( Set to Type )
open import Data.Product      using ( _,_ ; Ξ£-syntax )
open import Function.Bundles  using ( Surjection )   renaming ( Func to _⟢_ )
open import Function          using ( IsSurjection )
open import Relation.Binary   using ( Setoid )

open import Function.Construct.Composition using ()  renaming ( isSurjection to isOnto )

import Function.Definitions as FD

-- Imports from agda-algebras -----------------------------------------------
open import Base.Overture.Preliminaries         using ( ∣_∣ ; βˆ₯_βˆ₯ ; βˆƒ-syntax ; transport )
open import Setoid.Overture.Preliminaries  using ( _∘_ )
open import Setoid.Overture.Inverses       using ( Img_βˆ‹_ ; Image_βˆ‹_ ; Inv ; InvIsInverseΚ³ )


private variable
 Ξ± ρᡃ Ξ² ρᡇ Ξ³ ρᢜ : Level

open Image_βˆ‹_

module _ {𝑨 : Setoid Ξ± ρᡃ}{𝑩 : Setoid Ξ² ρᡇ} where

 open Setoid 𝑨  using ()               renaming (Carrier to A; _β‰ˆ_ to _β‰ˆβ‚_; isEquivalence to isEqA )
 open Setoid 𝑩  using ( trans ; sym )  renaming (Carrier to B; _β‰ˆ_ to _β‰ˆβ‚‚_; isEquivalence to isEqB )

 open Surjection {a = Ξ±}{ρᡃ}{Ξ²}{ρᡇ}{From = 𝑨}{To = 𝑩}  renaming (f to _⟨$⟩_)
 open _⟢_ {a = Ξ±}{ρᡃ}{Ξ²}{ρᡇ}{From = 𝑨}{To = 𝑩}         renaming (f to _⟨$⟩_ )
 open FD _β‰ˆβ‚_ _β‰ˆβ‚‚_

 isSurj : (A β†’ B) β†’  Type (Ξ± βŠ” Ξ² βŠ” ρᡇ)
 isSurj f = βˆ€ {y} β†’ Img_βˆ‹_ {𝑨 = 𝑨}{𝑩 = 𝑩} f y

 IsSurjective : (𝑨 ⟢ 𝑩) β†’  Type (Ξ± βŠ” Ξ² βŠ” ρᡇ)
 IsSurjective F = βˆ€ {y} β†’ Image F βˆ‹ y

 isSurjβ†’IsSurjective : (F : 𝑨 ⟢ 𝑩) β†’ isSurj (_⟨$⟩_ F) β†’ IsSurjective F
 isSurj→IsSurjective F isSurjF {y} = hyp isSurjF
  where
  hyp : Img (_⟨$⟩_ F) βˆ‹ y β†’ Image F βˆ‹ y
  hyp (Img_βˆ‹_.eq a x) = eq a x

 open Image_βˆ‹_

 SurjectionIsSurjective : (Surjection 𝑨 𝑩) β†’ Ξ£[ g ∈ (𝑨 ⟢ 𝑩) ] (IsSurjective g)
 SurjectionIsSurjective s = g , gE
  where
  g : 𝑨 ⟢ 𝑩
  g = (record { f = _⟨$⟩_ s ; cong = cong s })
  gE : IsSurjective g
  gE {y} = eq ∣ (surjective s) y ∣ (sym βˆ₯ (surjective s) y βˆ₯)

 SurjectionIsSurjection : (Surjection 𝑨 𝑩) β†’ Ξ£[ g ∈ (𝑨 ⟢ 𝑩) ] (IsSurjection _β‰ˆβ‚_ _β‰ˆβ‚‚_ (_⟨$⟩_ g))
 SurjectionIsSurjection s = g , gE
  where
  g : 𝑨 ⟢ 𝑩
  g = (record { f = _⟨$⟩_ s ; cong = cong s })
  gE : IsSurjection _β‰ˆβ‚_ _β‰ˆβ‚‚_ (_⟨$⟩_ g)
  IsSurjection.isCongruent gE = record { cong = cong g ; isEquivalence₁ = isEqA ; isEquivalenceβ‚‚ = isEqB }
  IsSurjection.surjective gE y = ∣ (surjective s) y ∣ , βˆ₯ (surjective s) y βˆ₯

With the next definition, we can represent a right-inverse of a surjective function.


 SurjInv : (f : 𝑨 ⟢ 𝑩) β†’ IsSurjective f β†’ B β†’ A
 SurjInv f fE b = Inv f (fE {b})

Thus, a right-inverse of f is obtained by applying Inv to f and a proof of IsSurjective f. Next we prove that this does indeed give the right-inverse.


 SurjInvIsInverseΚ³ : (f : 𝑨 ⟢ 𝑩)(fE : IsSurjective f) β†’ βˆ€ {b} β†’ (f ⟨$⟩ ((SurjInv f fE) b)) β‰ˆβ‚‚ b
 SurjInvIsInverseΚ³ f fE = InvIsInverseΚ³ fE

Next, we prove composition laws for epics.


module _ {𝑨 : Setoid Ξ± ρᡃ}{𝑩 : Setoid Ξ² ρᡇ}{π‘ͺ : Setoid Ξ³ ρᢜ} where

 open Setoid 𝑨  using ()               renaming (Carrier to A; _β‰ˆ_ to _β‰ˆβ‚_)
 open Setoid 𝑩  using ( trans ; sym )  renaming (Carrier to B; _β‰ˆ_ to _β‰ˆβ‚‚_)
 open Setoid π‘ͺ  using ()               renaming (Carrier to C; _β‰ˆ_ to _β‰ˆβ‚ƒ_)

 open Surjection  renaming (f to _⟨$⟩_)
 open _⟢_         renaming (f to _⟨$⟩_ )
 open FD _β‰ˆβ‚_ _β‰ˆβ‚‚_


 ∘-IsSurjective : {G : 𝑨 ⟢ π‘ͺ}{H : π‘ͺ ⟢ 𝑩} β†’ IsSurjective G β†’ IsSurjective H β†’ IsSurjective (H ∘ G)
 ∘-IsSurjective {G} {H} gE hE {y} = Goal
  where
  mp : Image H βˆ‹ y β†’ Image H ∘ G βˆ‹ y
  mp (eq c p) = Ξ· gE
   where
   Ξ· : Image G βˆ‹ c β†’ Image H ∘ G βˆ‹ y
   Ξ· (eq a q) = eq a (trans p (cong H q))

  Goal : Image H ∘ G βˆ‹ y
  Goal = mp hE


 ∘-epic : Surjection 𝑨 π‘ͺ β†’ Surjection π‘ͺ 𝑩 β†’ Surjection 𝑨 𝑩
 Surjection.f (∘-epic g h) x = h ⟨$⟩ (g ⟨$⟩ x)
 Surjection.cong (∘-epic g h) {x} {y} xy = cong h (cong g xy)
 Surjection.surjective (∘-epic g h) = IsSurjection.surjective hgSurj
  where
  gSurj : Ξ£[ G ∈ (𝑨 ⟢ π‘ͺ) ] (IsSurjection _β‰ˆβ‚_ _β‰ˆβ‚ƒ_ (_⟨$⟩_ G))
  gSurj = SurjectionIsSurjection g
  hSurj : Ξ£[ H ∈ (π‘ͺ ⟢ 𝑩) ] (IsSurjection _β‰ˆβ‚ƒ_ _β‰ˆβ‚‚_ (_⟨$⟩_ H))
  hSurj = SurjectionIsSurjection h

  hgSurj : IsSurjection _β‰ˆβ‚_ _β‰ˆβ‚‚_ (Ξ» x β†’ h ⟨$⟩ (g ⟨$⟩ x))
  hgSurj = isOnto βˆ₯ gSurj βˆ₯ βˆ₯ hSurj βˆ₯


 epic-factor : (f : 𝑨 ⟢ 𝑩)(g : 𝑨 ⟢ π‘ͺ)(h : π‘ͺ ⟢ 𝑩)
  β†’            IsSurjective f β†’ (βˆ€ i β†’ (f ⟨$⟩ i) β‰ˆβ‚‚ ((h ∘ g) ⟨$⟩ i)) β†’ IsSurjective h

 epic-factor f g h fE compId {y} = Goal
  where
   finv : B β†’ A
   finv = SurjInv f fE

   ΞΆ : y β‰ˆβ‚‚ (f ⟨$⟩ (finv y))
   ΞΆ = sym (SurjInvIsInverseΚ³ f fE)

   Ξ· : y β‰ˆβ‚‚ ((h ∘ g) ⟨$⟩ (finv y))
   Ξ· = trans ΞΆ (compId (finv y))

   Goal : Image h βˆ‹ y
   Goal = eq (g ⟨$⟩ (finv y)) η

← Setoid.Overture.Injective Setoid.Overture.Bijective β†’