The product on the normalized cubical chains of a topological monoid

For a topological monoid G, the multiplication G × G → G and the cross product of normalized cubical chains give the Pontryagin product a · b := mul_* (a × b) : C^□_{p + q}(G; R) for a ∈ C^□_p(G; R) and b ∈ C^□_q(G; R). It is strictly associative and strictly unital, with unit the 0-cube at 1, and the boundary is a derivation for it with the Koszul sign. These are the multiplication, the unit and the Leibniz rule that make ⨁_n C^□_n(G; R) a differential graded algebra.

The product, the Leibniz rule and the augmentation only use a continuous multiplication; the unit only uses a distinguished element; associativity and the unit laws use the corresponding monoid axioms.

The statements are made at the level of the individual degrees, with the explicit reindexings (p + q) + r = p + (q + r) and 0 + q = q = q + 0 (NormalizedCubicalChain.cast), exactly as for the cross product.

Main definitions

• TauCeti.mulMap G: the multiplication of a topological monoid as a continuous map G × G → G.
• TauCeti.NormalizedCubicalChain.mul G R p q: the product C^□_p(G; R) ⊗ C^□_q(G; R) → C^□_{p + q}(G; R).
• TauCeti.NormalizedCubicalChain.one G R: the unit, the 0-cube at 1.

Main results

• TauCeti.NormalizedCubicalChain.mul_def, TauCeti.NormalizedCubicalChain.one_def: the product is mul_* (a × b) and the unit is the class of the 0-cube at 1.
• TauCeti.NormalizedCubicalChain.mul_assoc: strict associativity.
• TauCeti.NormalizedCubicalChain.one_mul, TauCeti.NormalizedCubicalChain.mul_one: strict units.
• TauCeti.NormalizedCubicalChain.boundary_mul: the Leibniz rule, with boundary_mul_zero_left and boundary_mul_zero_right for a factor of degree 0.
• TauCeti.NormalizedCubicalChain.augment_mul, augment_one: the augmentation is multiplicative and unital.
• TauCeti.NormalizedCubicalChain.map_mul, TauCeti.NormalizedCubicalChain.map_one: pushing forward along a continuous monoid homomorphism preserves the product and the unit.

References

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

def TauCeti.mulMap (G : Type u_1) [Mul G] [TopologicalSpace G] [ContinuousMul G] : C(G × G, G)

The multiplication of a topological magma as a continuous map G × G → G.

@[simp]

theorem TauCeti.mulMap_apply (G : Type u_1) [Mul G] [TopologicalSpace G] [ContinuousMul G] (x : G × G) : (mulMap G) x = x.1 * x.2

noncomputable def TauCeti.NormalizedCubicalChain.mul (G : Type u_1) [Mul G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] (p q : ℕ) : NormalizedCubicalChain G R p →ₗ[R] NormalizedCubicalChain G R q →ₗ[R] NormalizedCubicalChain G R (p + q)

The Pontryagin product on normalized cubical chains of a topological monoid: a · b = mul_* (a × b).

theorem TauCeti.NormalizedCubicalChain.mul_def {G : Type u_1} [Mul G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_2} [CommRing R] {p q : ℕ} (a : NormalizedCubicalChain G R p) (b : NormalizedCubicalChain G R q) : ((mul G R p q) a) b = (map R (mulMap G) (p + q)) (((crossProduct G G R p q) a) b)

The Pontryagin product is the push-forward of the cross product along the multiplication.

@[simp]

theorem TauCeti.NormalizedCubicalChain.mul_ofCube {G : Type u_1} [Mul G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_2} [CommRing R] {p q : ℕ} (c : SingularCube G p) (d : SingularCube G q) : ((mul G R p q) (ofCube G R c)) (ofCube G R d) = ofCube G R ((mulMap G).comp (c.crossProduct d))

The product of two cubes is the class of the cube of products.

theorem TauCeti.NormalizedCubicalChain.boundary_mul {G : Type u_1} [Mul G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_2} [CommRing R] {p q : ℕ} (a : NormalizedCubicalChain G R (p + 1)) (b : NormalizedCubicalChain G R (q + 1)) : (boundary G R (p + q + 1)) ((cast R ⋯) (((mul G R (p + 1) (q + 1)) a) b)) = ((mul G R p (q + 1)) ((boundary G R p) a)) b + (-1) ^ (p + 1) • (cast R ⋯) (((mul G R (p + 1) q) a) ((boundary G R q) b))

The Leibniz rule for the Pontryagin product: 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_mul_zero_right {G : Type u_1} [Mul G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_2} [CommRing R] {p : ℕ} (a : NormalizedCubicalChain G R (p + 1)) (b : NormalizedCubicalChain G R 0) : (boundary G R p) (((mul G R (p + 1) 0) a) b) = ((mul G R p 0) ((boundary G R p) a)) b

The Leibniz rule for the Pontryagin product with a 0-chain on the right.

theorem TauCeti.NormalizedCubicalChain.boundary_mul_zero_left {G : Type u_1} [Mul G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_2} [CommRing R] {q : ℕ} (a : NormalizedCubicalChain G R 0) (b : NormalizedCubicalChain G R (q + 1)) : (boundary G R q) ((cast R ⋯) (((mul G R 0 (q + 1)) a) b)) = (cast R ⋯) (((mul G R 0 q) a) ((boundary G R q) b))

The Leibniz rule for the Pontryagin product with a 0-chain on the left.

theorem TauCeti.NormalizedCubicalChain.augment_mul {G : Type u_1} [Mul G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_2} [CommRing R] (a b : NormalizedCubicalChain G R 0) : (augment G R) (((mul G R 0 0) a) b) = (augment G R) a * (augment G R) b

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

noncomputable def TauCeti.NormalizedCubicalChain.one (G : Type u_1) [One G] [TopologicalSpace G] (R : Type u_2) [Ring R] : NormalizedCubicalChain G R 0

The unit of the Pontryagin product: the 0-cube at 1.

theorem TauCeti.NormalizedCubicalChain.one_def (G : Type u_1) [One G] [TopologicalSpace G] (R : Type u_2) [Ring R] : one G R = ofCube G R (SingularCube.point 1)

The unit of the Pontryagin product is the class of the 0-cube at 1.

theorem TauCeti.NormalizedCubicalChain.mul_assoc {R : Type u_1} [CommRing R] {G : Type u_2} [Semigroup G] [TopologicalSpace G] [ContinuousMul G] {p q r : ℕ} (a : NormalizedCubicalChain G R p) (b : NormalizedCubicalChain G R q) (c : NormalizedCubicalChain G R r) : (cast R ⋯) (((mul G R (p + q) r) (((mul G R p q) a) b)) c) = ((mul G R p (q + r)) a) (((mul G R q r) b) c)

Strict associativity of the Pontryagin product, after the reindexing (p + q) + r = p + (q + r).

@[simp]

theorem TauCeti.NormalizedCubicalChain.one_mul {R : Type u_1} [CommRing R] {G : Type u_2} [MulOneClass G] [TopologicalSpace G] [ContinuousMul G] {q : ℕ} (b : NormalizedCubicalChain G R q) : (cast R ⋯) (((mul G R 0 q) (one G R)) b) = b

The unit is a left unit, after the reindexing 0 + q = q.

theorem TauCeti.NormalizedCubicalChain.mul_one {R : Type u_1} [CommRing R] {G : Type u_2} [MulOneClass G] [TopologicalSpace G] [ContinuousMul G] {p : ℕ} (a : NormalizedCubicalChain G R p) : (cast R ⋯) (((mul G R p 0) a) (one G R)) = a

The unit is a right unit, after the reindexing p + 0 = p.

@[simp]

theorem TauCeti.NormalizedCubicalChain.mul_one_eq_self {R : Type u_1} [CommRing R] {G : Type u_2} [MulOneClass G] [TopologicalSpace G] [ContinuousMul G] {p : ℕ} (a : NormalizedCubicalChain G R p) : ((mul G R p 0) a) (one G R) = a

The right unit law in simp normal form: since p + 0 reduces to p, no reindexing is needed.

@[simp]

theorem TauCeti.NormalizedCubicalChain.augment_one {R : Type u_1} [CommRing R] {G : Type u_2} [Monoid G] [TopologicalSpace G] : (augment G R) (one G R) = 1

The augmentation of the unit is 1.

theorem TauCeti.NormalizedCubicalChain.map_mul {R : Type u_1} [CommRing R] {G : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {G' : Type u_3} [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] (φ : G →ₜ* G') {p q : ℕ} (a : NormalizedCubicalChain G R p) (b : NormalizedCubicalChain G R q) : (map R φ.toContinuousMap (p + q)) (((mul G R p q) a) b) = ((mul G' R p q) ((map R φ.toContinuousMap p) a)) ((map R φ.toContinuousMap q) b)

Pushing forward along a continuous monoid homomorphism is multiplicative for the Pontryagin product.

theorem TauCeti.NormalizedCubicalChain.map_one {R : Type u_1} [CommRing R] {G : Type u_2} [Monoid G] [TopologicalSpace G] {G' : Type u_3} [Monoid G'] [TopologicalSpace G'] (φ : G →ₜ* G') : (map R φ.toContinuousMap 0) (one G R) = one G' R

Pushing forward along a continuous monoid homomorphism sends the unit to the unit.