Cubical prisms

A homotopy sweeps an n-cube out into an (n + 1)-cube, with time as the first coordinate. This construction preserves Massey's degeneracies, so it induces a degree-one operator on normalized cubical chains. With the boundary convention ∑ i, (-1)^i (face i 0 - face i 1), we take the negative of the swept cube. The resulting identity is ∂ prism + prism ∂ = map g - map f for a homotopy from f to g.

In particular, a contraction supplies explicit fillings of cycles. These fillings give the acyclicity of the standard cubes needed by the acyclic-models comparison of cubical and simplicial chains.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II.

def TauCeti.SingularCube.prism {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g) {n : ℕ} (c : SingularCube X n) : SingularCube Y (n + 1)

The cube swept out by a homotopy, with time as the first coordinate.

@[simp]

theorem TauCeti.SingularCube.prism_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g) {n : ℕ} (c : SingularCube X n) (x : Fin (n + 1) → ↑unitInterval) : (prism H c) x = H (x 0, c (Fin.tail x))

@[simp]

theorem TauCeti.SingularCube.face_zero_prism {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g) {n : ℕ} (c : SingularCube X n) : face 0 0 (prism H c) = f.comp c

The time faces of a prism are the two endpoint maps.

@[simp]

theorem TauCeti.SingularCube.face_one_prism {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g) {n : ℕ} (c : SingularCube X n) : face 0 1 (prism H c) = g.comp c

@[simp]

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

Taking a spatial face commutes with sweeping out the cube.

theorem TauCeti.SingularCube.IsDegenerateAt.prism {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} {n : ℕ} {c : SingularCube X n} {i : Fin n} (hc : c.IsDegenerateAt i) (H : f.Homotopy g) : (SingularCube.prism H c).IsDegenerateAt i.succ

A prism is degenerate in the shifted coordinate whenever its input is degenerate.

theorem TauCeti.SingularCube.IsDegenerate.prism {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} {n : ℕ} {c : SingularCube X n} (hc : c.IsDegenerate) (H : f.Homotopy g) : (SingularCube.prism H c).IsDegenerate

Sweeping out a degenerate cube gives a degenerate cube.

noncomputable def TauCeti.CubicalChain.prism {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) (n : ℕ) : CubicalChain X R n →ₗ[R] CubicalChain Y R (n + 1)

The negative swept-cube operator, extended linearly to unnormalized chains.

@[simp]

theorem TauCeti.CubicalChain.prism_single {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) {n : ℕ} (c : SingularCube X n) (a : R) : (prism R H n) (Finsupp.single c a) = -Finsupp.single (SingularCube.prism H c) a

theorem TauCeti.CubicalChain.prism_mem_degenerate {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) {n : ℕ} {c : CubicalChain X R n} (hc : c ∈ degenerate X R n) : (prism R H n) c ∈ degenerate Y R (n + 1)

The prism operator preserves the submodules of degenerate chains.

theorem TauCeti.CubicalChain.boundary_prism_add_prism_boundary {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) (n : ℕ) : boundary Y R (n + 1) ∘ₗ prism R H (n + 1) + prism R H n ∘ₗ boundary X R n = map R g (n + 1) - map R f (n + 1)

The prism identity in positive degrees.

theorem TauCeti.CubicalChain.boundary_prism_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) : boundary Y R 0 ∘ₗ prism R H 0 = map R g 0 - map R f 0

In degree zero the prism has just its two endpoint faces.

noncomputable def TauCeti.NormalizedCubicalChain.prism {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) (n : ℕ) : NormalizedCubicalChain X R n →ₗ[R] NormalizedCubicalChain Y R (n + 1)

The prism operator on normalized cubical chains.

@[simp]

theorem TauCeti.NormalizedCubicalChain.prism_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) {n : ℕ} (c : CubicalChain X R n) : (prism R H n) (Submodule.Quotient.mk c) = Submodule.Quotient.mk ((CubicalChain.prism R H n) c)

@[simp]

theorem TauCeti.NormalizedCubicalChain.prism_ofCube {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) {n : ℕ} (c : SingularCube X n) : (prism R H n) (ofCube X R c) = -ofCube Y R (SingularCube.prism H c)

theorem TauCeti.NormalizedCubicalChain.boundary_prism_add_prism_boundary {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) (n : ℕ) (c : NormalizedCubicalChain X R (n + 1)) : (boundary Y R (n + 1)) ((prism R H (n + 1)) c) + (prism R H n) ((boundary X R n) c) = (map R g (n + 1)) c - (map R f (n + 1)) c

The normalized prism identity in positive degrees.

theorem TauCeti.NormalizedCubicalChain.boundary_prism_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (R : Type u_3) [Ring R] (H : f.Homotopy g) (c : NormalizedCubicalChain X R 0) : (boundary Y R 0) ((prism R H 0) c) = (map R g 0) c - (map R f 0) c

The normalized prism identity in degree zero.