Isomorphisms in precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-13.
Last modified on 2024-02-06.

module category-theory.isomorphisms-in-precategories where
Imports
open import category-theory.precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

Idea

An isomorphism in a precategory C is a morphism f : x → y in C for which there exists a morphism g : y → x such that f ∘ g = id and g ∘ f = id.

Definitions

The predicate of being an isomorphism in a precategory

is-iso-Precategory :
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  (f : hom-Precategory C x y) 
  UU l2
is-iso-Precategory C {x} {y} f =
  Σ ( hom-Precategory C y x)
    ( λ g 
      ( comp-hom-Precategory C f g  id-hom-Precategory C) ×
      ( comp-hom-Precategory C g f  id-hom-Precategory C))

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  {f : hom-Precategory C x y}
  where

  hom-inv-is-iso-Precategory :
    is-iso-Precategory C f  hom-Precategory C y x
  hom-inv-is-iso-Precategory = pr1

  is-section-hom-inv-is-iso-Precategory :
    (H : is-iso-Precategory C f) 
    comp-hom-Precategory C f (hom-inv-is-iso-Precategory H) 
    id-hom-Precategory C
  is-section-hom-inv-is-iso-Precategory = pr1  pr2

  is-retraction-hom-inv-is-iso-Precategory :
    (H : is-iso-Precategory C f) 
    comp-hom-Precategory C (hom-inv-is-iso-Precategory H) f 
    id-hom-Precategory C
  is-retraction-hom-inv-is-iso-Precategory = pr2  pr2

Isomorphisms in a precategory

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  (x y : obj-Precategory C)
  where

  iso-Precategory : UU l2
  iso-Precategory = Σ (hom-Precategory C x y) (is-iso-Precategory C)

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  (f : iso-Precategory C x y)
  where

  hom-iso-Precategory : hom-Precategory C x y
  hom-iso-Precategory = pr1 f

  is-iso-iso-Precategory :
    is-iso-Precategory C hom-iso-Precategory
  is-iso-iso-Precategory = pr2 f

  hom-inv-iso-Precategory : hom-Precategory C y x
  hom-inv-iso-Precategory =
    hom-inv-is-iso-Precategory C
      ( is-iso-iso-Precategory)

  is-section-hom-inv-iso-Precategory :
    ( comp-hom-Precategory C
      ( hom-iso-Precategory)
      ( hom-inv-iso-Precategory)) 
    ( id-hom-Precategory C)
  is-section-hom-inv-iso-Precategory =
    is-section-hom-inv-is-iso-Precategory C
      ( is-iso-iso-Precategory)

  is-retraction-hom-inv-iso-Precategory :
    ( comp-hom-Precategory C
      ( hom-inv-iso-Precategory)
      ( hom-iso-Precategory)) 
    ( id-hom-Precategory C)
  is-retraction-hom-inv-iso-Precategory =
    is-retraction-hom-inv-is-iso-Precategory C
      ( is-iso-iso-Precategory)

Examples

The identity isomorphisms

For any object x : A, the identity morphism id_x : hom x x is an isomorphism from x to x since id_x ∘ id_x = id_x (it is its own inverse).

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x : obj-Precategory C}
  where

  is-iso-id-hom-Precategory :
    is-iso-Precategory C (id-hom-Precategory C {x})
  pr1 is-iso-id-hom-Precategory = id-hom-Precategory C
  pr1 (pr2 is-iso-id-hom-Precategory) =
    left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
  pr2 (pr2 is-iso-id-hom-Precategory) =
    left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)

  id-iso-Precategory : iso-Precategory C x x
  pr1 id-iso-Precategory = id-hom-Precategory C
  pr2 id-iso-Precategory = is-iso-id-hom-Precategory

Equalities induce isomorphisms

An equality between objects x y : A gives rise to an isomorphism between them. This is because, by the J-rule, it is enough to construct an isomorphism given refl : x = x, from x to itself. We take the identity morphism as such an isomorphism.

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  where

  iso-eq-Precategory :
    (x y : obj-Precategory C)  x  y  iso-Precategory C x y
  pr1 (iso-eq-Precategory x y p) = hom-eq-Precategory C x y p
  pr2 (iso-eq-Precategory x .x refl) = is-iso-id-hom-Precategory C

  compute-hom-iso-eq-Precategory :
    {x y : obj-Precategory C} 
    (p : x  y) 
    hom-eq-Precategory C x y p 
    hom-iso-Precategory C (iso-eq-Precategory x y p)
  compute-hom-iso-eq-Precategory p = refl

Properties

Being an isomorphism is a proposition

Let f : hom x y and suppose g g' : hom y x are both two-sided inverses to f. It is enough to show that g = g' since the equalities are propositions (since the hom-types are sets). But we have the following chain of equalities: g = g ∘ id_y = g ∘ (f ∘ g') = (g ∘ f) ∘ g' = id_x ∘ g' = g'.

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  where

  all-elements-equal-is-iso-Precategory :
    (f : hom-Precategory C x y)
    (H K : is-iso-Precategory C f)  H  K
  all-elements-equal-is-iso-Precategory f
    (g , p , q) (g' , p' , q') =
    eq-type-subtype
      ( λ g 
        product-Prop
          ( Id-Prop
            ( hom-set-Precategory C y y)
            ( comp-hom-Precategory C f g)
            ( id-hom-Precategory C))
          ( Id-Prop
            ( hom-set-Precategory C x x)
            ( comp-hom-Precategory C g f)
            ( id-hom-Precategory C)))
      ( ( inv (right-unit-law-comp-hom-Precategory C g)) 
        ( ap ( comp-hom-Precategory C g) (inv p')) 
        ( inv (associative-comp-hom-Precategory C g f g')) 
        ( ap ( comp-hom-Precategory' C g') q) 
        ( left-unit-law-comp-hom-Precategory C g'))

  is-prop-is-iso-Precategory :
    (f : hom-Precategory C x y) 
    is-prop (is-iso-Precategory C f)
  is-prop-is-iso-Precategory f =
    is-prop-all-elements-equal
      ( all-elements-equal-is-iso-Precategory f)

  is-iso-prop-Precategory :
    (f : hom-Precategory C x y)  Prop l2
  pr1 (is-iso-prop-Precategory f) = is-iso-Precategory C f
  pr2 (is-iso-prop-Precategory f) = is-prop-is-iso-Precategory f

Equality of isomorphism is equality of their underlying morphisms

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  where

  eq-iso-eq-hom-Precategory :
    (f g : iso-Precategory C x y) 
    hom-iso-Precategory C f  hom-iso-Precategory C g  f  g
  eq-iso-eq-hom-Precategory f g =
    eq-type-subtype (is-iso-prop-Precategory C)

The type of isomorphisms form a set

The type of isomorphisms between objects x y : A is a subtype of the [foundation-core.sets.md) hom x y since being an isomorphism is a proposition.

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  where

  is-set-iso-Precategory : is-set (iso-Precategory C x y)
  is-set-iso-Precategory =
    is-set-type-subtype
      ( is-iso-prop-Precategory C)
      ( is-set-hom-Precategory C x y)

  iso-set-Precategory : Set l2
  pr1 iso-set-Precategory = iso-Precategory C x y
  pr2 iso-set-Precategory = is-set-iso-Precategory

Isomorphisms are closed under composition

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y z : obj-Precategory C}
  {g : hom-Precategory C y z}
  {f : hom-Precategory C x y}
  where

  hom-comp-is-iso-Precategory :
    is-iso-Precategory C g 
    is-iso-Precategory C f 
    hom-Precategory C z x
  hom-comp-is-iso-Precategory q p =
    comp-hom-Precategory C
      ( hom-inv-is-iso-Precategory C p)
      ( hom-inv-is-iso-Precategory C q)

  is-section-comp-is-iso-Precategory :
    (q : is-iso-Precategory C g)
    (p : is-iso-Precategory C f) 
    comp-hom-Precategory C
      ( comp-hom-Precategory C g f)
      ( hom-comp-is-iso-Precategory q p) 
    id-hom-Precategory C
  is-section-comp-is-iso-Precategory q p =
    ( associative-comp-hom-Precategory C g f _) 
    ( ap
      ( comp-hom-Precategory C g)
      ( ( inv
          ( associative-comp-hom-Precategory C f
            ( hom-inv-is-iso-Precategory C p)
            ( hom-inv-is-iso-Precategory C q))) 
        ( ap
          ( λ h 
            comp-hom-Precategory C h (hom-inv-is-iso-Precategory C q))
          ( is-section-hom-inv-is-iso-Precategory C p) 
          ( left-unit-law-comp-hom-Precategory C
            ( hom-inv-is-iso-Precategory C q))))) 
    ( is-section-hom-inv-is-iso-Precategory C q)

  is-retraction-comp-is-iso-Precategory :
    (q : is-iso-Precategory C g)
    (p : is-iso-Precategory C f) 
    ( comp-hom-Precategory C
      ( hom-comp-is-iso-Precategory q p)
      ( comp-hom-Precategory C g f)) 
    ( id-hom-Precategory C)
  is-retraction-comp-is-iso-Precategory q p =
    ( associative-comp-hom-Precategory C
      ( hom-inv-is-iso-Precategory C p)
      ( hom-inv-is-iso-Precategory C q)
      ( comp-hom-Precategory C g f)) 
    ( ap
      ( comp-hom-Precategory
        ( C)
        ( hom-inv-is-iso-Precategory C p))
      ( ( inv
          ( associative-comp-hom-Precategory C
            ( hom-inv-is-iso-Precategory C q)
            ( g)
            ( f))) 
        ( ap
            ( λ h  comp-hom-Precategory C h f)
            ( is-retraction-hom-inv-is-iso-Precategory C q)) 
        ( left-unit-law-comp-hom-Precategory C f))) 
    ( is-retraction-hom-inv-is-iso-Precategory C p)

  is-iso-comp-is-iso-Precategory :
    is-iso-Precategory C g  is-iso-Precategory C f 
    is-iso-Precategory C (comp-hom-Precategory C g f)
  pr1 (is-iso-comp-is-iso-Precategory q p) =
    hom-comp-is-iso-Precategory q p
  pr1 (pr2 (is-iso-comp-is-iso-Precategory q p)) =
    is-section-comp-is-iso-Precategory q p
  pr2 (pr2 (is-iso-comp-is-iso-Precategory q p)) =
    is-retraction-comp-is-iso-Precategory q p

The composition operation on isomorphisms

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y z : obj-Precategory C}
  (g : iso-Precategory C y z)
  (f : iso-Precategory C x y)
  where

  hom-comp-iso-Precategory :
    hom-Precategory C x z
  hom-comp-iso-Precategory =
    comp-hom-Precategory C
      ( hom-iso-Precategory C g)
      ( hom-iso-Precategory C f)

  is-iso-comp-iso-Precategory :
    is-iso-Precategory C hom-comp-iso-Precategory
  is-iso-comp-iso-Precategory =
    is-iso-comp-is-iso-Precategory C
      ( is-iso-iso-Precategory C g)
      ( is-iso-iso-Precategory C f)

  comp-iso-Precategory : iso-Precategory C x z
  pr1 comp-iso-Precategory = hom-comp-iso-Precategory
  pr2 comp-iso-Precategory = is-iso-comp-iso-Precategory

  hom-inv-comp-iso-Precategory : hom-Precategory C z x
  hom-inv-comp-iso-Precategory =
    hom-inv-iso-Precategory C comp-iso-Precategory

  is-section-inv-comp-iso-Precategory :
    ( comp-hom-Precategory C
      ( hom-comp-iso-Precategory)
      ( hom-inv-comp-iso-Precategory)) 
    ( id-hom-Precategory C)
  is-section-inv-comp-iso-Precategory =
    is-section-hom-inv-iso-Precategory C comp-iso-Precategory

  is-retraction-inv-comp-iso-Precategory :
    ( comp-hom-Precategory C
      ( hom-inv-comp-iso-Precategory)
      ( hom-comp-iso-Precategory)) 
    ( id-hom-Precategory C)
  is-retraction-inv-comp-iso-Precategory =
    is-retraction-hom-inv-iso-Precategory C comp-iso-Precategory

Inverses of isomorphisms are isomorphisms

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  {f : hom-Precategory C x y}
  where

  is-iso-inv-is-iso-Precategory :
    (p : is-iso-Precategory C f) 
    is-iso-Precategory C (hom-inv-iso-Precategory C (f , p))
  pr1 (is-iso-inv-is-iso-Precategory p) = f
  pr1 (pr2 (is-iso-inv-is-iso-Precategory p)) =
    is-retraction-hom-inv-is-iso-Precategory C p
  pr2 (pr2 (is-iso-inv-is-iso-Precategory p)) =
    is-section-hom-inv-is-iso-Precategory C p

Inverses of isomorphisms

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  where

  inv-iso-Precategory :
    iso-Precategory C x y  iso-Precategory C y x
  pr1 (inv-iso-Precategory f) = hom-inv-iso-Precategory C f
  pr2 (inv-iso-Precategory f) =
    is-iso-inv-is-iso-Precategory C (is-iso-iso-Precategory C f)

  is-iso-inv-iso-Precategory :
    (f : iso-Precategory C x y) 
    is-iso-Precategory C (hom-inv-iso-Precategory C f)
  is-iso-inv-iso-Precategory f =
    is-iso-iso-Precategory C (inv-iso-Precategory f)

Groupoid laws of isomorphisms in precategories

Composition of isomorphisms satisfies the unit laws

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  (f : iso-Precategory C x y)
  where

  left-unit-law-comp-iso-Precategory :
    comp-iso-Precategory C (id-iso-Precategory C) f  f
  left-unit-law-comp-iso-Precategory =
    eq-iso-eq-hom-Precategory C
      ( comp-iso-Precategory C (id-iso-Precategory C) f)
      ( f)
      ( left-unit-law-comp-hom-Precategory C
        ( hom-iso-Precategory C f))

  right-unit-law-comp-iso-Precategory :
    comp-iso-Precategory C f (id-iso-Precategory C)  f
  right-unit-law-comp-iso-Precategory =
    eq-iso-eq-hom-Precategory C
      ( comp-iso-Precategory C f (id-iso-Precategory C))
      ( f)
      ( right-unit-law-comp-hom-Precategory C
        ( hom-iso-Precategory C f))

Composition of isomorphisms is associative

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y z w : obj-Precategory C}
  (h : iso-Precategory C z w)
  (g : iso-Precategory C y z)
  (f : iso-Precategory C x y)
  where

  associative-comp-iso-Precategory :
    ( comp-iso-Precategory C (comp-iso-Precategory C h g) f) 
    ( comp-iso-Precategory C h (comp-iso-Precategory C g f))
  associative-comp-iso-Precategory =
    eq-iso-eq-hom-Precategory C
      ( comp-iso-Precategory C (comp-iso-Precategory C h g) f)
      ( comp-iso-Precategory C h (comp-iso-Precategory C g f))
      ( associative-comp-hom-Precategory C
        ( hom-iso-Precategory C h)
        ( hom-iso-Precategory C g)
        ( hom-iso-Precategory C f))

Composition of isomorphisms satisfies inverse laws

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  (f : iso-Precategory C x y)
  where

  left-inverse-law-comp-iso-Precategory :
    ( comp-iso-Precategory C (inv-iso-Precategory C f) f) 
    ( id-iso-Precategory C)
  left-inverse-law-comp-iso-Precategory =
    eq-iso-eq-hom-Precategory C
      ( comp-iso-Precategory C (inv-iso-Precategory C f) f)
      ( id-iso-Precategory C)
      ( is-retraction-hom-inv-iso-Precategory C f)

  right-inverse-law-comp-iso-Precategory :
    ( comp-iso-Precategory C f (inv-iso-Precategory C f)) 
    ( id-iso-Precategory C)
  right-inverse-law-comp-iso-Precategory =
    eq-iso-eq-hom-Precategory C
      ( comp-iso-Precategory C f (inv-iso-Precategory C f))
      ( id-iso-Precategory C)
      ( is-section-hom-inv-iso-Precategory C f)

The inverse operation is a fibered involution on isomorphisms

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  where

  is-fibered-involution-inv-iso-Precategory :
    {x y : obj-Precategory C} 
    inv-iso-Precategory C {y} {x}  inv-iso-Precategory C {x} {y} ~ id
  is-fibered-involution-inv-iso-Precategory f = refl

  is-equiv-inv-iso-Precategory :
    {x y : obj-Precategory C}  is-equiv (inv-iso-Precategory C {x} {y})
  is-equiv-inv-iso-Precategory =
    is-equiv-is-invertible
      ( inv-iso-Precategory C)
      ( is-fibered-involution-inv-iso-Precategory)
      ( is-fibered-involution-inv-iso-Precategory)

  equiv-inv-iso-Precategory :
    {x y : obj-Precategory C}  iso-Precategory C x y  iso-Precategory C y x
  pr1 equiv-inv-iso-Precategory = inv-iso-Precategory C
  pr2 equiv-inv-iso-Precategory = is-equiv-inv-iso-Precategory

A morphism f is an isomorphism if and only if precomposition by f is an equivalence

Proof: If f is an isomorphism with inverse f⁻¹, then precomposing with f⁻¹ is an inverse of precomposing with f. The only interesting direction is therefore the converse.

Suppose that precomposing with f is an equivalence, for any object z. Then

  - ∘ f : hom y x → hom x x

is an equivalence. In particular, there is a unique morphism g : y → x such that g ∘ f = id. Thus we have a retraction of f. To see that g is also a section, note that the map

  - ∘ f : hom y y → hom x y

is an equivalence. In particular, it is injective. Therefore it suffices to show that (f ∘ g) ∘ f = id ∘ f. To see this, we calculate

  (f ∘ g) ∘ f = f ∘ (g ∘ f) = f ∘ id = f = id ∘ f.

This completes the proof.

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  {f : hom-Precategory C x y}
  (H : (z : obj-Precategory C)  is-equiv (precomp-hom-Precategory C f z))
  where

  hom-inv-is-iso-is-equiv-precomp-hom-Precategory : hom-Precategory C y x
  hom-inv-is-iso-is-equiv-precomp-hom-Precategory =
    map-inv-is-equiv (H x) (id-hom-Precategory C)

  is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Precategory :
    ( comp-hom-Precategory C
      ( hom-inv-is-iso-is-equiv-precomp-hom-Precategory)
      ( f)) 
    ( id-hom-Precategory C)
  is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Precategory =
    is-section-map-inv-is-equiv (H x) (id-hom-Precategory C)

  is-section-hom-inv-is-iso-is-equiv-precomp-hom-Precategory :
    ( comp-hom-Precategory C
      ( f)
      ( hom-inv-is-iso-is-equiv-precomp-hom-Precategory)) 
    ( id-hom-Precategory C)
  is-section-hom-inv-is-iso-is-equiv-precomp-hom-Precategory =
    is-injective-is-equiv
      ( H y)
      ( ( associative-comp-hom-Precategory C
          ( f)
          ( hom-inv-is-iso-is-equiv-precomp-hom-Precategory)
          ( f)) 
        ( ap
          ( comp-hom-Precategory C f)
          ( is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Precategory)) 
        ( right-unit-law-comp-hom-Precategory C f) 
        ( inv (left-unit-law-comp-hom-Precategory C f)))

  is-iso-is-equiv-precomp-hom-Precategory : is-iso-Precategory C f
  pr1 is-iso-is-equiv-precomp-hom-Precategory =
    hom-inv-is-iso-is-equiv-precomp-hom-Precategory
  pr1 (pr2 is-iso-is-equiv-precomp-hom-Precategory) =
    is-section-hom-inv-is-iso-is-equiv-precomp-hom-Precategory
  pr2 (pr2 is-iso-is-equiv-precomp-hom-Precategory) =
    is-retraction-hom-inv-is-iso-is-equiv-precomp-hom-Precategory

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  {f : hom-Precategory C x y}
  (is-iso-f : is-iso-Precategory C f)
  (z : obj-Precategory C)
  where

  map-inv-precomp-hom-is-iso-Precategory :
    hom-Precategory C x z  hom-Precategory C y z
  map-inv-precomp-hom-is-iso-Precategory =
    precomp-hom-Precategory C (hom-inv-is-iso-Precategory C is-iso-f) z

  is-section-map-inv-precomp-hom-is-iso-Precategory :
    is-section
      ( precomp-hom-Precategory C f z)
      ( map-inv-precomp-hom-is-iso-Precategory)
  is-section-map-inv-precomp-hom-is-iso-Precategory g =
    ( associative-comp-hom-Precategory C
      ( g)
      ( hom-inv-is-iso-Precategory C is-iso-f)
      ( f)) 
    ( ap
      ( comp-hom-Precategory C g)
      ( is-retraction-hom-inv-is-iso-Precategory C is-iso-f)) 
    ( right-unit-law-comp-hom-Precategory C g)

  is-retraction-map-inv-precomp-hom-is-iso-Precategory :
    is-retraction
      ( precomp-hom-Precategory C f z)
      ( map-inv-precomp-hom-is-iso-Precategory)
  is-retraction-map-inv-precomp-hom-is-iso-Precategory g =
    ( associative-comp-hom-Precategory C
      ( g)
      ( f)
      ( hom-inv-is-iso-Precategory C is-iso-f)) 
    ( ap
      ( comp-hom-Precategory C g)
      ( is-section-hom-inv-is-iso-Precategory C is-iso-f)) 
    ( right-unit-law-comp-hom-Precategory C g)

  is-equiv-precomp-hom-is-iso-Precategory :
    is-equiv (precomp-hom-Precategory C f z)
  is-equiv-precomp-hom-is-iso-Precategory =
    is-equiv-is-invertible
      ( map-inv-precomp-hom-is-iso-Precategory)
      ( is-section-map-inv-precomp-hom-is-iso-Precategory)
      ( is-retraction-map-inv-precomp-hom-is-iso-Precategory)

  equiv-precomp-hom-is-iso-Precategory :
    hom-Precategory C y z  hom-Precategory C x z
  pr1 equiv-precomp-hom-is-iso-Precategory =
    precomp-hom-Precategory C f z
  pr2 equiv-precomp-hom-is-iso-Precategory =
    is-equiv-precomp-hom-is-iso-Precategory

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  (f : iso-Precategory C x y)
  (z : obj-Precategory C)
  where

  is-equiv-precomp-hom-iso-Precategory :
    is-equiv (precomp-hom-Precategory C (hom-iso-Precategory C f) z)
  is-equiv-precomp-hom-iso-Precategory =
    is-equiv-precomp-hom-is-iso-Precategory C (is-iso-iso-Precategory C f) z

  equiv-precomp-hom-iso-Precategory :
    hom-Precategory C y z  hom-Precategory C x z
  equiv-precomp-hom-iso-Precategory =
    equiv-precomp-hom-is-iso-Precategory C (is-iso-iso-Precategory C f) z

A morphism f is an isomorphism if and only if postcomposition by f is an equivalence

Proof: If f is an isomorphism with inverse f⁻¹, then postcomposing with f⁻¹ is an inverse of postcomposing with f. The only interesting direction is therefore the converse.

Suppose that postcomposing with f is an equivalence, for any object z. Then

  f ∘ - : hom y x → hom y y

is an equivalence. In particular, there is a unique morphism g : y → x such that f ∘ g = id. Thus we have a section of f. To see that g is also a retraction, note that the map

  f ∘ - : hom x x → hom x y

is an equivalence. In particular, it is injective. Therefore it suffices to show that f ∘ (g ∘ f) = f ∘ id. To see this, we calculate

  f ∘ (g ∘ f) = (f ∘ g) ∘ f = id ∘ f = f = f ∘ id.

This completes the proof.

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  {f : hom-Precategory C x y}
  (H : (z : obj-Precategory C)  is-equiv (postcomp-hom-Precategory C f z))
  where

  hom-inv-is-iso-is-equiv-postcomp-hom-Precategory : hom-Precategory C y x
  hom-inv-is-iso-is-equiv-postcomp-hom-Precategory =
    map-inv-is-equiv (H y) (id-hom-Precategory C)

  is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Precategory :
    ( comp-hom-Precategory C
      ( f)
      ( hom-inv-is-iso-is-equiv-postcomp-hom-Precategory)) 
    ( id-hom-Precategory C)
  is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Precategory =
    is-section-map-inv-is-equiv (H y) (id-hom-Precategory C)

  is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Precategory :
    comp-hom-Precategory C
      ( hom-inv-is-iso-is-equiv-postcomp-hom-Precategory)
      ( f) 
    ( id-hom-Precategory C)
  is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Precategory =
    is-injective-is-equiv
      ( H x)
      ( ( inv
          ( associative-comp-hom-Precategory C
            ( f)
            ( hom-inv-is-iso-is-equiv-postcomp-hom-Precategory)
            ( f))) 
        ( ap
          ( comp-hom-Precategory' C f)
          ( is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Precategory)) 
        ( left-unit-law-comp-hom-Precategory C f) 
        ( inv (right-unit-law-comp-hom-Precategory C f)))

  is-iso-is-equiv-postcomp-hom-Precategory : is-iso-Precategory C f
  pr1 is-iso-is-equiv-postcomp-hom-Precategory =
    hom-inv-is-iso-is-equiv-postcomp-hom-Precategory
  pr1 (pr2 is-iso-is-equiv-postcomp-hom-Precategory) =
    is-section-hom-inv-is-iso-is-equiv-postcomp-hom-Precategory
  pr2 (pr2 is-iso-is-equiv-postcomp-hom-Precategory) =
    is-retraction-hom-inv-is-iso-is-equiv-postcomp-hom-Precategory

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  {f : hom-Precategory C x y}
  (is-iso-f : is-iso-Precategory C f)
  (z : obj-Precategory C)
  where

  map-inv-postcomp-hom-is-iso-Precategory :
    hom-Precategory C z y  hom-Precategory C z x
  map-inv-postcomp-hom-is-iso-Precategory =
    postcomp-hom-Precategory C (hom-inv-is-iso-Precategory C is-iso-f) z

  is-section-map-inv-postcomp-hom-is-iso-Precategory :
    is-section
      ( postcomp-hom-Precategory C f z)
      ( map-inv-postcomp-hom-is-iso-Precategory)
  is-section-map-inv-postcomp-hom-is-iso-Precategory g =
    ( inv
      ( associative-comp-hom-Precategory C
        ( f)
        ( hom-inv-is-iso-Precategory C is-iso-f)
        ( g))) 
    ( ap
      ( comp-hom-Precategory' C g)
      ( is-section-hom-inv-is-iso-Precategory C is-iso-f)) 
    ( left-unit-law-comp-hom-Precategory C g)

  is-retraction-map-inv-postcomp-hom-is-iso-Precategory :
    is-retraction
      ( postcomp-hom-Precategory C f z)
      ( map-inv-postcomp-hom-is-iso-Precategory)
  is-retraction-map-inv-postcomp-hom-is-iso-Precategory g =
    ( inv
      ( associative-comp-hom-Precategory C
        ( hom-inv-is-iso-Precategory C is-iso-f)
        ( f)
        ( g))) 
    ( ap
      ( comp-hom-Precategory' C g)
      ( is-retraction-hom-inv-is-iso-Precategory C is-iso-f)) 
    ( left-unit-law-comp-hom-Precategory C g)

  is-equiv-postcomp-hom-is-iso-Precategory :
    is-equiv (postcomp-hom-Precategory C f z)
  is-equiv-postcomp-hom-is-iso-Precategory =
    is-equiv-is-invertible
      ( map-inv-postcomp-hom-is-iso-Precategory)
      ( is-section-map-inv-postcomp-hom-is-iso-Precategory)
      ( is-retraction-map-inv-postcomp-hom-is-iso-Precategory)

  equiv-postcomp-hom-is-iso-Precategory :
    hom-Precategory C z x  hom-Precategory C z y
  pr1 equiv-postcomp-hom-is-iso-Precategory =
    postcomp-hom-Precategory C f z
  pr2 equiv-postcomp-hom-is-iso-Precategory =
    is-equiv-postcomp-hom-is-iso-Precategory

module _
  {l1 l2 : Level}
  (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  (f : iso-Precategory C x y)
  (z : obj-Precategory C)
  where

  is-equiv-postcomp-hom-iso-Precategory :
    is-equiv (postcomp-hom-Precategory C (hom-iso-Precategory C f) z)
  is-equiv-postcomp-hom-iso-Precategory =
    is-equiv-postcomp-hom-is-iso-Precategory C (is-iso-iso-Precategory C f) z

  equiv-postcomp-hom-iso-Precategory :
    hom-Precategory C z x  hom-Precategory C z y
  equiv-postcomp-hom-iso-Precategory =
    equiv-postcomp-hom-is-iso-Precategory C (is-iso-iso-Precategory C f) z

When hom x y is a proposition, The type of isomorphisms from x to y is a proposition

The type of isomorphisms between objects x y : A is a subtype of hom x y, so when this type is a proposition, then the type of isomorphisms from x to y form a proposition.

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  where

  is-prop-iso-is-prop-hom-Precategory :
    is-prop (hom-Precategory C x y)  is-prop (iso-Precategory C x y)
  is-prop-iso-is-prop-hom-Precategory =
    is-prop-type-subtype (is-iso-prop-Precategory C)

  iso-prop-is-prop-hom-Precategory :
    is-prop (hom-Precategory C x y)  Prop l2
  pr1 (iso-prop-is-prop-hom-Precategory is-prop-hom-C-x-y) =
    iso-Precategory C x y
  pr2 (iso-prop-is-prop-hom-Precategory is-prop-hom-C-x-y) =
    is-prop-iso-is-prop-hom-Precategory is-prop-hom-C-x-y

When hom x y and hom y x are propositions, it suffices to provide a morphism in each direction to construct an isomorphism

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  {x y : obj-Precategory C}
  where

  is-iso-is-prop-hom-Precategory' :
    is-prop (hom-Precategory C x x) 
    is-prop (hom-Precategory C y y) 
    (f : hom-Precategory C x y) 
    hom-Precategory C y x 
    is-iso-Precategory C f
  pr1 (is-iso-is-prop-hom-Precategory' _ _ f g) = g
  pr1 (pr2 (is-iso-is-prop-hom-Precategory' _ is-prop-hom-C-y-y f g)) =
    eq-is-prop is-prop-hom-C-y-y
  pr2 (pr2 (is-iso-is-prop-hom-Precategory' is-prop-hom-C-x-x _ f g)) =
    eq-is-prop is-prop-hom-C-x-x

  iso-is-prop-hom-Precategory' :
    is-prop (hom-Precategory C x x) 
    is-prop (hom-Precategory C y y) 
    hom-Precategory C x y 
    hom-Precategory C y x 
    iso-Precategory C x y
  pr1 (iso-is-prop-hom-Precategory' _ _ f g) = f
  pr2 (iso-is-prop-hom-Precategory' is-prop-hom-C-x-x is-prop-hom-C-y-y f g) =
    is-iso-is-prop-hom-Precategory' is-prop-hom-C-x-x is-prop-hom-C-y-y f g

  is-iso-is-prop-hom-Precategory :
    ((x' y' : obj-Precategory C)  is-prop (hom-Precategory C x' y')) 
    (f : hom-Precategory C x y)  hom-Precategory C y x 
    is-iso-Precategory C f
  is-iso-is-prop-hom-Precategory is-prop-hom-C =
    is-iso-is-prop-hom-Precategory' (is-prop-hom-C x x) (is-prop-hom-C y y)

  iso-is-prop-hom-Precategory :
    ((x' y' : obj-Precategory C)  is-prop (hom-Precategory C x' y')) 
    hom-Precategory C x y 
    hom-Precategory C y x 
    iso-Precategory C x y
  iso-is-prop-hom-Precategory is-prop-hom-C =
    iso-is-prop-hom-Precategory' (is-prop-hom-C x x) (is-prop-hom-C y y)

Functoriality of iso-eq

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  {x y z : obj-Precategory C}
  where

  preserves-concat-iso-eq-Precategory :
    (p : x  y) (q : y  z) 
    iso-eq-Precategory C x z (p  q) 
    comp-iso-Precategory C
      ( iso-eq-Precategory C y z q)
      ( iso-eq-Precategory C x y p)
  preserves-concat-iso-eq-Precategory refl q =
    inv (right-unit-law-comp-iso-Precategory C (iso-eq-Precategory C y z q))

Recent changes