Pointed isomorphisms

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-03-13.
Last modified on 2024-04-11.

module structured-types.pointed-isomorphisms where
Imports 
open import foundation.cartesian-product-types
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.structure-identity-principle
open import foundation.universe-levels

open import structured-types.pointed-equivalences
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-retractions
open import structured-types.pointed-sections
open import structured-types.pointed-types

Idea

A pointed isomorphism is an isomorphism in the wild category of pointed types, i.e., it is a pointed map equipped with a pointed section and a pointed retraction.

Definitions

The predicate of being a pointed isomorphism

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  is-pointed-iso : UU (l1 ⊔ l2)
  is-pointed-iso = pointed-section f × pointed-retraction f

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {f : A →∗ B}
  (H : is-pointed-iso f)
  where

  pointed-section-is-pointed-iso : pointed-section f
  pointed-section-is-pointed-iso = pr1 H

  pointed-retraction-is-pointed-iso : pointed-retraction f
  pointed-retraction-is-pointed-iso = pr2 H

  pointed-map-pointed-section-is-pointed-iso : B →∗ A
  pointed-map-pointed-section-is-pointed-iso =
    pointed-map-pointed-section f pointed-section-is-pointed-iso

  is-pointed-section-pointed-section-is-pointed-iso :
    is-pointed-section f pointed-map-pointed-section-is-pointed-iso
  is-pointed-section-pointed-section-is-pointed-iso =
    is-pointed-section-pointed-section f
      pointed-section-is-pointed-iso

  map-pointed-section-is-pointed-iso :
    type-Pointed-Type B → type-Pointed-Type A
  map-pointed-section-is-pointed-iso =
    map-pointed-section f pointed-section-is-pointed-iso

  preserves-point-pointed-map-pointed-section-is-pointed-iso :
    map-pointed-section-is-pointed-iso (point-Pointed-Type B) ＝
    point-Pointed-Type A
  preserves-point-pointed-map-pointed-section-is-pointed-iso =
    preserves-point-pointed-map-pointed-section f
      pointed-section-is-pointed-iso

  is-section-pointed-section-is-pointed-iso :
    is-section (map-pointed-map f) map-pointed-section-is-pointed-iso
  is-section-pointed-section-is-pointed-iso =
    is-section-pointed-section f pointed-section-is-pointed-iso

  section-is-pointed-iso :
    section (map-pointed-map f)
  section-is-pointed-iso =
    section-pointed-section f pointed-section-is-pointed-iso

  coherence-point-is-section-pointed-section-is-pointed-iso :
    coherence-point-unpointed-htpy-pointed-Π
      ( f ∘∗ pointed-map-pointed-section-is-pointed-iso)
      ( id-pointed-map)
      ( is-section-pointed-section-is-pointed-iso)
  coherence-point-is-section-pointed-section-is-pointed-iso =
    coherence-point-is-section-pointed-section f
      pointed-section-is-pointed-iso

  pointed-map-pointed-retraction-is-pointed-iso : B →∗ A
  pointed-map-pointed-retraction-is-pointed-iso =
    pr1 pointed-retraction-is-pointed-iso

  is-pointed-retraction-pointed-retraction-is-pointed-iso :
    is-pointed-retraction f pointed-map-pointed-retraction-is-pointed-iso
  is-pointed-retraction-pointed-retraction-is-pointed-iso =
    pr2 pointed-retraction-is-pointed-iso

  map-pointed-retraction-is-pointed-iso :
    type-Pointed-Type B → type-Pointed-Type A
  map-pointed-retraction-is-pointed-iso =
    map-pointed-map pointed-map-pointed-retraction-is-pointed-iso

  preserves-point-pointed-map-pointed-retraction-is-pointed-iso :
    map-pointed-retraction-is-pointed-iso (point-Pointed-Type B) ＝
    point-Pointed-Type A
  preserves-point-pointed-map-pointed-retraction-is-pointed-iso =
    preserves-point-pointed-map
      pointed-map-pointed-retraction-is-pointed-iso

  is-retraction-pointed-retraction-is-pointed-iso :
    is-retraction
      ( map-pointed-map f)
      ( map-pointed-retraction-is-pointed-iso)
  is-retraction-pointed-retraction-is-pointed-iso =
    htpy-pointed-htpy
      is-pointed-retraction-pointed-retraction-is-pointed-iso

  retraction-is-pointed-iso :
    retraction (map-pointed-map f)
  retraction-is-pointed-iso =
    retraction-pointed-retraction f pointed-retraction-is-pointed-iso

  coherence-point-is-retraction-pointed-retraction-is-pointed-iso :
    coherence-point-unpointed-htpy-pointed-Π
      ( pointed-map-pointed-retraction-is-pointed-iso ∘∗ f)
      ( id-pointed-map)
      ( is-retraction-pointed-retraction-is-pointed-iso)
  coherence-point-is-retraction-pointed-retraction-is-pointed-iso =
    coherence-point-pointed-htpy
      is-pointed-retraction-pointed-retraction-is-pointed-iso

Pointed isomorphisms

module _
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
  where

  pointed-iso : UU (l1 ⊔ l2)
  pointed-iso = Σ (A →∗ B) is-pointed-iso

  infix 6 _≅∗_

  _≅∗_ : UU (l1 ⊔ l2)
  _≅∗_ = pointed-iso

module _
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
  (f : A ≅∗ B)
  where

  pointed-map-pointed-iso : A →∗ B
  pointed-map-pointed-iso = pr1 f

  map-pointed-iso : type-Pointed-Type A → type-Pointed-Type B
  map-pointed-iso = map-pointed-map pointed-map-pointed-iso

  preserves-point-pointed-iso :
    map-pointed-iso (point-Pointed-Type A) ＝ point-Pointed-Type B
  preserves-point-pointed-iso =
    preserves-point-pointed-map pointed-map-pointed-iso

  is-pointed-iso-pointed-iso : is-pointed-iso pointed-map-pointed-iso
  is-pointed-iso-pointed-iso = pr2 f

  pointed-section-pointed-iso : pointed-section pointed-map-pointed-iso
  pointed-section-pointed-iso =
    pointed-section-is-pointed-iso (is-pointed-iso-pointed-iso)

  pointed-retraction-pointed-iso : pointed-retraction pointed-map-pointed-iso
  pointed-retraction-pointed-iso =
    pointed-retraction-is-pointed-iso (is-pointed-iso-pointed-iso)

  pointed-map-pointed-section-pointed-iso : B →∗ A
  pointed-map-pointed-section-pointed-iso =
    pointed-map-pointed-section-is-pointed-iso (is-pointed-iso-pointed-iso)

  is-pointed-section-pointed-section-pointed-iso :
    is-pointed-section
      ( pointed-map-pointed-iso)
      ( pointed-map-pointed-section-pointed-iso)
  is-pointed-section-pointed-section-pointed-iso =
    is-pointed-section-pointed-section-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  map-pointed-section-pointed-iso :
    type-Pointed-Type B → type-Pointed-Type A
  map-pointed-section-pointed-iso =
    map-pointed-section-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  preserves-point-pointed-map-pointed-section-pointed-iso :
    map-pointed-section-pointed-iso (point-Pointed-Type B) ＝
    point-Pointed-Type A
  preserves-point-pointed-map-pointed-section-pointed-iso =
    preserves-point-pointed-map-pointed-section-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  is-section-pointed-section-pointed-iso :
    is-section (map-pointed-iso) map-pointed-section-pointed-iso
  is-section-pointed-section-pointed-iso =
    is-section-pointed-section-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  section-pointed-iso :
    section (map-pointed-iso)
  section-pointed-iso =
    section-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  coherence-point-is-section-pointed-section-pointed-iso :
    coherence-point-unpointed-htpy-pointed-Π
      ( pointed-map-pointed-iso ∘∗ pointed-map-pointed-section-pointed-iso)
      ( id-pointed-map)
      ( is-section-pointed-section-pointed-iso)
  coherence-point-is-section-pointed-section-pointed-iso =
    coherence-point-is-section-pointed-section-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  pointed-map-pointed-retraction-pointed-iso : B →∗ A
  pointed-map-pointed-retraction-pointed-iso =
    pointed-map-pointed-retraction-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  is-pointed-retraction-pointed-retraction-pointed-iso :
    is-pointed-retraction
      ( pointed-map-pointed-iso)
      ( pointed-map-pointed-retraction-pointed-iso)
  is-pointed-retraction-pointed-retraction-pointed-iso =
    is-pointed-retraction-pointed-retraction-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  map-pointed-retraction-pointed-iso :
    type-Pointed-Type B → type-Pointed-Type A
  map-pointed-retraction-pointed-iso =
    map-pointed-retraction-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  preserves-point-pointed-map-pointed-retraction-pointed-iso :
    map-pointed-retraction-pointed-iso (point-Pointed-Type B) ＝
    point-Pointed-Type A
  preserves-point-pointed-map-pointed-retraction-pointed-iso =
    preserves-point-pointed-map-pointed-retraction-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  is-retraction-pointed-retraction-pointed-iso :
    is-retraction
      ( map-pointed-iso)
      ( map-pointed-retraction-pointed-iso)
  is-retraction-pointed-retraction-pointed-iso =
    is-retraction-pointed-retraction-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  retraction-pointed-iso :
    retraction (map-pointed-iso)
  retraction-pointed-iso =
    retraction-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

  coherence-point-is-retraction-pointed-retraction-pointed-iso :
    coherence-point-unpointed-htpy-pointed-Π
      ( pointed-map-pointed-retraction-pointed-iso ∘∗ pointed-map-pointed-iso)
      ( id-pointed-map)
      ( is-retraction-pointed-retraction-pointed-iso)
  coherence-point-is-retraction-pointed-retraction-pointed-iso =
    coherence-point-is-retraction-pointed-retraction-is-pointed-iso
      ( is-pointed-iso-pointed-iso)

Properties

Any pointed equivalence is a pointed isomorphism

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  abstract
    is-pointed-iso-is-pointed-equiv :
      is-pointed-equiv f → is-pointed-iso f
    pr1 (pr1 (is-pointed-iso-is-pointed-equiv H)) =
      pointed-map-inv-is-pointed-equiv f H
    pr2 (pr1 (is-pointed-iso-is-pointed-equiv H)) =
      is-pointed-section-pointed-map-inv-is-pointed-equiv f H
    pr1 (pr2 (is-pointed-iso-is-pointed-equiv H)) =
      pointed-map-inv-is-pointed-equiv f H
    pr2 (pr2 (is-pointed-iso-is-pointed-equiv H)) =
      is-pointed-retraction-pointed-map-inv-is-pointed-equiv f H

Any pointed isomorphism is a pointed equivalence

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  abstract
    is-pointed-equiv-is-pointed-iso :
      is-pointed-iso f → is-pointed-equiv f
    pr1 (is-pointed-equiv-is-pointed-iso H) = section-is-pointed-iso H
    pr2 (is-pointed-equiv-is-pointed-iso H) = retraction-is-pointed-iso H

Being a pointed isomorphism is a property

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  abstract
    is-contr-section-is-pointed-equiv :
      is-pointed-equiv f → is-contr (pointed-section f)
    is-contr-section-is-pointed-equiv H =
      is-torsorial-Eq-structure
        ( is-contr-section-is-equiv H)
        ( map-inv-is-equiv H , is-section-map-inv-is-equiv H)
        ( is-contr-map-is-equiv
          ( is-equiv-comp _ _
            ( is-emb-is-equiv H _ _)
            ( is-equiv-concat' _ (preserves-point-pointed-map f)))
          ( _))

  abstract
    is-contr-retraction-is-pointed-equiv :
      is-pointed-equiv f → is-contr (pointed-retraction f)
    is-contr-retraction-is-pointed-equiv H =
      is-torsorial-Eq-structure
        ( is-contr-retraction-is-equiv H)
        ( map-inv-is-equiv H , is-retraction-map-inv-is-equiv H)
        ( is-contr-map-is-equiv
          ( is-equiv-concat _ _)
          ( _))

  abstract
    is-contr-is-pointed-iso-is-pointed-equiv :
      is-pointed-equiv f → is-contr (is-pointed-iso f)
    is-contr-is-pointed-iso-is-pointed-equiv H =
      is-contr-product
        ( is-contr-section-is-pointed-equiv H)
        ( is-contr-retraction-is-pointed-equiv H)

  abstract
    is-prop-is-pointed-iso : is-prop (is-pointed-iso f)
    is-prop-is-pointed-iso =
      is-prop-is-proof-irrelevant
        ( λ H →
          is-contr-is-pointed-iso-is-pointed-equiv
            ( is-pointed-equiv-is-pointed-iso f H))

Being a pointed equivalence is equivalent to being a pointed isomorphism

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  equiv-is-pointed-iso-is-pointed-equiv :
    is-pointed-equiv f ≃ (is-pointed-iso f)
  pr1 equiv-is-pointed-iso-is-pointed-equiv =
    is-pointed-iso-is-pointed-equiv f
  pr2 equiv-is-pointed-iso-is-pointed-equiv =
    is-equiv-has-converse-is-prop
      ( is-property-is-equiv (map-pointed-map f))
      ( is-prop-is-pointed-iso f)
      ( is-pointed-equiv-is-pointed-iso f)

Recent changes