Agda UALib ↑

Inverses

This is the Overture.Inverses module of the Agda Universal Algebra Library.


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

module Overture.Inverses where

open import Overture.FunExtensionality public

open import MGS-Embeddings
 using (equivs-are-embeddings; invertible; invertibles-are-equivs) public

We begin by defining an inductive type that represents the semantic concept of inverse image of a function.


module _ {A : 𝓀 Μ‡ }{B : 𝓦 Μ‡ } where

 data Image_βˆ‹_ (f : A β†’ B) : B β†’ 𝓀 βŠ” 𝓦 Μ‡
  where
  im : (x : A) β†’ Image f βˆ‹ f x
  eq : (b : B) β†’ (a : A) β†’ b ≑ f a β†’ Image f βˆ‹ b

Next we verify that the type behaves as we expect.


 ImageIsImage : (f : A β†’ B)(b : B)(a : A) β†’ b ≑ f a β†’ Image f βˆ‹ b
 ImageIsImage f b a b≑fa = eq b a b≑fa

An inhabitant of Image f βˆ‹ b is a dependent pair (a , p), where a : A and p : b ≑ f a is a proof that f maps a to b. Since the proof that b belongs to the image of f is always accompanied by a witness a : A, we can actually compute a (pseudo)inverse of f. For convenience, we define this inverse function, which we call Inv, and which takes an arbitrary b : B and a (witness, proof)-pair, (a , p) : Image f βˆ‹ b, and returns the witness a.


 Inv : (f : A β†’ B){b : B} β†’ Image f βˆ‹ b  β†’  A
 Inv f {.(f a)} (im a) = a
 Inv f (eq _ a _) = a

We can prove that Inv f is the right-inverse of f, as follows.


 InvIsInv : (f : A β†’ B){b : B}(q : Image f βˆ‹ b) β†’ f(Inv f q) ≑ b
 InvIsInv f {.(f a)} (im a) = refl
 InvIsInv f (eq _ _ p) = p ⁻¹

Epics (surjective functions)

An epic (or surjective) function from A to B is as an inhabitant of the Epic type, which we now define.


 Epic : (A β†’ B) β†’  𝓀 βŠ” 𝓦 Μ‡
 Epic f = βˆ€ y β†’ Image f βˆ‹ y

With the next definition, we can represent the right-inverse of an epic function.


 EpicInv : (f : A β†’ B) β†’ Epic f β†’ B β†’ A
 EpicInv f fE b = Inv f (fE b)

The right-inverse of f is obtained by applying EpicInv to f and a proof of Epic f. To see that this does indeed give the right-inverse we prove the EpicInvIsRightInv lemma below. This requires function composition, denoted ∘ and defined in the Type Topology library.


module hide-∘ {A : 𝓀 Μ‡}{B : 𝓦 Μ‡}{C : B β†’ 𝓦 Μ‡ } where

 _∘_ : Ξ  C β†’ (f : A β†’ B) β†’ (x : A) β†’ C (f x)
 g ∘ f = Ξ» x β†’ g (f x)

open import MGS-MLTT using (_∘_) public

Note that the next proof requires function extensionality, which we postulate in the module declaration.


module _ {fe : funext 𝓦 𝓦}{A : 𝓀 Μ‡}{B : 𝓦 Μ‡} where

 EpicInvIsRightInv : (f : A β†’ B)(fE : Epic f) β†’ f ∘ (EpicInv f fE) ≑ 𝑖𝑑 B
 EpicInvIsRightInv f fE = fe (Ξ» x β†’ InvIsInv f (fE x))

We can also prove the following composition law for epics.


 epic-factor : {C : 𝓩 Μ‡}(f : A β†’ B)(g : A β†’ C)(h : C β†’ B)
  β†’            f ≑ h ∘ g β†’ Epic f β†’ Epic h

 epic-factor f g h compId fe y = Ξ³
  where
   finv : B β†’ A
   finv = EpicInv f fe

   ΞΆ : f (finv y) ≑ y
   ΞΆ = cong-app (EpicInvIsRightInv f fe) y

   Ξ· : (h ∘ g) (finv y) ≑ y
   Ξ· = (cong-app (compId ⁻¹)(finv y)) βˆ™ ΞΆ

   Ξ³ : Image h βˆ‹ y
   γ = eq y (g (finv y)) (η ⁻¹)

Monics (injective functions)

We say that a function f : A β†’ B is monic (or injective) if it does not map distinct elements to a common point. This following type manifests this property.


module _ {A : 𝓀 Μ‡}{B : 𝓦 Μ‡} where

 Monic : (f : A β†’ B) β†’ 𝓀 βŠ” 𝓦 Μ‡
 Monic f = βˆ€ x y β†’ f x ≑ f y β†’ x ≑ y

Again, we obtain a pseudoinverse. Here it is obtained by applying the function MonicInv to g and a proof that g is monic.


 MonicInv : (f : A β†’ B) β†’ Monic f β†’ (b : B) β†’ Image f βˆ‹ b β†’ A
 MonicInv f _ = Ξ» b imfb β†’ Inv f imfb

The function defined by MonicInv f fM is the left-inverse of f.


 MonicInvIsLeftInv : {f : A β†’ B}{fM : Monic f}{x : A} β†’ (MonicInv f fM)(f x)(im x) ≑ x
 MonicInvIsLeftInv = refl

Embeddings

The is-embedding type is defined in the Type Topology library in the following way.

module hide-is-embedding{A : 𝓀 Μ‡}{B : 𝓦 Μ‡} where

 is-embedding : (A β†’ B) β†’ 𝓀 βŠ” 𝓦 Μ‡
 is-embedding f = βˆ€ b β†’ is-subsingleton (fiber f b)

open import MGS-Embeddings using (is-embedding) public

Thus, is-embedding f asserts that f is a function all of whose fibers are subsingletons. Observe that an embedding is not simply an injective map. However, if we assume that the codomain B has unique identity proofs (UIP), then we can prove that a monic function into B is an embedding. We will do exactly that in the Relations.Truncation module when we take up the topic of sets and the UIP.

Finding a proof that a function is an embedding isn’t always easy, but one path that is often straightforward is to first prove that the function is invertible and then invoke the following theorem.


module _ {A : 𝓀 Μ‡}{B : 𝓦 Μ‡} where

 invertibles-are-embeddings : (f : A β†’ B) β†’ invertible f β†’ is-embedding f
 invertibles-are-embeddings f fi = equivs-are-embeddings f (invertibles-are-equivs f fi)

Finally, embeddings are monic; from a proof p : is-embedding f that f is an embedding we can construct a proof of Monic f. We confirm this as follows.


 embedding-is-monic : (f : A β†’ B) β†’ is-embedding f β†’ Monic f
 embedding-is-monic f femb x y fxfy = ap pr₁ ((femb (f x)) fx fy)
  where
  fx fy : fiber f (f x)
  fx = x , refl
  fy = y , (fxfy ⁻¹)

← Overture.FunExtensionality Overture.Lifts β†’