Powers of loops
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-04-26.
Last modified on 2023-07-19.
module synthetic-homotopy-theory.powers-of-loops where
Imports
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 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 = ap (concat' (point-Pointed-Type A) refl) (power-nat-refl-Ω n A)
ωⁿ⁺¹ = ωⁿ ∙ ω
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 ω = ( ap (concat' (point-Pointed-Type A) ω) (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 ω = ( ap (concat' (point-Pointed-Type A) ω) (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 ω) ∙ ( ( ap ( concat' (point-Pointed-Type A) (power-nat-Ω n A ω)) ( power-nat-mul-Ω m 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 (power-nat-Ω n A ω) ω) ∙ ( ap ( concat' (point-Pointed-Type B) (map-Ω f ω)) ( map-power-nat-Ω n f ω))
Recent changes
- 2023-07-19. Egbert Rijke. refactoring pointed maps (#682).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-05-03. Fredrik Bakke. Define the smash product of pointed types and refactor pointed types (#583).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).