Maps Images

1. Image

1 Image

module Lib.Image where

This file defines the notion of image in univalent mathematics, and the associated notion of surjectiveness of a function. These notions are defined using propositional truncation as they would give too much structure to the function otherwise.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Stdlib.Prelude
import Lib.PropTrunc
import Lib.Prop.Equiv
import Lib.Prop.Levels

1.2 Image

im (A X : U) (f : A → X) : U =
  Σ X (λx. Prop-trunc (Fib A X f x))

im/inclusion (A X : U) (f : A → X) : im A X f → X =
  λt. t.1

im/q (A X : U) (f : A → X) : A → im A X f =
  λx. (f x, Prop-trunc/unit (x, refl X (f x)))

Moreover, the composition of the inclusion function and of q is f.

im/htpy (A X : U) (f : A → X) : Htpy' A X (λx. im/inclusion A X f (im/q A X f x)) f =
  λx. refl X (f x)

im/htpy' (A X : U) (f : A → X) : Htpy' A X f (λx. im/inclusion A X f (im/q A X f x)) =
  λx. refl X (f x)

Furthermore, image inclusion is injective.

im/is-injective (A X : U) (f : A → X) (t u : im A X f) (p : Path X (im/inclusion A X f t) (im/inclusion A X f u)) : Path (im A X f) t u =
  SgPath-prop X
    ( λx. Prop-trunc (Fib A X f x))
    ( λx. Prop-trunc/is-prop (Fib A X f x))
    t u p

Note that if X is a set, then the image of a map to X is a set.

im/Set (A : U) (X : UU-Set) (f : A → Set/type X) : UU-Set =
  Set/closed-Σ X
    ( λx. Prop/Set (Prop-trunc/Prop (Fib A (Set/type X) f x)))

im/is-set (A : U) (X : UU-Set) (f : A → Set/type X) : is-set (im A (Set/type X) f) =
  Set/is-set
    ( im/Set A X f)

1.3 Surjection

A map f : A → B is surjective if for all b : B, there exists an unspecified x such that f x = b.

is-surj (A B : U) (f : A → B) : U =
  (b : B) → Prop-trunc (Fib A B f b)

is-surj lives in the universe of propositions.

is-surj/is-prop (A B : U) (f : A → B) : is-prop (is-surj A B f) =
  is-prop/pi B
    ( λb. Prop-trunc (Fib A B f b))
    ( λb. Prop-trunc/is-prop (Fib A B f b))

is-surj/Prop (A B : U) (f : A → B) : UU-Prop =
  ( is-surj A B f,
    is-surj/is-prop A B f)

The image quotient is surjective.

im/q/is-surj (A X : U) (f : A → X) : is-surj A (im A X f) (im/q A X f) =
  λt.
    rec-Prop-trunc
      ( Fib A X f t.1)
      ( Prop-trunc/Prop (Fib A (im A X f) (im/q A X f) t))
      ( λu.
        Prop-trunc/unit
        ( u.1,
          SgPath-prop X
            ( λz. Prop-trunc (Fib A X f z))
            ( λz. Prop-trunc/is-prop (Fib A X f z)) t
            ( im/q A X f u.1)
            ( u.2))) t.2

The composition of two surjective maps is surjective.

is-surj/comp (A B C : U) (g : B → C) (is-surj-g : is-surj B C g) (f : A → B) (is-surj-f : is-surj A B f)
                    : is-surj A C (λx. g (f x)) =
  λc.
    rec-Prop-trunc
    ( Fib B C g c)
    ( Prop-trunc/Prop (Fib A C (λx. g (f x)) c))
    ( λt. rec-Prop-trunc
          ( Fib A B f t.1)
          ( Prop-trunc/Prop (Fib A C (λx. g (f x)) c))
          ( λu.
              Prop-trunc/unit
              ( u.1,
                comp C c
                ( g t.1) t.2
                ( g (f u.1))
                ( ap B C g t.1 (f u.1) u.2))) (is-surj-f t.1))
    ( is-surj-g c)

1.4 injection implies propositional fibrations

If f : A → B is injective, then the fibrations of f are a proposition.

is-inj/is-prop-fib (A B : U) (f : A → B) (is-inj-f : (x y : A) → Path B (f x) (f y) → Path A x y)
                   (is-set-B : is-set B) (y : B) : is-prop (Fib A B f y) =
  λt u.
    SgPath-prop A
    ( λx. Path B y (f x))
    ( λx. is-set-B y (f x)) t u
    ( is-inj-f t.1 u.1
      ( comp B
        ( f t.1) y
        ( inv B y (f t.1) t.2)
        ( f u.1) u.2))

1.5 injection + surjection = equivalence

We show that if a map f is injective and surjective and its codomain is a set, then it is an equivalence. In fact, we do not need that the codomain is a set but it greatly simplifies the proof and it's the only case used in this formalization.

is-inj-is-surj/is-equiv (A B : U) (is-set-B : is-set B) (f : A → B) (is-surj-f : is-surj A B f) (is-inj-f : (x y : A) → Path B (f x) (f y) → Path A x y)
                             : is-equiv A B f =
  λy.
    rec-Prop-trunc
    ( Fib A B f y)
    ( is-contr (Fib A B f y),
      is-contr/is-prop (Fib A B f y))
    ( λv.
      let p : is-prop (Fib A B f y) =
      ( λt u.
        SgPath-prop A
        ( λx. Path B y (f x))
        ( λx. is-set-B y (f x)) t u
        ( is-inj-f t.1 u.1
        ( comp B (f t.1) y
          ( inv B y (f t.1) t.2)
          ( f u.1) u.2))) in
        ( v, p v))
    ( is-surj-f y)

1.6 Image of `Unit`

If f : Unit → A, then the image is contractible whenever A is a set.

im-Unit/is-contr (A : U) (H : is-set A) (f : Unit → A) : is-contr (im Unit A f) =
  is-prop/is-proof-irrelevant
    ( im Unit A f)
    ( λt u.
        SgPath-prop A
        ( λx. Prop-trunc (Fib Unit A f x))
        ( λx. Prop-trunc/is-prop (Fib Unit A f x)) t u
        ( rec-Prop-trunc
          ( Fib Unit A f t.1)
          ( Set/eq/Prop
            ( A, H) t.1 u.1)
          ( λv. rec-Prop-trunc
                ( Fib Unit A f u.1)
                ( Set/eq/Prop
                  ( A, H) t.1 u.1)
                ( λw. comp-n A three-Nat t.1
                      ( f v.1) v.2
                      ( f w.1)
                      ( ap Unit A f v.1 w.1
                        ( is-contr/all-elements-equal Unit
                          ( Unit/is-contr) v.1 w.1)) u.1
                      ( inv A u.1 (f w.1) w.2)) u.2) t.2))
    ( im/q Unit A f star)