Moore loop components and the fundamental group

The path components of the Moore loop space identify with the fundamental group. The map on loops is multiplicative when a loop is sent to the inverse of its fixed-interval homotopy class: Mathlib multiplies endomorphisms by reversed categorical composition (FundamentalGroup.mul_def), while Moore loops concatenate in traversal order.

The component identification uses the Moore/fixed-interval homotopy equivalence and HomotopyGroup.zerothHomotopyLoopSpaceEquivFundamentalGroup. This convention gives the multiplicative comparison needed for the degree-zero Pontryagin algebra. In particular, Moore loops are path connected exactly when the fundamental group is trivial.

See W. S. Massey, Singular Homology Theory, Chapter VII, and Barraud--Damian--Humilière--Oancea, Floer homology with DG coefficients, §2.2, https://arxiv.org/html/2404.07953v3#S2.SS2.

noncomputable def TauCeti.MooreLoopSpace.fundamentalGroupHom {X : Type u_1} [TopologicalSpace X] (x : X) : MooreLoopSpace X x →* FundamentalGroup X x

The multiplicative class of a Moore loop. The inverse compensates for Mathlib's convention that the product of fundamental-group elements traverses the right factor first.

@[simp]

theorem TauCeti.MooreLoopSpace.fundamentalGroupHom_apply {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : (fundamentalGroupHom x) γ = (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ.toPath))⁻¹

The generator equation for the multiplicative Moore-loop class.

noncomputable def TauCeti.MooreLoopSpace.zerothHomotopyEquivFundamentalGroup {X : Type u_1} [TopologicalSpace X] (x : X) : ZerothHomotopy (MooreLoopSpace X x) ≃ FundamentalGroup X x

Path components of Moore loops identify with the fundamental group, in the multiplicative convention of fundamentalGroupHom.

@[simp]

theorem TauCeti.MooreLoopSpace.zerothHomotopyEquivFundamentalGroup_mk {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : (zerothHomotopyEquivFundamentalGroup x) (ZerothHomotopy.mk γ) = (fundamentalGroupHom x) γ

The component equivalence agrees with the multiplicative class on loops.

theorem TauCeti.MooreLoopSpace.fundamentalGroupHom_surjective {X : Type u_1} [TopologicalSpace X] (x : X) : Function.Surjective ⇑(fundamentalGroupHom x)

Every element of the fundamental group is the multiplicative class of a Moore loop.

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_iff {X : Type u_1} [TopologicalSpace X] (x : X) : PathConnectedSpace (MooreLoopSpace X x) ↔ Subsingleton (FundamentalGroup X x)

Moore loops are path connected exactly when the fundamental group at their basepoint is trivial.

@[simp]

theorem TauCeti.MooreLoopSpace.fundamentalGroupHom_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (γ : MooreLoopSpace X x) : (fundamentalGroupHom y) ((map f hf) γ) = (FundamentalGroup.mapOfEq f hf) ((fundamentalGroupHom x) γ)

The multiplicative loop class is natural under based continuous maps.