Associativity and units of the cubical cross product

The cross product of cubical chains of TauCeti.AlgebraicTopology.Singular.Cubical.CrossProduct.Chains is strictly associative and strictly unital: no shuffle or Eilenberg–Zilber correction is needed.

• Associativity is an equality of chains in X × Y × Z of dimension (p + q) + r, after pushing (a × b) × c forward along the associator (X × Y) × Z ≃ₜ X × Y × Z and reindexing p + (q + r) = (p + q) + r (CubicalChain.crossProduct_assoc).
• A 0-cube point x at a point x is a unit up to the maps y ↦ (x, y) and y ↦ (y, x) (CubicalChain.crossProduct_point_left, CubicalChain.crossProduct_point_right), in particular PUnit × X ≅ X ≅ X × PUnit (CubicalChain.crossProduct_punit_left).
• The augmentation is multiplicative (CubicalChain.augment_crossProduct).

All three statements hold on normalized chains as well.

Main results

• TauCeti.CubicalChain.crossProduct_assoc, TauCeti.NormalizedCubicalChain.crossProduct_assoc.
• TauCeti.CubicalChain.crossProduct_point_left, TauCeti.CubicalChain.crossProduct_point_right and their normalized versions.
• TauCeti.CubicalChain.augment_crossProduct, TauCeti.NormalizedCubicalChain.augment_crossProduct.
• TauCeti.NormalizedCubicalChain.map_crossProduct_map_assoc: associativity of push-forwards of iterated cross products, the common form of the associativity of products and actions built from the cross product.

References

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

theorem TauCeti.CubicalChain.crossProduct_assoc {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {p q r : ℕ} (R : Type u_4) [CommSemiring R] (a : CubicalChain X R p) (b : CubicalChain Y R q) (c : CubicalChain Z R r) : (map R (↑(Homeomorph.prodAssoc X Y Z)) (p + q + r)) (((crossProduct (X × Y) Z R (p + q) r) (((crossProduct X Y R p q) a) b)) c) = (cast R ⋯) (((crossProduct X (Y × Z) R p (q + r)) a) (((crossProduct Y Z R q r) b) c))

Strict associativity of the cross product: (a × b) × c = a × (b × c), after the associator of the spaces and the reindexing p + (q + r) = (p + q) + r.

theorem TauCeti.CubicalChain.crossProduct_point_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {q : ℕ} (R : Type u_4) [CommSemiring R] (x : X) (b : CubicalChain Y R q) : (cast R ⋯) (((crossProduct X Y R 0 q) (Finsupp.single (SingularCube.point x) 1)) b) = (map R ((ContinuousMap.const Y x).prodMk (ContinuousMap.id Y)) q) b

A point on the left is a unit for the cross product of chains: the cross product with the 0-cube at x is the push-forward along y ↦ (x, y), up to reindexing 0 + q = q.

theorem TauCeti.CubicalChain.crossProduct_point_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : ℕ} (R : Type u_4) [CommSemiring R] (a : CubicalChain X R p) (y : Y) : (cast R ⋯) (((crossProduct X Y R p 0) a) (Finsupp.single (SingularCube.point y) 1)) = (map R ((ContinuousMap.id X).prodMk (ContinuousMap.const X y)) p) a

A point on the right is a unit for the cross product of chains: the cross product with the 0-cube at y is the push-forward along x ↦ (x, y), up to reindexing p + 0 = p.

theorem TauCeti.CubicalChain.crossProduct_punit_left {Y : Type u_2} [TopologicalSpace Y] {q : ℕ} (R : Type u_4) [CommSemiring R] (b : CubicalChain Y R q) : (map R ContinuousMap.snd q) ((cast R ⋯) (((crossProduct PUnit.{u_5 + 1} Y R 0 q) (Finsupp.single (SingularCube.point PUnit.unit) 1)) b)) = b

The cross product with the 0-cube of the point PUnit is the identity, up to the identification PUnit × Y ≅ Y and the reindexing 0 + q = q.

theorem TauCeti.CubicalChain.crossProduct_punit_right {X : Type u_1} [TopologicalSpace X] {p : ℕ} (R : Type u_4) [CommSemiring R] (a : CubicalChain X R p) : (map R ContinuousMap.fst p) ((cast R ⋯) (((crossProduct X PUnit.{u_5 + 1} R p 0) a) (Finsupp.single (SingularCube.point PUnit.unit) 1))) = a

The cross product with the 0-cube of the point PUnit is the identity, up to the identification X × PUnit ≅ X and the reindexing p + 0 = p.

theorem TauCeti.CubicalChain.augment_crossProduct {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [CommSemiring R] (a : CubicalChain X R 0) (b : CubicalChain Y R 0) : (augment (X × Y) R) (((crossProduct X Y R 0 0) a) b) = (augment X R) a * (augment Y R) b

The augmentation is multiplicative on the cross product of 0-chains.

theorem TauCeti.NormalizedCubicalChain.crossProduct_assoc {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {p q r : ℕ} (R : Type u_4) [CommRing R] (a : NormalizedCubicalChain X R p) (b : NormalizedCubicalChain Y R q) (c : NormalizedCubicalChain Z R r) : (map R (↑(Homeomorph.prodAssoc X Y Z)) (p + q + r)) (((crossProduct (X × Y) Z R (p + q) r) (((crossProduct X Y R p q) a) b)) c) = (cast R ⋯) (((crossProduct X (Y × Z) R p (q + r)) a) (((crossProduct Y Z R q r) b) c))

Strict associativity of the cross product of normalized chains, after the associator of the spaces and the reindexing p + (q + r) = (p + q) + r.

theorem TauCeti.NormalizedCubicalChain.map_crossProduct_map_assoc {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {p q r : ℕ} (R : Type u_4) [CommRing R] {U : Type u_5} {W : Type u_6} {V : Type u_7} [TopologicalSpace U] [TopologicalSpace W] [TopologicalSpace V] {f : C(X × Y, U)} {g : C(U × Z, V)} {f' : C(Y × Z, W)} {g' : C(X × W, V)} (h : g.comp (f.prodMap (ContinuousMap.id Z)) = g'.comp (((ContinuousMap.id X).prodMap f').comp ↑(Homeomorph.prodAssoc X Y Z))) (a : NormalizedCubicalChain X R p) (b : NormalizedCubicalChain Y R q) (c : NormalizedCubicalChain Z R r) : (cast R ⋯) ((map R g (p + q + r)) (((crossProduct U Z R (p + q) r) ((map R f (p + q)) (((crossProduct X Y R p q) a) b))) c)) = (map R g' (p + (q + r))) (((crossProduct X W R p (q + r)) a) ((map R f' (q + r)) (((crossProduct Y Z R q r) b) c)))

Associativity of push-forwards of iterated cross products. Two ways of combining three factors, g ∘ (f × id) on (X × Y) × Z and g' ∘ (id × f') on X × (Y × Z), which agree through the associator give the same chains, after the reindexing (p + q) + r = p + (q + r).

theorem TauCeti.NormalizedCubicalChain.crossProduct_point_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {q : ℕ} (R : Type u_4) [CommRing R] (x : X) (b : NormalizedCubicalChain Y R q) : (cast R ⋯) (((crossProduct X Y R 0 q) (ofCube X R (SingularCube.point x))) b) = (map R ((ContinuousMap.const Y x).prodMk (ContinuousMap.id Y)) q) b

A point on the left is a unit for the cross product of normalized chains.

theorem TauCeti.NormalizedCubicalChain.crossProduct_point_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : ℕ} (R : Type u_4) [CommRing R] (a : NormalizedCubicalChain X R p) (y : Y) : (cast R ⋯) (((crossProduct X Y R p 0) a) (ofCube Y R (SingularCube.point y))) = (map R ((ContinuousMap.id X).prodMk (ContinuousMap.const X y)) p) a

A point on the right is a unit for the cross product of normalized chains.

theorem TauCeti.NormalizedCubicalChain.augment_crossProduct {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [CommRing R] (a : NormalizedCubicalChain X R 0) (b : NormalizedCubicalChain Y R 0) : (augment (X × Y) R) (((crossProduct X Y R 0 0) a) b) = (augment X R) a * (augment Y R) b

The augmentation is multiplicative on the cross product of normalized 0-chains.