Concatenation and reversal of maps out of a cube

Mathlib concatenates and reverses generalized loops I^N → X along a direction j : N of the cube (GenLoop.transAt, GenLoop.symmAt), using that they are constant on the boundary. This file does the same for arbitrary continuous maps Z × I^N → Y, with an extra parameter space Z:

• TauCeti.cubeTransAt j f g h runs f on the half t j ≤ 1 / 2 and g on the other half, when the face t j = 1 of f agrees with the face t j = 0 of g (the hypothesis h);
• TauCeti.cubeSymmAt j f reverses f by t j ↦ 1 - t j.

Both operations preserve maps of pairs (I × I^N, ∂(I × I^N)) → (Y, B) (TauCeti.mapsTo_cubeTransAt, TauCeti.mapsTo_cubeSymmAt), and concatenating two homotopies through maps of pairs that agree on the common face gives a homotopy through maps of pairs between the concatenations (TauCeti.homotopicWith_cubeTransAt). For relative cubes they are TauCeti.RelGenLoop.transAt and TauCeti.RelGenLoop.symmAt, which is how the group laws of relative homotopy groups extend to maps of pairs that are not relative cubes.

Main definitions and results

• TauCeti.cubeTransAt, TauCeti.cubeSymmAt: concatenation and reversal along a direction of the cube, with their faces TauCeti.cubeTransAt_update_zero, TauCeti.cubeTransAt_update_one, TauCeti.cubeSymmAt_update_zero, TauCeti.cubeSymmAt_update_one, and the involution TauCeti.cubeSymmAt_cubeSymmAt.
• TauCeti.mapsTo_cubeTransAt, TauCeti.mapsTo_cubeSymmAt: both preserve maps of pairs.
• TauCeti.homotopicWith_cubeTransAt: concatenation of homotopies through maps of pairs.

noncomputable def TauCeti.cubeTransAt {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f g : C(Z × (N → ↑unitInterval), Y)) (h : ∀ (s : Z) (t : N → ↑unitInterval), f (s, Function.update t j 1) = g (s, Function.update t j 0)) : C(Z × (N → ↑unitInterval), Y)

Concatenation of two maps f g : Z × I^N → Y along a direction j : N of the cube I^N, when the face t j = 1 of f agrees with the face t j = 0 of g: the map runs f on the half t j ≤ 1 / 2 and g on the other half, both reparametrised. For relative cubes this is TauCeti.RelGenLoop.transAt (TauCeti.RelGenLoop.coe_transAt).

theorem TauCeti.cubeTransAt_apply {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f g : C(Z × (N → ↑unitInterval), Y)) (h : ∀ (s : Z) (t : N → ↑unitInterval), f (s, Function.update t j 1) = g (s, Function.update t j 0)) (w : Z × (N → ↑unitInterval)) : (cubeTransAt j f g h) w = if ↑(w.2 j) ≤ 1 / 2 then f (w.1, Function.update w.2 j (Set.projIcc 0 1 ⋯ (2 * ↑(w.2 j)))) else g (w.1, Function.update w.2 j (Set.projIcc 0 1 ⋯ (2 * ↑(w.2 j) - 1)))

@[simp]

theorem TauCeti.cubeTransAt_update_zero {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f g : C(Z × (N → ↑unitInterval), Y)) (h : ∀ (s : Z) (t : N → ↑unitInterval), f (s, Function.update t j 1) = g (s, Function.update t j 0)) (s : Z) (t : N → ↑unitInterval) : (cubeTransAt j f g h) (s, Function.update t j 0) = f (s, Function.update t j 0)

The face t j = 0 of the concatenation along j is the face t j = 0 of the first map.

@[simp]

theorem TauCeti.cubeTransAt_update_one {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f g : C(Z × (N → ↑unitInterval), Y)) (h : ∀ (s : Z) (t : N → ↑unitInterval), f (s, Function.update t j 1) = g (s, Function.update t j 0)) (s : Z) (t : N → ↑unitInterval) : (cubeTransAt j f g h) (s, Function.update t j 1) = g (s, Function.update t j 1)

The face t j = 1 of the concatenation along j is the face t j = 1 of the second map.

def TauCeti.cubeSymmAt {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f : C(Z × (N → ↑unitInterval), Y)) : C(Z × (N → ↑unitInterval), Y)

Reversal of a map f : Z × I^N → Y along a direction j : N of the cube I^N, by t j ↦ 1 - t j. For relative cubes this is TauCeti.RelGenLoop.symmAt (TauCeti.RelGenLoop.coe_symmAt).

theorem TauCeti.cubeSymmAt_apply {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f : C(Z × (N → ↑unitInterval), Y)) (w : Z × (N → ↑unitInterval)) : (cubeSymmAt j f) w = f (w.1, fun (i : N) => if i = j then unitInterval.symm (w.2 j) else w.2 i)

@[simp]

theorem TauCeti.cubeSymmAt_update_zero {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f : C(Z × (N → ↑unitInterval), Y)) (s : Z) (t : N → ↑unitInterval) : (cubeSymmAt j f) (s, Function.update t j 0) = f (s, Function.update t j 1)

Reversal along j exchanges the faces t j = 0 and t j = 1.

@[simp]

theorem TauCeti.cubeSymmAt_update_one {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f : C(Z × (N → ↑unitInterval), Y)) (s : Z) (t : N → ↑unitInterval) : (cubeSymmAt j f) (s, Function.update t j 1) = f (s, Function.update t j 0)

Reversal along j exchanges the faces t j = 1 and t j = 0.

@[simp]

theorem TauCeti.cubeSymmAt_cubeSymmAt {N : Type u_1} {Z : Type u_2} {Y : Type u_3} [TopologicalSpace Z] [TopologicalSpace Y] [DecidableEq N] (j : N) (f : C(Z × (N → ↑unitInterval), Y)) : cubeSymmAt j (cubeSymmAt j f) = f

Reversal along a direction is an involution.

theorem TauCeti.mapsTo_cubeTransAt {N : Type u_1} {Y : Type u_3} [TopologicalSpace Y] [DecidableEq N] {B : Set Y} {j : N} {f g : C(↑unitInterval × (N → ↑unitInterval), Y)} (hf : Set.MapsTo (⇑f) (Cube.prodBoundary N) B) (hg : Set.MapsTo (⇑g) (Cube.prodBoundary N) B) (h : ∀ (s : ↑unitInterval) (t : N → ↑unitInterval), f (s, Function.update t j 1) = g (s, Function.update t j 0)) : Set.MapsTo (⇑(cubeTransAt j f g h)) (Cube.prodBoundary N) B

theorem TauCeti.mapsTo_cubeSymmAt {N : Type u_1} {Y : Type u_3} [TopologicalSpace Y] [DecidableEq N] {B : Set Y} {j : N} {f : C(↑unitInterval × (N → ↑unitInterval), Y)} (hf : Set.MapsTo (⇑f) (Cube.prodBoundary N) B) : Set.MapsTo (⇑(cubeSymmAt j f)) (Cube.prodBoundary N) B

theorem TauCeti.homotopicWith_cubeTransAt {N : Type u_1} {Y : Type u_3} [TopologicalSpace Y] [DecidableEq N] {B : Set Y} {j : N} {f g f' g' : C(↑unitInterval × (N → ↑unitInterval), Y)} {h : ∀ (s : ↑unitInterval) (t : N → ↑unitInterval), f (s, Function.update t j 1) = g (s, Function.update t j 0)} {h' : ∀ (s : ↑unitInterval) (t : N → ↑unitInterval), f' (s, Function.update t j 1) = g' (s, Function.update t j 0)} (F : f.HomotopyWith f' fun (k : C(↑unitInterval × (N → ↑unitInterval), Y)) => Set.MapsTo (⇑k) (Cube.prodBoundary N) B) (G : g.HomotopyWith g' fun (k : C(↑unitInterval × (N → ↑unitInterval), Y)) => Set.MapsTo (⇑k) (Cube.prodBoundary N) B) (hFG : ∀ (t s : ↑unitInterval) (z : N → ↑unitInterval), F (t, s, Function.update z j 1) = G (t, s, Function.update z j 0)) : (cubeTransAt j f g h).HomotopicWith (cubeTransAt j f' g' h') fun (k : C(↑unitInterval × (N → ↑unitInterval), Y)) => Set.MapsTo (⇑k) (Cube.prodBoundary N) B

Concatenating along j two homotopies through maps of pairs that agree on the common face at all times gives a homotopy through maps of pairs between the concatenations.