This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Powers of loops

module synthetic-homotopy-theory.powers-of-loops where

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.equivalences
open import foundation.identity-types
open import foundation.iterating-automorphisms
open import foundation.iterating-functions
open import foundation.universe-levels
open import foundation.whiskering-identifications-concatenation

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

open import synthetic-homotopy-theory.functoriality-loop-spaces
open import synthetic-homotopy-theory.loop-spaces

Idea

The n-th power of a loop ω in a type A is defined by iterated concatenation of ω with itself.

Definitions

Powers of loops by natural numbers

power-nat-Ω :
  {l : Level} → ℕ → (A : Pointed-Type l) → type-Ω A → type-Ω A
power-nat-Ω n A ω = iterate n (concat' (point-Pointed-Type A) ω) refl

Powers of loops by integers

equiv-power-int-Ω :
  {l : Level} → ℤ → (A : Pointed-Type l) → type-Ω A → type-Ω A ≃ type-Ω A
equiv-power-int-Ω k A ω =
  iterate-automorphism-ℤ k (equiv-concat' (point-Pointed-Type A) ω)

power-int-Ω :
  {l : Level} → ℤ → (A : Pointed-Type l) → type-Ω A → type-Ω A
power-int-Ω k A ω = map-equiv (equiv-power-int-Ω k A ω) refl

Properties

reflⁿ = refl

power-nat-refl-Ω :
  {l : Level} (n : ℕ) (A : Pointed-Type l) →
  power-nat-Ω n A refl ＝ refl
power-nat-refl-Ω zero-ℕ A = refl
power-nat-refl-Ω (succ-ℕ n) A =
  right-whisker-concat (power-nat-refl-Ω n A) refl

ωⁿ⁺¹ = ωⁿ ∙ ω

power-nat-succ-Ω :
  {l : Level} (n : ℕ) (A : Pointed-Type l) (ω : type-Ω A) →
  power-nat-Ω (succ-ℕ n) A ω ＝ (power-nat-Ω n A ω ∙ ω)
power-nat-succ-Ω n A ω = refl

power-nat-succ-Ω' :
  {l : Level} (n : ℕ) (A : Pointed-Type l) (ω : type-Ω A) →
  power-nat-Ω (succ-ℕ n) A ω ＝ (ω ∙ power-nat-Ω n A ω)
power-nat-succ-Ω' zero-ℕ A ω = inv right-unit
power-nat-succ-Ω' (succ-ℕ n) A ω =
  ( right-whisker-concat (power-nat-succ-Ω' n A ω) ω) ∙
  ( assoc ω (power-nat-Ω n A ω) ω)

ωᵐ⁺ⁿ ＝ ωᵐ ∙ ωⁿ

power-nat-add-Ω :
  {l : Level} (m n : ℕ) (A : Pointed-Type l) (ω : type-Ω A) →
  power-nat-Ω (m +ℕ n) A ω ＝ (power-nat-Ω m A ω ∙ power-nat-Ω n A ω)
power-nat-add-Ω m zero-ℕ A ω = inv right-unit
power-nat-add-Ω m (succ-ℕ n) A ω =
  ( right-whisker-concat (power-nat-add-Ω m n A ω) ω) ∙
  ( assoc (power-nat-Ω m A ω) (power-nat-Ω n A ω) ω)

ωᵐⁿ = (ωᵐ)ⁿ

power-nat-mul-Ω :
  {l : Level} (m n : ℕ) (A : Pointed-Type l) (ω : type-Ω A) →
  power-nat-Ω (m *ℕ n) A ω ＝ power-nat-Ω m A (power-nat-Ω n A ω)
power-nat-mul-Ω zero-ℕ n A ω = refl
power-nat-mul-Ω (succ-ℕ m) n A ω =
  ( power-nat-add-Ω (m *ℕ n) n A ω) ∙
  ( ( right-whisker-concat
      ( power-nat-mul-Ω m n A ω)
      ( power-nat-Ω n A ω)))

power-nat-mul-Ω' :
  {l : Level} (m n : ℕ) (A : Pointed-Type l) (ω : type-Ω A) →
  power-nat-Ω (m *ℕ n) A ω ＝ power-nat-Ω n A (power-nat-Ω m A ω)
power-nat-mul-Ω' m n A ω =
  ( ap (λ u → power-nat-Ω u A ω) (commutative-mul-ℕ m n)) ∙
  ( power-nat-mul-Ω n m A ω)

The action on identifications of a function preserves powers

map-power-nat-Ω :
  {l1 l2 : Level} (n : ℕ) {A : Pointed-Type l1} {B : Pointed-Type l2}
  (f : A →∗ B) (ω : type-Ω A) →
  map-Ω f (power-nat-Ω n A ω) ＝ power-nat-Ω n B (map-Ω f ω)
map-power-nat-Ω zero-ℕ {A} {B} f ω = preserves-refl-map-Ω f
map-power-nat-Ω (succ-ℕ n) {A} {B} f ω =
  ( preserves-mul-map-Ω f) ∙
  ( right-whisker-concat (map-power-nat-Ω n f ω) (map-Ω f ω))