The DG algebra of normalized cubical chains of a topological monoid

For a topological monoid G, the graded algebra ⨁ n, C^□_n(G; R) of TauCeti.AlgebraicTopology.Singular.Cubical.MonoidAlgebra.Graded is a differential graded algebra, with the boundary as differential and C^□_n in cohomological degree -n (the convention C^{-n} = C_n). The grading and the differential make sense for the chains of any space; they are also those of the DG right modules of chains of a space with a right action of G (TauCeti.AlgebraicTopology.Singular.Cubical.MonoidAlgebra.Action).

Main definitions

• TauCeti.cubicalChainGrading G R: the ℤ-grading of normalizedCubicalChainAlgebra G R, with C^□_n in degree -n.
• TauCeti.cubicalChainDifferential G R: the boundary as an R-linear endomorphism.
• TauCeti.cubicalChainSumMap R f: the push-forward ⨁ n, C^□_n(X; R) → ⨁ n, C^□_n(Y; R) along a continuous map f : X → Y.
• The GradedAlgebra instance on cubicalChainGrading G R.

Main results

• TauCeti.cubicalChainSumMap_id, TauCeti.cubicalChainSumMap_comp, TauCeti.cubicalChainDifferential_cubicalChainSumMap: the push-forward is a functorial chain map.
• TauCeti.cubicalChain_isDGAlgebra: normalizedCubicalChainAlgebra G R with this grading and differential is a differential graded algebra.

References

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

noncomputable def TauCeti.cubicalChainGrading (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] (i : ℤ) : Submodule R (normalizedCubicalChainAlgebra G R)

The graded piece of cohomological degree i of the algebra of cubical chains: the chains of dimension -i when i ≤ 0, and zero otherwise.

theorem TauCeti.mem_cubicalChainGrading_iff (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] {i : ℤ} {x : normalizedCubicalChainAlgebra G R} : x ∈ cubicalChainGrading G R i ↔ x = 0 ∨ ∃ (n : ℕ) (y : NormalizedCubicalChain G R n), ↑n = -i ∧ (cubicalChainLof G R n) y = x

Membership in a graded piece: zero, or a chain of the dimension -i.

theorem TauCeti.cubicalChainGrading_eq_bot (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] {i : ℤ} (hi : 0 < i) : cubicalChainGrading G R i = ⊥

The cubical chains have no elements of positive cohomological degree.

theorem TauCeti.eq_zero_of_mem_cubicalChainGrading_of_pos (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] {i : ℤ} (hi : 0 < i) {x : normalizedCubicalChainAlgebra G R} (hx : x ∈ cubicalChainGrading G R i) : x = 0

A chain of positive cohomological degree vanishes.

theorem TauCeti.cubicalChainLof_mem (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] {n : ℕ} (y : NormalizedCubicalChain G R n) : (cubicalChainLof G R n) y ∈ cubicalChainGrading G R (-↑n)

A chain of dimension n lies in cohomological degree -n.

noncomputable def TauCeti.cubicalChainDecompose (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] : normalizedCubicalChainAlgebra G R →+ DirectSum ℤ fun (i : ℤ) => ↥(cubicalChainGrading G R i)

The decomposition of the algebra of cubical chains along its ℤ-grading.

@[instance_reducible]

noncomputable instance TauCeti.instDecompositionIntNormalizedCubicalChainAlgebraSubmoduleCubicalChainGrading (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] : DirectSum.Decomposition (cubicalChainGrading G R)

The algebra of cubical chains is the internal direct sum of its graded pieces.

instance TauCeti.instGradedMonoidIntNormalizedCubicalChainAlgebraSubmoduleCubicalChainGrading (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] [Monoid G] [ContinuousMul G] : SetLike.GradedMonoid (cubicalChainGrading G R)

The Pontryagin product adds cohomological degrees.

@[instance_reducible]

noncomputable instance TauCeti.instGradedAlgebraNormalizedCubicalChainAlgebra (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] [Monoid G] [ContinuousMul G] : GradedAlgebra (cubicalChainGrading G R)

The algebra of cubical chains is a ℤ-graded algebra.

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

The boundary of the chains of dimension n, as a map into the graded algebra; it vanishes in dimension 0.

noncomputable def TauCeti.cubicalChainDifferential (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] : normalizedCubicalChainAlgebra G R →ₗ[R] normalizedCubicalChainAlgebra G R

The differential of the algebra of cubical chains: the boundary, of cohomological degree +1.

theorem TauCeti.cubicalChainDifferential_lof (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] (n : ℕ) (y : NormalizedCubicalChain G R n) : (cubicalChainDifferential G R) ((cubicalChainLof G R n) y) = (cubicalChainBoundaryLof G R n) y

The differential on the chains of a given dimension.

@[simp]

theorem TauCeti.cubicalChainDifferential_lof_zero (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] (y : NormalizedCubicalChain G R 0) : (cubicalChainDifferential G R) ((cubicalChainLof G R 0) y) = 0

The differential vanishes on 0-chains.

@[simp]

theorem TauCeti.cubicalChainDifferential_lof_succ (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] (k : ℕ) (y : NormalizedCubicalChain G R (k + 1)) : (cubicalChainDifferential G R) ((cubicalChainLof G R (k + 1)) y) = (cubicalChainLof G R k) ((NormalizedCubicalChain.boundary G R k) y)

The differential on (k + 1)-chains is the boundary.

theorem TauCeti.negOnePow_neg_natCast_smul (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] (n : ℕ) (x : normalizedCubicalChainAlgebra G R) : (-↑n).negOnePow • x = (-1) ^ n • x

The sign (-1) ^ (-n) acts on the graded algebra as (-1) ^ n ∈ R.

theorem TauCeti.cubicalChainDifferential_mem (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] {i : ℤ} {x : normalizedCubicalChainAlgebra G R} (hx : x ∈ cubicalChainGrading G R i) : (cubicalChainDifferential G R) x ∈ cubicalChainGrading G R (i + 1)

The differential raises the cohomological degree by one.

theorem TauCeti.cubicalChainDifferential_eq_zero_of_nonneg (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] {i : ℤ} (hi : 0 ≤ i) {x : normalizedCubicalChainAlgebra G R} (hx : x ∈ cubicalChainGrading G R i) : (cubicalChainDifferential G R) x = 0

The differential of a chain of nonnegative cohomological degree vanishes.

@[simp]

theorem TauCeti.cubicalChainDifferential_cubicalChainDifferential (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] (x : normalizedCubicalChainAlgebra G R) : (cubicalChainDifferential G R) ((cubicalChainDifferential G R) x) = 0

The differential squares to zero.

noncomputable def TauCeti.cubicalChainSumMap (R : Type u_2) [CommRing R] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : normalizedCubicalChainAlgebra X R →ₗ[R] normalizedCubicalChainAlgebra Y R

The push-forward f_* : ⨁ n, C^□_n(X; R) → ⨁ n, C^□_n(Y; R) along a continuous map, dimension by dimension.

@[simp]

theorem TauCeti.cubicalChainSumMap_lof {R : Type u_2} [CommRing R] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {n : ℕ} (c : NormalizedCubicalChain X R n) : (cubicalChainSumMap R f) ((cubicalChainLof X R n) c) = (cubicalChainLof Y R n) ((NormalizedCubicalChain.map R f n) c)

The push-forward on a chain of dimension n.

theorem TauCeti.cubicalChainSumMap_apply {R : Type u_2} [CommRing R] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : normalizedCubicalChainAlgebra X R) (n : ℕ) : ((cubicalChainSumMap R f) x) n = (NormalizedCubicalChain.map R f n) (x n)

The dimension n component of a push-forward is the push-forward of the component.

@[simp]

theorem TauCeti.cubicalChainSumMap_id {R : Type u_2} [CommRing R] {X : Type u_3} [TopologicalSpace X] : cubicalChainSumMap R (ContinuousMap.id X) = LinearMap.id

The push-forward along the identity is the identity.

theorem TauCeti.cubicalChainSumMap_comp {R : Type u_2} [CommRing R] {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (f : C(X, Y)) : cubicalChainSumMap R (g.comp f) = cubicalChainSumMap R g ∘ₗ cubicalChainSumMap R f

The push-forward along a composite is the composite of the push-forwards.

theorem TauCeti.cubicalChainSumMap_mem {R : Type u_2} [CommRing R] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {i : ℤ} {a : normalizedCubicalChainAlgebra X R} (ha : a ∈ cubicalChainGrading X R i) : (cubicalChainSumMap R f) a ∈ cubicalChainGrading Y R i

The push-forward preserves the cohomological degree.

theorem TauCeti.cubicalChainDifferential_cubicalChainSumMap {R : Type u_2} [CommRing R] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (a : normalizedCubicalChainAlgebra X R) : (cubicalChainDifferential Y R) ((cubicalChainSumMap R f) a) = (cubicalChainSumMap R f) ((cubicalChainDifferential X R) a)

The push-forward is a chain map: it commutes with the boundary.

theorem TauCeti.cubicalChainDifferential_lof_mul_lof (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] [Monoid G] [ContinuousMul G] {m q : ℕ} (y : NormalizedCubicalChain G R m) (z : NormalizedCubicalChain G R q) : (cubicalChainDifferential G R) ((cubicalChainLof G R m) y * (cubicalChainLof G R q) z) = (cubicalChainDifferential G R) ((cubicalChainLof G R m) y) * (cubicalChainLof G R q) z + (-↑m).negOnePow • ((cubicalChainLof G R m) y * (cubicalChainDifferential G R) ((cubicalChainLof G R q) z))

The graded Leibniz rule on homogeneous chains.

theorem TauCeti.cubicalChain_isDGAlgebra (G : Type u_1) [TopologicalSpace G] (R : Type u_2) [CommRing R] [Monoid G] [ContinuousMul G] : IsDGAlgebra (cubicalChainGrading G R) (cubicalChainDifferential G R)

The normalized cubical chains of a topological monoid form a differential graded algebra: ⨁ n, C^□_n(G; R) with the Pontryagin product, C^□_n in cohomological degree -n, and the boundary as differential.