Deforming the top cells of a skeleton through their characteristic maps

Let C be a relative CW complex, A a set of n-cells, and Ψ : I × Dⁿ → Dⁿ a family of maps of the closed unit ball which fix the unit sphere. Reading Ψ through the characteristic map of every cell of A, and fixing every other point, gives a family of maps TauCeti.cellDeformation A Ψ of the n-skeleton skeletonLT C (n + 1), continuous in the time and the point. Deformations of the closed unit ball fixing its boundary therefore become deformations of the n-skeleton supported in the open cells of A.

Main definitions

• TauCeti.cellDeformation A Ψ: Ψ read through the characteristic maps of the cells of A.

Main results

• TauCeti.cellDeformation_map: through the characteristic map of a cell of A, the deformation is Ψ.
• TauCeti.cellDeformation_of_notMem: points outside the open cells of A are fixed.
• TauCeti.cellDeformation_mem: the deformation keeps the n-skeleton inside itself.
• TauCeti.continuous_cellDeformation: the deformation is continuous on I × skeletonLT C (n + 1).
• TauCeti.exists_homotopicRel_openCell: a deformation of the closed unit ball fixing the unit sphere, read through the characteristic map of one n-cell j, deforms maps into the n-skeleton relative to the points not sent into the open cell j.

noncomputable def TauCeti.cellDeformation {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} (A : Set (Topology.RelCWComplex.cell C n)) (Ψ : C(↑unitInterval × (Fin n → ℝ), Fin n → ℝ)) (q : ↑unitInterval × X) : X

The family of maps Ψ of the closed unit ball read through the characteristic maps of a set A of n-cells, at time t: a point of the open cell of some j ∈ A moves by Ψ read through the characteristic map of j, and every other point is fixed.

theorem TauCeti.cellDeformation_of_notMem {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set (Topology.RelCWComplex.cell C n)} {Ψ : C(↑unitInterval × (Fin n → ℝ), Fin n → ℝ)} {t : ↑unitInterval} {x : X} (hx : ∀ j ∈ A, x ∉ Topology.RelCWComplex.openCell n j) : cellDeformation A Ψ (t, x) = x

A point outside the open cells of A is fixed.

theorem TauCeti.cellDeformation_of_mem {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set (Topology.RelCWComplex.cell C n)} {Ψ : C(↑unitInterval × (Fin n → ℝ), Fin n → ℝ)} {t : ↑unitInterval} {x : X} {j : Topology.RelCWComplex.cell C n} (hj : j ∈ A) (hx : x ∈ Topology.RelCWComplex.openCell n j) : cellDeformation A Ψ (t, x) = ↑(Topology.RelCWComplex.map n j) (Ψ (t, ↑(Topology.RelCWComplex.map n j).symm x))

A point of the open cell of j ∈ A moves by Ψ, read through the characteristic map of j.

theorem TauCeti.cellDeformation_of_mem_skeletonLT {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} [T2Space X] {A : Set (Topology.RelCWComplex.cell C n)} {Ψ : C(↑unitInterval × (Fin n → ℝ), Fin n → ℝ)} {t : ↑unitInterval} {x : X} (hx : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑n)) : cellDeformation A Ψ (t, x) = x

The (n-1)-skeleton misses every open n-cell, and is fixed.

theorem TauCeti.cellDeformation_map {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} [T2Space X] {A : Set (Topology.RelCWComplex.cell C n)} {Ψ : C(↑unitInterval × (Fin n → ℝ), Fin n → ℝ)} (hΨ : ∀ (t : ↑unitInterval) (y : Fin n → ℝ), ‖y‖ = 1 → Ψ (t, y) = y) {j : Topology.RelCWComplex.cell C n} (hj : j ∈ A) (t : ↑unitInterval) {y : Fin n → ℝ} (hy : ‖y‖ ≤ 1) : cellDeformation A Ψ (t, ↑(Topology.RelCWComplex.map n j) y) = ↑(Topology.RelCWComplex.map n j) (Ψ (t, y))

Through the characteristic map of a cell of A, the deformation is Ψ, provided Ψ fixes the unit sphere.

theorem TauCeti.cellDeformation_mem {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} [T2Space X] {A : Set (Topology.RelCWComplex.cell C n)} {Ψ : C(↑unitInterval × (Fin n → ℝ), Fin n → ℝ)} (hΨb : ∀ (t : ↑unitInterval) (y : Fin n → ℝ), ‖y‖ ≤ 1 → ‖Ψ (t, y)‖ ≤ 1) (t : ↑unitInterval) {x : X} (hx : x ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) : cellDeformation A Ψ (t, x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))

The deformation keeps the n-skeleton inside itself, provided Ψ keeps the closed unit ball inside itself.

theorem TauCeti.continuous_cellDeformation {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} [T2Space X] (A : Set (Topology.RelCWComplex.cell C n)) {Ψ : C(↑unitInterval × (Fin n → ℝ), Fin n → ℝ)} (hΨ : ∀ (t : ↑unitInterval) (y : Fin n → ℝ), ‖y‖ = 1 → Ψ (t, y) = y) (hΨb : ∀ (t : ↑unitInterval) (y : Fin n → ℝ), ‖y‖ ≤ 1 → ‖Ψ (t, y)‖ ≤ 1) : Continuous fun (q : ↑unitInterval × ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) => cellDeformation A Ψ (q.1, ↑q.2)

The deformation is continuous on I × skeletonLT C (n + 1), provided Ψ fixes the unit sphere and keeps the closed unit ball inside itself.

theorem TauCeti.exists_homotopicRel_openCell {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} [T2Space X] (j : Topology.RelCWComplex.cell C n) {g : C(Fin n → ℝ, Fin n → ℝ)} (Ψ : (ContinuousMap.id (Fin n → ℝ)).HomotopyRel g (frontier (Metric.closedBall 0 1))) (hΨb : ∀ (t : ↑unitInterval) (y : Fin n → ℝ), ‖y‖ ≤ 1 → ‖Ψ (t, y)‖ ≤ 1) {Z : Type u_1} [TopologicalSpace Z] (f : C(Z, ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1)))) {S : Set Z} (hS : ∀ z ∈ S, ↑(f z) ∉ Topology.RelCWComplex.openCell n j) : ∃ (f' : C(Z, ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1)))), f.HomotopicRel f' S ∧ (∀ (z : Z), ↑(f z) ∈ Topology.RelCWComplex.openCell n j → ↑(f' z) = ↑(Topology.RelCWComplex.map n j) (g (↑(Topology.RelCWComplex.map n j).symm ↑(f z)))) ∧ ∀ (z : Z), ↑(f z) ∉ Topology.RelCWComplex.openCell n j → f' z = f z

A deformation of the closed unit ball fixing the unit sphere, read through the characteristic map of an n-cell j, deforms maps into the n-skeleton relative to the points not sent into the open cell j. A point z sent into the open cell, at map n j y, ends at map n j (g y).