Currying a loop direction of generalized loops

Mathlib's generalized loops Ω^ N X x are the maps I^N → X sending the cube boundary to x. Reindexing the cube directions along M ≃ N is a homeomorphism GenLoop.congr, and Mathlib's GenLoop.genLoopGenLoopEquiv curries Ω^ M (Ω^ N X x) const ≃ₜ Ω^ (M ⊕ N) X x. This file specializes the latter to a single extra direction, which is the path parameter of the loop space Ω X x: cube loops in the directions M of Ω X x, based at the constant loop, are cube loops of X in the directions M ⊕ Fin 1, and, for Fin k, in k + 1 directions. These are statements about the topology of spaces of cube loops, and use no homotopy groups.

Main declarations

• GenLoop.genLoopLoopSumHomeomorph: Ω^ M (Ω X x) (refl x) ≃ₜ Ω^ (M ⊕ Fin 1) X x.
• GenLoop.genLoopLoopHomeomorph: Ω^ (Fin k) (Ω X x) (refl x) ≃ₜ Ω^ (Fin (k + 1)) X x.

@[simp]

theorem GenLoop.congr_apply {M : Type u_1} {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} (e : M ≃ N) (p : ↑(GenLoop M X x)) (t : N → ↑unitInterval) : ((congr x e) p) t = p fun (m : M) => t (e m)

@[simp]

theorem GenLoop.genLoopGenLoopEquiv_apply {M : Type u_1} {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} (p : ↑(GenLoop M (↑(GenLoop N X x)) const)) (y : M ⊕ N → ↑unitInterval) : ((genLoopGenLoopEquiv x) p) y = (p fun (m : M) => y (Sum.inl m)) fun (n : N) => y (Sum.inr n)

def GenLoop.genLoopLoopSumHomeomorph {X : Type u_3} [TopologicalSpace X] (x : X) (M : Type u_5) : ↑(GenLoop M (LoopSpace X x) (Path.refl x)) ≃ₜ ↑(GenLoop (M ⊕ Fin 1) X x)

Currying one extra cube direction: cube loops in the directions M of the loop space Ω X x, based at the constant loop, are cube loops of X in the directions M ⊕ Fin 1.

@[simp]

theorem GenLoop.genLoopLoopSumHomeomorph_apply {X : Type u_3} [TopologicalSpace X] (x : X) (M : Type u_5) (p : ↑(GenLoop M (LoopSpace X x) (Path.refl x))) (t : M ⊕ Fin 1 → ↑unitInterval) : ((genLoopLoopSumHomeomorph x M) p) t = (p fun (i : M) => t (Sum.inl i)) (t (Sum.inr 0))

The extra cube direction of genLoopLoopSumHomeomorph is the path parameter.

@[simp]

theorem GenLoop.genLoopLoopSumHomeomorph_const {X : Type u_3} [TopologicalSpace X] (x : X) (M : Type u_5) : (genLoopLoopSumHomeomorph x M) const = const

The homeomorphism genLoopLoopSumHomeomorph is based: it carries the constant cube loop to the constant cube loop.

@[simp]

theorem GenLoop.genLoopLoopSumHomeomorph_symm_const {X : Type u_3} [TopologicalSpace X] (x : X) (M : Type u_5) : (genLoopLoopSumHomeomorph x M).symm const = const

The inverse of genLoopLoopSumHomeomorph also carries the constant cube loop to the constant cube loop.

@[simp]

theorem GenLoop.genLoopLoopSumHomeomorph_symm_apply {X : Type u_3} [TopologicalSpace X] (x : X) (M : Type u_5) (q : ↑(GenLoop (M ⊕ Fin 1) X x)) (s : M → ↑unitInterval) (u : ↑unitInterval) : (((genLoopLoopSumHomeomorph x M).symm q) s) u = q (Sum.elim s fun (x : Fin 1) => u)

The inverse of genLoopLoopSumHomeomorph evaluated at the cube coordinates s in the directions M and the path parameter u.

theorem ContinuousMap.genLoopLoopSumHomeomorph_map {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (F : C(LoopSpace X x, LoopSpace Y y)) (hFf : ∀ (γ : LoopSpace X x) (t : ↑unitInterval), (F γ) t = f (γ t)) (M : Type u_5) (p : ↑(GenLoop M (LoopSpace X x) (Path.refl x))) : (GenLoop.genLoopLoopSumHomeomorph y M) (GenLoop.map F ⋯ p) = GenLoop.map f hf ((GenLoop.genLoopLoopSumHomeomorph x M) p)

Naturality of the currying homeomorphism: genLoopLoopSumHomeomorph commutes with the maps induced on cube loops by a based continuous map f : X → Y, and by any map F of loop spaces that postcomposes loops with f, for any index type of cube directions.

def GenLoop.genLoopLoopHomeomorph {X : Type u_3} [TopologicalSpace X] (x : X) (k : ℕ) : ↑(GenLoop (Fin k) (LoopSpace X x) (Path.refl x)) ≃ₜ ↑(GenLoop (Fin (k + 1)) X x)

Currying the last cube direction: cube loops in k directions of the loop space Ω X x, based at the constant loop, are cube loops of X in k + 1 directions. This is genLoopLoopSumHomeomorph with the directions Fin k ⊕ Fin 1 identified with Fin (k + 1).

theorem GenLoop.genLoopLoopHomeomorph_apply_eq {X : Type u_3} [TopologicalSpace X] (x : X) (k : ℕ) (p : ↑(GenLoop (Fin k) (LoopSpace X x) (Path.refl x))) : (genLoopLoopHomeomorph x k) p = (congr x finSumFinEquiv) ((genLoopLoopSumHomeomorph x (Fin k)) p)

genLoopLoopHomeomorph is genLoopLoopSumHomeomorph followed by the reindexing of the cube directions Fin k ⊕ Fin 1 ≃ Fin (k + 1).

@[simp]

theorem GenLoop.genLoopLoopHomeomorph_apply {X : Type u_3} [TopologicalSpace X] (x : X) (k : ℕ) (p : ↑(GenLoop (Fin k) (LoopSpace X x) (Path.refl x))) (t : Fin (k + 1) → ↑unitInterval) : ((genLoopLoopHomeomorph x k) p) t = (p fun (i : Fin k) => t i.castSucc) (t (Fin.last k))

The last cube direction of genLoopLoopHomeomorph is the path parameter.

@[simp]

theorem GenLoop.genLoopLoopHomeomorph_const {X : Type u_3} [TopologicalSpace X] (x : X) (k : ℕ) : (genLoopLoopHomeomorph x k) const = const

The homeomorphism genLoopLoopHomeomorph is based: it carries the constant cube loop to the constant cube loop.

@[simp]

theorem GenLoop.genLoopLoopHomeomorph_symm_const {X : Type u_3} [TopologicalSpace X] (x : X) (k : ℕ) : (genLoopLoopHomeomorph x k).symm const = const

The inverse of genLoopLoopHomeomorph also carries the constant cube loop to the constant cube loop.

@[simp]

theorem GenLoop.genLoopLoopHomeomorph_symm_apply {X : Type u_3} [TopologicalSpace X] (x : X) (k : ℕ) (q : ↑(GenLoop (Fin (k + 1)) X x)) (s : Fin k → ↑unitInterval) (u : ↑unitInterval) : (((genLoopLoopHomeomorph x k).symm q) s) u = q (Fin.snoc s u)

The inverse of genLoopLoopHomeomorph evaluated at the first k coordinates s and the path parameter u.

Concatenation under reindexing and currying

@[simp]

theorem GenLoop.congr_transAt {M : Type u_1} {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} [DecidableEq M] [DecidableEq N] (e : M ≃ N) (i : M) (p q : ↑(GenLoop M X x)) : (congr x e) (transAt i p q) = transAt (e i) ((congr x e) p) ((congr x e) q)

Reindexing carries a concatenation in the cube direction i to a concatenation in the direction e i.

@[simp]

theorem GenLoop.genLoopGenLoopEquiv_transAt {M : Type u_1} {N : Type u_2} {X : Type u_3} [TopologicalSpace X] {x : X} [DecidableEq M] [DecidableEq N] (i : M) (p q : ↑(GenLoop M (↑(GenLoop N X x)) const)) : (genLoopGenLoopEquiv x) (transAt i p q) = transAt (Sum.inl i) ((genLoopGenLoopEquiv x) p) ((genLoopGenLoopEquiv x) q)

Currying carries a concatenation in the cube direction i of the outer cube to a concatenation in the direction Sum.inl i.

theorem ContinuousMap.genLoopLoopHomeomorph_map {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (F : C(LoopSpace X x, LoopSpace Y y)) (hFf : ∀ (γ : LoopSpace X x) (t : ↑unitInterval), (F γ) t = f (γ t)) (k : ℕ) (p : ↑(GenLoop (Fin k) (LoopSpace X x) (Path.refl x))) : (GenLoop.genLoopLoopHomeomorph y k) (GenLoop.map F ⋯ p) = GenLoop.map f hf ((GenLoop.genLoopLoopHomeomorph x k) p)

Naturality of the currying homeomorphism for k cube directions: the specialization of ContinuousMap.genLoopLoopSumHomeomorph_map to Fin k.