Isomorphisms in precategories

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

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

Idea

An isomorphism between objects x y : A in a precategory C is a morphism f : hom x y for which there exists a morphism g : hom y x such that

  • G ∘ F = id_x and
  • F ∘ G = id_y.

Definition

The property of being an isomorphism

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

  is-iso-Precategory :
    {x y : obj-Precategory C} (f : type-hom-Precategory C x y) → UU l2
  is-iso-Precategory {x} {y} f =
    Σ ( type-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))

  hom-inv-is-iso-Precategory :
    {x y : obj-Precategory C} {f : type-hom-Precategory C x y} →
    is-iso-Precategory f → type-hom-Precategory C y x
  hom-inv-is-iso-Precategory H = pr1 H

  issec-hom-inv-is-iso-Precategory :
    {x y : obj-Precategory C} {f : type-hom-Precategory C x y}
    (H : is-iso-Precategory f) →
    comp-hom-Precategory C f (hom-inv-is-iso-Precategory H) ＝
    id-hom-Precategory C
  issec-hom-inv-is-iso-Precategory H = pr1 (pr2 H)

  isretr-hom-inv-is-iso-Precategory :
    {x y : obj-Precategory C} {f : type-hom-Precategory C x y}
    (H : is-iso-Precategory f) →
    comp-hom-Precategory C (hom-inv-is-iso-Precategory H) f ＝
    id-hom-Precategory C
  isretr-hom-inv-is-iso-Precategory H = pr2 (pr2 H)

  abstract
    is-proof-irrelevant-is-iso-Precategory :
      {x y : obj-Precategory C} (f : type-hom-Precategory C x y) →
      is-proof-irrelevant (is-iso-Precategory f)
    pr1 (is-proof-irrelevant-is-iso-Precategory f H) = H
    pr2
      ( is-proof-irrelevant-is-iso-Precategory {x} {y} f
        ( pair g (pair p q)))
        ( pair g' (pair p' q')) =
      eq-type-subtype
        ( λ h →
          prod-Prop
            ( Id-Prop
              ( hom-Precategory C y y)
              ( comp-hom-Precategory C f h)
              ( id-hom-Precategory C))
            ( Id-Prop
              ( hom-Precategory C x x)
              ( comp-hom-Precategory C h 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 :
      {x y : obj-Precategory C} (f : type-hom-Precategory C x y) →
      is-prop (is-iso-Precategory f)
    is-prop-is-iso-Precategory f =
      is-prop-is-proof-irrelevant (is-proof-irrelevant-is-iso-Precategory f)

  is-iso-Precategory-Prop :
    {x y : obj-Precategory C} (f : type-hom-Precategory C x y) → Prop l2
  pr1 (is-iso-Precategory-Prop f) = is-iso-Precategory f
  pr2 (is-iso-Precategory-Prop f) = is-prop-is-iso-Precategory f

The type of isomorphisms between two objects in a precategory

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

  iso-Precategory : (x y : obj-Precategory C) → UU l2
  iso-Precategory x y = type-subtype (is-iso-Precategory-Prop C {x} {y})

  hom-iso-Precategory :
    {x y : obj-Precategory C} →
    iso-Precategory x y → type-hom-Precategory C x y
  hom-iso-Precategory f = inclusion-subtype (is-iso-Precategory-Prop C) f

  is-iso-hom-iso-Precategory :
    {x y : obj-Precategory C} (f : iso-Precategory x y) →
    is-iso-Precategory C (hom-iso-Precategory f)
  is-iso-hom-iso-Precategory f =
    is-in-subtype-inclusion-subtype (is-iso-Precategory-Prop C) f

  hom-inv-iso-Precategory :
    {x y : obj-Precategory C} →
    iso-Precategory x y → type-hom-Precategory C y x
  hom-inv-iso-Precategory f = pr1 (is-iso-hom-iso-Precategory f)

  issec-hom-inv-iso-Precategory :
    {x y : obj-Precategory C} (f : iso-Precategory x y) →
    ( comp-hom-Precategory C
      ( hom-iso-Precategory f)
      ( hom-inv-iso-Precategory f)) ＝
    ( id-hom-Precategory C)
  issec-hom-inv-iso-Precategory f = pr1 (pr2 (is-iso-hom-iso-Precategory f))

  isretr-hom-inv-iso-Precategory :
    {x y : obj-Precategory C} (f : iso-Precategory x y) →
    ( comp-hom-Precategory C
      ( hom-inv-iso-Precategory f)
      ( hom-iso-Precategory f)) ＝
    ( id-hom-Precategory C)
  isretr-hom-inv-iso-Precategory f = pr2 (pr2 (is-iso-hom-iso-Precategory f))

Examples

The identity morphisms are 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)
  where

  is-iso-id-hom-Precategory :
    {x : obj-Precategory C} → 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 : {x : obj-Precategory C} → iso-Precategory C x x
  pr1 id-iso-Precategory = id-hom-Precategory C
  pr2 id-iso-Precategory = is-iso-id-hom-Precategory

Equalities give rise to 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 : Id x x, from x to itself. We take the identity morphism as such an isomorphism.

iso-eq-Precategory :
  {l1 l2 : Level} (C : Precategory l1 l2) →
  (x y : obj-Precategory C) → x ＝ y → iso-Precategory C x y
iso-eq-Precategory C x .x refl = id-iso-Precategory C

Properties

The property of 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)
  where

The type of isomorphisms form a set

The type of isomorphisms between objects x y : A is a subtype of the set hom x y since being an isomorphism is a proposition.

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

  is-set-iso-Precategory :
    (x y : obj-Precategory C) → is-set (iso-Precategory C x y)
  is-set-iso-Precategory x y =
    is-set-type-subtype
      ( is-iso-Precategory-Prop C)
      ( is-set-type-hom-Precategory C x y)

  iso-Precategory-Set : (x y : obj-Precategory C) → Set l2
  pr1 (iso-Precategory-Set x y) = iso-Precategory C x y
  pr2 (iso-Precategory-Set x y) = is-set-iso-Precategory x y

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

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

  precomp-hom-inv-is-iso-Precategory :
    (H : is-iso-Precategory C f) (z : obj-Precategory C) →
    type-hom-Precategory C x z → type-hom-Precategory C y z
  precomp-hom-inv-is-iso-Precategory H z =
    precomp-hom-Precategory C (hom-inv-is-iso-Precategory C H) z

  issec-precomp-hom-inv-is-iso-Precategory :
    (H : is-iso-Precategory C f) (z : obj-Precategory C) →
    ( precomp-hom-Precategory C f z ∘ precomp-hom-inv-is-iso-Precategory H z) ~
    ( id)
  issec-precomp-hom-inv-is-iso-Precategory H z g =
    equational-reasoning
      comp-hom-Precategory
        ( C)
        ( comp-hom-Precategory C g (hom-inv-is-iso-Precategory C H))
        ( f)
      ＝ comp-hom-Precategory
          ( C)
          ( g)
          ( comp-hom-Precategory C (hom-inv-is-iso-Precategory C H) f)
        by
        associative-comp-hom-Precategory C g (hom-inv-is-iso-Precategory C H) f
      ＝ comp-hom-Precategory C g (id-hom-Precategory C)
        by ap (comp-hom-Precategory C g) (isretr-hom-inv-is-iso-Precategory C H)
      ＝ g
        by right-unit-law-comp-hom-Precategory C g

  isretr-precomp-hom-inv-is-iso-Precategory :
    (H : is-iso-Precategory C f) (z : obj-Precategory C) →
    ( precomp-hom-inv-is-iso-Precategory H z ∘ precomp-hom-Precategory C f z) ~
    ( id)
  isretr-precomp-hom-inv-is-iso-Precategory H z g =
    equational-reasoning
      comp-hom-Precategory
        ( C)
        ( comp-hom-Precategory C g f)
        ( hom-inv-is-iso-Precategory C H)
      ＝ comp-hom-Precategory
          ( C)
          ( g)
          ( comp-hom-Precategory C f (hom-inv-is-iso-Precategory C H))
        by
        associative-comp-hom-Precategory C g f (hom-inv-is-iso-Precategory C H)
      ＝ comp-hom-Precategory C g (id-hom-Precategory C)
        by ap (comp-hom-Precategory C g) (issec-hom-inv-is-iso-Precategory C H)
      ＝ g
        by right-unit-law-comp-hom-Precategory C g

  is-equiv-precomp-is-iso-Precategory :
    (H : is-iso-Precategory C f) (z : obj-Precategory C) →
    is-equiv (precomp-hom-Precategory C f z)
  is-equiv-precomp-is-iso-Precategory H z =
    is-equiv-has-inverse
      ( precomp-hom-inv-is-iso-Precategory H z)
      ( issec-precomp-hom-inv-is-iso-Precategory H z)
      ( isretr-precomp-hom-inv-is-iso-Precategory H z)