The cross product of cubical chains

The cross product of singular cubes (TauCeti.SingularCube.crossProduct) extends bilinearly to cubical chains, CubicalChain X R p →ₗ[R] CubicalChain Y R q →ₗ[R] CubicalChain (X × Y) R (p + q). It is natural in both spaces, and it sends degenerate chains to degenerate chains in each variable, so it descends to the normalized chains. The boundary is a derivation for it, with the Koszul sign: ∂ (a × b) = ∂ a × b + (-1) ^ p • (a × ∂ b) for a of degree p.

The boundary CubicalChain.boundary X R n is defined on (n + 1)-chains, so the Leibniz rule is stated for factors of positive degree p + 1 and q + 1, where the product has degree (p + 1) + (q + 1) = (p + q + 1) + 1 after the reindexing CubicalChain.cast; the two cases where a factor has degree 0 are stated separately.

Main definitions

• TauCeti.CubicalChain.crossProduct X Y R p q: the cross product of cubical chains.
• TauCeti.NormalizedCubicalChain.crossProduct X Y R p q: the cross product of normalized chains.

Main results

• TauCeti.CubicalChain.crossProduct_single: the cross product of two cubes.
• TauCeti.CubicalChain.map_crossProduct: naturality.
• TauCeti.CubicalChain.crossProduct_left_mem_degenerate, TauCeti.CubicalChain.crossProduct_right_mem_degenerate: degenerate chains go to degenerate chains, so the product descends to TauCeti.NormalizedCubicalChain.crossProduct.
• TauCeti.CubicalChain.boundary_crossProduct: the Leibniz rule, with boundary_crossProduct_zero_left and boundary_crossProduct_zero_right for a factor of degree 0.
• TauCeti.NormalizedCubicalChain.boundary_crossProduct: the Leibniz rule on normalized chains, with boundary_crossProduct_zero_left and boundary_crossProduct_zero_right.

References

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

noncomputable def TauCeti.CubicalChain.crossProduct (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_5) [CommSemiring R] (p q : ℕ) : CubicalChain X R p →ₗ[R] CubicalChain Y R q →ₗ[R] CubicalChain (X × Y) R (p + q)

The cross product of cubical chains, the bilinear extension of the cross product of singular cubes.

@[simp]

theorem TauCeti.CubicalChain.crossProduct_single {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (R : Type u_5) [CommSemiring R] (c : SingularCube X p) (d : SingularCube Y q) (a b : R) : ((crossProduct X Y R p q) (Finsupp.single c a)) (Finsupp.single d b) = Finsupp.single (c.crossProduct d) (a * b)

The cross product of two cubes with coefficients.

theorem TauCeti.CubicalChain.map_crossProduct {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 : ℕ} (R : Type u_5) [CommSemiring R] (f : C(X, Z)) (g : C(Y, W)) (a : CubicalChain X R p) (b : CubicalChain Y R q) : (map R (f.prodMap g) (p + q)) (((crossProduct X Y R p q) a) b) = ((crossProduct Z W R p q) ((map R f p) a)) ((map R g q) b)

The cross product of chains is natural in both spaces.

theorem TauCeti.CubicalChain.crossProduct_left_mem_degenerate {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (R : Type u_5) [CommSemiring R] {a : CubicalChain X R p} (ha : a ∈ degenerate X R p) (b : CubicalChain Y R q) : ((crossProduct X Y R p q) a) b ∈ degenerate (X × Y) R (p + q)

The cross product of a degenerate chain with any chain is degenerate.

theorem TauCeti.CubicalChain.crossProduct_right_mem_degenerate {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (R : Type u_5) [CommSemiring R] (a : CubicalChain X R p) {b : CubicalChain Y R q} (hb : b ∈ degenerate Y R q) : ((crossProduct X Y R p q) a) b ∈ degenerate (X × Y) R (p + q)

The cross product of any chain with a degenerate chain is degenerate.

theorem TauCeti.CubicalChain.boundaryCube_crossProduct {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (R : Type u_5) [CommRing R] (c : SingularCube X (p + 1)) (d : SingularCube Y (q + 1)) : boundaryCube R (SingularCube.cast ⋯ (c.crossProduct d)) = ((crossProduct X Y R p (q + 1)) (boundaryCube R c)) (Finsupp.single d 1) + (-1) ^ (p + 1) • (cast R ⋯) (((crossProduct X Y R (p + 1) q) (Finsupp.single c 1)) (boundaryCube R d))

The Leibniz rule for cubes: the boundary of the cross product of a (p + 1)-cube and a (q + 1)-cube is the sum of the cross products of the boundary of the first factor with the second, and of the first factor with the boundary of the second, with the sign (-1) ^ (p + 1).

theorem TauCeti.CubicalChain.boundary_crossProduct {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p q : ℕ} (R : Type u_5) [CommRing R] (a : CubicalChain X R (p + 1)) (b : CubicalChain Y R (q + 1)) : (boundary (X × Y) R (p + q + 1)) ((cast R ⋯) (((crossProduct X Y R (p + 1) (q + 1)) a) b)) = ((crossProduct X Y R p (q + 1)) ((boundary X R p) a)) b + (-1) ^ (p + 1) • (cast R ⋯) (((crossProduct X Y R (p + 1) q) a) ((boundary Y R q) b))

The Leibniz rule for cubical chains: for a of degree p + 1 and b of degree q + 1, ∂ (a × b) = ∂ a × b + (-1) ^ (p + 1) • (a × ∂ b), in degree p + q + 1.

theorem TauCeti.CubicalChain.boundaryCube_crossProduct_zero_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : ℕ} (R : Type u_5) [CommRing R] (c : SingularCube X (p + 1)) (d : SingularCube Y 0) : boundaryCube R (c.crossProduct d) = ((crossProduct X Y R p 0) (boundaryCube R c)) (Finsupp.single d 1)

The Leibniz rule for cubes when the second factor is a point.

theorem TauCeti.CubicalChain.boundaryCube_crossProduct_zero_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {q : ℕ} (R : Type u_5) [CommRing R] (c : SingularCube X 0) (d : SingularCube Y (q + 1)) : boundaryCube R (SingularCube.cast ⋯ (c.crossProduct d)) = (cast R ⋯) (((crossProduct X Y R 0 q) (Finsupp.single c 1)) (boundaryCube R d))

The Leibniz rule for cubes when the first factor is a point.

theorem TauCeti.CubicalChain.boundary_crossProduct_zero_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : ℕ} (R : Type u_5) [CommRing R] (a : CubicalChain X R (p + 1)) (b : CubicalChain Y R 0) : (boundary (X × Y) R p) (((crossProduct X Y R (p + 1) 0) a) b) = ((crossProduct X Y R p 0) ((boundary X R p) a)) b

The Leibniz rule for chains when the second factor has degree 0.

theorem TauCeti.CubicalChain.boundary_crossProduct_zero_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {q : ℕ} (R : Type u_5) [CommRing R] (a : CubicalChain X R 0) (b : CubicalChain Y R (q + 1)) : (boundary (X × Y) R q) ((cast R ⋯) (((crossProduct X Y R 0 (q + 1)) a) b)) = (cast R ⋯) (((crossProduct X Y R 0 q) a) ((boundary Y R q) b))

The Leibniz rule for chains when the first factor has degree 0.

noncomputable def TauCeti.NormalizedCubicalChain.crossProduct (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_5) [CommRing R] (p q : ℕ) : NormalizedCubicalChain X R p →ₗ[R] NormalizedCubicalChain Y R q →ₗ[R] NormalizedCubicalChain (X × Y) R (p + q)

The cross product of normalized cubical chains, induced by the cross product of the unnormalized chains, since degenerate chains go to degenerate chains in each variable.

@[simp]

theorem TauCeti.NormalizedCubicalChain.crossProduct_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_5) [CommRing R] {p q : ℕ} (a : CubicalChain X R p) (b : CubicalChain Y R q) : ((crossProduct X Y R p q) (Submodule.Quotient.mk a)) (Submodule.Quotient.mk b) = Submodule.Quotient.mk (((CubicalChain.crossProduct X Y R p q) a) b)

The cross product of the classes of two chains is the class of their cross product.

@[simp]

theorem TauCeti.NormalizedCubicalChain.crossProduct_ofCube {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_5) [CommRing R] {p q : ℕ} (c : SingularCube X p) (d : SingularCube Y q) : ((crossProduct X Y R p q) (ofCube X R c)) (ofCube Y R d) = ofCube (X × Y) R (c.crossProduct d)

The cross product of the classes of two cubes is the class of their cross product.

theorem TauCeti.NormalizedCubicalChain.map_crossProduct {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] (R : Type u_5) [CommRing R] {p q : ℕ} (f : C(X, Z)) (g : C(Y, W)) (a : NormalizedCubicalChain X R p) (b : NormalizedCubicalChain Y R q) : (map R (f.prodMap g) (p + q)) (((crossProduct X Y R p q) a) b) = ((crossProduct Z W R p q) ((map R f p) a)) ((map R g q) b)

The cross product of normalized chains is natural in both spaces.

theorem TauCeti.NormalizedCubicalChain.boundary_crossProduct {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_5) [CommRing R] {p q : ℕ} (a : NormalizedCubicalChain X R (p + 1)) (b : NormalizedCubicalChain Y R (q + 1)) : (boundary (X × Y) R (p + q + 1)) ((cast R ⋯) (((crossProduct X Y R (p + 1) (q + 1)) a) b)) = ((crossProduct X Y R p (q + 1)) ((boundary X R p) a)) b + (-1) ^ (p + 1) • (cast R ⋯) (((crossProduct X Y R (p + 1) q) a) ((boundary Y R q) b))

The Leibniz rule for normalized cubical chains: for a of degree p + 1 and b of degree q + 1, ∂ (a × b) = ∂ a × b + (-1) ^ (p + 1) • (a × ∂ b), in degree p + q + 1.

theorem TauCeti.NormalizedCubicalChain.boundary_crossProduct_zero_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_5) [CommRing R] {p : ℕ} (a : NormalizedCubicalChain X R (p + 1)) (b : NormalizedCubicalChain Y R 0) : (boundary (X × Y) R p) (((crossProduct X Y R (p + 1) 0) a) b) = ((crossProduct X Y R p 0) ((boundary X R p) a)) b

The Leibniz rule for normalized chains when the second factor has degree 0.

theorem TauCeti.NormalizedCubicalChain.boundary_crossProduct_zero_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_5) [CommRing R] {q : ℕ} (a : NormalizedCubicalChain X R 0) (b : NormalizedCubicalChain Y R (q + 1)) : (boundary (X × Y) R q) ((cast R ⋯) (((crossProduct X Y R 0 (q + 1)) a) b)) = (cast R ⋯) (((crossProduct X Y R 0 q) a) ((boundary Y R q) b))

The Leibniz rule for normalized chains when the first factor has degree 0.