Bi-invertible Maps

1. Bi-invertible maps properties

1 Bi-invertible maps properties

module Lib.Prop.BiInv where

This file states and shows useful properties of bi-invertible maps.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Lib.QInv
import Lib.Data.Nat 
import Lib.Prop.Contr
import Lib.Prop.QInv

1.2 Equivalence relation

BiInv is an equivalence relation.

BiInv/sym (A B : U) (b : BiInv A B) : BiInv B A =
  ( BiInv/right-inv A B b,
    is-bi-inv/inv-is-bi-inv A B
    ( BiInv/map A B b)
    ( BiInv/is-bi-inv A B b))

1.3 `id` is bi invertible

Identity is clearly bi-invertible.

is-bi-inv/id-is-bi-inv (A : U) : is-bi-inv A A (id A) =
  ((id A, λx. refl A x), (id A, λx. refl A x))

1.4 is-bi-inv is closed for ap

-- is-bi-inv/closed-ap-tr-inv-map (A B : U) (f g : A → B) (p : Path (A → B) f g) (x y : A) (b : is-bi-inv (Path A x y) (Path B (f x) (f y)) (ap A B f x y))
--                                     : (Path B (g x) (g y)) → (Path A x y) =
--   let i : (Path B (f x) (f y)) → Path A x y = is-bi-inv/inv-map (Path A x y) (Path B (f x) (f y)) (ap A B f x y) b
--   in (tr (A → B) f g p (λh. Path B (h x) (h y) → Path A x y) i)

-- is-bi-inv/closed-ap-tr-inv-right-htpy (A B : U) (f g : A → B) (p : Path (A → B) f g) (x y : A) (b : is-bi-inv (Path A x y) (Path B (f x) (f y)) (ap A B f x y)) (q : Path B (g x) (g y))
--                                            : Path (Path B (g x) (g y))
--                                                   ((tr (A → B) f g p (λh. Path A x y → Path B (h x) (h y)) (ap A B f x y))
--                                                    (tr (A → B) f g p (λh. Path B (h x) (h y) → Path A x y) (is-bi-inv/inv-map (Path A x y) (Path B (f x) (f y)) (ap A B f x y) b) q))
--                                                   q =
--   let i : (Path B (f x) (f y)) → Path A x y = is-bi-inv/inv-map (Path A x y) (Path B (f x) (f y)) (ap A B f x y) b
--       R : Htpy' (Path B (f x) (f y)) (Path B (f x) (f y)) (λr. (ap A B f x y) (i r)) (id (Path B (f x) (f y))) = is-bi-inv/inv-right-htpy (Path A x y) (Path B (f x) (f y)) (ap A B f x y) b
--   in tr (Path B (f x) (f y)) ((ap A B f x y) (i (tr (A → B) g f (inv (A → B) f g p) (λh. Path B (h x) (h y)) q)))
--                              (tr (A → B) g f (inv (A → B) f g p) (λh. Path B (h x) (h y)) q)
--                              (R (tr (A → B) g f (inv (A → B) f g p) (λh. Path B (h x) (h y)) q))
--                              (λr.
-- is-bi-inv/closed-tr (A B : U) (f g : A → B) (p : Path (A → B) f g) (x y : A) (b : is-bi-inv (Path A x y) (Path B (f x) (f y)) (ap A B f x y))
--                          : is-bi-inv (Path A x y) (Path B (g x) (g y)) (tr (A → B) f g p (λh. Path A x y → Path B (h x) (h y)) (ap A B f x y)) =


-- is-bi-inv/is-equiv-ap-comp-right-is-bi-inv (A B : U) (g : B → A) (b : is-bi-inv B A g) (x y : A)
--                                                 : is-bi-inv (Path A x y) (Path A (g (f x)) (g (f y)))
--                                                             (ap A A (λz. g (f z)) x y) =

1.5 3-for-2 property of composition

An important property of bi-invertible maps is that, for two maps f : A \to B and g : B \to C, then if any two of

f is bi-invertible ;
g is bi-invertible ;
g \circ f is bi-invertible

hold, then the third also hold. In fact, we use the fact that it is the case for quasi-inverses. As bi-invertible maps have quasi-inverses, it also hold for bi-invertible maps.

1.5.1 Composition

is-bi-inv/comp-is-bi-inv (A B C : U) (f : A → B) (g : B → C) (b : is-bi-inv A B f) (b' : is-bi-inv B C g) : is-bi-inv A C (map/comp A B C g f) =
  has-inverse-is-bi-inv A C (map/comp A B C g f)
    (has-inverse/comp-has-inverse A B C f g
      (is-bi-inv-has-inverse A B f b)
      (is-bi-inv-has-inverse B C g b'))

1.5.2 Left map

is-bi-inv/is-bi-inv-comp-left (A B C : U) (f : A → B) (g : B → C) (b : is-bi-inv B C g) (b' : is-bi-inv A C (map/comp A B C g f)) : is-bi-inv A B f =
  has-inverse-is-bi-inv A B f
    (has-inverse/has-inverse-comp-left A B C f g
      (is-bi-inv-has-inverse B C g b)
      (is-bi-inv-has-inverse A C (map/comp A B C g f) b'))

1.5.3 Right map

is-bi-inv/is-bi-inv-comp-right (A B C : U) (f : A → B) (g : B → C) (b : is-bi-inv A B f)
                               (b' : is-bi-inv A C (map/comp A B C g f)) : is-bi-inv B C g =
  has-inverse-is-bi-inv B C g
    (has-inverse/has-inverse-comp-right A B C f g
      (is-bi-inv-has-inverse A B f b)
      (is-bi-inv-has-inverse A C (map/comp A B C g f) b'))

1.6 3-for-2 property of contraction

If there is a bi-invertible map between A and B, then one of them is contractible iff the other is also contractible.

is-bi-inv/is-contr-is-bi-inv (A B : U) (f : A → B) (b : is-bi-inv A B f) (c : is-contr B) : is-contr A =
  let g : B → A = is-bi-inv/inv-map A B f b
      L : Htpy' A A (λz. g (f z)) (id A) = is-bi-inv/inv-left-htpy A B f b
      x : A = g (center B c)
  in (x, λy. comp A x (g (f y)) (ap B A g (center B c) (f y) (contraction B c (f y)))
                    y (L y))

is-bi-inv/is-contr-is-bi-inv' (A B : U) (f : A → B) (b : is-bi-inv A B f) (c : is-contr A) : is-contr B =
  let g : B → A = is-bi-inv/inv-map A B f b
      R : Htpy' B B (λz. f (g z)) (id B) = is-bi-inv/inv-right-htpy A B f b
      L : Htpy' A A (λz. g (f z)) (id A) = is-bi-inv/inv-left-htpy A B f b
  in is-bi-inv/is-contr-is-bi-inv B A g ((f, L), (f, R)) c

Moreover, if both A and B are contractible, then there is a bi-invertible map between A and B.

is-bi-inv/is-bi-inv-contr-map (A B : U) (cB : is-contr B) : A → B =
  λ_. (center B cB)

is-bi-inv/is-bi-inv-contr-inv-map (A B : U) (cA : is-contr A) : B → A =
  λ_. (center A cA)  

is-bi-inv/is-bi-inv-contr (A B : U) (cA : is-contr A) (cB : is-contr B) : is-bi-inv A B (is-bi-inv/is-bi-inv-contr-map A B cB) =
  let f : A → B = is-bi-inv/is-bi-inv-contr-map A B cB
      g : B → A = is-bi-inv/is-bi-inv-contr-inv-map A B cA
      R : Htpy' B B (λz. f (g z)) (id B) = λx. (contraction B cB x)
      L : Htpy' A A (λz. g (f z)) (id A) = λx. (contraction A cA x)
  in ((g, R), (g, L))

is-bi-inv/is-bi-inv-contr' (A B : U) (f : A → B) (cA : is-contr A) (cB : is-contr B) : is-bi-inv A B f =
  let g : B → A = is-bi-inv/is-bi-inv-contr-inv-map A B cA
      R : Htpy' B B (λz. f (g z)) (id B) = λx. comp B (f (g x)) (center B cB) (inv B (center B cB) (f (g x)) (contraction B cB (f (g x)))) x (contraction B cB x)
      L : Htpy' A A (λz. g (f z)) (id A) = λx. (contraction A cA x)
  in ((g, R), (g, L))

1.7 Double-composition property

Assume that there are maps f : A \to B, g : B \to C and h : C \to D such that g \circ f and h \circ g are bi-invertible. We show that f, g and h are all bi-invertible.

1.7.1 `g` is injective

In this setting, we can show that g is injective. Indeed, if g x is equal to g y then h (g x) must also be equal to h (g y). By bi-invertibility of h \circ g, x is thus equal to y.

is-bi-inv-comp/injective (B C D : U) (g : B → C) (h : C → D) (K : is-bi-inv B D (map/comp B C D h g))
                         : is-injective B C g = λx y p.
  let i : D → B = is-bi-inv/inv-map B D (map/comp B C D h g) K
      q : Path D (h (g x)) (h (g y)) = ap C D h (g x) (g y) p
      r : Path B (i (h (g x))) (i (h (g y))) = ap D B i (h (g x)) (h (g y)) q
      H : Htpy B (λ_. B) (λz. i (h (g z))) (id B) = is-bi-inv/inv-left-htpy B D (map/comp B C D h g) K
  in
  comp-n B three-Nat x (i (h (g x))) (inv B (i (h (g x))) x (H x))
                       (i (h (g y))) r
                       y (H y)

1.7.2 `f` is bi-invertible

We show a more general lemma – that is, for any f : A \to B and g : B \to C such that g \circ f is bi-invertible, then f is bi-invertible whenever g is injective. Indeed, let i be the inverse of g \circ f. Then, i \circ g is the inverse of f: i \circ g \circ f is obviously the identity, and g \circ f \circ i \circ g ~ g hence the result.

is-bi-inv-comp/is-inj-is-bi-inv-left-map (A B C : U) (f : A → B) (g : B → C) (inj : is-injective B C g) (H : is-bi-inv A C (map/comp A B C g f)) : is-bi-inv A B f =
  let i : C → A = is-bi-inv/inv-map A C (map/comp A B C g f) H
      h : B → A = map/comp B C A i g
      K : Htpy B (λ_. B) (map/comp B A B f h) (id B) =
          λx. inj (f (h x)) x (is-bi-inv/inv-right-htpy A C (map/comp A B C g f) H (g x))
  in
  has-inverse-is-bi-inv A B f
                        (h, (K, is-bi-inv/inv-left-htpy A C (map/comp A B C g f) H))

We can directly conclude that f is bi-invertible.

is-bi-inv-comp/is-bi-inv-left-map (A B C D : U) (f : A → B) (g : B → C) (h : C → D) (H : is-bi-inv A C (map/comp A B C g f))
                                  (K : is-bi-inv B D (map/comp B C D h g)) : is-bi-inv A B f =
  is-bi-inv-comp/is-inj-is-bi-inv-left-map A B C f g (is-bi-inv-comp/injective B C D g h K) H

1.7.3 `g` and `h` are bi-invertible

Using the 3-for-2 property of composition, as g \circ f and f are both bi-invertible, g is also bi-invertible.

is-bi-inv-comp/is-bi-inv-middle-map (A B C D : U) (f : A → B) (g : B → C) (h : C → D) (H : is-bi-inv A C (map/comp A B C g f))
                                   (K : is-bi-inv B D (map/comp B C D h g)) : is-bi-inv B C g =
  is-bi-inv/is-bi-inv-comp-right A B C f g (is-bi-inv-comp/is-bi-inv-left-map A B C D f g h H K) H

Now that we have shown that g is bi-invertible, we can use the 3-for-2 property of composition on h \circ g and g, to conclude that h is also bi-invertible.

is-bi-inv-comp/is-bi-inv-right-map (A B C D : U) (f : A → B) (g : B → C) (h : C → D) (H : is-bi-inv A C (map/comp A B C g f))
                                   (K : is-bi-inv B D (map/comp B C D h g)) : is-bi-inv C D h =
  is-bi-inv/is-bi-inv-comp-right B C D g h (is-bi-inv-comp/is-bi-inv-middle-map A B C D f g h H K) K