The graded algebra of normalized cubical chains of a topological monoid

For a topological monoid G, the Pontryagin product of TauCeti.AlgebraicTopology.Singular.Cubical.MonoidAlgebra.Basic makes the family n ↦ C^□_n(G; R) of normalized cubical chains a graded R-algebra, in the sense of Mathlib's DirectSum.GAlgebra: the product of a p-chain and a q-chain is a (p + q)-chain, the unit is the 0-cube at 1, and the scalars act through r ↦ r • 1. The strict associativity and unit laws hold up to the reindexings of NormalizedCubicalChain.cast, which are the equalities of graded components HEq required by GradedMonoid.GMonoid.

Hence ⨁ n : ℕ, C^□_n(G; R) is an R-algebra, TauCeti.normalizedCubicalChainAlgebra G R, in which the product of homogeneous elements is their Pontryagin product (DirectSum.of_mul_of and NormalizedCubicalChain.gMul_mul), with unit the 0-cube at 1 (NormalizedCubicalChain.gOne_one).

Main definitions

• TauCeti.cubicalChainLof G R n: the inclusion of the n-chains, with cubicalChainLof_mul.
• TauCeti.normalizedCubicalChainAlgebra G R: the graded algebra ⨁ n, C^□_n(G; R).
• TauCeti.NormalizedCubicalChain.gMonoid, .gRing, .gAlgebra: the graded structures.

References

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

@[instance_reducible]

noncomputable instance TauCeti.NormalizedCubicalChain.gOne (G : Type u_1) [Monoid G] [TopologicalSpace G] (R : Type u_2) [CommRing R] : GradedMonoid.GOne fun (n : ℕ) => NormalizedCubicalChain G R n

The unit of the graded structure.

@[instance_reducible]

noncomputable instance TauCeti.NormalizedCubicalChain.gMul (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] : GradedMonoid.GMul fun (n : ℕ) => NormalizedCubicalChain G R n

The multiplication of the graded structure.

@[simp]

theorem TauCeti.NormalizedCubicalChain.gOne_one {G : Type u_1} [Monoid G] [TopologicalSpace G] {R : Type u_2} [CommRing R] : GradedMonoid.GOne.one = one G R

The unit of the graded structure is the 0-cube at 1.

@[simp]

theorem TauCeti.NormalizedCubicalChain.gMul_mul {G : Type u_1} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_2} [CommRing R] {p q : ℕ} (a : NormalizedCubicalChain G R p) (b : NormalizedCubicalChain G R q) : GradedMonoid.GMul.mul a b = ((mul G R p q) a) b

The multiplication of the graded structure is the Pontryagin product.

@[instance_reducible]

noncomputable instance TauCeti.NormalizedCubicalChain.gMonoid (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] : GradedMonoid.GMonoid fun (n : ℕ) => NormalizedCubicalChain G R n

The Pontryagin product makes the normalized cubical chains a graded monoid.

@[instance_reducible]

noncomputable instance TauCeti.NormalizedCubicalChain.gRing (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] : DirectSum.GRing fun (n : ℕ) => NormalizedCubicalChain G R n

The Pontryagin product makes the normalized cubical chains a graded ring.

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

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

@[instance_reducible]

noncomputable instance TauCeti.NormalizedCubicalChain.gSemiring (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] : DirectSum.GSemiring fun (n : ℕ) => NormalizedCubicalChain G R n

The graded semiring structure underlying gRing.

@[instance_reducible]

noncomputable instance TauCeti.NormalizedCubicalChain.gNonUnitalNonAssocSemiring (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] : DirectSum.GNonUnitalNonAssocSemiring fun (n : ℕ) => NormalizedCubicalChain G R n

The graded nonunital nonassociative semiring structure underlying gRing.

@[instance_reducible]

noncomputable instance TauCeti.NormalizedCubicalChain.gAlgebra (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] : DirectSum.GAlgebra R fun (n : ℕ) => NormalizedCubicalChain G R n

Scalar multiples of the unit make the normalized cubical chains a graded R-algebra.

@[reducible, inline]

abbrev TauCeti.normalizedCubicalChainAlgebra (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] : Type (max u_2 u_1)

The direct sum ⨁ n, C^□_n(G; R) of the normalized cubical chains of a space. When G is a topological monoid it is the graded algebra of normalized cubical chains, with the Pontryagin product.

@[instance_reducible]

noncomputable instance TauCeti.instAddCommGroupNormalizedCubicalChainAlgebra (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] : AddCommGroup (normalizedCubicalChainAlgebra G R)

The additive group structure of the direct sum of the normalized cubical chains. It is supplied explicitly because instance search does not find the additive group structures of the summands under the binder.

@[reducible, inline]

noncomputable abbrev TauCeti.cubicalChainLof (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] (n : ℕ) : NormalizedCubicalChain G R n →ₗ[R] normalizedCubicalChainAlgebra G R

The inclusion of the chains of dimension n into the direct sum.

theorem TauCeti.cubicalChainLof_cast (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] {n m : ℕ} (h : n = m) (x : NormalizedCubicalChain G R n) : (cubicalChainLof G R m) ((NormalizedCubicalChain.cast R h) x) = (cubicalChainLof G R n) x

Reindexing a chain does not change its image in the direct sum.

@[instance_reducible]

noncomputable instance TauCeti.instRingNormalizedCubicalChainAlgebra (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] : Ring (normalizedCubicalChainAlgebra G R)

The ring structure of the graded algebra of normalized cubical chains.

theorem TauCeti.cubicalChainLof_mul (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_2) [CommRing R] {p q : ℕ} (a : NormalizedCubicalChain G R p) (b : NormalizedCubicalChain G R q) : (cubicalChainLof G R p) a * (cubicalChainLof G R q) b = (cubicalChainLof G R (p + q)) (((NormalizedCubicalChain.mul G R p q) a) b)

The product of homogeneous chains in the graded algebra is their Pontryagin product.