The augmented DG algebra of chains on the Moore loop space

For a pointed space (B, b), the Moore loop space Ω_b B = MooreLoopSpace B b is a topological monoid, strictly associative and strictly unital under concatenation. Its normalized cubical chains C_*(Ω_b B; R), with the Pontryagin product, C_n in cohomological degree -n and the boundary as differential, form an augmented differential graded algebra: the DG algebra over which the DG local systems on (B, b) are right modules.

A based map f : (B, b) → (B', b') induces the continuous monoid homomorphism MooreLoopSpace.map f, hence a morphism of augmented DG algebras C_*(Ωf) : C_*(Ω_b B; R) → C_*(Ω_{b'} B'; R), functorially in f.

Main definitions

• TauCeti.loopChainAlgebra B b R: the algebra C_*(Ω_b B; R).
• TauCeti.loopChainAugmentation B b R: its augmentation.
• TauCeti.loopChainMap R f hf: the DG algebra morphism C_*(Ωf) of a based map.
• TauCeti.loopChainToGroupAlgebra B b R: the algebra map to the group algebra R[π₁(B, b)], the zeroth-homology projection loopZeroChainToGroupAlgebra in dimension zero and zero in positive dimension.
• TauCeti.loopChainToGroupAlgebraDGAlgHom B b R: the same map as a morphism of DG algebras to the trivially graded group algebra with the zero differential.
• TauCeti.groupAlgebraToLoopChainCohomology B b R: the algebra map R[π₁(B, b)] → H(C_*(Ω_b B; R)), the inverse of loopZeroChainToGroupAlgebra on classes of zero chains.

Main results

• TauCeti.loopChain_isDGAlgebra: C_*(Ω_b B; R) is a differential graded algebra.
• TauCeti.loopChainMap_lof, TauCeti.loopChainAugmentation_lof_zero, TauCeti.loopChainAugmentation_lof_succ: the values on chains of a given dimension.
• TauCeti.loopChainMap_id, TauCeti.loopChainMap_comp: functoriality.
• TauCeti.loopChainAugmentation_comp_loopChainMap: compatibility with the augmentations.
• TauCeti.loopChainToGroupAlgebra_differential, TauCeti.loopChainToGroupAlgebra_eq_zero_of_mem: it kills boundaries and elements of nonzero cohomological degree.
• TauCeti.loopChainToGroupAlgebra_loopChainMap: naturality in based maps.
• TauCeti.loopChainToGroupAlgebra_apply, TauCeti.loopChainToGroupAlgebra_surjective: it only sees the component of dimension zero, and it is surjective.
• TauCeti.groupAlgebraToLoopChainCohomology_of_fundamentalGroupHom: the basis element of the class of a Moore loop goes to the cohomology class of its point chain.
• TauCeti.groupAlgebraToLoopChainCohomology_mem_cohomologyGrading_zero: the group ring lands in cohomological degree zero.
• TauCeti.cohomologyMap_loopChainToGroupAlgebraDGAlgHom_groupAlgebraToLoopChainCohomology: the degree-zero truncation is a left inverse of the inclusion of zeroth homology, on cohomology.
• TauCeti.groupAlgebraToLoopChainCohomology_injective: the inclusion of zeroth homology is injective.

References

• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §1.4.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, Chapter 2.

@[reducible, inline]

abbrev TauCeti.loopChainAlgebra (B : Type u_1) [TopologicalSpace B] (b : B) (R : Type u_2) [CommRing R] : Type (max u_2 u_1)

The chain algebra of the Moore loop space: C_*(Ω_b B; R), the normalized cubical chains of the Moore loops at b, with the Pontryagin product.

theorem TauCeti.loopChain_isDGAlgebra (B : Type u_1) [TopologicalSpace B] (b : B) (R : Type u_2) [CommRing R] : IsDGAlgebra (cubicalChainGrading (MooreLoopSpace B b) R) (cubicalChainDifferential (MooreLoopSpace B b) R)

C_*(Ω_b B; R) is a differential graded algebra, with the chains of dimension n in cohomological degree -n and the boundary as differential.

noncomputable def TauCeti.loopChainAugmentation (B : Type u_1) [TopologicalSpace B] (b : B) (R : Type u_2) [CommRing R] : DGAlgAugmentation ⋯

The augmentation of C_*(Ω_b B; R), induced by the map to a point.

theorem TauCeti.loopChainAugmentation_def (B : Type u_1) [TopologicalSpace B] (b : B) (R : Type u_2) [CommRing R] : loopChainAugmentation B b R = cubicalChainAugmentation (MooreLoopSpace B b) R

The augmentation of C_*(Ω_b B; R) is the augmentation of the chains of the monoid Ω_b B.

@[simp]

theorem TauCeti.loopChainAugmentation_lof_zero {B : Type u_1} [TopologicalSpace B] {b : B} {R : Type u_2} [CommRing R] (y : NormalizedCubicalChain (MooreLoopSpace B b) R 0) : (loopChainAugmentation B b R) ((cubicalChainLof (MooreLoopSpace B b) R 0) y) = (NormalizedCubicalChain.augment (MooreLoopSpace B b) R) y

The augmentation of a 0-chain of Moore loops.

@[simp]

theorem TauCeti.loopChainAugmentation_lof_succ {B : Type u_1} [TopologicalSpace B] {b : B} {R : Type u_2} [CommRing R] (k : ℕ) (y : NormalizedCubicalChain (MooreLoopSpace B b) R (k + 1)) : (loopChainAugmentation B b R) ((cubicalChainLof (MooreLoopSpace B b) R (k + 1)) y) = 0

The augmentation vanishes on chains of Moore loops of positive dimension.

noncomputable def TauCeti.loopChainMap {B : Type u_1} {B' : Type u_2} [TopologicalSpace B] [TopologicalSpace B'] {b : B} {b' : B'} (R : Type u_4) [CommRing R] (f : C(B, B')) (hf : f b = b') : DGAlgHom ⋯ ⋯

The morphism of DG algebras C_*(Ωf) induced by a based map f : (B, b) → (B', b').

@[simp]

theorem TauCeti.loopChainMap_lof {B : Type u_1} {B' : Type u_2} [TopologicalSpace B] [TopologicalSpace B'] {b : B} {b' : B'} (R : Type u_4) [CommRing R] (f : C(B, B')) (hf : f b = b') (n : ℕ) (y : NormalizedCubicalChain (MooreLoopSpace B b) R n) : (loopChainMap R f hf) ((cubicalChainLof (MooreLoopSpace B b) R n) y) = (cubicalChainLof (MooreLoopSpace B' b') R n) ((NormalizedCubicalChain.map R (MooreLoopSpace.map f hf).toContinuousMap n) y)

C_*(Ωf) on a chain of dimension n is the push-forward along Ωf.

@[simp]

theorem TauCeti.loopChainMap_id {B : Type u_1} [TopologicalSpace B] {b : B} (R : Type u_4) [CommRing R] : loopChainMap R (ContinuousMap.id B) ⋯ = DGAlgHom.id ⋯

The identity map induces the identity.

theorem TauCeti.loopChainMap_comp {B : Type u_1} {B' : Type u_2} {B'' : Type u_3} [TopologicalSpace B] [TopologicalSpace B'] [TopologicalSpace B''] {b : B} {b' : B'} {b'' : B''} (R : Type u_4) [CommRing R] (g : C(B', B'')) (f : C(B, B')) (hg : g b' = b'') (hf : f b = b') : loopChainMap R (g.comp f) ⋯ = (loopChainMap R g hg).comp (loopChainMap R f hf)

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

theorem TauCeti.loopChainAugmentation_comp_loopChainMap {B : Type u_1} {B' : Type u_2} [TopologicalSpace B] [TopologicalSpace B'] {b : B} {b' : B'} (R : Type u_4) [CommRing R] (f : C(B, B')) (hf : f b = b') : DGAlgHom.comp (loopChainAugmentation B' b' R) (loopChainMap R f hf) = loopChainAugmentation B b R

The morphisms induced by based maps are compatible with the augmentations.

noncomputable def TauCeti.loopChainToGroupAlgebra (B : Type u) [TopologicalSpace B] (b : B) (R : Type u) [CommRing R] : loopChainAlgebra B b R →ₐ[R] MonoidAlgebra R (FundamentalGroup B b)

The degree-zero ring map: the algebra map from the chains on the Moore loop space to the group ring of the fundamental group, which is loopZeroChainToGroupAlgebra on 0-chains and zero on chains of positive dimension.

@[simp]

theorem TauCeti.loopChainToGroupAlgebra_lof_zero {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] (y : NormalizedCubicalChain (MooreLoopSpace B b) R 0) : (loopChainToGroupAlgebra B b R) ((cubicalChainLof (MooreLoopSpace B b) R 0) y) = (loopZeroChainToGroupAlgebra B b R) y

The degree-zero ring map on a 0-chain is the projection to the group algebra.

@[simp]

theorem TauCeti.loopChainToGroupAlgebra_lof_succ {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] (k : ℕ) (y : NormalizedCubicalChain (MooreLoopSpace B b) R (k + 1)) : (loopChainToGroupAlgebra B b R) ((cubicalChainLof (MooreLoopSpace B b) R (k + 1)) y) = 0

The degree-zero ring map kills the chains of positive dimension.

theorem TauCeti.loopChainToGroupAlgebra_apply {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] (a : loopChainAlgebra B b R) : (loopChainToGroupAlgebra B b R) a = (loopZeroChainToGroupAlgebra B b R) (a 0)

The degree-zero ring map only sees the component of dimension zero.

theorem TauCeti.loopChainToGroupAlgebra_surjective {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] : Function.Surjective ⇑(loopChainToGroupAlgebra B b R)

The degree-zero ring map is surjective: every element of the group ring is the class of a 0-chain.

@[simp]

theorem TauCeti.loopChainToGroupAlgebra_differential {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] (a : loopChainAlgebra B b R) : (loopChainToGroupAlgebra B b R) ((cubicalChainDifferential (MooreLoopSpace B b) R) a) = 0

The degree-zero ring map kills boundaries.

theorem TauCeti.loopChainToGroupAlgebra_eq_zero_of_mem {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] {i : ℤ} (hi : i ≠ 0) {a : loopChainAlgebra B b R} (ha : a ∈ cubicalChainGrading (MooreLoopSpace B b) R i) : (loopChainToGroupAlgebra B b R) a = 0

The degree-zero ring map kills homogeneous elements of nonzero cohomological degree.

@[simp]

theorem TauCeti.loopChainToGroupAlgebra_loopChainMap {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] {B' : Type u} [TopologicalSpace B'] {b' : B'} (f : C(B, B')) (hf : f b = b') (a : loopChainAlgebra B b R) : (loopChainToGroupAlgebra B' b' R) ((loopChainMap R f hf) a) = (MonoidAlgebra.mapDomainRingHom R (FundamentalGroup.mapOfEq f hf)) ((loopChainToGroupAlgebra B b R) a)

Naturality of the degree-zero ring map: it intertwines C_*(Ωf) with the map of group rings induced by π₁(f).

noncomputable def TauCeti.loopChainToGroupAlgebraDGAlgHom (B : Type u) [TopologicalSpace B] (b : B) (R : Type u) [CommRing R] : DGAlgHom ⋯ ⋯

The degree-zero truncation as a morphism of DG algebras: loopChainToGroupAlgebra from C_*(Ω_b B; R) to the group ring R[π₁(B, b)], trivially graded with the zero differential. It kills the chains of positive dimension and the boundaries.

@[simp]

theorem TauCeti.loopChainToGroupAlgebraDGAlgHom_apply {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] (a : loopChainAlgebra B b R) : (loopChainToGroupAlgebraDGAlgHom B b R) a = (loopChainToGroupAlgebra B b R) a

The DG algebra morphism loopChainToGroupAlgebraDGAlgHom is loopChainToGroupAlgebra.

noncomputable def TauCeti.groupAlgebraToLoopChainCohomology (B : Type u) [TopologicalSpace B] (b : B) (R : Type u) [CommRing R] : MonoidAlgebra R (FundamentalGroup B b) →ₐ[R] ⋯.Cohomology

The group ring in the cohomology of the loop chain algebra: the algebra map R[π₁(B, b)] → H(C_*(Ω_b B; R)) sending the basis element MooreLoopSpace.fundamentalGroupHom b γ of the class of a Moore loop γ to the cohomology class of the point chain of γ. It is the inverse of the identification of H₀(Ω_b B; R) with R[π₁(B, b)] by loopZeroChainToGroupAlgebra, followed by the inclusion of degree zero.

@[simp]

theorem TauCeti.groupAlgebraToLoopChainCohomology_loopZeroChainToGroupAlgebra (B : Type u) [TopologicalSpace B] (b : B) (R : Type u) [CommRing R] (a : NormalizedCubicalChain (MooreLoopSpace B b) R 0) : (groupAlgebraToLoopChainCohomology B b R) ((loopZeroChainToGroupAlgebra B b R) a) = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal ⋯.boundaries)) ⟨(cubicalChainLof (MooreLoopSpace B b) R 0) a, ⋯⟩

groupAlgebraToLoopChainCohomology sends the image of a zero chain in the group ring to the cohomology class of the zero chain.

theorem TauCeti.groupAlgebraToLoopChainCohomology_of_fundamentalGroupHom {B : Type u} [TopologicalSpace B] {b : B} {R : Type u} [CommRing R] (γ : MooreLoopSpace B b) : (groupAlgebraToLoopChainCohomology B b R) ((MonoidAlgebra.of R (FundamentalGroup B b)) ((MooreLoopSpace.fundamentalGroupHom b) γ)) = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal ⋯.boundaries)) ⟨(cubicalChainLof (MooreLoopSpace B b) R 0) (NormalizedCubicalChain.ofCube (MooreLoopSpace B b) R (SingularCube.point γ)), ⋯⟩

groupAlgebraToLoopChainCohomology sends the basis element of the class of a Moore loop γ to the cohomology class of the point chain of γ.

theorem TauCeti.groupAlgebraToLoopChainCohomology_mem_cohomologyGrading_zero (B : Type u) [TopologicalSpace B] (b : B) (R : Type u) [CommRing R] (a : MonoidAlgebra R (FundamentalGroup B b)) : (groupAlgebraToLoopChainCohomology B b R) a ∈ ⋯.cohomologyGrading 0

groupAlgebraToLoopChainCohomology lands in degree zero: the group ring is H₀(Ω_b B; R).

@[simp]

theorem TauCeti.cohomologyMap_loopChainToGroupAlgebraDGAlgHom_groupAlgebraToLoopChainCohomology (B : Type u) [TopologicalSpace B] (b : B) (R : Type u) [CommRing R] (a : MonoidAlgebra R (FundamentalGroup B b)) : (loopChainToGroupAlgebraDGAlgHom B b R).cohomologyMap ((groupAlgebraToLoopChainCohomology B b R) a) = (algEquivCohomologyOfZero (trivialGrading R (MonoidAlgebra R (FundamentalGroup B b)))) a

The degree-zero truncation inverts the inclusion of zeroth homology. On cohomology, C_*(Ω_b B; R) → R[π₁(B, b)] sends the class of a group-ring element, included as a class of zero chains, back to that element.

theorem TauCeti.groupAlgebraToLoopChainCohomology_injective (B : Type u) [TopologicalSpace B] (b : B) (R : Type u) [CommRing R] : Function.Injective ⇑(groupAlgebraToLoopChainCohomology B b R)

The inclusion R[π₁(B, b)] → H(C_*(Ω_b B; R)) of zeroth homology is injective, for every space: the degree-zero truncation is a left inverse on cohomology.