The retraction of cubical chains onto the chains of a compressible subspace

Let D be a TauCeti.SubspaceCubeDeformation A n: a homotopy of every singular cube c of X, ending at a cube with values in A ⊆ X when the dimension of c is less than n, compatible with faces and degeneracies and constant on the cubes that already have values in A. This file turns D into chain-level data on Massey's normalized cubical chains and shows that, for n = ⊤, the inclusion A → X induces a chain homotopy equivalence of normalized cubical chains.

• The end of the homotopy of c is a cube D.endCube c of X. It commutes with faces and preserves degeneracies, so it induces a chain endomorphism D.endChainMap R of the normalized cubical chains of X. It fixes the chains pushed forward into A, and below dimension n it carries every chain into them.
• The homotopy of c, with time as the first coordinate, sweeps out the cube D.sweep c of one dimension more. Its first two faces are c and D.endCube c, and its other faces are the swept faces of c. The negative swept-cube operator D.prismChain R therefore satisfies ∂ P + P ∂ = ε - id for the end ε of the deformation, so the swept-cube operator -D.prismChain R is a chain homotopy D.endHomotopy R from the identity to D.endChainMap R. It kills the chains of A, whose deformations are constant.
• For n = ⊤, the end of the homotopy of c is a cube D.retract c of A, which induces a chain map D.retractChainMap R from the normalized cubical chains of X to those of A. As the homotopy of a cube of A is constant, this chain map is a left inverse of the chain map induced by the inclusion, on the nose, and its composite with the inclusion is D.endChainMap R.

Through the comparison of cubical and simplicial singular chains, for n = ⊤ the inclusion of A then induces isomorphisms on singular homology with coefficients in any ring (TauCeti.SubspaceCubeDeformation.isIso_singularHomologyMap). By the compression lemma this applies as soon as every point of X is joined by a path to A and all relative homotopy sets π_{k+1}(X, A, a) vanish (TauCeti.isIso_singularHomologyMap_subtypeVal_of_relHomotopyGroup). For the inclusion of the bottom of the mapping cylinder of a weak homotopy equivalence, this gives the invariance of normalized cubical chains under weak homotopy equivalences (Hatcher, Proposition 4.21), proved as ContinuousMap.IsWeakHomotopyEquivalence.quasiIso_normalizedCubicalChainComplex_map.

Main definitions

• TauCeti.SubspaceCubeDeformation.endCube, TauCeti.SubspaceCubeDeformation.cubeHomotopy, TauCeti.SubspaceCubeDeformation.sweep: the end of the deformation of a cube, the deformation as a homotopy, and the cube it sweeps out (its SingularCube.prism).
• TauCeti.SubspaceCubeDeformation.endChain, TauCeti.SubspaceCubeDeformation.prismChain: the induced operators on normalized cubical chains.
• TauCeti.SubspaceCubeDeformation.endChainMap, TauCeti.SubspaceCubeDeformation.endHomotopy: the end of the deformation as an endomorphism of the normalized cubical chain complex, and the chain homotopy from the identity to it.
• TauCeti.SubspaceCubeDeformation.retract, TauCeti.SubspaceCubeDeformation.retractChain: for n = ⊤, the end of the deformation as a cube of A, and the induced operator on chains.
• TauCeti.SubspaceCubeDeformation.retractChainMap, TauCeti.SubspaceCubeDeformation.retractHomotopy: the retraction as a chain map onto the normalized cubical chains of A, and the chain homotopy from the identity to its composite with the inclusion.
• TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplexHomotopyEquiv: the chain homotopy equivalence between the normalized cubical chains of A and of X induced by the inclusion.

Main results

• TauCeti.SubspaceCubeDeformation.boundary_prismChain_add_prismChain_boundary: the prism identity ∂ P + P ∂ = ε - id.
• TauCeti.SubspaceCubeDeformation.endChain_map, TauCeti.SubspaceCubeDeformation.prismChain_map, TauCeti.SubspaceCubeDeformation.endChain_mem_range_map: for a deformation into the range of a map f, the end of the deformation fixes the chains pushed forward along f and the swept-cube operator kills them; below dimension n, the end of the deformation lands in them.
• TauCeti.SubspaceCubeDeformation.retractChain_map_subtypeVal: the retraction is a left inverse of the inclusion.
• TauCeti.SubspaceCubeDeformation.quasiIso_normalizedCubicalChainComplex_map, TauCeti.SubspaceCubeDeformation.isIso_singularHomologyMap: the inclusion of A induces a quasi-isomorphism of normalized cubical chains and isomorphisms on singular homology.
• TauCeti.isIso_singularHomologyMap_subtypeVal_of_relHomotopyGroup: the same conclusion from the vanishing of the relative homotopy sets.

References

• The chain-level construction follows the parallel formalization in TauCeti.AlgebraicTopology.Singular.Cubical.Based.Retraction, adapted so that, for n = ⊤, the retraction lands in the chains of the subspace.
• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407–447, for the deformation of singular chains into the subcomplex of a subspace.
• A. Hatcher, Algebraic Topology, Section 4.1, Proposition 4.21 (a weak homotopy equivalence induces isomorphisms on homology).
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for normalized cubical chains and their prism operators.

The end of the deformation and the swept cube

def TauCeti.SubspaceCubeDeformation.endCube {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) : SingularCube X m

The cube of X at the end of the deformation of the singular cube c.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.endCube_apply {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) (y : Fin m → ↑unitInterval) : (D.endCube c) y = (D.homotopy c) (1, y)

theorem TauCeti.SubspaceCubeDeformation.endCube_of_range_subset {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} {c : SingularCube X m} (hc : Set.range ⇑c ⊆ A) : D.endCube c = c

A cube with values in A is fixed by the deformation.

theorem TauCeti.SubspaceCubeDeformation.range_endCube_subset {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (hm : ↑m < n) (c : SingularCube X m) : Set.range ⇑(D.endCube c) ⊆ A

The deformation of a cube of dimension less than n ends in A.

theorem TauCeti.SubspaceCubeDeformation.mapsTo_endCube_boundary {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (hm : ↑m < n) (c : SingularCube X (m + 1)) : Set.MapsTo (⇑(D.endCube c)) (Cube.boundary (Fin (m + 1))) A

The deformation of a cube whose faces have dimension less than n ends in a cube sending the boundary of the cube into A.

theorem TauCeti.SubspaceCubeDeformation.face_endCube {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) : SingularCube.face i t (D.endCube c) = D.endCube (SingularCube.face i t c)

The end of the deformation commutes with the faces at the endpoints of the interval.

theorem TauCeti.SubspaceCubeDeformation.isDegenerate_endCube {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} {c : SingularCube X m} (hc : c.IsDegenerate) : (D.endCube c).IsDegenerate

The end of the deformation of a degenerate cube is degenerate.

def TauCeti.SubspaceCubeDeformation.cubeHomotopy {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) : ContinuousMap.Homotopy c (D.endCube c)

The deformation of the singular cube c, as a homotopy from c to the cube D.endCube c.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.cubeHomotopy_apply {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) (p : ↑unitInterval × (Fin m → ↑unitInterval)) : (D.cubeHomotopy c) p = (D.homotopy c) p

def TauCeti.SubspaceCubeDeformation.sweep {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) : SingularCube X (m + 1)

The cube swept out by the deformation of the singular cube c, with time as the first coordinate.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.sweep_apply {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) (y : Fin (m + 1) → ↑unitInterval) : (D.sweep c) y = (D.homotopy c) (y 0, Fin.tail y)

theorem TauCeti.SubspaceCubeDeformation.sweep_apply_zero {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) : (D.sweep c) 0 = c 0

The swept cube starts at the origin of c.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.face_zero_zero_sweep {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) : SingularCube.face 0 0 (D.sweep c) = c

The swept cube starts at c.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.face_zero_one_sweep {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X m) : SingularCube.face 0 1 (D.sweep c) = D.endCube c

The swept cube ends at the end of the deformation of c.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.face_succ_sweep {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) : SingularCube.face i.succ t (D.sweep c) = D.sweep (SingularCube.face i t c)

The faces of the swept cube in the spatial coordinates are the swept faces.

theorem TauCeti.SubspaceCubeDeformation.isDegenerateAt_sweep {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} {c : SingularCube X m} {i : Fin m} (hc : c.IsDegenerateAt i) : (D.sweep c).IsDegenerateAt i.succ

If c does not depend on its coordinate i, then its swept cube does not depend on the coordinate i.succ.

theorem TauCeti.SubspaceCubeDeformation.isDegenerate_sweep {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} {c : SingularCube X m} (hc : c.IsDegenerate) : (D.sweep c).IsDegenerate

The cube swept out by the deformation of a degenerate cube is degenerate.

theorem TauCeti.SubspaceCubeDeformation.isDegenerate_sweep_of_range_subset {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} {c : SingularCube X m} (hc : Set.range ⇑c ⊆ A) : (D.sweep c).IsDegenerate

The cube swept out by the constant deformation of a cube with values in A does not depend on the time coordinate.

The operators on normalized chains

noncomputable def TauCeti.SubspaceCubeDeformation.endChain {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u_2) [Ring R] (m : ℕ) : NormalizedCubicalChain X R m →ₗ[R] NormalizedCubicalChain X R m

The end of the deformation, on normalized cubical chains of X.

noncomputable def TauCeti.SubspaceCubeDeformation.prismChain {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u_2) [Ring R] (m : ℕ) : NormalizedCubicalChain X R m →ₗ[R] NormalizedCubicalChain X R (m + 1)

The negative swept-cube operator on normalized cubical chains.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.endChain_ofCube {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u_2) [Ring R] {m : ℕ} (c : SingularCube X m) : (D.endChain R m) (NormalizedCubicalChain.ofCube X R c) = NormalizedCubicalChain.ofCube X R (D.endCube c)

@[simp]

theorem TauCeti.SubspaceCubeDeformation.prismChain_ofCube {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u_2) [Ring R] {m : ℕ} (c : SingularCube X m) : (D.prismChain R m) (NormalizedCubicalChain.ofCube X R c) = -NormalizedCubicalChain.ofCube X R (D.sweep c)

theorem TauCeti.SubspaceCubeDeformation.boundary_endChain {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u_2) [Ring R] (m : ℕ) (g : NormalizedCubicalChain X R (m + 1)) : (NormalizedCubicalChain.boundary X R m) ((D.endChain R (m + 1)) g) = (D.endChain R m) ((NormalizedCubicalChain.boundary X R m) g)

The end of the deformation commutes with the boundary.

theorem TauCeti.SubspaceCubeDeformation.boundary_prismChain_add_prismChain_boundary {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u_2) [Ring R] (m : ℕ) (g : NormalizedCubicalChain X R (m + 1)) : (NormalizedCubicalChain.boundary X R (m + 1)) ((D.prismChain R (m + 1)) g) + (D.prismChain R m) ((NormalizedCubicalChain.boundary X R m) g) = (D.endChain R (m + 1)) g - g

The prism identity ∂ P + P ∂ = ε - id in positive degrees, for the swept-cube operator P and the end ε of the deformation.

theorem TauCeti.SubspaceCubeDeformation.boundary_prismChain_zero {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u_2) [Ring R] (g : NormalizedCubicalChain X R 0) : (NormalizedCubicalChain.boundary X R 0) ((D.prismChain R 0) g) = (D.endChain R 0) g - g

The prism identity ∂ P = ε - id in degree zero.

Chains pushed forward into the subspace

@[simp]

theorem TauCeti.SubspaceCubeDeformation.endChain_map {X : Type u_1} [TopologicalSpace X] {n : ℕ∞} (R : Type u_2) [Ring R] {Y : Type u_3} [TopologicalSpace Y] {f : C(Y, X)} (D : SubspaceCubeDeformation (Set.range ⇑f) n) {m : ℕ} (g : NormalizedCubicalChain Y R m) : (D.endChain R m) ((NormalizedCubicalChain.map R f m) g) = (NormalizedCubicalChain.map R f m) g

The end of a deformation into the range of f fixes the chains pushed forward along f.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.prismChain_map {X : Type u_1} [TopologicalSpace X] {n : ℕ∞} (R : Type u_2) [Ring R] {Y : Type u_3} [TopologicalSpace Y] {f : C(Y, X)} (D : SubspaceCubeDeformation (Set.range ⇑f) n) {m : ℕ} (g : NormalizedCubicalChain Y R m) : (D.prismChain R m) ((NormalizedCubicalChain.map R f m) g) = 0

The swept-cube operator of a deformation into the range of f kills the chains pushed forward along f, whose deformations are constant.

theorem TauCeti.SubspaceCubeDeformation.endChain_mem_range_map {X : Type u_1} [TopologicalSpace X] {n : ℕ∞} (R : Type u_2) [Ring R] {Y : Type u_3} [TopologicalSpace Y] {f : C(Y, X)} (D : SubspaceCubeDeformation (Set.range ⇑f) n) (hf : Topology.IsInducing ⇑f) {m : ℕ} (hm : ↑m < n) (g : NormalizedCubicalChain X R m) : (D.endChain R m) g ∈ (NormalizedCubicalChain.map R f m).range

Below dimension n, the end of a deformation into the range of an inducing map f lands in the chains pushed forward along f.

The retraction onto the cubes of A

def TauCeti.SubspaceCubeDeformation.retract {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube X m) : SingularCube (↑A) m

The cube of A at the end of the deformation of the singular cube c of X.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.coe_retract_apply {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube X m) (y : Fin m → ↑unitInterval) : ↑((D.retract c) y) = (D.homotopy c) (1, y)

@[simp]

theorem TauCeti.SubspaceCubeDeformation.subtypeVal_comp_retract {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube X m) : (ContinuousMap.subtypeVal A).comp (D.retract c) = D.endCube c

Read in X, the cube D.retract c is the end of the deformation of c.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.retract_subtypeVal_comp {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube (↑A) m) : D.retract ((ContinuousMap.subtypeVal A).comp c) = c

The deformation fixes the cubes of A.

theorem TauCeti.SubspaceCubeDeformation.face_retract {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) : SingularCube.face i t (D.retract c) = D.retract (SingularCube.face i t c)

The end of the deformation commutes with the faces at the endpoints of the interval.

theorem TauCeti.SubspaceCubeDeformation.isDegenerateAt_retract {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} {c : SingularCube X m} {i : Fin m} (hc : c.IsDegenerateAt i) : (D.retract c).IsDegenerateAt i

If c does not depend on its coordinate i, then neither does the end of its deformation.

theorem TauCeti.SubspaceCubeDeformation.isDegenerate_retract {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) {m : ℕ} {c : SingularCube X m} (hc : c.IsDegenerate) : (D.retract c).IsDegenerate

The end of the deformation of a degenerate cube is degenerate.

noncomputable def TauCeti.SubspaceCubeDeformation.retractChain {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) (R : Type u_2) [Ring R] (m : ℕ) : NormalizedCubicalChain X R m →ₗ[R] NormalizedCubicalChain (↑A) R m

The retraction onto the cubes of A, on normalized cubical chains.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.retractChain_ofCube {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) (R : Type u_2) [Ring R] {m : ℕ} (c : SingularCube X m) : (D.retractChain R m) (NormalizedCubicalChain.ofCube X R c) = NormalizedCubicalChain.ofCube (↑A) R (D.retract c)

@[simp]

theorem TauCeti.SubspaceCubeDeformation.retractChain_map_subtypeVal {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) (R : Type u_2) [Ring R] {m : ℕ} (g : NormalizedCubicalChain (↑A) R m) : (D.retractChain R m) ((NormalizedCubicalChain.map R (ContinuousMap.subtypeVal A) m) g) = g

The retraction is a left inverse of the inclusion on normalized cubical chains, since the deformation fixes the cubes of A.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.map_subtypeVal_retractChain {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) (R : Type u_2) [Ring R] {m : ℕ} (g : NormalizedCubicalChain X R m) : (NormalizedCubicalChain.map R (ContinuousMap.subtypeVal A) m) ((D.retractChain R m) g) = (D.endChain R m) g

Read in X, the retraction onto the cubes of A is the end of the deformation.

theorem TauCeti.SubspaceCubeDeformation.boundary_retractChain {X : Type u_1} [TopologicalSpace X] {A : Set X} (D : SubspaceCubeDeformation A ⊤) (R : Type u_2) [Ring R] (m : ℕ) (g : NormalizedCubicalChain X R (m + 1)) : (NormalizedCubicalChain.boundary (↑A) R m) ((D.retractChain R (m + 1)) g) = (D.retractChain R m) ((NormalizedCubicalChain.boundary X R m) g)

The retraction commutes with the boundary.

The chain homotopy from the identity to the end of the deformation

noncomputable def TauCeti.SubspaceCubeDeformation.endChainMap {X : TopCat} {A : Set ↑X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u) [Ring R] : (normalizedCubicalChainComplex R).obj X ⟶ (normalizedCubicalChainComplex R).obj X

The end of the deformation, as an endomorphism of the normalized cubical chain complex of X.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.endChainMap_f_apply {X : TopCat} {A : Set ↑X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u) [Ring R] (m : ℕ) (g : NormalizedCubicalChain (↑X) R m) : (CategoryTheory.ConcreteCategory.hom ((D.endChainMap R).f m)) g = (D.endChain R m) g

noncomputable def TauCeti.SubspaceCubeDeformation.endHomotopy {X : TopCat} {A : Set ↑X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u) [Ring R] : Homotopy (CategoryTheory.CategoryStruct.id ((normalizedCubicalChainComplex R).obj X)) (D.endChainMap R)

The chain homotopy from the identity to the end of the deformation, given in degree m by the swept-cube operator -D.prismChain R m.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.endHomotopy_hom_succ {X : TopCat} {A : Set ↑X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) (R : Type u) [Ring R] (m : ℕ) (g : NormalizedCubicalChain (↑X) R m) : (CategoryTheory.ConcreteCategory.hom ((D.endHomotopy R).hom m (m + 1))) g = -(D.prismChain R m) g

The chain homotopy equivalence of normalized cubical chain complexes

noncomputable def TauCeti.SubspaceCubeDeformation.retractChainMap {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] : (normalizedCubicalChainComplex R).obj X ⟶ (normalizedCubicalChainComplex R).obj ↧↑A

The retraction onto the cubes of A, as a chain map from the normalized cubical chains of X to those of A.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.retractChainMap_f_apply {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] (m : ℕ) (g : NormalizedCubicalChain (↑X) R m) : (CategoryTheory.ConcreteCategory.hom ((D.retractChainMap R).f m)) g = (D.retractChain R m) g

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplex_map_comp_retractChainMap {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] : CategoryTheory.CategoryStruct.comp ((normalizedCubicalChainComplex R).map (TopCat.ofHom (ContinuousMap.subtypeVal A))) (D.retractChainMap R) = CategoryTheory.CategoryStruct.id ((normalizedCubicalChainComplex R).obj ↧↑A)

The retraction chain map is a left inverse of the chain map induced by the inclusion of A.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplex_map_comp_retractChainMap_assoc {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] {Z : ChainComplex (ModuleCat R) ℕ} (h : (normalizedCubicalChainComplex R).obj ↧↑A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((normalizedCubicalChainComplex R).map (TopCat.ofHom (ContinuousMap.subtypeVal A))) (CategoryTheory.CategoryStruct.comp (D.retractChainMap R) h) = h

The retraction chain map is a left inverse of the chain map induced by the inclusion of A.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.retractChainMap_comp_normalizedCubicalChainComplex_map {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] : CategoryTheory.CategoryStruct.comp (D.retractChainMap R) ((normalizedCubicalChainComplex R).map (TopCat.ofHom (ContinuousMap.subtypeVal A))) = D.endChainMap R

Followed by the inclusion of A, the retraction chain map is the end of the deformation.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.retractChainMap_comp_normalizedCubicalChainComplex_map_assoc {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] {Z : ChainComplex (ModuleCat R) ℕ} (h : (normalizedCubicalChainComplex R).obj ↧↑X ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.retractChainMap R) (CategoryTheory.CategoryStruct.comp ((normalizedCubicalChainComplex R).map (TopCat.ofHom (ContinuousMap.subtypeVal A))) h) = CategoryTheory.CategoryStruct.comp (D.endChainMap R) h

Followed by the inclusion of A, the retraction chain map is the end of the deformation.

noncomputable def TauCeti.SubspaceCubeDeformation.retractHomotopy {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] : Homotopy (CategoryTheory.CategoryStruct.id ((normalizedCubicalChainComplex R).obj X)) (CategoryTheory.CategoryStruct.comp (D.retractChainMap R) ((normalizedCubicalChainComplex R).map (TopCat.ofHom (ContinuousMap.subtypeVal A))))

The chain homotopy from the identity to the composite of the retraction and the inclusion of A, given in degree m by the swept-cube operator -D.prismChain R m.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.retractHomotopy_hom_succ {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] (m : ℕ) (g : NormalizedCubicalChain (↑X) R m) : (CategoryTheory.ConcreteCategory.hom ((D.retractHomotopy R).hom m (m + 1))) g = -(D.prismChain R m) g

noncomputable def TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplexHomotopyEquiv {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] : HomotopyEquiv ((normalizedCubicalChainComplex R).obj ↧↑A) ((normalizedCubicalChainComplex R).obj X)

The inclusion of A induces a chain homotopy equivalence of normalized cubical chains, with the retraction as homotopy inverse.

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplexHomotopyEquiv_hom {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] : (D.normalizedCubicalChainComplexHomotopyEquiv R).hom = (normalizedCubicalChainComplex R).map (TopCat.ofHom (ContinuousMap.subtypeVal A))

@[simp]

theorem TauCeti.SubspaceCubeDeformation.normalizedCubicalChainComplexHomotopyEquiv_inv {X : TopCat} {A : Set ↑X} (D : SubspaceCubeDeformation A ⊤) (R : Type u) [Ring R] : (D.normalizedCubicalChainComplexHomotopyEquiv R).inv = D.retractChainMap R

theorem TauCeti.SubspaceCubeDeformation.quasiIso_normalizedCubicalChainComplex_map {X : TopCat} {A : Set ↑X} (R : Type u) [Ring R] (D : SubspaceCubeDeformation A ⊤) : QuasiIso ((normalizedCubicalChainComplex R).map (TopCat.ofHom (ContinuousMap.subtypeVal A)))

The inclusion of A induces a quasi-isomorphism of normalized cubical chains.

theorem TauCeti.SubspaceCubeDeformation.isIso_singularHomologyMap {X : TopCat} {A : Set ↑X} (R : Type u) [Ring R] (D : SubspaceCubeDeformation A ⊤) (n : ℕ) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) n).obj ↧R).map (TopCat.ofHom (ContinuousMap.subtypeVal A)))

The inclusion of A induces isomorphisms on singular homology, with coefficients in any ring, when the singular cubes of X deform into A.

theorem TauCeti.isIso_singularHomologyMap_subtypeVal_of_relHomotopyGroup {X : TopCat} {A : Set ↑X} (h₀ : ∀ (x : ↑X), ∃ a ∈ A, Joined x a) (h : ∀ (n : ℕ) (a : ↑A), Subsingleton (RelHomotopyGroup (Fin n) { pair := TopPair.ofSubset A, basepoint := a })) (R : Type u) [Ring R] (n : ℕ) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) n).obj ↧R).map (TopCat.ofHom (ContinuousMap.subtypeVal A)))

The inclusion of a subspace with vanishing relative homotopy sets induces isomorphisms on singular homology. If every point of X is joined by a path to a point of A, and the relative homotopy set π_{n+1}(X, A, a) is trivial for every n and every a ∈ A, then the inclusion of A into X induces isomorphisms H_n(A; R) ≅ H_n(X; R) for every n and every coefficient ring R.