Functoriality of the loop space operation
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Raymond Baker.
Created on 2022-03-10.
Last modified on 2023-09-10.
module synthetic-homotopy-theory.functoriality-loop-spaces where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.faithful-maps open import foundation.identity-types open import foundation.universe-levels open import structured-types.faithful-pointed-maps open import structured-types.pointed-equivalences open import structured-types.pointed-maps open import structured-types.pointed-types open import synthetic-homotopy-theory.loop-spaces
Idea
Any pointed map f : A →∗ B
induces a map map-Ω f : Ω A →∗ Ω B
. Furthermore,
this operation respects the groupoidal operations on loop spaces.
Definition
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) where map-Ω : type-Ω A → type-Ω B map-Ω p = tr-type-Ω ( preserves-point-pointed-map f) ( ap (map-pointed-map f) p) preserves-refl-map-Ω : Id (map-Ω refl) refl preserves-refl-map-Ω = preserves-refl-tr-Ω (pr2 f) pointed-map-Ω : Ω A →∗ Ω B pointed-map-Ω = pair map-Ω preserves-refl-map-Ω preserves-mul-map-Ω : (x y : type-Ω A) → Id (map-Ω (mul-Ω A x y)) (mul-Ω B (map-Ω x) (map-Ω y)) preserves-mul-map-Ω x y = ( ap ( tr-type-Ω (preserves-point-pointed-map f)) ( ap-concat (map-pointed-map f) x y)) ∙ ( preserves-mul-tr-Ω ( preserves-point-pointed-map f) ( ap (map-pointed-map f) x) ( ap (map-pointed-map f) y)) preserves-inv-map-Ω : (x : type-Ω A) → Id (map-Ω (inv-Ω A x)) (inv-Ω B (map-Ω x)) preserves-inv-map-Ω x = ( ap ( tr-type-Ω (preserves-point-pointed-map f)) ( ap-inv (map-pointed-map f) x)) ∙ ( preserves-inv-tr-Ω ( preserves-point-pointed-map f) ( ap (map-pointed-map f) x))
Faithful pointed maps induce embeddings on loop spaces
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} where is-emb-map-Ω : (f : A →∗ B) → is-faithful (map-pointed-map f) → is-emb (map-Ω f) is-emb-map-Ω f H = is-emb-comp ( tr-type-Ω (preserves-point-pointed-map f)) ( ap (map-pointed-map f)) ( is-emb-is-equiv ( is-equiv-tr-type-Ω (preserves-point-pointed-map f))) ( H (point-Pointed-Type A) (point-Pointed-Type A)) emb-Ω : faithful-pointed-map A B → type-Ω A ↪ type-Ω B pr1 (emb-Ω f) = map-Ω (pointed-map-faithful-pointed-map f) pr2 (emb-Ω f) = is-emb-map-Ω ( pointed-map-faithful-pointed-map f) ( is-faithful-faithful-pointed-map f)
Pointed embeddings induce pointed equivalences on loop spaces
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) (t : is-emb (map-pointed-map f)) where is-equiv-map-Ω-emb : is-equiv (map-Ω f) is-equiv-map-Ω-emb = is-equiv-comp ( tr-type-Ω (preserves-point-pointed-map f)) ( ap (map-pointed-map f)) ( t (point-Pointed-Type A) (point-Pointed-Type A)) ( is-equiv-tr-type-Ω (preserves-point-pointed-map f)) equiv-map-Ω-emb : type-Ω A ≃ type-Ω B pr1 equiv-map-Ω-emb = map-Ω f pr2 equiv-map-Ω-emb = is-equiv-map-Ω-emb pointed-equiv-pointed-map-Ω-emb : Ω A ≃∗ Ω B pr1 pointed-equiv-pointed-map-Ω-emb = equiv-map-Ω-emb pr2 pointed-equiv-pointed-map-Ω-emb = preserves-refl-map-Ω f
the operator pointed-map-Ω
preserves equivalences
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (e : A ≃∗ B) where equiv-map-Ω-pointed-equiv : type-Ω A ≃ type-Ω B equiv-map-Ω-pointed-equiv = equiv-map-Ω-emb ( pointed-map-pointed-equiv e) ( is-emb-is-equiv (is-equiv-map-equiv-pointed-equiv e))
pointed-map-Ω
preserves pointed equivalences
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (e : A ≃∗ B) where pointed-equiv-Ω-pointed-equiv : Ω A ≃∗ Ω B pr1 pointed-equiv-Ω-pointed-equiv = equiv-map-Ω-pointed-equiv e pr2 pointed-equiv-Ω-pointed-equiv = preserves-refl-map-Ω (pointed-map-pointed-equiv e)
Recent changes
- 2023-09-10. Raymond Baker and Fredrik Bakke. Refactor shift, pointed identity types are loop spaces (#727).
- 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-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).