Functoriality and augmentation of the DG algebra of cubical chains of a monoid

For a continuous monoid homomorphism φ : G →ₜ* G' between topological monoids, pushing chains forward along φ is multiplicative for the Pontryagin product and sends the unit to the unit, so it induces a morphism of differential graded algebras cubicalChainDGAlgHom R φ : C^□_*(G; R) → C^□_*(G'; R), functorially in φ.

The augmentation of 0-chains, extended by zero to the chains of positive dimension, is an augmentation of the DG algebra C^□_*(G; R) in the sense of TauCeti.Algebra.Homology.DG.Algebra.Augmentation: a DG algebra morphism to R, placed in degree zero with zero differential. The morphisms induced by continuous monoid homomorphisms are compatible with these augmentations.

For a continuous monoid homomorphism, the underlying linear map of cubicalChainAlgHom R φ is the push-forward TauCeti.cubicalChainSumMap of the direct sums of chains.

Main definitions

• TauCeti.cubicalChainAlgHom R φ: the algebra homomorphism induced by φ : G →ₜ* G'.
• TauCeti.cubicalChainDGAlgHom R φ: the same as a morphism of DG algebras.
• TauCeti.cubicalChainAugmentation G R: the augmentation of C^□_*(G; R).

Main results

• TauCeti.cubicalChainDGAlgHom_id, TauCeti.cubicalChainDGAlgHom_comp: functoriality.
• TauCeti.cubicalChainAugmentation_comp_dgAlgHom: compatibility with the augmentations.

References

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

noncomputable def TauCeti.cubicalChainAlgHom {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] (R : Type u_4) [CommRing R] (φ : G →ₜ* G') : normalizedCubicalChainAlgebra G R →ₐ[R] normalizedCubicalChainAlgebra G' R

The algebra homomorphism C^□_*(G; R) → C^□_*(G'; R) induced by a continuous monoid homomorphism φ : G →ₜ* G': the push-forward of chains, dimension by dimension.

@[simp]

theorem TauCeti.cubicalChainAlgHom_lof {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] {R : Type u_4} [CommRing R] (φ : G →ₜ* G') (n : ℕ) (y : NormalizedCubicalChain G R n) : (cubicalChainAlgHom R φ) ((cubicalChainLof G R n) y) = (cubicalChainLof G' R n) ((NormalizedCubicalChain.map R φ.toContinuousMap n) y)

The induced algebra homomorphism on a chain of dimension n.

theorem TauCeti.cubicalChainAlgHom_toLinearMap {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] {R : Type u_4} [CommRing R] (φ : G →ₜ* G') : (cubicalChainAlgHom R φ).toLinearMap = cubicalChainSumMap R φ.toContinuousMap

The underlying linear map of the induced algebra homomorphism is the push-forward along φ.

theorem TauCeti.cubicalChainAlgHom_mem {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] {R : Type u_4} [CommRing R] (φ : G →ₜ* G') {i : ℤ} {a : normalizedCubicalChainAlgebra G R} (ha : a ∈ cubicalChainGrading G R i) : (cubicalChainAlgHom R φ) a ∈ cubicalChainGrading G' R i

The induced algebra homomorphism preserves the cohomological degree.

theorem TauCeti.cubicalChainDifferential_cubicalChainAlgHom {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] {R : Type u_4} [CommRing R] (φ : G →ₜ* G') (a : normalizedCubicalChainAlgebra G R) : (cubicalChainDifferential G' R) ((cubicalChainAlgHom R φ) a) = (cubicalChainAlgHom R φ) ((cubicalChainDifferential G R) a)

The induced algebra homomorphism commutes with the differentials.

noncomputable def TauCeti.cubicalChainDGAlgHom {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] (R : Type u_4) [CommRing R] (φ : G →ₜ* G') : DGAlgHom ⋯ ⋯

The morphism of DG algebras C^□_*(G; R) → C^□_*(G'; R) induced by a continuous monoid homomorphism.

@[simp]

theorem TauCeti.cubicalChainDGAlgHom_lof {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] {R : Type u_4} [CommRing R] (φ : G →ₜ* G') (n : ℕ) (y : NormalizedCubicalChain G R n) : (cubicalChainDGAlgHom R φ) ((cubicalChainLof G R n) y) = (cubicalChainLof G' R n) ((NormalizedCubicalChain.map R φ.toContinuousMap n) y)

The induced DG algebra morphism on a chain of dimension n.

theorem TauCeti.cubicalChain_dgAlgHom_ext {G : Type u_1} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_4} [CommRing R] {B : Type u_5} [Ring B] [Algebra R B] {ℬ : ℤ → Submodule R B} [GradedAlgebra ℬ] {dB : B →ₗ[R] B} {hB : IsDGAlgebra ℬ dB} {f g : DGAlgHom ⋯ hB} (h : ∀ (n : ℕ) (y : NormalizedCubicalChain G R n), f ((cubicalChainLof G R n) y) = g ((cubicalChainLof G R n) y)) : f = g

Two DG algebra morphisms out of C^□_*(G; R) agree if they agree on chains of each dimension.

@[simp]

theorem TauCeti.cubicalChainDGAlgHom_id {G : Type u_1} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_4} [CommRing R] : cubicalChainDGAlgHom R (ContinuousMonoidHom.id G) = DGAlgHom.id ⋯

The identity homomorphism induces the identity.

theorem TauCeti.cubicalChainDGAlgHom_comp {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] [Monoid G''] [TopologicalSpace G''] [ContinuousMul G''] {R : Type u_4} [CommRing R] (ψ : G' →ₜ* G'') (φ : G →ₜ* G') : cubicalChainDGAlgHom R (ψ.comp φ) = (cubicalChainDGAlgHom R ψ).comp (cubicalChainDGAlgHom R φ)

The induced morphism of a composite is the composite of the induced morphisms.

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

The augmentation on the chains of dimension n: the augmentation of 0-chains, and zero in positive dimension.

@[simp]

theorem TauCeti.cubicalChainAugmentLof_zero {G : Type u_1} [TopologicalSpace G] {R : Type u_4} [CommRing R] (y : NormalizedCubicalChain G R 0) : (cubicalChainAugmentLof G R 0) y = (NormalizedCubicalChain.augment G R) y

The augmentation on 0-chains.

theorem TauCeti.cubicalChainAugmentLof_of_ne_zero {G : Type u_1} [TopologicalSpace G] {R : Type u_4} [CommRing R] {n : ℕ} (hn : n ≠ 0) (y : NormalizedCubicalChain G R n) : (cubicalChainAugmentLof G R n) y = 0

The augmentation vanishes on chains of positive dimension.

noncomputable def TauCeti.cubicalChainAugmentAlgHom (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_4) [CommRing R] : normalizedCubicalChainAlgebra G R →ₐ[R] R

The augmentation C^□_*(G; R) → R as an algebra homomorphism.

@[simp]

theorem TauCeti.cubicalChainAugmentAlgHom_lof {G : Type u_1} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_4} [CommRing R] (n : ℕ) (y : NormalizedCubicalChain G R n) : (cubicalChainAugmentAlgHom G R) ((cubicalChainLof G R n) y) = (cubicalChainAugmentLof G R n) y

The augmentation on a chain of dimension n.

theorem TauCeti.cubicalChainAugmentAlgHom_mem {G : Type u_1} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_4} [CommRing R] {i : ℤ} {a : normalizedCubicalChainAlgebra G R} (ha : a ∈ cubicalChainGrading G R i) : (cubicalChainAugmentAlgHom G R) a ∈ trivialGrading R R i

The augmentation is concentrated in degree 0.

theorem TauCeti.cubicalChainAugmentAlgHom_differential {G : Type u_1} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_4} [CommRing R] (a : normalizedCubicalChainAlgebra G R) : (cubicalChainAugmentAlgHom G R) ((cubicalChainDifferential G R) a) = 0

The augmentation vanishes on boundaries.

noncomputable def TauCeti.cubicalChainAugmentation (G : Type u_1) [Monoid G] [TopologicalSpace G] [ContinuousMul G] (R : Type u_4) [CommRing R] : DGAlgAugmentation ⋯

The augmentation of the DG algebra of cubical chains: the augmentation of 0-chains, extended by zero, as a DG algebra morphism to the ground ring.

@[simp]

theorem TauCeti.cubicalChainAugmentation_lof {G : Type u_1} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {R : Type u_4} [CommRing R] (n : ℕ) (y : NormalizedCubicalChain G R n) : (cubicalChainAugmentation G R) ((cubicalChainLof G R n) y) = (cubicalChainAugmentLof G R n) y

The augmentation on a chain of dimension n.

theorem TauCeti.cubicalChainAugmentation_comp_dgAlgHom {G : Type u_1} {G' : Type u_2} [Monoid G] [TopologicalSpace G] [ContinuousMul G] [Monoid G'] [TopologicalSpace G'] [ContinuousMul G'] {R : Type u_4} [CommRing R] (φ : G →ₜ* G') : DGAlgHom.comp (cubicalChainAugmentation G' R) (cubicalChainDGAlgHom R φ) = cubicalChainAugmentation G R

The morphisms induced by continuous monoid homomorphisms are compatible with the augmentations.