↑ Top


Surjective functions

This is the Base.Functions.Surjective module of the agda-algebras library.


{-# OPTIONS --without-K --exact-split --safe #-}
module Base.Functions.Surjective where

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Agda.Primitive    using () renaming ( Set to Type )
open import Data.Empty        using (⊥-elim)
open import Function          using ( Surjective ; _∘_ )
open import Level             using ( _⊔_ ; Level )
open import Relation.Binary   using ( Decidable )
open import Relation.Nullary  using ( Dec ; yes ; no )
open import Data.Product      using ( _,_ ; Σ ; Σ-syntax )
                              renaming ( proj₁ to fst ; proj₂ to snd )
open import Axiom.UniquenessOfIdentityProofs
                              using ( module Decidable⇒UIP )
open import Relation.Binary.PropositionalEquality
                              using ( _≡_ ; sym ; cong-app ; cong ; refl )

-- Imports from agda-algebras -----------------------------------------------------
open import Overture.Basic     using ( _≈_ ; _∙_ ; transport )
open import Base.Functions.Inverses  using ( Image_∋_ ; eq ; Inv ; InvIsInverseʳ )

private variable α β γ c ι : Level

A surjective function from A to B is a function f : A → B 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. The following types manifest this notion.


module _ {A : Type α}{B : Type β} where

 IsSurjective : (A  B)   Type (α  β)
 IsSurjective f =  y  Image f  y

 onto : Type (α  β)
 onto = Σ (A  B) IsSurjective

 IsSurjective→Surjective :  (f : A  B)  IsSurjective f
                           Surjective{A = A} _≡_ _≡_ f

 IsSurjective→Surjective f fE y = imgfy→A (fE y)
  where
  imgfy→A : Image f  y  Σ[ a  A ] f a  y
  imgfy→A (eq a p) = a , sym p

 Surjective→IsSurjective :  (f : A  B)  Surjective{A = A} _≡_ _≡_ f
                           IsSurjective f

 Surjective→IsSurjective f fE y = eq (fst (fE y)) (sym (snd(fE y)))

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


 SurjInv : (f : A  B)  IsSurjective f  B  A
 SurjInv f fE b = Inv f (fE b)

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


module _ {A : Type α}{B : Type β} where

 SurjInvIsInverseʳ :  (f : A  B)(fE : IsSurjective f)
                      b  f ((SurjInv f fE) b)  b

 SurjInvIsInverseʳ f fE b = InvIsInverseʳ (fE b)

 -- composition law for epics
 epic-factor :  {C : Type γ}(f : A  B)(g : A  C)(h : C  B)
               f  h  g  IsSurjective f  IsSurjective h

 epic-factor f g h compId fe y = Goal
  where
   finv : B  A
   finv = SurjInv f fe

   ζ : y  f (finv y)
   ζ = sym (SurjInvIsInverseʳ f fe y)

   η : y  (h  g) (finv y)
   η = ζ  compId (finv y)

   Goal : Image h  y
   Goal = eq (g (finv y)) η

 epic-factor-intensional :  {C : Type γ}(f : A  B)(g : A  C)(h : C  B)
                           f  h  g  IsSurjective f  IsSurjective h

 epic-factor-intensional f g h compId fe y = Goal
  where
   finv : B  A
   finv = SurjInv f fe

   ζ : f (finv y)  y
   ζ = SurjInvIsInverseʳ f fe y

   η : (h  g) (finv y)  y
   η = (cong-app (sym compId)(finv y))  ζ

   Goal : Image h  y
   Goal = eq (g (finv y)) (sym η)

Later we will need the fact that the projection of an arbitrary product onto one (or any number) of its factors is surjective.


module _  {I : Set ι}(_≟_ : Decidable{A = I} _≡_)
          {B : I  Set β}
          (bs₀ :  i  (B i))
 where
 open Decidable⇒UIP _≟_ using ( ≡-irrelevant )

 proj : (j : I)  (∀ i  (B i))  (B j)
 proj j xs = xs j

 update : (∀ i  B i)  ((j , _) : Σ I B)  (∀ i  Dec (i  j)  B i)
 update _   (_ , b)  i (yes x) = transport B (sym x) b
 update bs  _        i (no  _) = bs i

 update-id : ∀{j b}  (c : Dec (j  j))  update bs₀ (j , b) j c  b
 update-id {j}{b}  (yes p) = cong  x  transport B x b)(≡-irrelevant (sym p) refl)
 update-id         (no ¬p) = ⊥-elim (¬p refl)

 proj-is-onto : ∀{j}  Surjective{A =  i  (B i)} _≡_ _≡_ (proj j)
 proj-is-onto {j} b = bs , pf
  where
  bs : (i : I)  B i
  bs i = update bs₀ (j , b) i (i  j)

  pf : proj j bs  b
  pf = update-id (j  j)

 projIsOnto : ∀{j}  IsSurjective (proj j)
 projIsOnto {j} = Surjective→IsSurjective (proj j) proj-is-onto

← Base.Functions.Injective Base.Functions.Transformers →