Functoriality of generalized loops

Mathlib defines the generalized loop space Ω^ N X x, the maps I^N → X sending the cube boundary to x. This file supplies the map induced by a based continuous map: postcomposition sends generalized loops based at x to generalized loops based at y; it respects identity and composition, constant maps, homotopies relative to the cube boundary, and concatenation and inversion in a cube direction.

def GenLoop.map {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop N X x)) : ↑(GenLoop N Y y)

A based continuous map sends generalized loops to generalized loops by postcomposition.

@[simp]

theorem GenLoop.map_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop N X x)) (t : N → ↑unitInterval) : (map f hf p) t = f (p t)

theorem GenLoop.coe_map {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop N X x)) : ↑(map f hf p) = f.comp ↑p

The underlying continuous map of GenLoop.map f hf p is the composite f ∘ p.

theorem GenLoop.continuous_map {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) : Continuous (map f hf)

Postcomposition GenLoop.map f is continuous for the compact-open topologies on spaces of generalized loops.

@[simp]

theorem GenLoop.map_const {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) : map f hf const = const

theorem GenLoop.map_continuousMap_const {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} (y : Y) (p : ↑(GenLoop N X x)) : map (ContinuousMap.const X y) ⋯ p = const

Postcomposition by a constant map yields the constant generalized loop.

@[simp]

theorem GenLoop.map_id {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (p : ↑(GenLoop N X x)) : map (ContinuousMap.id X) ⋯ p = p

@[simp]

theorem GenLoop.map_comp {N : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {x : X} {y : Y} {z : Z} (g : C(Y, Z)) (hg : g y = z) (f : C(X, Y)) (hf : f x = y) (p : ↑(GenLoop N X x)) : map g hg (map f hf p) = map (g.comp f) ⋯ p

theorem GenLoop.map_homotopic {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {f g : ↑(GenLoop N X x)} (h : Homotopic f g) (F : C(X, Y)) (hF : F x = y) : Homotopic (map F hF f) (map F hF g)

Postcomposition preserves homotopy relative to the cube boundary.

@[simp]

theorem GenLoop.map_transAt {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] (F : C(X, Y)) (hF : F x = y) (i : N) (p q : ↑(GenLoop N X x)) : map F hF (transAt i p q) = transAt i (map F hF p) (map F hF q)

@[simp]

theorem GenLoop.map_symmAt {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [DecidableEq N] (F : C(X, Y)) (hF : F x = y) (i : N) (p : ↑(GenLoop N X x)) : map F hF (symmAt i p) = symmAt i (map F hF p)