The loop homotopy on the circle

Content created by Fredrik Bakke.

Created on 2024-06-04.
Last modified on 2024-06-04.

module synthetic-homotopy-theory.loop-homotopy-circle where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.negated-equality
open import foundation.negation
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps

open import synthetic-homotopy-theory.circle

Idea

The loop homotopy on the circle is the family of equalities

  loop-htpy-𝕊¹ : (x : 𝕊¹) → x ＝ x

defined by transporting along the loop of the circle. This homotopy is distinct from the constant homotopy and has winding number 1.

Definitions

The loop homotopy on the circle

loop-htpy-𝕊¹ : (x : 𝕊¹) → x ＝ x
loop-htpy-𝕊¹ =
  function-apply-dependent-universal-property-𝕊¹
    ( eq-value id id)
    ( loop-𝕊¹)
    ( map-compute-dependent-identification-eq-value-id-id
      ( loop-𝕊¹)
      ( loop-𝕊¹)
      ( loop-𝕊¹)
      ( refl))

compute-base-loop-htpy-𝕊¹ : loop-htpy-𝕊¹ base-𝕊¹ ＝ loop-𝕊¹
compute-base-loop-htpy-𝕊¹ =
  base-dependent-universal-property-𝕊¹
    ( eq-value id id)
    ( loop-𝕊¹)
    ( map-compute-dependent-identification-eq-value-id-id
      ( loop-𝕊¹)
      ( loop-𝕊¹)
      ( loop-𝕊¹)
      ( refl))

Properties

The loop homotopy on the circle is nontrivial

abstract
  is-not-refl-ev-base-loop-htpy-𝕊¹ : loop-htpy-𝕊¹ base-𝕊¹ ≠ refl
  is-not-refl-ev-base-loop-htpy-𝕊¹ p =
    is-nontrivial-loop-𝕊¹ (inv compute-base-loop-htpy-𝕊¹ ∙ p)

is-nontrivial-loop-htpy-𝕊¹' : ¬ (loop-htpy-𝕊¹ ~ refl-htpy)
is-nontrivial-loop-htpy-𝕊¹' H =
  is-not-refl-ev-base-loop-htpy-𝕊¹ (H base-𝕊¹)

is-nontrivial-loop-htpy-𝕊¹ : loop-htpy-𝕊¹ ≠ refl-htpy
is-nontrivial-loop-htpy-𝕊¹ =
  nonequal-Π loop-htpy-𝕊¹ refl-htpy base-𝕊¹ is-not-refl-ev-base-loop-htpy-𝕊¹

Recent changes