Cross products of singular cubes

The cross product of a p-cube and a q-cube uses the first p and last q coordinates of I^(p+q), respectively. This is the geometric operation underlying the cross product of cubical chains. Faces in either block are the cross products with the corresponding face of that factor. Degeneracy in a coordinate is equivalent to degeneracy of the corresponding factor, so this operation preserves Massey's degenerate cubes in both variables.

Associativity holds as an equality after the canonical reindexing of finite coordinates and reassociation of Cartesian products. For zero-dimensional factors, the formulas retain the chosen point in the product. No homotopy or shuffle correction is involved.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Chapter VII.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Chapter 5.

def TauCeti.SingularCube.crossProduct {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (c : SingularCube X p) (d : SingularCube Y q) : SingularCube (X × Y) (p + q)

The cross product of singular cubes, with the coordinates of the first factor first.

@[simp]

theorem TauCeti.SingularCube.crossProduct_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (c : SingularCube X p) (d : SingularCube Y q) (x : Fin (p + q) → ↑unitInterval) : (c.crossProduct d) x = (c fun (i : Fin p) => x (Fin.castAdd q i), d fun (j : Fin q) => x (Fin.natAdd p j))

theorem TauCeti.SingularCube.crossProduct_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {p q : ℕ} (f : C(X, Z)) (g : C(Y, W)) (c : SingularCube X p) (d : SingularCube Y q) : crossProduct (f.comp c) (g.comp d) = (f.prodMap g).comp (c.crossProduct d)

The cross product is natural in both spaces.

theorem TauCeti.SingularCube.crossProduct_assoc {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {p q r : ℕ} (c : SingularCube X p) (d : SingularCube Y q) (e : SingularCube Z r) : cast ⋯ (c.crossProduct (d.crossProduct e)) = (↑(Homeomorph.prodAssoc X Y Z)).comp ((c.crossProduct d).crossProduct e)

Cross products are associative after the canonical coordinate and product identifications.

theorem TauCeti.SingularCube.crossProduct_zero_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {q : ℕ} (c : SingularCube X 0) (d : SingularCube Y q) (x : Fin (0 + q) → ↑unitInterval) : (c.crossProduct d) x = (c Fin.elim0, d (x ∘ Fin.cast ⋯))

The cross product with a zero-dimensional left factor retains its point in the product.

theorem TauCeti.SingularCube.crossProduct_zero_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : ℕ} (c : SingularCube X p) (d : SingularCube Y 0) (x : Fin (p + 0) → ↑unitInterval) : (c.crossProduct d) x = (c (x ∘ Fin.cast ⋯), d Fin.elim0)

The cross product with a zero-dimensional right factor retains its point in the product.

theorem TauCeti.SingularCube.cast_crossProduct_point_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {q : ℕ} (x : X) (d : SingularCube Y q) : cast ⋯ ((point x).crossProduct d) = ((ContinuousMap.const Y x).prodMk (ContinuousMap.id Y)).comp d

A point on the left is a unit for the cross product of cubes, up to reindexing.

theorem TauCeti.SingularCube.cast_crossProduct_point_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : ℕ} (c : SingularCube X p) (y : Y) : cast ⋯ (c.crossProduct (point y)) = ((ContinuousMap.id X).prodMk (ContinuousMap.const X y)).comp c

A point on the right is a unit for the cross product of cubes, up to reindexing.

@[simp]

theorem TauCeti.SingularCube.isDegenerateAt_crossProduct_castAdd_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (c : SingularCube X p) (d : SingularCube Y q) (i : Fin p) : (c.crossProduct d).IsDegenerateAt (Fin.castAdd q i) ↔ c.IsDegenerateAt i

Degeneracy in the first coordinate block is exactly degeneracy of the first factor.

@[simp]

theorem TauCeti.SingularCube.isDegenerateAt_crossProduct_natAdd_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (c : SingularCube X p) (d : SingularCube Y q) (i : Fin q) : (c.crossProduct d).IsDegenerateAt (Fin.natAdd p i) ↔ d.IsDegenerateAt i

Degeneracy in the second coordinate block is exactly degeneracy of the second factor.

@[simp]

theorem TauCeti.SingularCube.face_crossProduct_castAdd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (c : SingularCube X (p + 1)) (d : SingularCube Y q) (i : Fin (p + 1)) (t : ↑unitInterval) : face (Fin.cast ⋯ (Fin.castAdd q i)) t (cast ⋯ (c.crossProduct d)) = (face i t c).crossProduct d

Faces in the first block are cross products with faces of the first factor.

@[simp]

theorem TauCeti.SingularCube.face_crossProduct_natAdd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (c : SingularCube X p) (d : SingularCube Y (q + 1)) (i : Fin (q + 1)) (t : ↑unitInterval) : face (Fin.natAdd p i) t (c.crossProduct d) = c.crossProduct (face i t d)

Faces in the second block are cross products with faces of the second factor.

@[simp]

theorem TauCeti.SingularCube.isDegenerate_crossProduct_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (c : SingularCube X p) (d : SingularCube Y q) : (c.crossProduct d).IsDegenerate ↔ c.IsDegenerate ∨ d.IsDegenerate

A cross product is degenerate if and only if at least one factor is degenerate.