Transporting a generalized loop along a path

Let γ : Path x y and let f : Ω^ N X x be a generalized loop based at x. This file constructs the generalized loop TauCeti.GenLoop.transport γ f : Ω^ N X y obtained by shrinking f into the half-size cube and running γ outwards along the resulting collar, together with the homotopy realising the deformation, and proves that this construction is canonical: any homotopy whose boundary traces γ ends, up to homotopy relative to the cube boundary, at transport γ f.

Everything is written in terms of the radial coordinate TauCeti.cubeRadius of TauCeti/Topology/Homotopy/Cube/Radius.lean, which is 1 exactly on Cube.boundary N. The basic gadget is TauCeti.collar: given a radius function r ≥ 1/2, an inner family F of maps on the cube and an outer family G of paths, it returns the map sending a point of radius at most r to F at the point rescaled by 1 / r, and a point of radius u > r to G at the reparametrised time 2 - 2 * r / u. The two branches agree where u = r, because rescaling by 1 / r lands on the cube boundary, where F is required to equal G at time 0.

With the shrinking radius r t = (2 - t) / 2 this is the collar homotopy TauCeti.GenLoop.collarHomotopy γ f, which starts at f, traces γ on the cube boundary, and ends at the transported loop, which is defined as its value at time 1.

TauCeti.GenLoop.HomotopyAlong γ f g packages the data of a homotopy from f to g whose restriction to the cube boundary is γ. Canonicity, HomotopyAlong.homotopic_transport, is the homotopy extension property of the pair (I^N, Cube.boundary N) in the only form needed here. It is proved by a file-local map cubeTopFaceRetract : C(I^N, I × (I^N)): the restriction to the top face {1} × I^N of the radial projection of the cylinder I × I^N away from the point at height 2 above the centre of the cube. That projection lands in the union of the bottom face {0} × I^N and the sides I × Cube.boundary N, and is the identity there, so its restriction to the top face fixes the cube boundary. Composing a homotopy along γ with it reproduces transport γ f on the nose, and the straight-line homotopy in the convex cylinder from the inclusion of the top face to it is stationary on the cube boundary, so it descends to a homotopy relative to the boundary.

Main declarations

• TauCeti.collar: the collar construction on a parametrised family.
• TauCeti.GenLoop.collarHomotopy: the collar homotopy attached to γ and f.
• TauCeti.GenLoop.transport: the generalized loop f transported along γ.
• TauCeti.GenLoop.HomotopyAlong: a homotopy of generalized loops whose boundary traces γ.
• TauCeti.GenLoop.collarHomotopyAlong: the collar homotopy, as such a homotopy.
• TauCeti.GenLoop.HomotopyAlong.homotopic_transport: any homotopy along γ starting at f ends at a loop homotopic to transport γ f.

References

This is the analytic core of the base-point-change isomorphisms of higher homotopy groups requested in TauCetiRoadmap/UniversalCovers/README.md, Stage 3, item 9. The construction is the classical one; see Hatcher, Algebraic Topology, Section 4.1.

The collar construction

noncomputable def TauCeti.collar {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {P : Type u_3} [TopologicalSpace P] (r : C(P, ℝ)) (F : C(P × (N → ↑unitInterval), X)) (G : C(P × ↑unitInterval, X)) (hr : ∀ (p : P), 1 / 2 ≤ r p) (hFG : ∀ (p : P), ∀ z ∈ Cube.boundary N, F (p, z) = G (p, 0)) : C(P × (N → ↑unitInterval), X)

The collar construction. Given a radius function r ≥ 1/2, a family F of maps on the cube and a family G of paths agreeing with F on the cube boundary at time 0, this sends a cube point of radius at most r to F at the point rescaled by 1 / r, and a cube point of larger radius u to G at the time 2 - 2 * r / u.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.collar_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {P : Type u_3} [TopologicalSpace P] (r : C(P, ℝ)) (F : C(P × (N → ↑unitInterval), X)) (G : C(P × ↑unitInterval, X)) (hr : ∀ (p : P), 1 / 2 ≤ r p) (hFG : ∀ (p : P), ∀ z ∈ Cube.boundary N, F (p, z) = G (p, 0)) (p : P) (z : N → ↑unitInterval) : (collar r F G hr hFG) (p, z) = if cubeRadius z ≤ r p then F (p, cubeScale (1 / r p) z) else G (p, Set.projIcc 0 1 ⋯ (2 - 2 * r p / max (cubeRadius z) (1 / 2)))

The collar homotopy and the transported loop

noncomputable def TauCeti.GenLoop.collarHomotopy {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) : C(↑unitInterval × (N → ↑unitInterval), X)

The collar homotopy of a generalized loop f along a path γ: at time t it is f shrunk into the cube of radius (2 - t) / 2, with γ restricted to [0, t] filling the collar outside.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.GenLoop.collarHomotopy_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) (t : ↑unitInterval) (z : N → ↑unitInterval) : (collarHomotopy γ f) (t, z) = if cubeRadius z ≤ (2 - ↑t) / 2 then f (cubeScale (1 / ((2 - ↑t) / 2)) z) else γ (Set.projIcc 0 1 ⋯ (2 - 2 * ((2 - ↑t) / 2) / max (cubeRadius z) (1 / 2)))

@[simp]

theorem TauCeti.GenLoop.collarHomotopy_zero {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) (z : N → ↑unitInterval) : (collarHomotopy γ f) (0, z) = f z

theorem TauCeti.GenLoop.collarHomotopy_boundary {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) (t : ↑unitInterval) {z : N → ↑unitInterval} (hz : z ∈ Cube.boundary N) : (collarHomotopy γ f) (t, z) = γ t

On the cube boundary the collar homotopy traces the path γ.

noncomputable def TauCeti.GenLoop.transport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) : ↑(GenLoop N X y)

The generalized loop f transported along the path γ: the value at time 1 of the collar homotopy, a generalized loop based at the far endpoint of γ.

Equations

• TauCeti.GenLoop.transport γ f = ⟨(TauCeti.GenLoop.collarHomotopy γ f).curry 1, ⋯⟩

theorem TauCeti.GenLoop.transport_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) (z : N → ↑unitInterval) : (transport γ f) z = (collarHomotopy γ f) (1, z)

theorem TauCeti.GenLoop.transport_apply_eq {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) (z : N → ↑unitInterval) : (transport γ f) z = if cubeRadius z ≤ 1 / 2 then f (cubeScale 2 z) else γ (Set.projIcc 0 1 ⋯ (2 - 1 / max (cubeRadius z) (1 / 2)))

The radial retraction of the cylinder

Homotopies along a path, and canonicity of the transported loop

structure TauCeti.GenLoop.HomotopyAlong {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) (g : ↑(GenLoop N X y)) extends (↑f).Homotopy ↑g : Type (max u_1 u_2)

A homotopy from a generalized loop f based at x to a generalized loop g based at y whose restriction to the cube boundary traces the path γ from x to y.

• toFun : ↑unitInterval × (N → ↑unitInterval) → X
• continuous_toFun : Continuous self.toFun
• map_zero_left (x : N → ↑unitInterval) : self.toFun (0, x) = ↑f x
• map_one_left (x : N → ↑unitInterval) : self.toFun (1, x) = ↑g x
• map_boundary (t : ↑unitInterval) (z : N → ↑unitInterval) : z ∈ Cube.boundary N → self.toHomotopy (t, z) = γ t

  on the cube boundary the homotopy traces γ

@[instance_reducible]

instance TauCeti.GenLoop.HomotopyAlong.instFunLike {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} {f : ↑(GenLoop N X x)} {g : ↑(GenLoop N X y)} : FunLike (HomotopyAlong γ f g) (↑unitInterval × (N → ↑unitInterval)) X

Equations

• TauCeti.GenLoop.HomotopyAlong.instFunLike = { coe := fun (h : TauCeti.GenLoop.HomotopyAlong γ f g) => ⇑h.toHomotopy, coe_injective := ⋯ }

instance TauCeti.GenLoop.HomotopyAlong.instHomotopyLikeForallElemRealUnitIntervalValContinuousMapMemSetGenLoop {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} {f : ↑(GenLoop N X x)} {g : ↑(GenLoop N X y)} : ContinuousMap.HomotopyLike (HomotopyAlong γ f g) ↑f ↑g

def TauCeti.GenLoop.HomotopyAlong.ofHomotopyRel {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} {f g : ↑(GenLoop N X x)} (K : (↑f).HomotopyRel (↑g) (Cube.boundary N)) : HomotopyAlong (Path.refl x) f g

A homotopy relative to the cube boundary is a homotopy along the constant path: the base point does not move.

Equations

• TauCeti.GenLoop.HomotopyAlong.ofHomotopyRel K = { toHomotopy := K.toHomotopy, map_boundary := ⋯ }

noncomputable def TauCeti.GenLoop.collarHomotopyAlong {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) : HomotopyAlong γ f (transport γ f)

The collar homotopy is a homotopy along γ from f to the transported loop.

Equations

• TauCeti.GenLoop.collarHomotopyAlong γ f = { toContinuousMap := TauCeti.GenLoop.collarHomotopy γ f, map_zero_left := ⋯, map_one_left := ⋯, map_boundary := ⋯ }

theorem TauCeti.GenLoop.HomotopyAlong.homotopic_transport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} {f : ↑(GenLoop N X x)} {g : ↑(GenLoop N X y)} (h : HomotopyAlong γ f g) : GenLoop.Homotopic g (transport γ f)

Canonicity of the transported loop. A homotopy along γ starting at f ends at a generalized loop homotopic, relative to the cube boundary, to transport γ f.