Singular cubes, their faces and degeneracies

A singular n-cube in a topological space X is a continuous map Iⁿ → X, where Iⁿ = Fin n → I is the standard cube. This file sets up the combinatorics of singular cubes that cubical singular homology is built on, following Massey, Singular Homology Theory, Chapter II:

• the faces face i t c : Iⁿ → X of an (n+1)-cube c, obtained by fixing the i-th coordinate at t ∈ I; the front and back faces of the literature are face i 0 and face i 1;
• the cubical identity face_face, which rewrites two successive faces in the other order;
• degenerate cubes, in Massey's sense: a cube is degenerate when it does not depend on at least one of its coordinates. This convention, rather than Serre's independence of the last coordinate, is the one closed under the cross product.

Faces do not preserve degeneracy: if c does not depend on its i-th coordinate, then its two i-faces coincide (face_eq_of_isDegenerateAt), and need not be degenerate, while its faces in every other coordinate are degenerate (isDegenerate_face_of_ne). Together these two facts are exactly what makes the degenerate chains a subcomplex of the cubical chains, which is where this file is used.

The cubical identity rests on Fin.insertNth_insertNth (TauCeti.Data.Fin.Basic), the commutation of two insertions, dual to Mathlib's Fin.removeNth_removeNth_eq_swap.

Main definitions

• TauCeti.SingularCube X n: singular n-cubes in X.
• TauCeti.SingularCube.cast: reindexing along an equality of dimensions.
• TauCeti.SingularCube.point: the 0-cube at a point.
• TauCeti.SingularCube.face: the face of a cube in a coordinate, at a parameter t ∈ I.
• TauCeti.SingularCube.degeneracy: the cube obtained by forgetting a coordinate.
• TauCeti.SingularCube.IsDegenerateAt, TauCeti.SingularCube.IsDegenerate: degeneracy at a coordinate, and degeneracy.

Main results

• TauCeti.SingularCube.face_face: the cubical identity.
• TauCeti.SingularCube.face_degeneracy_self: a degeneracy followed by the matching face.
• TauCeti.SingularCube.isDegenerate_iff_exists_eq_degeneracy: degeneracies exhaust the degenerate cubes.
• TauCeti.SingularCube.isDegenerateAt_iff, TauCeti.SingularCube.isDegenerate_iff, TauCeti.SingularCube.IsDegenerateAt.apply_update: the characterizations of degeneracy.
• TauCeti.SingularCube.face_eq_of_isDegenerateAt, TauCeti.SingularCube.isDegenerate_face_of_ne: the behaviour of faces on a degenerate cube.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II.
• J.-P. Serre, Homologie singulière des espaces fibrés. Applications, Ann. of Math. 54 (1951), Chapter II, for the alternative convention.

@[reducible, inline]

abbrev TauCeti.SingularCube (X : Type u_4) [TopologicalSpace X] (n : ℕ) : Type u_4

A singular n-cube in X: a continuous map from the standard cube Iⁿ = Fin n → I.

def TauCeti.SingularCube.cast {X : Type u_1} [TopologicalSpace X] {n m : ℕ} (h : n = m) (c : SingularCube X n) : SingularCube X m

Reindex a singular cube along an equality of dimensions.

@[simp]

theorem TauCeti.SingularCube.cast_apply {X : Type u_1} [TopologicalSpace X] {n m : ℕ} (h : n = m) (c : SingularCube X n) (x : Fin m → ↑unitInterval) : (cast h c) x = c (x ∘ Fin.cast h)

def TauCeti.SingularCube.point {X : Type u_1} [TopologicalSpace X] (x : X) : SingularCube X 0

The 0-cube at a point.

@[simp]

theorem TauCeti.SingularCube.point_apply {X : Type u_1} [TopologicalSpace X] (x : X) (t : Fin 0 → ↑unitInterval) : (point x) t = x

theorem TauCeti.SingularCube.eq_point {X : Type u_1} [TopologicalSpace X] (c : SingularCube X 0) : c = point (c fun (i : Fin 0) => i.elim0)

Every 0-cube is the constant cube at its value.

@[simp]

theorem TauCeti.SingularCube.cast_rfl {X : Type u_1} [TopologicalSpace X] {n : ℕ} (c : SingularCube X n) : cast ⋯ c = c

@[simp]

theorem TauCeti.SingularCube.cast_cast {X : Type u_1} [TopologicalSpace X] {n m k : ℕ} (h : n = m) (h' : m = k) (c : SingularCube X n) : cast h' (cast h c) = cast ⋯ c

Reindexing along successive dimension equalities is reindexing along their composite.

def TauCeti.SingularCube.face {X : Type u_1} [TopologicalSpace X] {n : ℕ} (i : Fin (n + 1)) (t : ↑unitInterval) (c : SingularCube X (n + 1)) : SingularCube X n

The face of an (n+1)-cube in its i-th coordinate, at the parameter t: the n-cube x ↦ c (i.insertNth t x). The front and back faces are face i 0 and face i 1.

@[simp]

theorem TauCeti.SingularCube.face_apply {X : Type u_1} [TopologicalSpace X] {n : ℕ} (i : Fin (n + 1)) (t : ↑unitInterval) (c : SingularCube X (n + 1)) (x : Fin n → ↑unitInterval) : (face i t c) x = c (i.insertNth t x)

theorem TauCeti.SingularCube.range_face_subset {X : Type u_1} [TopologicalSpace X] {n : ℕ} (i : Fin (n + 1)) (t : ↑unitInterval) (c : SingularCube X (n + 1)) : Set.range ⇑(face i t c) ⊆ Set.range ⇑c

A face of a cube takes its values among those of the cube.

theorem TauCeti.SingularCube.face_face {X : Type u_1} [TopologicalSpace X] {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (a b : ↑unitInterval) (c : SingularCube X (n + 2)) : face j b (face i a c) = face (j.predAbove i) a (face (i.succAbove j) b c)

The cubical identity: a face of a face, in the other order.

theorem TauCeti.SingularCube.face_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} (i : Fin (n + 1)) (t : ↑unitInterval) (f : C(X, Y)) (c : SingularCube X (n + 1)) : face i t (f.comp c) = f.comp (face i t c)

Faces commute with composition by a continuous map.

theorem TauCeti.SingularCube.comp_face_id {X : Type u_1} [TopologicalSpace X] {n : ℕ} (c : SingularCube X (n + 1)) (i : Fin (n + 1)) (t : ↑unitInterval) : ContinuousMap.comp c (face i t (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))) = face i t c

A cube composed with the face inclusion face i t id of the standard cube is its face.

theorem TauCeti.SingularCube.face_id_comp_face_id {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (a b : ↑unitInterval) : ContinuousMap.comp (face i a (ContinuousMap.id (Fin (n + 1 + 1) → ↑unitInterval))) (face j b (ContinuousMap.id (Fin (n + 1) → ↑unitInterval))) = ContinuousMap.comp (face (i.succAbove j) b (ContinuousMap.id (Fin (n + 1 + 1) → ↑unitInterval))) (face (j.predAbove i) a (ContinuousMap.id (Fin (n + 1) → ↑unitInterval)))

The cubical identity for the face inclusions of the standard cube.

theorem TauCeti.SingularCube.face_cast {X : Type u_1} [TopologicalSpace X] {n m : ℕ} (h : n = m) (i : Fin (n + 1)) (t : ↑unitInterval) (c : SingularCube X (n + 1)) : face (Fin.cast ⋯ i) t (cast ⋯ c) = cast h (face i t c)

Faces commute with reindexing.

@[reducible, inline]

abbrev TauCeti.SingularCube.forgetCoordinate {n : ℕ} (i : Fin (n + 1)) : C(Fin (n + 1) → ↑unitInterval, Fin n → ↑unitInterval)

The projection of the cube Iⁿ⁺¹ forgetting the i-th coordinate.

def TauCeti.SingularCube.degeneracy {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X n) (i : Fin (n + 1)) : SingularCube X (n + 1)

The degeneracy along coordinate i forgets that coordinate before applying the cube.

theorem TauCeti.SingularCube.degeneracy_eq_comp {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X n) (i : Fin (n + 1)) : s.degeneracy i = ContinuousMap.comp s (forgetCoordinate i)

A degeneracy is the composite with the projection forgetting a coordinate.

@[simp]

theorem TauCeti.SingularCube.degeneracy_apply {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X n) (i : Fin (n + 1)) (x : Fin (n + 1) → ↑unitInterval) : (s.degeneracy i) x = s (i.removeNth x)

Evaluation of a degeneracy.

@[simp]

theorem TauCeti.SingularCube.degeneracy_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} (f : C(X, Y)) (s : SingularCube X n) (i : Fin (n + 1)) : degeneracy (f.comp s) i = f.comp (s.degeneracy i)

Degeneracies commute with postcomposition by a continuous map.

@[simp]

theorem TauCeti.SingularCube.face_degeneracy_self {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X n) (i : Fin (n + 1)) (t : ↑unitInterval) : face i t (s.degeneracy i) = s

A degeneracy followed by the face in the forgotten coordinate is the original cube.

@[simp]

theorem TauCeti.SingularCube.degeneracy_cast {X : Type u_1} [TopologicalSpace X] {n m : ℕ} (h : n = m) (s : SingularCube X n) (i : Fin (n + 1)) : (cast h s).degeneracy (Fin.cast ⋯ i) = cast ⋯ (s.degeneracy i)

Degeneracies commute with reindexing along an equality of dimensions.

theorem TauCeti.SingularCube.degeneracy_degeneracy {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X n) (i : Fin (n + 1)) (j : Fin (n + 2)) : (s.degeneracy i).degeneracy j = (s.degeneracy (i.predAbove j)).degeneracy (j.succAbove i)

Two degeneracies commute after reindexing the forgotten coordinates.

@[simp]

theorem TauCeti.SingularCube.face_degeneracy_succAbove {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X (n + 1)) (j : Fin (n + 2)) (i : Fin (n + 1)) (t : ↑unitInterval) : face (j.succAbove i) t (s.degeneracy j) = (face i t s).degeneracy (i.predAbove j)

A face in a coordinate other than the forgotten coordinate commutes with degeneracy.

def TauCeti.SingularCube.IsDegenerateAt {X : Type u_1} [TopologicalSpace X] {n : ℕ} (c : SingularCube X n) (i : Fin n) : Prop

A cube is degenerate at the coordinate i when it does not depend on it.

def TauCeti.SingularCube.IsDegenerate {X : Type u_1} [TopologicalSpace X] {n : ℕ} (c : SingularCube X n) : Prop

A cube is degenerate when it does not depend on at least one of its coordinates (Massey's convention).

theorem TauCeti.SingularCube.isDegenerateAt_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X n} {i : Fin n} : c.IsDegenerateAt i ↔ ∀ (x : Fin n → ↑unitInterval) (t : ↑unitInterval), c (Function.update x i t) = c x

theorem TauCeti.SingularCube.isDegenerate_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X n} : c.IsDegenerate ↔ ∃ (i : Fin n), c.IsDegenerateAt i

@[simp]

theorem TauCeti.SingularCube.IsDegenerateAt.apply_update {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X n} {i : Fin n} (h : c.IsDegenerateAt i) (x : Fin n → ↑unitInterval) (t : ↑unitInterval) : c (Function.update x i t) = c x

theorem TauCeti.SingularCube.IsDegenerateAt.isDegenerate {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X n} {i : Fin n} (h : c.IsDegenerateAt i) : c.IsDegenerate

@[simp]

theorem TauCeti.SingularCube.isDegenerateAt_degeneracy {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X n) (i : Fin (n + 1)) : (s.degeneracy i).IsDegenerateAt i

A degeneracy is independent of the coordinate it forgets.

@[simp]

theorem TauCeti.SingularCube.isDegenerate_degeneracy {X : Type u_1} [TopologicalSpace X] {n : ℕ} (s : SingularCube X n) (i : Fin (n + 1)) : (s.degeneracy i).IsDegenerate

Every coordinate-forgetting degeneracy is a degenerate singular cube.

theorem TauCeti.SingularCube.isDegenerate_iff_exists_eq_degeneracy {X : Type u_1} [TopologicalSpace X] {n : ℕ} {s : SingularCube X (n + 1)} : s.IsDegenerate ↔ ∃ (i : Fin (n + 1)) (t : SingularCube X n), s = t.degeneracy i

The degenerate singular cubes are exactly the images of degeneracy operators.

@[simp]

theorem TauCeti.SingularCube.isDegenerate_const {X : Type u_1} [TopologicalSpace X] {n : ℕ} (x : X) : IsDegenerate (ContinuousMap.const (Fin (n + 1) → ↑unitInterval) x)

A constant cube of positive dimension is degenerate.

theorem TauCeti.SingularCube.not_isDegenerate_zero {X : Type u_1} [TopologicalSpace X] (c : SingularCube X 0) : ¬c.IsDegenerate

A 0-cube, a point, is never degenerate.

theorem TauCeti.SingularCube.IsDegenerateAt.comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} {c : SingularCube X n} {i : Fin n} (h : c.IsDegenerateAt i) (f : C(X, Y)) : IsDegenerateAt (f.comp c) i

theorem TauCeti.SingularCube.IsDegenerate.comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} {c : SingularCube X n} (h : c.IsDegenerate) (f : C(X, Y)) : IsDegenerate (f.comp c)

Composition with a continuous map preserves degeneracy.

theorem TauCeti.SingularCube.isDegenerateAt_comp_iff_of_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} (f : C(X, Y)) (hf : Function.Injective ⇑f) (c : SingularCube X n) (i : Fin n) : IsDegenerateAt (f.comp c) i ↔ c.IsDegenerateAt i

An injective continuous map reflects degeneracy in each coordinate.

theorem TauCeti.SingularCube.isDegenerate_comp_iff_of_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {n : ℕ} (f : C(X, Y)) (hf : Function.Injective ⇑f) (c : SingularCube X n) : IsDegenerate (f.comp c) ↔ c.IsDegenerate

An injective continuous map preserves and reflects degeneracy.

theorem TauCeti.SingularCube.face_eq_of_isDegenerateAt {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X (n + 1)} {i : Fin (n + 1)} (h : c.IsDegenerateAt i) (t t' : ↑unitInterval) : face i t c = face i t' c

The two faces of a cube in a coordinate it does not depend on coincide.

theorem TauCeti.SingularCube.IsDegenerateAt.face_succAbove {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X (n + 1)} {j : Fin (n + 1)} {k : Fin n} (h : c.IsDegenerateAt (j.succAbove k)) (t : ↑unitInterval) : (face j t c).IsDegenerateAt k

If a cube does not depend on its coordinate j.succAbove k, then its faces in the coordinate j do not depend on their coordinate k.

theorem TauCeti.SingularCube.isDegenerate_face_of_ne {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X (n + 1)} {i j : Fin (n + 1)} (h : c.IsDegenerateAt i) (hij : i ≠ j) (t : ↑unitInterval) : (face j t c).IsDegenerate

If a cube does not depend on its i-th coordinate, then its faces in any other coordinate j ≠ i are degenerate.