Zeroth homology of the Moore loop algebra

Normalized cubical zeroth homology of the Moore loop space is the group algebra of the fundamental group, over any commutative coefficient ring. The identification uses the existing cubical/simplicial comparison and Mathlib's singular zeroth-homology computation, rather than a second classification of boundaries.

The point chain of a Moore loop is sent to the basis element indexed by the inverse of its fixed-interval homotopy class. This is the multiplicative convention forced by Mathlib's FundamentalGroup.mul_def: categorical multiplication traverses the right factor first. The Pontryagin product still concatenates loops in traversal order.

The unital Pontryagin algebra structure on loopHomologyZero preserves its original module structure. loopHomologyZeroAlgEquiv identifies it with the group algebra, and loopHomologyZeroπ_mul and loopHomologyZeroπ_one identify the actual chain product and unit with the homology operations. The projection loopZeroChainToGroupAlgebra of zero chains is surjective, and its kernel is exactly the boundaries (loopZeroChainToGroupAlgebra_eq_zero_iff). This supplies the algebraic bridge from loop chains to classical local coefficients. References: W. S. Massey, Singular Homology Theory, Chapter VII; Barraud--Damian--Humilière--Oancea, Floer homology with DG coefficients, §2.2, https://arxiv.org/html/2404.07953v3#S2.SS2. The formal construction reuses TopCat.singularHomology₀Iso and ModuleCat.finsuppCoconeIsColimit.

@[reducible, inline]

noncomputable abbrev TauCeti.loopHomologyZero (X : Type u) [TopologicalSpace X] (x : X) (R : Type u) [CommRing R] : ModuleCat R

Cubical homology of the Moore loop space in degree zero, with coefficients in R.

noncomputable def TauCeti.loopHomologyZeroIso (X : Type u) [TopologicalSpace X] (x : X) (R : Type u) [CommRing R] : loopHomologyZero X x R ≅ ↧(MonoidAlgebra R (FundamentalGroup X x))

The identification of cubical H₀(ΩX; R) with R[π₁(X, x)]. Its convention on generators is the inverse path class, so it preserves traversal-order Pontryagin multiplication.

noncomputable def TauCeti.loopHomologyZeroπ (X : Type u) [TopologicalSpace X] (x : X) (R : Type u) [CommRing R] : NormalizedCubicalChain (MooreLoopSpace X x) R 0 →ₗ[R] ↑(loopHomologyZero X x R)

The homology class of a normalized cubical zero chain of Moore loops.

noncomputable def TauCeti.loopZeroChainToGroupAlgebra (X : Type u) [TopologicalSpace X] (x : X) (R : Type u) [CommRing R] : NormalizedCubicalChain (MooreLoopSpace X x) R 0 →ₗ[R] MonoidAlgebra R (FundamentalGroup X x)

Projection of zero chains to the fundamental-group algebra through actual cubical homology.

@[simp]

theorem TauCeti.loopHomologyZeroIso_hom_π {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (CategoryTheory.ConcreteCategory.hom (loopHomologyZeroIso X x R).hom) ((loopHomologyZeroπ X x R) a) = (loopZeroChainToGroupAlgebra X x R) a

The isomorphism on homology agrees with the zero-chain group-algebra projection.

theorem TauCeti.loopHomologyZeroπ_surjective {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] : Function.Surjective ⇑(loopHomologyZeroπ X x R)

Every zeroth homology class is represented by a normalized cubical zero chain.

@[simp]

theorem TauCeti.loopZeroChainToGroupAlgebra_ofCube {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (c : SingularCube (MooreLoopSpace X x) 0) : (loopZeroChainToGroupAlgebra X x R) (NormalizedCubicalChain.ofCube (MooreLoopSpace X x) R c) = MonoidAlgebra.single ((MooreLoopSpace.fundamentalGroupHom x) (c 0)) 1

A zero-dimensional cube of a Moore loop projects to its fundamental-group basis element.

@[simp]

theorem TauCeti.loopHomologyZeroπ_boundary {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a : NormalizedCubicalChain (MooreLoopSpace X x) R 1) : (loopHomologyZeroπ X x R) ((NormalizedCubicalChain.boundary (MooreLoopSpace X x) R 0) a) = 0

Boundaries of one chains vanish under the canonical homology projection.

@[simp]

theorem TauCeti.loopZeroChainToGroupAlgebra_boundary {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a : NormalizedCubicalChain (MooreLoopSpace X x) R 1) : (loopZeroChainToGroupAlgebra X x R) ((NormalizedCubicalChain.boundary (MooreLoopSpace X x) R 0) a) = 0

The group-algebra projection annihilates cubical boundaries.

theorem TauCeti.loopHomologyZeroπ_eq_zero_iff {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (loopHomologyZeroπ X x R) a = 0 ↔ a ∈ (NormalizedCubicalChain.boundary (MooreLoopSpace X x) R 0).range

A zero chain of Moore loops has zero homology class exactly when it is a boundary.

theorem TauCeti.loopZeroChainToGroupAlgebra_eq_zero_iff {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (loopZeroChainToGroupAlgebra X x R) a = 0 ↔ a ∈ (NormalizedCubicalChain.boundary (MooreLoopSpace X x) R 0).range

A zero chain of Moore loops lies in the kernel of the projection to the group algebra exactly when it is a boundary.

theorem TauCeti.loopZeroChainToGroupAlgebra_surjective {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] : Function.Surjective ⇑(loopZeroChainToGroupAlgebra X x R)

The projection of zero chains of Moore loops to the group algebra is surjective.

@[simp]

theorem TauCeti.loopZeroChainToGroupAlgebra_mul {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a b : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (loopZeroChainToGroupAlgebra X x R) (((NormalizedCubicalChain.mul (MooreLoopSpace X x) R 0 0) a) b) = (loopZeroChainToGroupAlgebra X x R) a * (loopZeroChainToGroupAlgebra X x R) b

Projection to the group algebra preserves the Pontryagin product of arbitrary zero chains. Thus the linear identification on actual homology identifies its induced product with the convolution product in the group algebra.

@[simp]

theorem TauCeti.loopZeroChainToGroupAlgebra_one {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] : (loopZeroChainToGroupAlgebra X x R) (NormalizedCubicalChain.one (MooreLoopSpace X x) R) = 1

Projection takes the constant, duration-zero loop unit to the group-algebra unit.

@[instance_reducible]

noncomputable instance TauCeti.loopHomologyZeroRing (X : Type u) [TopologicalSpace X] (x : X) (R : Type u) [CommRing R] : Ring ↑(loopHomologyZero X x R)

The unital Pontryagin ring on actual cubical zeroth homology. Only multiplication, the unit, and their powers and casts are transported through the linear comparison; the existing homology addition, negation and scalar action are preserved. The equations loopHomologyZeroπ_mul and loopHomologyZeroπ_one identify this structure with the product and unit induced by Moore-loop chains, rather than an independently chosen ring structure.

@[instance_reducible]

noncomputable instance TauCeti.loopHomologyZeroAlgebra (X : Type u) [TopologicalSpace X] (x : X) (R : Type u) [CommRing R] : Algebra R ↑(loopHomologyZero X x R)

The Pontryagin algebra uses the original coefficient action on cubical homology.

noncomputable def TauCeti.loopHomologyZeroAlgEquiv (X : Type u) [TopologicalSpace X] (x : X) (R : Type u) [CommRing R] : ↑(loopHomologyZero X x R) ≃ₐ[R] MonoidAlgebra R (FundamentalGroup X x)

The unital algebra identification H₀(ΩX; R) ≃ₐ[R] R[π₁(X, x)], using inverse path classes to reconcile traversal-order Pontryagin multiplication with Mathlib's group convention. Its underlying linear equivalence is exactly loopHomologyZeroIso.

theorem TauCeti.loopHomologyZeroAlgEquiv_apply {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a : ↑(loopHomologyZero X x R)) : (loopHomologyZeroAlgEquiv X x R) a = (CategoryTheory.ConcreteCategory.hom (loopHomologyZeroIso X x R).hom) a

The algebra equivalence preserves the original linear homology comparison.

@[simp]

theorem TauCeti.loopHomologyZeroAlgEquiv_π {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (loopHomologyZeroAlgEquiv X x R) ((loopHomologyZeroπ X x R) a) = (loopZeroChainToGroupAlgebra X x R) a

The algebra equivalence agrees with the existing zero-chain projection.

@[simp]

theorem TauCeti.loopHomologyZeroπ_mul {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] (a b : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (loopHomologyZeroπ X x R) (((NormalizedCubicalChain.mul (MooreLoopSpace X x) R 0 0) a) b) = (loopHomologyZeroπ X x R) a * (loopHomologyZeroπ X x R) b

The product on homology is represented by the actual Pontryagin product on zero chains. Surjectivity of loopHomologyZeroπ makes this equation characterize the homology product.

@[simp]

theorem TauCeti.loopHomologyZeroπ_one {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] : (loopHomologyZeroπ X x R) (NormalizedCubicalChain.one (MooreLoopSpace X x) R) = 1

The constant duration-zero Moore loop represents the unit of the homology algebra.

@[simp]

theorem TauCeti.loopHomologyZeroπ_map {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] {Y : Type u} [TopologicalSpace Y] {y : Y} (f : C(X, Y)) (hf : f x = y) (a : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (loopHomologyZeroπ Y y R) ((NormalizedCubicalChain.map R (↑(MooreLoopSpace.map f hf)) 0) a) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((normalizedCubicalChainComplex R).map (TopCat.ofHom ↑(MooreLoopSpace.map f hf))) 0)) ((loopHomologyZeroπ X x R) a)

Taking the zeroth homology class of a chain commutes with a based continuous map.

@[simp]

theorem TauCeti.loopZeroChainToGroupAlgebra_map {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] {Y : Type u} [TopologicalSpace Y] {y : Y} (f : C(X, Y)) (hf : f x = y) (a : NormalizedCubicalChain (MooreLoopSpace X x) R 0) : (loopZeroChainToGroupAlgebra Y y R) ((NormalizedCubicalChain.map R (↑(MooreLoopSpace.map f hf)) 0) a) = (MonoidAlgebra.mapDomainLinearMap R R ⇑(FundamentalGroup.mapOfEq f hf)) ((loopZeroChainToGroupAlgebra X x R) a)

The zero-chain projection is natural under based continuous maps.

theorem TauCeti.loopHomologyZeroIso_hom_naturality {X : Type u} [TopologicalSpace X] {x : X} {R : Type u} [CommRing R] {Y : Type u} [TopologicalSpace Y] {y : Y} (f : C(X, Y)) (hf : f x = y) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((normalizedCubicalChainComplex R).map (TopCat.ofHom ↑(MooreLoopSpace.map f hf))) 0) (loopHomologyZeroIso Y y R).hom = CategoryTheory.CategoryStruct.comp (loopHomologyZeroIso X x R).hom (ModuleCat.ofHom (MonoidAlgebra.mapDomainLinearMap R R ⇑(FundamentalGroup.mapOfEq f hf)))

The homology identification is natural under based maps: it carries the homology map of Moore loops to the linear map induced by the fundamental-group map.